proposition: Lemma identity_morphism (M : Metacategory) (i : arr M) : identity M i → composite M i i i.
proof: Proof. intro H; apply H. Qed.
imports: Coq.Structures.DecidableTypeEx Coq.FSets.FMapFacts Category.Lib.FMapExt Coq.Arith.PeanoNat Category.Lib Category.Theory.Category