Let x0 of type ι → ο be given.

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

Let x2 of type ι → ι be given.

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

Assume H0: MetaCat x0 x1 x2 x3.

Assume H1: ∃ x4 x5 : ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x4 x5 x6.

Assume H2: ∃ x4 x5 x6 : ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x4 x5 x6 x7.

Apply H1 with ∃ x4 x5 x6 : ι → ι → ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x4 x5 x6 x7.

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

Assume H3: (λ x5 : ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x5 x6 x7) x4.

Apply H3 with ∃ x5 x6 x7 : ι → ι → ι → ι → ι → ι . ∃ x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x5 x6 x7 x8.

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

Assume H4: (λ x6 : ι → ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x4 x6 x7) x5.

Apply H4 with ∃ x6 x7 x8 : ι → ι → ι → ι → ι → ι . ∃ x9 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x6 x7 x8 x9.

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

Assume H5: MetaCat_equalizer_struct_p x0 x1 x2 x3 x4 x5 x6.

Apply H2 with ∃ x7 x8 x9 : ι → ι → ι → ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x7 x8 x9 x10.

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

Assume H6: (λ x8 : ι → ι → ι . ∃ x9 x10 : ι → ι → ι . ∃ x11 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x8 x9 x10 x11) x7.

Apply H6 with ∃ x8 x9 x10 : ι → ι → ι → ι → ι → ι . ∃ x11 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x8 x9 x10 x11.

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

Assume H7: (λ x9 : ι → ι → ι . ∃ x10 : ι → ι → ι . ∃ x11 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x7 x9 x10 x11) x8.

Apply H7 with ∃ x9 x10 x11 : ι → ι → ι → ι → ι → ι . ∃ x12 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x9 x10 x11 x12.

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

Assume H8: (λ x10 : ι → ι → ι . ∃ x11 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x7 x8 x10 x11) x9.

Apply H8 with ∃ x10 x11 x12 : ι → ι → ι → ι → ι → ι . ∃ x13 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x10 x11 x12 x13.

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

Assume H9: MetaCat_product_constr_p x0 x1 x2 x3 x7 x8 x9 x10.

Let x11 of type ο be given.

Assume H10: ∀ x12 : ι → ι → ι → ι → ι → ι . (∃ x13 x14 : ι → ι → ι → ι → ι → ι . ∃ x15 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x12 x13 x14 x15) ⟶ x11.

Apply H10 with λ x12 x13 x14 x15 x16 . x4 (x7 x12 x13) x14 (x3 (x7 x12 x13) x12 x14 x15 (x8 x12 x13)) (x3 (x7 x12 x13) x13 x14 x16 (x9 x12 x13)).

Let x12 of type ο be given.

Assume H11: ∀ x13 : ι → ι → ι → ι → ι → ι . (∃ x14 : ι → ι → ι → ι → ι → ι . ∃ x15 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 (λ x16 x17 x18 x19 x20 . x4 (x7 x16 x17) x18 (x3 (x7 x16 x17) x16 ... ... ...) ...) ... ... ...) ⟶ x12.

...

■

Proofgold Proof