| ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ο . (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x2 x3 x4 x5 ⟶ x5 ∈ setexp (x1 x4) (x1 x3)) ⟶ MetaFunctor x0 x2 (λ x3 . lam_id (x1 x3)) (λ x3 x4 x5 . lam_comp (x1 x3)) (λ x3 . True) HomSet lam_id (λ x3 x4 x5 . lam_comp x3) x1 (λ x3 x4 x5 . x5) |
|
|
|
|
|
|
|
|
|
|