fact: Record Functor := { object_of :> C -> D; morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d); composition_of : forall s d d' (m1 : morphism C s d) (m2: morphism C d d'), morphism_of _ _ (m2 o m1) = (morphism_of _ _ m2) o (morphism_of _ _ m1); identity_of : forall x, morphism_of _ _ (identity x) = identity (object_of x) }.
imports: Category.Core