Let x0 of type ο be given.

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

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

Let x1 of type ο be given.

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

Claim L2: ∀ x2 . Permutation x2 ⟶ struct_u x2

Let x2 of type ι be given.

Assume H2: Permutation x2.

Apply H2 with struct_u x2.

Assume H3: struct_u x2.

Assume H4: unpack_u_o x2 (λ x3 . bij x3 x3).

The subproof is completed by applying H3.

Claim L3: Permutation (pack_u 0 (λ x2 . x2))

Apply unknownprop_ec657b7f97f95410adb1c5a290530d603e515202daab84a65beca23cc201c12b with 0, λ x2 . x2 leaving 3 subgoals.

Let x2 of type ι be given.

Assume H3: x2 ∈ 0.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H3: x2 ∈ 0.

Apply FalseE with ∀ x3 . x3 ∈ 0 ⟶ (λ x4 . x4) x2 = (λ x4 . x4) x3 ⟶ x2 = x3.

Apply EmptyE with x2.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H3: x2 ∈ 0.

Apply FalseE with ∃ x3 . and (x3 ∈ 0) ((λ x4 . x4) x3 = x2).

Apply EmptyE with x2.

The subproof is completed by applying H3.

Apply unknownprop_c7314f2432739dec7e3d09b8b84398b3dfe5e7bfe33d21fac0129a984e9f917e with Permutation leaving 2 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying L3.

■

Proofgold Proof