proposition: 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: 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.
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