Proposition cod_left_beck_chevalley_mor_mor_inv (φ : C/x) : cod_left_beck_chevalley_mor φ · cod_left_beck_chevalley_mor_inv φ = 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. use (MorphismsIntoPullbackEqual (isPullback_Pullback P)). + rewrite !assoc'. etrans. { apply maponpaths. apply (PullbackArrow_PullbackPr1 P). } rewrite !assoc. rewrite PullbackArrow_PullbackPr1. apply PullbackSqrCommutes. + rewrite !assoc'. etrans. { apply maponpaths. apply (PullbackArrow_PullbackPr2 P). } apply PullbackArrow_PullbackPr2. 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.