Definition cod_left_beck_chevalley_mor (φ : C/x) : cod_dom (cod_pb HC k φ) --> cod_dom (cod_pb HC g (cod_fib_comp f φ)). Proof. use PullbackArrow. - exact (PullbackPr1 _). - exact (PullbackPr2 _ · h). - abstract (cbn ; rewrite !assoc ; refine (maponpaths (λ z, z · _) (PullbackSqrCommutes _) @ _) ; rewrite !assoc' ; rewrite p ; 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.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums.