proposition: Proposition cartesian_cod_disp_comm_pr1 : cartesian_cod_disp_map · l = k.
proof: Proof. apply (PullbackArrow_PullbackPr1 P). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Fibrations