Let Obj, U and Hom be given.

Assume H1 H2 H3.

Apply MetaFunctor_strict_I to the current goal.

An exact proof term for the current goal is MetaCatConcrete Obj U Hom H1 H2 H3.

An exact proof term for the current goal is MetaCatSet.

An exact proof term for the current goal is MetaCatConcreteForgetful Obj U Hom H1.

∎