Apply unknownprop_d9aa9b9eefe69fcb1547c6d0a72dc23fdc58939ecb48b57c7307edb196c6e653 with ∃ x0 . ∃ x1 : ι → ι . MetaCat_initial_p EquivReln BinRelnHom struct_id struct_comp x0 x1.

Let x0 of type ι → ι be given.

Assume H0: (λ x1 : ι → ι . ∃ x2 : ι → ι → ι → ι . ∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet lam_id (λ x5 x6 x7 . lam_comp x5) EquivReln BinRelnHom struct_id struct_comp x1 x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) x0.

Apply H0 with ∃ x1 . ∃ x2 : ι → ι . MetaCat_initial_p EquivReln BinRelnHom struct_id struct_comp x1 x2.

Let x1 of type ι → ι → ι → ι be given.

Assume H1: (λ x2 : ι → ι → ι → ι . ∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet lam_id (λ x5 x6 x7 . lam_comp x5) EquivReln BinRelnHom struct_id struct_comp x0 x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) x1.

Apply H1 with ∃ x2 . ∃ x3 : ι → ι . MetaCat_initial_p EquivReln BinRelnHom struct_id struct_comp x2 x3.

Let x2 of type ι → ι be given.

Assume H2: (λ x3 : ι → ι . ∃ x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet lam_id (λ x5 x6 x7 . lam_comp x5) EquivReln BinRelnHom struct_id struct_comp x0 x1 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) x2.

Apply H2 with ∃ x3 . ∃ x4 : ι → ι . MetaCat_initial_p EquivReln BinRelnHom struct_id struct_comp x3 x4.

Let x3 of type ι → ι be given.

Assume H3: MetaAdjunction_strict (λ x4 . True) HomSet (λ x4 . lam_id x4) (λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8) EquivReln BinRelnHom struct_id struct_comp x0 x1 (λ x4 . ap x4 0) (λ x4 x5 x6 . x6) x2 x3.

Apply unknownprop_6482952e7e0a4bf00d28fb92ecd380f707bb40e0d65cb44f18a4b021cf4cfdbf with ∃ x4 . ∃ x5 : ι → ι . MetaCat_initial_p EquivReln BinRelnHom struct_id struct_comp x4 x5.

Let x4 of type ι be given.

Assume H4: (λ x5 . ∃ x6 : ι → ι . MetaCat_initial_p (λ x7 . True) HomSet (λ x7 . lam x7 (λ x8 . x8)) (λ x7 x8 x9 x10 x11 . lam x7 (λ x12 . ap x10 (ap x11 x12))) x5 x6) x4.

Apply H4 with ∃ x5 . ∃ x6 : ι → ι . MetaCat_initial_p EquivReln BinRelnHom struct_id struct_comp x5 x6.

Let x5 of type ι → ι be given.

Assume H5: MetaCat_initial_p (λ x6 . True) HomSet (λ x6 . lam x6 (λ x7 . x7)) (λ x6 x7 x8 x9 x10 . lam x6 (λ x11 . ap x9 (ap x10 x11))) x4 x5.

Let x6 of type ο be given.

Assume H6: ∀ x7 . (∃ x8 : ι → ι . MetaCat_initial_p EquivReln BinRelnHom struct_id struct_comp x7 x8) ⟶ x6.

Apply H6 with x0 x4.

Apply unknownprop_9e4a4e86d499216c8785bdcb6ea98c9ec4aee7ee82bde465e88bf0a451f2bef0 with λ x7 . True, HomSet, λ x7 . lam_id x7, λ x7 x8 x9 x10 x11 . lam_comp x7 x10 x11, EquivReln, BinRelnHom, struct_id, struct_comp, x0, x1, λ x7 . ap x7 0, λ x7 x8 x9 . x9, x2, x3, x4, x5 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H5.

■

Proofgold Proof