Lemma αinv_f_unique y (ccGy : cocone (mapdiagram G d) y) (f : D⟦F L,y⟧) (Hf : is_cocone_mor (mapcocone F d cc) (ccFy y ccGy) f) (HHf : ∏ t : ∑ x, is_cocone_mor (mapcocone F d cc) (ccFy y ccGy) x, t = f,, Hf) f' (Hf' : ∏ v, # G (coconeIn cc v) · f' = coconeIn ccGy v) : f' = pr1 αinv L · f. Proof. transparent assert (HH : (∑ x : D ⟦ F L, y ⟧, is_cocone_mor (mapcocone F d cc) (ccFy y ccGy) x)). { use tpair. - apply (pr1 α L · f'). - unfold is_cocone_mor; cbn. abstract (intro v; rewrite <- Hf', !assoc; apply cancel_postcomposition, nat_trans_ax). } apply pathsinv0. generalize (maponpaths pr1 (HHf HH)); intro Htemp; simpl in *. rewrite <- Htemp; 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 apply id_left. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Slice. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Adjunctions.Examples. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Chains.Chains.