proposition: Lemma composition_respects {x y z : object} : Proper (equiv ==> equiv ==> equiv) (@composition x y z).
proof: Proof. proper. destruct x0, y0, x1, y1; simpl in *; subst. repeat destruct (composite_correct _ _ _); simpl in *. unfold composite, arrow in *. rewrite e in e0. inversion_clear e0. reflexivity. Qed.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor