| ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaAdjunction_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 : ο . (MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11 ⟶ MetaNatTrans x0 x1 x2 x3 x0 x1 x2 x3 (λ x15 . x15) (λ x15 x16 x17 . x17) (λ x15 . x10 (x8 x15)) (λ x15 x16 x17 . x11 (x8 x15) (x8 x16) (x9 x15 x16 x17)) x12 ⟶ MetaNatTrans x4 x5 x6 x7 x4 x5 x6 x7 (λ x15 . x8 (x10 x15)) (λ x15 x16 x17 . x9 (x10 x15) (x10 x16) (x11 x15 x16 x17)) (λ x15 . x15) (λ x15 x16 x17 . x17) x13 ⟶ MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ x14) ⟶ x14 |
|