proposition: Proposition total_category_BinCoproductUnique : isaprop (∑ (fg : total_category_BinCoproduct --> t_w), (total_category_BinCoproductIn1 · fg = t_f) × (total_category_BinCoproductIn2 · fg = t_g)).
proof: 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.
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