fact: Definition combine (f g : Morphism) : Morphism := match f, g with | Identity, g => g | f, Identity => f | Morphisms fs, Morphisms gs => Morphisms (append fs gs) end.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify