| ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 : ο . ((∀ x15 . x0 x15 ⟶ x7 (x8 x15) (x8 (x10 (x8 x15))) (x8 x15) (x13 (x8 x15)) (x9 x15 (x10 (x8 x15)) (x12 x15)) = x6 (x8 x15)) ⟶ (∀ x15 . x4 x15 ⟶ x3 (x10 x15) (x10 (x8 (x10 x15))) (x10 x15) (x11 (x8 (x10 x15)) x15 (x13 x15)) (x12 (x10 x15)) = x2 (x10 x15)) ⟶ x14) ⟶ x14 |
|