Definition cod_fiber_functor_pb {x y : C} (f : x --> y) {zg₁ zg₂ : C/y} (gp : zg₁ --> zg₂) : cod_pb HC f zg₁ --> cod_pb HC f zg₂. Proof. simple refine (_ ,, _) ; cbn. - use PullbackArrow. + exact (PullbackPr1 _ · pr1 gp). + apply PullbackPr2. + abstract (refine (_ @ PullbackSqrCommutes (HC y (pr1 zg₁) x (pr2 zg₁) f)) ; rewrite !assoc' ; apply maponpaths ; refine (pr2 gp @ _) ; apply id_right). - abstract (rewrite PullbackArrow_PullbackPr2 ; rewrite id_right ; 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.