Proposition hset_binary_coprod_struct_sumofmaps {X Y Z : hSet} {PX : P X} {PY : P Y} {PZ : P Z} {f : X → Z} {g : Y → Z} (Pf : mor_hset_struct P PX PZ f) (Pg : mor_hset_struct P PY PZ g) : mor_hset_struct P (hset_struct_binary_coprod EP PX PY) PZ (sumofmaps f g). Proof. exact (pr222 EP X Y Z PX PY PZ f g Pf Pg). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Binproducts. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.MonadAlgebras. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure.