Proposition isPullback_to_isBinproduct_cod_fib_unique : isaprop (∑ (fg : wh --> gp), fg · π₁ = φq × fg · π₂ = ψr). Proof. use invproofirrelevance. intros ζ₁ ζ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use eq_mor_cod_fib. use (MorphismsIntoPullbackEqual (isPullback_Pullback P)). - pose (s := maponpaths dom_mor (pr12 ζ₁ @ !(pr12 ζ₂))). rewrite !comp_in_cod_fib in s. exact s. - pose (s := maponpaths dom_mor (pr22 ζ₁ @ !(pr22 ζ₂))). rewrite !comp_in_cod_fib in s. exact s. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.PullbackConstructions. Require Import UniMath.CategoryTheory.Limits.Preservation. 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.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseEqualizers. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLeftAdjoint. Section FromEqCodFib. End FromEqCodFib. Section FromUMP. End FromUMP.