proposition: Proposition binary_coprod_algebra_arrow_unique : isaprop (∑ fg, (binary_coprod_algebra_in1 · fg = φ₁) × (binary_coprod_algebra_in2 · fg = φ₂)).
proof: Proof. use invproofirrelevance. intros ψ₁ ψ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use CoequalizerOutsEq. use BinCoproductArrowsEq. - use mor_from_free_alg_eq. exact (maponpaths pr1 (pr12 ψ₁ @ !(pr12 ψ₂))). - use mor_from_free_alg_eq. exact (maponpaths pr1 (pr22 ψ₁ @ !(pr22 ψ₂))). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits UniMath.CategoryTheory.DisplayedCats.Examples.AlgebraStructures UniMath.CategoryTheory.Monads.Monads