proposition: Lemma cartesian'_limit_arrow_unique (arrow' : cartesian' ⟦ tip', lim L,, cartesian'_limit_tip ⟧) (arrow'_commutes : is_cone_mor cone' (make_cone _ cartesian'_limit_forms_cone) arrow') : (arrow' ,, arrow'_commutes) = (cartesian'_limit_arrow ,, cartesian'_limit_arrow_commutes).
proof: Proof. use total2_paths_f. - use total2_paths2. + apply (limArrowUnique L). intro u. exact (maponpaths pr1 (arrow'_commutes u)). + apply (limArrowUnique L'). intro u. refine (maponpaths (λ x, x _) (!transportf_const _ _) @ _). exact (fiber_paths (arrow'_commutes u)). - apply impred_isaprop; intro; apply (homset_property (total_category _)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Examples UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.Limits UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Fiber