proposition: Lemma cochain_dmor_paths {C : precategory} {ver1 ver2 : vertex conat_graph} (cochn : cochain C) (p1 p2 : edge ver1 ver2) : dmor cochn p1 = dmor cochn p2.
proof: Proof. apply maponpaths, proofirrelevance, isasetnat. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.WeakEquivalences UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.Type.Core UniMath.CategoryTheory.Categories.Type.Limits UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.Cochains UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.Induction.FunctorCoalgebras_legacy UniMath.Induction.PolynomialFunctors UniMath.Induction.M.Limits UniMath.Induction.M.Core