proposition: Proposition cod_left_beck_chevalley_mor_inv_mor (φ : C/x) : cod_left_beck_chevalley_mor_inv φ · cod_left_beck_chevalley_mor φ = identity _.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod UniMath.CategoryTheory.DisplayedCats.DependentSums