fact: Definition identity (x : object) : morphism x x := {| mor_arr := obj_arr x ; mor_dom := obj_def x ; mor_cod := obj_def x |}.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor