Let x0 of type ο be given.

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

Apply H0 with pack_b 0 (λ x1 x2 . x1).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_initial_p struct_b MagmaHom struct_id struct_comp (pack_b 0 (λ x3 x4 . x3)) x2 ⟶ x1.

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

Apply unknownprop_bcecd31c43f08102a5dbeba9f564468d78a0f8f72c35b7e854348988607dabb0 with struct_b leaving 2 subgoals.

Let x2 of type ι be given.

Assume H2: struct_b x2.

The subproof is completed by applying H2.

Apply pack_struct_b_I with 0, λ x2 x3 . x2.

Let x2 of type ι be given.

Assume H2: x2 ∈ 0.

Let x3 of type ι be given.

Assume H3: x3 ∈ 0.

The subproof is completed by applying H2.

■

Proofgold Proof