Proposition to_is_pullback_slice_mor_unique : isaprop (∑ hk, hk · πs₁ = ζr₁ × hk · πs₂ = ζr₂). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use eq_cod_mor. use (MorphismsIntoPullbackEqual H). - refine (_ @ maponpaths pr1 (pr12 φ₁ @ !pr12 φ₂) @ _). + exact (!(comp_in_cod_fib _ _)). + exact (comp_in_cod_fib _ _). - refine (_ @ maponpaths pr1 (pr22 φ₁ @ !pr22 φ₂) @ _). + exact (!(comp_in_cod_fib _ _)). + exact (comp_in_cod_fib _ _). 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.