proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions