Lemma dispPrecompWithBinProductArrow {c d : C} {Pcd : BinProduct C c d} {cc : D c} {dd : D d} (dPcd : dispBinProduct c d Pcd cc dd) {a : C} {aa : D a} {f : a --> c} {g : a --> d} (ff: aa -->[f] cc) (gg: aa -->[g] dd) {x : C} {xx : D x} {k : x --> a} (kk: xx -->[k] aa) : kk ;; dispBinProductArrow Pcd dPcd ff gg = transportb _ (precompWithBinProductArrow C Pcd f g k) (dispBinProductArrow Pcd dPcd (kk ;; ff) (kk ;; gg)). Proof. apply transportb_transpose_right. apply dispBinProductArrowUnique. - rewrite mor_disp_transportf_postwhisker. rewrite assoc_disp_var. rewrite dispBinProductPr1Commutes. rewrite transport_f_f. etrans. { apply maponpaths. apply mor_disp_transportf_prewhisker. } rewrite transport_f_f. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - rewrite mor_disp_transportf_postwhisker. rewrite assoc_disp_var. rewrite dispBinProductPr2Commutes. rewrite transport_f_f. etrans. { apply maponpaths. apply mor_disp_transportf_prewhisker. } rewrite transport_f_f. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.