Definition from_stable_inv : PB y (BC a b) x (cod_fib_coproduct_ob_mor ag₁ bg₂ (BC a b)) f --> apbp. Proof. use (PullbackArrow Hpb). - apply PullbackPr1. - apply PullbackPr2. - abstract (apply PullbackSqrCommutes). Defined.
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.