Proposition cod_fiber_functor_from_cleaving_comp {x y z : C} (f : x --> y) (g : y --> z) (φ : C/z) : fiber_functor_from_cleaving_comp HD g f φ = cod_fiber_functor_from_cleaving_comp_mor f g φ. Proof. use eq_mor_cod_fib. use (MorphismsIntoPullbackEqual (isPullback_Pullback _)). - cbn. unfold cartesian_cod_disp_map ; cbn. refine (PullbackArrow_PullbackPr1 _ _ _ _ _ @ _). rewrite PullbackArrow_PullbackPr1. unfold transportb ; cbn. rewrite pr1_transportf, transportf_const. cbn. apply idpath. - cbn. unfold cartesian_cod_disp_map ; cbn. refine (PullbackArrow_PullbackPr2 _ _ _ _ _ @ _). rewrite PullbackArrow_PullbackPr2. 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.