fact: Fixpoint morD `(t : Mor x y) : x ~> y := match t with | Ident => id | Morph f => f | Comp f g => morD f ∘ morD g end.
imports: Category.Lib Category.Lib.TList Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Adjunction Category.Instance.Sets