Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . MetaCat_initial_p struct_u UnaryFuncHom struct_id struct_comp x1 x2) ⟶ x0.

Apply H0 with pack_u 0 (λ x1 . x1).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_initial_p struct_u UnaryFuncHom struct_id struct_comp (pack_u 0 (λ x3 . x3)) x2 ⟶ x1.

Apply H1 with λ x2 . lam 0 (λ x3 . x3).

Apply unknownprop_c7314f2432739dec7e3d09b8b84398b3dfe5e7bfe33d21fac0129a984e9f917e with struct_u leaving 2 subgoals.

Let x2 of type ι be given.

Assume H2: struct_u x2.

The subproof is completed by applying H2.

Apply pack_struct_u_I with 0, λ x2 . x2.

Let x2 of type ι be given.

Assume H2: x2 ∈ 0.

The subproof is completed by applying H2.

■

Proofgold Proof