fact: Definition id_nat_trans `{Arrows D} `{!CatId D} `(F: C → D): F ⇛ F := λ _, cat_id.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.jections