proposition: Lemma αinv_f_commutes y (ccGy : cocone (mapdiagram G d) y) (f : D⟦F L,y⟧) (Hf : is_cocone_mor (mapcocone F d cc) (ccFy y ccGy) f) : ∏ v, # G (coconeIn cc v) · (pr1 αinv L · f) = coconeIn ccGy v.
proof: Proof. intro v; rewrite assoc. eapply pathscomp0; [apply cancel_postcomposition, nat_trans_ax|]. rewrite <- assoc; eapply pathscomp0; [apply maponpaths, (Hf v)|]; simpl; rewrite assoc. eapply pathscomp0. apply cancel_postcomposition. apply (nat_trans_eq_pointwise (@z_iso_after_z_iso_inv [C, D] _ _ (make_z_iso' _ Hα))). now rewrite id_left. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Slice UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Adjunctions.Examples UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.RightKanExtension UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Chains.Chains