Lemma sigma_lim_arrow_unique (t : ∑ x, is_cone_mor d'_cone (make_cone _ forms_cone_sigma_disp_cat) x) : t = sigma_lim_arrow ,, sigma_lim_arrow_commutes. Proof. use subtypePairEquality. { intro. apply impred_isaprop. intro. apply homset_property. } pose (f' := (# sigma_to_E_total_functor)%cat (pr1 t)). pose (Hf' := λ u, maponpaths (# sigma_to_E_total_functor)%cat (pr2 t u)). pose (uniq := limArrowUnique d_cone _ e_cone f' Hf'). exact (maponpaths (# E_to_sigma_total_functor)%cat uniq). 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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core. 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.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Limits.