fact: Definition setoid_morphism_id@{o h p} {x : SetoidObject@{o p}} : SetoidMorphism@{o h p} x x := {| morphism := Datatypes.id |}.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Functor