proposition: Lemma morDA_tlistDA `{f : tlist hom x y} : morDA (tlistDA f) = f.
proof: Proof. induction f; simpl; auto. rewrite <- tlist_app_cons. now rewrite IHf. Qed.
imports: Category.Lib Category.Lib.TList Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Adjunction Category.Instance.Sets