Let x0 of type ο be given.

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

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

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_terminal_p Quasigroup MagmaHom struct_id struct_comp (pack_b 1 (λ x3 x4 . x3)) x2 ⟶ x1.

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

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 1 (λ x2 x3 . x2))

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

Let x2 of type ι be given.

Assume H3: x2 ∈ 1.

Let x3 of type ι be given.

Assume H4: x3 ∈ 1.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H3: x2 ∈ 1.

Apply unknownprop_569f409550977198f5ccf4cbea4f1b769b1a85b714e9a8d2e906bfabefd07e7a with λ x3 . x2.

Apply cases_1 with x2, λ x3 . (λ x4 . x3) 0 = 0 leaving 2 subgoals.

The subproof is completed by applying H3.

Let x3 of type ι → ι → ο be given.

Assume H4: x3 ((λ x4 . 0) 0) 0.

The subproof is completed by applying H4.

Let x2 of type ι be given.

Assume H3: x2 ∈ 1.

Apply unknownprop_569f409550977198f5ccf4cbea4f1b769b1a85b714e9a8d2e906bfabefd07e7a with λ x3 . x3.

Let x3 of type ι → ι → ο be given.

Assume H4: x3 ((λ x4 . x4) 0) 0.

The subproof is completed by applying H4.

Apply unknownprop_b85684d5d13773c983896044d4d43e914e6f740191b490f214049d237f32dd7c with Quasigroup leaving 2 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying L3.

■

Proofgold Proof