Definition cod_left_beck_chevalley_mor_inv (φ : C/x) : cod_dom (cod_pb HC g (cod_fib_comp f φ)) --> cod_dom (cod_pb HC k φ). Proof. use PullbackArrow. - exact (PullbackPr1 _). - use (PullbackArrow P). + exact (PullbackPr1 _ · cod_mor φ). + exact (PullbackPr2 _). + abstract (cbn ; rewrite !assoc' ; apply PullbackSqrCommutes). - abstract (exact (!(PullbackArrow_PullbackPr1 P _ _ _ _))). 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.