| ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ο . (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x2 x3 x4 x5 ⟶ x5 ∈ setexp (x1 x4) (x1 x3)) ⟶ (∀ x3 . x0 x3 ⟶ x2 x3 x3 (lam_id (x1 x3))) ⟶ (∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 x4 x6 ⟶ x2 x4 x5 x7 ⟶ x2 x3 x5 (lam_comp (x1 x3) x7 x6)) ⟶ MetaFunctor_strict 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) |
|