Definition cod_fiber_functor_from_cleaving_comp_mor {x y z : C} (f : x --> y) (g : y --> z) (φ : C/z) : cod_pb HC f (cod_pb HC g φ) --> cod_pb HC (f · g) φ. Proof. use make_cod_fib_mor. - use PullbackArrow. + exact (PullbackPr1 _ · PullbackPr1 _). + exact (PullbackPr2 _). + abstract (rewrite !assoc ; refine (_ @ maponpaths (λ z, z · g) (PullbackSqrCommutes _)) ; rewrite !assoc' ; apply maponpaths ; cbn ; apply PullbackSqrCommutes). - abstract (cbn ; rewrite PullbackArrow_PullbackPr2 ; 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.