proposition: Lemma morD_sound `{t : Mor x y} : morD t ≈ composition (morDA t).
proof: Proof. induction t; simpl; cat. rewrite IHt1, IHt2; simpl. now rewrite composition_tapp. Qed.
imports: Category.Lib Category.Lib.TList Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Adjunction Category.Instance.Sets