Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . MetaCat_terminal_p 6e587.. 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 6e587.. 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 . 6e587.. x2 ⟶ struct_b x2

Let x2 of type ι be given.

Assume H2: 6e587.. x2.

Apply H2 with struct_b x2.

Assume H3: struct_b x2.

Assume H4: unpack_b_o x2 (λ x3 . λ x4 : ι → ι → ι . and (and (∃ x5 . and (x5 ∈ x3) (∀ x6 . x6 ∈ x3 ⟶ and (x4 x6 x5 = x6) (x4 x5 x6 = x6))) (∀ 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: 6e587.. (pack_b 1 (λ x2 x3 . x2))

Apply unknownprop_16a3063ddfa60a14b1c6ca69023eaa9506c2f6d8adf6ca9427dd90fdc252365e with 1, λ x2 x3 . x2 leaving 4 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: ∀ x3 . and (x3 ∈ 1) (∀ x4 . x4 ∈ 1 ⟶ and ((λ x5 x6 . x5) x4 x3 = x4) ((λ x5 x6 . x5) x3 x4 = x4)) ⟶ x2.

Apply H3 with 0.

Apply andI with 0 ∈ 1, ∀ x3 . x3 ∈ 1 ⟶ and ((λ x4 x5 . x4) x3 0 = x3) ((λ x4 x5 . x4) 0 x3 = x3) leaving 2 subgoals.

The subproof is completed by applying In_0_1.

Let x3 of type ι be given.

Assume H4: x3 ∈ 1.

Apply andI with (λ x4 x5 . x4) x3 0 = x3, (λ x4 x5 . x4) 0 x3 = x3 leaving 2 subgoals.

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

Assume H5: x4 x3 x3.

The subproof is completed by applying H5.

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

The subproof is completed by applying H4.

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

Assume H5: x4 0 0.

The subproof is completed by applying H5.

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 6e587.. leaving 2 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying L3.

■

Proofgold Proof