Definition cod_fib_pb_comp {x y : C} (f : x --> y) (zg : C/x) : zg --> cod_pb HC f (cod_fib_comp f zg). Proof. simple refine (_ ,, _). - use PullbackArrow. + exact (identity _). + exact (pr2 zg). + abstract (apply id_left). - abstract (cbn ; rewrite PullbackArrow_PullbackPr2 ; rewrite id_right ; apply idpath). Defined.
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.