Lemma fiber_limit_arrow_unique (h : d' -->[ identity c] fiber_lim) (h_commutes : is_cone_mor d'_cone (fiber_lim_out,, fiber_lim_out_commutes) h) : (h ,, h_commutes) = fiber_limit_arrow,, fiber_limit_arrow_commutes. Proof. use subtypePairEquality. - intro. apply impred_isaprop. intro. apply (homset_property (fiber_category _ _)). - refine (base_paths _ _ (pr2 g (_ ,, _))). use (!fiber_paths (!fu ((identity c · Δ) ,, (h ;; pr12 candidate)) _) @ _). + intro u. use total2_paths_f. * simpl. rewrite id_left. apply (limArrowCommutes L). * abstract ( refine (_ @ (h_commutes u)); cbn; apply transportf_transpose_right; refine (_ @ !mor_disp_transportf_prewhisker _ _ _); apply transportf_transpose_right; refine (_ @ !assoc_disp _ _ _); apply transportf_transpose_right; do 3 refine (transport_f_f _ _ _ _ @ _); apply transportf_set; apply homset_property ). + apply transportf_transpose_right. refine (transport_f_f _ _ _ _ @ _). apply transportf_set. apply homset_property. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.