fact: Fixpoint to_morphism (t : Term) : Morphism := match t with | Ident => Identity | Morph a => Morphisms (Single (Arr a)) | Comp f g => combine (to_morphism f) (to_morphism g) end.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify