Definition disjoint_bincoproducts {C : category} (BC : BinCoproducts C) (I : Initial C) : UU := ∏ (x y : C), isMonic (BinCoproductIn1 (BC x y)) × isMonic (BinCoproductIn2 (BC x y)) × isPullback (bincoproduct_intersection BC I x y).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Section FromStable. End FromStable.