Proposition total_category_BinCoproductUnique : isaprop (∑ (fg : total_category_BinCoproduct --> t_w), (total_category_BinCoproductIn1 · fg = t_f) × (total_category_BinCoproductIn2 · fg = t_g)). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. use isapropdirprod ; apply homset_property. } use total2_paths_f. - use BinCoproductArrowsEq. + exact (maponpaths pr1 (pr12 φ₁ @ !(pr12 φ₂))). + exact (maponpaths pr1 (pr22 φ₁ @ !(pr22 φ₂))). - assert (r : pr11 φ₂ = BinCoproductArrow p f g). { use BinCoproductArrowsEq. + refine (maponpaths pr1 (pr12 φ₂) @ _). cbn. rewrite BinCoproductIn1Commutes. apply idpath. + refine (maponpaths pr1 (pr22 φ₂) @ _). cbn. rewrite BinCoproductIn2Commutes. apply idpath. } rewrite <- (transportbfinv (λ z, _ -->[ z ] _) r (pr21 φ₂)). rewrite <- (transportbfinv (λ z, _ -->[ z ] _) r (transportf _ _ _)). apply maponpaths. use (maponpaths pr1 (proofirrelevance _ (isapropifcontr (pr222 pp w ww f ff g gg)) (transportf _ _ _ ,, _) (transportf _ _ _ ,, _))). + cbn. split. * rewrite !mor_disp_transportf_prewhisker. rewrite !transport_f_f. refine (_ @ fiber_paths (pr12 φ₁)). apply maponpaths_2. apply homset_property. * rewrite !mor_disp_transportf_prewhisker. rewrite !transport_f_f. refine (_ @ fiber_paths (pr22 φ₁)). apply maponpaths_2. apply homset_property. + cbn. split. * rewrite !mor_disp_transportf_prewhisker. rewrite !transport_f_f. refine (_ @ fiber_paths (pr12 φ₂)). apply maponpaths_2. apply homset_property. * rewrite !mor_disp_transportf_prewhisker. rewrite !transport_f_f. refine (_ @ fiber_paths (pr22 φ₂)). 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.