Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . MetaCat_initial_p Quasigroup 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 Quasigroup MagmaHom struct_id struct_comp (pack_b 0 (λ x3 x4 . x3)) x2 ⟶ x1.

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

Claim L2: ∀ x2 . Quasigroup x2 ⟶ struct_b x2

Let x2 of type ι be given.

Assume H2: Quasigroup x2.

Apply H2 with struct_b x2.

Assume H3: struct_b x2.

Assume H4: unpack_b_o x2 (λ x3 . λ x4 : ι → ι → ι . and (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (x4 x5)) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))).

The subproof is completed by applying H3.

Claim L3: Quasigroup (pack_b 0 (λ x2 x3 . x2))

Apply unknownprop_e3d260e78a123ac716d567ab700d9fc3334efbbe9012a4545cf5b7c9b546016d with 0, λ x2 x3 . x2 leaving 3 subgoals.

Let x2 of type ι be given.

Assume H3: x2 ∈ 0.

Let x3 of type ι be given.

Assume H4: x3 ∈ 0.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H3: x2 ∈ 0.

Apply FalseE with bij 0 0 ((λ x3 x4 . x3) x2).

Apply EmptyE with x2.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H3: x2 ∈ 0.

Apply FalseE with bij 0 0 (λ x3 . (λ x4 x5 . x4) x3 x2).

Apply EmptyE with x2.

The subproof is completed by applying H3.

Apply unknownprop_bcecd31c43f08102a5dbeba9f564468d78a0f8f72c35b7e854348988607dabb0 with Quasigroup leaving 2 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying L3.

■

Proofgold Proof