fact: Record object : Set := { obj_arr : arrow M; obj_def : composite M obj_arr obj_arr obj_arr; obj_id : is_identity M obj_arr }.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor