proposition: Lemma nat_trans_preserve_cone {A B : category} {F G : functor A B} (α : nat_trans F G) {coch : cochain A} {b : B} (b_con : cone (mapdiagram F coch) b) : cone (mapdiagram G coch) b.
proof: Proof. exists (λ v, pr1 b_con v · α (dob coch v)). intros u v p. etrans. 1: apply assoc'. cbn. etrans. 1: apply maponpaths, pathsinv0, (pr2 α). etrans. 1: apply assoc. apply maponpaths_2. exact (pr2 b_con u v p). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Chains.All