Proposition cod_left_beck_chevalley_mor_inv_mor (φ : C/x) : cod_left_beck_chevalley_mor_inv φ · cod_left_beck_chevalley_mor φ = identity _. Proof. use (MorphismsIntoPullbackEqual (isPullback_Pullback _)). - unfold cod_left_beck_chevalley_mor, cod_left_beck_chevalley_mor_inv. rewrite !assoc'. etrans. { apply maponpaths. apply PullbackArrow_PullbackPr1. } etrans. { apply PullbackArrow_PullbackPr1. } rewrite id_left. apply idpath. - unfold cod_left_beck_chevalley_mor, cod_left_beck_chevalley_mor_inv. rewrite !assoc'. etrans. { apply maponpaths. apply PullbackArrow_PullbackPr2. } rewrite id_left. rewrite !assoc. rewrite PullbackArrow_PullbackPr2. apply (PullbackArrow_PullbackPr2 P). Qed.
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.