fact: Definition diagonal_functor (C:category) := functor_to_prod_cat (functor_id C) (functor_id C).
imports: Coq(ssreflect ssrfun) Coq.Relations(Relation_Definitions) Coq.Classes(RelationClasses Morphisms) Mon(SPropBase)