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