proposition: Lemma tlistDA_morDA `{f : Mor x y} : tlistDA (morDA f) ≈ f.
proof: Proof. induction f; simpl; auto. rewrite <- IHf1, <- IHf2. now rewrite morDA_tlistDA. Qed.
imports: Category.Lib Category.Lib.TList Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Adjunction Category.Theory.Universal.Arrow Category.Instance.StrictCat Category.Construction.Groupoid Category.Construction.Opposite Category.Construction.Product Category.Instance.Sets