proposition: Lemma cochain_dmor_paths_type {ver1 ver2 ver3 : vertex conat_graph} (cochn : cochain type_precat) (p1 : edge ver1 ver3) (p2 : edge ver2 ver3) (q1 : ver1 = ver2) : ∏ v1 : dob cochn ver1, dmor cochn p1 v1 = dmor cochn p2 (transportf _ q1 v1).
proof: Proof. intro v1; cbn in *. induction q1. cbn. exact (toforallpaths _ _ _ (cochain_dmor_paths cochn p1 p2) v1). 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