Proposition cod_fiber_functor_from_cleaving_comp_inv {x y z : C} (f : x --> y) (g : y --> z) (φ : C/z) : fiber_functor_from_cleaving_comp_inv HD g f φ = cod_fiber_functor_from_cleaving_comp_mor_inv 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. use (MorphismsIntoPullbackEqual (isPullback_Pullback _)). + refine (PullbackArrow_PullbackPr1 _ _ _ _ _ @ _). rewrite PullbackArrow_PullbackPr1. rewrite pr1_transportf, transportf_const ; cbn. apply idpath. + refine (PullbackArrow_PullbackPr2 _ _ _ _ _ @ _). rewrite PullbackArrow_PullbackPr2. rewrite id_left. 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.