Definition cod_fiber_functor_on_eq_mor {x y : C} {f g : x --> y} (p : f = g) (φ : C/y) : fiber_functor_from_cleaving (disp_codomain C) (disp_codomain_cleaving HC) f φ --> fiber_functor_from_cleaving (disp_codomain C) (disp_codomain_cleaving HC) g φ. Proof. use make_cod_fib_mor. - use PullbackArrow. + apply PullbackPr1. + apply PullbackPr2. + abstract (refine (PullbackSqrCommutes (HC y (pr1 φ) x (pr2 φ) f) @ _) ; apply maponpaths ; exact p). - abstract (cbn ; rewrite PullbackArrow_PullbackPr2 ; apply idpath). Defined.
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.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. 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.Univalence.