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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.All.