Proposition total_Equalizer_unique : isaprop (∑ (φ : t_w --> t_e), φ · t_i = t_h). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply homset_property. } use total2_paths_f. - use EqualizerInsEq. exact (maponpaths pr1 (pr2 φ₁ @ !(pr2 φ₂))). - assert (r : pr11 φ₂ = EqualizerIn e w h q). { exact (isEqualizerInUnique _ _ _ _ (pr22 e) _ _ _ (pr11 φ₂) (maponpaths pr1 (pr2 φ₂))). } rewrite <- (transportbfinv (λ z, _ -->[ z ] _) r (pr21 φ₂)). rewrite <- (transportbfinv (λ z, _ -->[ z ] _) r (transportf _ _ _)). apply maponpaths. use (maponpaths pr1 (proofirrelevance _ (isapropifcontr (pr222 ee w ww h hh q qq)) (transportf _ _ _ ,, _) (transportf _ _ _ ,, _))). + cbn. rewrite mor_disp_transportf_postwhisker. rewrite !transport_f_f. rewrite mor_disp_transportf_postwhisker. rewrite !transport_f_f. refine (_ @ fiber_paths (pr2 φ₁)). apply maponpaths_2. apply homset_property. + cbn. rewrite mor_disp_transportf_postwhisker. rewrite transport_f_f. refine (_ @ fiber_paths (pr2 φ₂)). apply maponpaths_2. apply homset_property. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.