| ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ ∀ x4 : ο . (MetaFunctor_prop1 x0 x1 x2 x3 ⟶ MetaFunctor_prop2 x0 x1 x2 x3 ⟶ (∀ x5 x6 x7 . x0 x5 ⟶ x0 x6 ⟶ x1 x5 x6 x7 ⟶ x3 x5 x5 x6 x7 (x2 x5) = x7) ⟶ (∀ x5 x6 x7 . x0 x5 ⟶ x0 x6 ⟶ x1 x5 x6 x7 ⟶ x3 x5 x6 x6 (x2 x6) x7 = x7) ⟶ (∀ x5 x6 x7 x8 x9 x10 x11 . x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x5 x6 x9 ⟶ x1 x6 x7 x10 ⟶ x1 x7 x8 x11 ⟶ x3 x5 x6 x8 (x3 x6 x7 x8 x11 x10) x9 = x3 x5 x7 x8 x11 (x3 x5 x6 x7 x10 x9)) ⟶ x4) ⟶ x4 |
|