FunctorCategories: eval : [C,D]xC -> D
Lift for ISetoids
Elements: Dom functor
Congruence: move indexes to parameters for _∼_
fix Lan and add Ran
Yoneda Lemma