proposition: Lemma simplify_cochain_cone : cone terminal_cochain C ≃ simplified_cone.
proof: Proof. unfold cone, Cone0. apply weqfibtototal; intro f. intermediate_weq ( (∏ (u v : vertex conat_graph) (e0 : edge u v), f _ · dmor terminal_cochain e0 ~ f v) ). { do 3 (apply weqonsecfibers; intro). apply invweq. apply weqfunextsec. } apply invweq. intermediate_weq (∏ u, (π u ∘ f (S u))%functions ~ f u). { apply invweq. apply weqonsecfibers; intro. apply weqfunextsec. } unfold homotsec. apply invweq. intermediate_weq ( (∏ (u v : vertex conat_graph) (c : C) (e0 : edge u v), (f u · dmor terminal_cochain e0) c = f v c)). { do 2 (apply weqonsecfibers; intro). apply flipsec_weq. } intermediate_weq ( (∏ (c : C) (u v : vertex conat_graph) (e0 : edge u v), (f u · dmor terminal_cochain e0) c = f v c)). { intermediate_weq ( (∏ (u : vertex conat_graph) (c : C) (v : vertex conat_graph) (e0 : edge u v), (f u · dmor terminal_cochain e0) c = f v c)). { apply weqonsecfibers; intro. apply flipsec_weq. } apply flipsec_weq. } apply invweq. intermediate_weq ((∏ (x : C) (u : nat), (π u ∘ f (S u))%functions x = f u x)); [apply flipsec_weq|]. apply weqonsecfibers; intro c. apply invweq. use weq_iso. - intros eq; intro; apply eq. - intros eq. intros ? ? e. induction e; apply eq. - abstract ( intro; do 2 (apply funextsec; intro); apply funextsec; intro e; induction e; reflexivity ). - abstract ( intro; apply funextsec; intro; reflexivity ). 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