Proposition from_is_pullback_slice_mor_unique : isaprop (∑ hk, hk · π₁ = ζ₁ × hk · π₂ = ζ₂). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } simple refine (maponpaths dom_mor (MorphismsIntoPullbackEqual H wφ (make_cod_fib_mor _ _) (make_cod_fib_mor _ _) _ _)). - cbn. rewrite <- (mor_eq πs₁). rewrite !assoc. refine (maponpaths (λ z, z · _) (pr12 φ₁) @ _). apply idpath. - cbn. rewrite <- (mor_eq πs₁). rewrite !assoc. refine (maponpaths (λ z, z · _) (pr12 φ₂) @ _). apply idpath. - use eq_mor_cod_fib. rewrite !comp_in_cod_fib ; cbn. exact (pr12 φ₁ @ !pr12 φ₂). - use eq_mor_cod_fib. rewrite !comp_in_cod_fib ; cbn. exact (pr22 φ₁ @ !pr22 φ₂). 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.