proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Codomain