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. 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 _ _) @ _). refine (_ @ fiber_paths (arrow'_commutes u)). exact (maponpaths (λ x, x _) (!transportf_const _ _)). - apply impred_isaprop; intro; apply (homset_property (total_category _)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Examples. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.DisplayedCats.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.