| ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ (∃ x4 x6 : ι → ι → ι → ι → ι . ∃ x8 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x4 x6 x8) ⟶ (∃ x4 x6 x8 : ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x4 x6 x8 x10) ⟶ ∃ x4 x6 x8 : ι → ι → ι → ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x4 x6 x8 x10 |
|
|
|
|
|
|
|
|
|
|