Definition to_bincoproduct_slice : isBinCoproduct (C/y) _ _ _ ι₁ ι₂. Proof. intros h ρ₁ ρ₂. use iscontraprop1. - exact (to_bincoproduct_slice_unique ρ₁ ρ₂). - simple refine (_ ,, _ ,, _). + exact (to_bincoproduct_slice_mor ρ₁ ρ₂). + apply to_bincoproduct_slice_mor_in1. + apply to_bincoproduct_slice_mor_in2. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.