proposition: Lemma composition_identity_left {x y : object} (f : morphism x y) : composition (identity y) f ≈ f.
proof: Proof. destruct f; simpl. destruct (composite_correct _ _ _); simpl in *. unfold composite, arrow in *. rewrite mor_cod0 in e. inversion_clear e. reflexivity. Qed.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor