Proposition cod_fiber_functor_on_mor {x y : C} (f : x --> y) {zg₁ zg₂ : C/y} (gp : zg₁ --> zg₂) : #(cod_pb HC f) gp = cod_fiber_functor_pb f gp. Proof. use eq_mor_cod_fib. cbn. unfold cartesian_cod_disp_map. use (MorphismsIntoPullbackEqual (isPullback_Pullback (HC y (pr1 zg₂) x (pr2 zg₂) f))) ; cbn. - rewrite !PullbackArrow_PullbackPr1. etrans. { apply (PullbackArrow_PullbackPr1 (HC y (pr1 zg₂) x (pr2 zg₂) f)). } rewrite transportf_cod_disp. cbn. apply idpath. - rewrite !PullbackArrow_PullbackPr2. etrans. { apply (PullbackArrow_PullbackPr2 (HC y (pr1 zg₂) x (pr2 zg₂) f)). } apply id_right. 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.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.