proposition: Proposition total_category_CoproductUnique : isaprop (∑ (φ : total_category_Coproduct --> t_w), ∏ (i : I), total_category_CoproductIn i · φ = t_f i).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. use impred ; intro. apply homset_property. } use total2_paths_f. - use CoproductArrow_eq. intro i. exact (maponpaths pr1 (pr2 φ₁ i @ !(pr2 φ₂ i))). - assert (r : pr11 φ₂ = CoproductArrow _ _ p f). { use CoproductArrow_eq. intro i. refine (maponpaths pr1 (pr2 φ₂ i) @ _). cbn. rewrite CoproductInCommutes. apply idpath. } rewrite <- (transportbfinv (λ z, _ -->[ z ] _) r (pr21 φ₂)). rewrite <- (transportbfinv (λ z, _ -->[ z ] _) r (transportf _ _ _)). apply maponpaths. use (maponpaths pr1 (proofirrelevance _ (isapropifcontr (pr22 pp w ww f ff)) (transportf _ _ _ ,, _) (transportf _ _ _ ,, _))). + cbn. intro i. rewrite mor_disp_transportf_prewhisker. rewrite !transport_f_f. rewrite mor_disp_transportf_prewhisker. rewrite !transport_f_f. refine (_ @ fiber_paths (pr2 φ₁ i)). apply maponpaths_2. apply homset_property. + cbn. intro i. rewrite mor_disp_transportf_prewhisker. rewrite transport_f_f. refine (_ @ fiber_paths (pr2 φ₂ i)). 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