Proposition cod_fiber_functor_on_eq {x y : C} {f g : x --> y} (p : f = g) (φ : C/y) : fiber_functor_on_eq HD p φ = cod_fiber_functor_on_eq_mor p φ. Proof. induction p. use eq_mor_cod_fib. use (MorphismsIntoPullbackEqual (isPullback_Pullback _)). - cbn. rewrite PullbackArrow_PullbackPr1. rewrite id_left. apply idpath. - cbn. rewrite PullbackArrow_PullbackPr2. rewrite id_left. apply idpath. 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.