proposition: Lemma identity_composition_between (M : Metacategory) : ∀ f g u, identity M u -> defined f u (pairs M) -> defined u g (pairs M) -> defined f g (pairs M).
proof: Proof. intros. destruct H as [c c0]. pose proof (@triple_composition M f u g f g (c f) (c0 g)) as H3; simpl in H3. destruct H3. apply composite_defined with (h:=x). exact H. Defined.
imports: Coq.Structures.DecidableTypeEx Coq.FSets.FMapFacts Category.Lib.FMapExt Coq.Arith.PeanoNat Category.Lib Category.Theory.Category