| λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 x4 x5 x6 : ι → ι → ι → ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x8 x9 x10 . x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ ∀ x11 x12 . x1 x8 x10 x11 ⟶ x1 x9 x10 x12 ⟶ MetaCat_pullback_p x0 x1 x2 x3 x8 x9 x10 x11 x12 (x4 x8 x9 x10 x11 x12) (x5 x8 x9 x10 x11 x12) (x6 x8 x9 x10 x11 x12) (x7 x8 x9 x10 x11 x12) |
|