proposition: Proposition total_Coequalizer_unique : isaprop (∑ (φ : t_e --> t_w), t_i · φ = t_h).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply homset_property. } use total2_paths_f. - use CoequalizerOutsEq. exact (maponpaths pr1 (pr2 φ₁ @ !(pr2 φ₂))). - assert (r : pr11 φ₂ = CoequalizerOut e w h q). { exact (isCoequalizerOutUnique _ _ _ _ (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_prewhisker. rewrite !transport_f_f. rewrite mor_disp_transportf_prewhisker. rewrite !transport_f_f. refine (_ @ fiber_paths (pr2 φ₁)). apply maponpaths_2. apply homset_property. + cbn. rewrite mor_disp_transportf_prewhisker. rewrite transport_f_f. refine (_ @ fiber_paths (pr2 φ₂)). apply maponpaths_2. apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total