Proposition binary_coprod_algebra_arrow_unique : isaprop (∑ fg, (binary_coprod_algebra_in1 · fg = φ₁) × (binary_coprod_algebra_in2 · fg = φ₂)). 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.BinProducts. 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.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.AlgebraStructures. Require Import UniMath.CategoryTheory.Monads.Monads.