Library UniMath.CategoryTheory.Monoidal.Examples.DisplayedCartesianMonoidal

********************************************************** Ralph Matthes 2022
********************************************************** Contents :
  • constructs a displayed monoidal category that is displayed over a cartesian monoidal category with the displayed tensor and displayed unit coming from displayed binary products and displayed terminal objects

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.terminal.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Binproducts.

Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal.
Require Import UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Import BifunctorNotations.
Import MonoidalNotations.
Import DisplayedBifunctorNotations.

Section FixADisplayedCategory.

  Context {C : category} (CP : BinProducts C) (terminal : Terminal C)
    (D : disp_cat C) (dP : dispBinProducts D CP) (dterminal : dispTerminal D terminal).

  Local Definition M : monoidal C := cartesian_monoidal C CP terminal.

  Definition DCM_tensor_data : disp_bifunctor_data M D D D.
  Show proof.
    use make_disp_bifunctor_data.
    - intros c d cc dd.
      exact (dispBinProductObject D (CP c d) (dP c d cc dd)).
    - intros c d1 d2 g cc dd1 dd2 gg.
      exact (dispBinProductOfArrows _ _ _ (id_disp cc) gg).
    - intros c1 c2 d f cc1 cc2 dd ff.
      exact (dispBinProductOfArrows _ _ _ ff (id_disp dd)).

  Definition DCM_tensor_laws : is_disp_bifunctor M DCM_tensor_data.
  Show proof.
    red; repeat split; red; intros.
    - cbn. unfold dispBinProductOfArrows. apply pathsinv0. apply dispBinProductArrowUnique.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        rewrite id_left_disp.
        rewrite id_right_disp.
        rewrite transport_b_b.
        apply transportf_comp_lemma.
        rewrite transport_f_b.
        apply transportf_comp_lemma_hset;
            try apply homset_property; apply idpath.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        rewrite id_left_disp.
        rewrite id_right_disp.
        rewrite transport_b_b.
        apply transportf_comp_lemma.
        rewrite transport_f_b.
        apply transportf_comp_lemma_hset;
          try apply homset_property; apply idpath.
    - cbn. unfold dispBinProductOfArrows. apply pathsinv0. apply dispBinProductArrowUnique.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        rewrite id_left_disp.
        rewrite id_right_disp.
        rewrite transport_b_b.
        apply transportf_comp_lemma.
        rewrite transport_f_b.
        apply transportf_comp_lemma_hset;
            try apply homset_property; apply idpath.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        rewrite id_left_disp.
        rewrite id_right_disp.
        rewrite transport_b_b.
        apply transportf_comp_lemma.
        rewrite transport_f_b.
        apply transportf_comp_lemma_hset;
          try apply homset_property; apply idpath.
    - cbn. unfold dispBinProductOfArrows. apply pathsinv0. apply dispBinProductArrowUnique.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        rewrite id_right_disp.
        rewrite transport_b_b.
        apply pathsinv0, transportf_comp_lemma.
        rewrite assoc_disp_var.
        etrans; [| apply maponpaths, maponpaths, pathsinv0, dispBinProductPr1Commutes].
        apply transportf_comp_lemma.
        rewrite id_right_disp.
        rewrite transport_b_b.
        etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
        apply transportf_comp_lemma.
        etrans; [| apply pathsinv0, dispBinProductPr1Commutes].
        rewrite transport_b_b.
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset;
          try apply homset_property; apply idpath.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        rewrite id_right_disp.
        apply pathsinv0, transportf_comp_lemma.
        rewrite assoc_disp_var.
        etrans; [| apply maponpaths, maponpaths, pathsinv0, dispBinProductPr2Commutes].
        apply transportf_comp_lemma.
        etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
        apply transportf_comp_lemma.
        etrans; [| rewrite assoc_disp; apply idpath].
        match goal with | [ |- _ = transportb _ _ (?auxH1 ;; gg2) ] => set (aux1 := auxH1) end.
        assert (H: aux1 = transportb (mor_disp (dispBinProductObject D (CP x y1) (dP x y1 xx yy1)) yy2)
           (BinProductPr2Commutes C x y2 (CP x y2) (BinProductObject C (CP x y1))
              (BinProductPr1 C (CP x y1) · identity x) (BinProductPr2 C (CP x y1) · g1))
           (dispBinProductPr2 D (CP x y1) (dP x y1 xx yy1) ;; gg1)).
        { apply dispBinProductPr2Commutes. }
        apply transportf_comp_lemma.
        unfold transportb in H.
        etrans; [| apply pathsinv0, (cancel_postcomposition_disp gg2 H)].
        clear aux1 H.
        rewrite assoc_disp_var.
        rewrite transport_f_f.
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset;
          try apply homset_property; apply idpath.
    - cbn. unfold dispBinProductOfArrows. apply pathsinv0. apply dispBinProductArrowUnique.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        rewrite id_right_disp.
        apply pathsinv0, transportf_comp_lemma.
        rewrite assoc_disp_var.
        etrans; [| apply maponpaths, maponpaths, pathsinv0, dispBinProductPr1Commutes].
        apply transportf_comp_lemma.
        etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
        etrans; [| rewrite assoc_disp; apply idpath].
        unfold transportb.
        rewrite transport_f_f.
        match goal with | [ |- _ = transportf _ _ (?auxH1 ;; ff2) ] => set (aux1 := auxH1) end.
        assert (H: aux1 = transportb (mor_disp (dispBinProductObject D (CP x1 y) (dP x1 y xx1 yy)) xx2)
           (BinProductPr1Commutes C x2 y (CP x2 y) (BinProductObject C (CP x1 y))
              (BinProductPr1 C (CP x1 y) · f1) (BinProductPr2 C (CP x1 y) · identity y))
           (dispBinProductPr1 D (CP x1 y) (dP x1 y xx1 yy) ;; ff1)).
        { apply dispBinProductPr1Commutes. }
        apply transportf_comp_lemma.
        unfold transportb in H.
        etrans; [| apply pathsinv0, (cancel_postcomposition_disp ff2 H)].
        clear aux1 H.
        rewrite assoc_disp_var.
        rewrite transport_f_f.
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset;
          try apply homset_property; apply idpath.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        do 2 rewrite id_right_disp.
        rewrite transport_b_b.
        apply pathsinv0, transportf_comp_lemma.
        rewrite assoc_disp_var.
        etrans; [| apply maponpaths, maponpaths, pathsinv0, dispBinProductPr2Commutes].
        apply transportf_comp_lemma.
        rewrite transport_b_b.
        etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
        apply transportf_comp_lemma.
        etrans; [| apply pathsinv0, dispBinProductPr2Commutes].
        rewrite transport_b_b.
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset;
          try apply homset_property; apply idpath.
    - cbn. unfold dispfunctoronmorphisms1, dispfunctoronmorphisms2,
        disp_leftwhiskering_on_morphisms, disp_rightwhiskering_on_morphisms.
      cbn. do 2 rewrite dispBinProductOfArrows_comp.
      do 2 rewrite id_left_disp.
      do 2 rewrite id_right_disp.
      rewrite transport_b_b.
      apply transportf_comp_lemma.
      unfold dispBinProductOfArrows. apply dispBinProductArrowUnique.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        etrans; [apply maponpaths, dispBinProductPr1Commutes |].
        rewrite transport_f_b.
        apply transportf_comp_lemma.
        etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
        etrans; [apply maponpaths, mor_disp_transportf_prewhisker |].
        rewrite transport_f_f.
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        etrans; [apply maponpaths, dispBinProductPr2Commutes |].
        rewrite transport_f_b.
        apply transportf_comp_lemma.
        etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
        etrans; [apply maponpaths, mor_disp_transportf_prewhisker |].
        rewrite transport_f_f.
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.

  Definition DCM_tensor : disp_tensor D M.
  Show proof.
    use make_disp_bifunctor.
    - exact DCM_tensor_data.
    - exact DCM_tensor_laws.

  Definition DCM_unit : D I_{ M} := dispTerminalObject _ dterminal.

  Definition DCM_leftunitor_data : disp_leftunitor_data DCM_tensor DCM_unit.
  Show proof.
    red; intros. apply dispBinProductPr2.

  Definition DCM_leftunitorinv_data : disp_leftunitorinv_data DCM_tensor DCM_unit.
  Show proof.
    red; intros. apply dispBinProductArrow.
    - apply dispTerminalArrow.
    - apply id_disp.

  Definition DCM_rightunitor_data : disp_rightunitor_data DCM_tensor DCM_unit.
  Show proof.
    red; intros. apply dispBinProductPr1.

  Definition DCM_rightunitorinv_data : disp_rightunitorinv_data DCM_tensor DCM_unit.
  Show proof.
    red; intros. apply dispBinProductArrow.
    - apply id_disp.
    - apply dispTerminalArrow.

  Definition DCM_associator_data : disp_associator_data DCM_tensor.
  Show proof.
    red; intros.
    apply dispBinProductArrow.
    + use comp_disp.
      2: {apply dispBinProductPr1. }
      apply dispBinProductPr1.
    + apply dispBinProductArrow.
      * use comp_disp.
        2: {apply dispBinProductPr1. }
        apply dispBinProductPr2.
      * apply dispBinProductPr2.

  Definition DCM_associatorinv_data : disp_associatorinv_data DCM_tensor.
  Show proof.
    red; intros.
    apply dispBinProductArrow.
    + apply dispBinProductArrow.
      * apply dispBinProductPr1.
      * use comp_disp.
        2: {apply dispBinProductPr2. }
        apply dispBinProductPr1.
    + use comp_disp.
      2: {apply dispBinProductPr2. }
      apply dispBinProductPr2.

  Definition DCM_data : disp_monoidal_data D M.
  Show proof.
    exists DCM_tensor. exists DCM_unit.
    repeat split.
    - exact DCM_leftunitor_data.
    - exact DCM_leftunitorinv_data.
    - exact DCM_rightunitor_data.
    - exact DCM_rightunitorinv_data.
    - exact DCM_associator_data.
    - exact DCM_associatorinv_data.


  Lemma DCM_leftunitor_law : disp_leftunitor_law DCM_leftunitor_data DCM_leftunitorinv_data.
  Show proof.
    split; [| split]; try red; intros.
    - cbn.
      etrans.
      { apply dispBinProductOfArrowsPr2. }
      unfold DCM_leftunitor_data.
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - cbn. unfold DCM_leftunitorinv_data, DCM_leftunitor_data.
      rewrite dispBinProductPr2Commutes.
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - cbn. unfold DCM_leftunitorinv_data, DCM_leftunitor_data.
      apply pathsinv0.
      etrans.
      2: { simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). shelve.            + apply dispTerminalArrowEq.            + shelve.            + rewrite assoc_disp_var.
             rewrite dispBinProductPr2Commutes.
             apply pathsinv0, transportf_comp_lemma.
             etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
             rewrite id_right_disp.
             rewrite transport_f_b.
             apply transportf_comp_lemma.
             apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      }
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      Unshelve.
      rewrite <- assoc. rewrite BinProductPr2Commutes. apply id_right.

  Lemma DCM_rightunitor_law : disp_rightunitor_law DCM_rightunitor_data DCM_rightunitorinv_data.
  Show proof.
    split; [| split]; try red; intros.
    - cbn. unfold DCM_rightunitor_data.
      etrans; [apply dispBinProductOfArrowsPr1 |].
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - cbn. unfold DCM_rightunitorinv_data, DCM_rightunitor_data.
      rewrite dispBinProductPr1Commutes.
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - cbn. unfold DCM_rightunitorinv_data, DCM_rightunitor_data.
      apply pathsinv0.
      etrans.
      2: { simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). shelve.            + rewrite assoc_disp_var.
             rewrite dispBinProductPr1Commutes.
             apply pathsinv0, transportf_comp_lemma.
             etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
             rewrite id_right_disp.
             rewrite transport_f_b.
             apply transportf_comp_lemma.
             apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
           + shelve.            + apply dispTerminalArrowEq.       }
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      Unshelve.
      rewrite <- assoc. rewrite BinProductPr1Commutes. apply id_right.


  Lemma DCM_associator_law : disp_associator_law DCM_associator_data DCM_associatorinv_data.
  Show proof.
    repeat split; try red; intros.
    - unfold DCM_associator_data. cbn.
      rewrite dispPostcompWithBinProductArrow.
      apply pathsinv0, transportf_comp_lemma.
      apply dispBinProductArrowUnique.
      + rewrite id_right_disp.
        rewrite transport_b_b.
        etrans; [apply mor_disp_transportf_postwhisker |].
        apply pathsinv0, transportf_comp_lemma.
        rewrite assoc_disp_var.
        rewrite dispBinProductPr1Commutes.
        apply transportf_comp_lemma.
        etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
        apply transportf_comp_lemma.
        rewrite assoc_disp.
        rewrite dispBinProductOfArrowsPr1.
        apply transportf_comp_lemma.
        rewrite id_right_disp.
        rewrite transport_b_b.
        etrans; [| apply pathsinv0, mor_disp_transportf_postwhisker].
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        rewrite assoc_disp_var.
        rewrite dispBinProductPr2Commutes.
        rewrite transport_f_f.
        etrans; [apply maponpaths, mor_disp_transportf_prewhisker |].
        rewrite transport_f_f.
        rewrite dispPrecompWithBinProductArrow.
        rewrite transport_f_b.
        apply pathsinv0, transportf_comp_lemma.
        apply dispBinProductArrowUnique.
        * etrans; [ apply mor_disp_transportf_postwhisker |].
          apply pathsinv0, transportf_comp_lemma.
          rewrite assoc_disp_var.
          rewrite dispBinProductOfArrowsPr1.
          rewrite id_right_disp.
          rewrite transport_b_b.
          apply transportf_comp_lemma.
          etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
          rewrite dispBinProductPr1Commutes.
          rewrite transport_f_b.
          apply pathsinv0, transportf_comp_lemma.
          rewrite assoc_disp.
          rewrite dispBinProductOfArrowsPr1.
          rewrite id_right_disp.
          rewrite transport_b_b.
          etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker].
          rewrite transport_b_f.
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
        * etrans; [ apply mor_disp_transportf_postwhisker |].
          apply pathsinv0, transportf_comp_lemma.
          rewrite assoc_disp_var.
          rewrite dispBinProductOfArrowsPr2.
          rewrite transport_f_b.
          apply transportf_comp_lemma.
          rewrite dispBinProductOfArrowsPr2.
          etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
          apply transportf_comp_lemma.
          rewrite assoc_disp.
          rewrite dispBinProductPr2Commutes.
          etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker].
          rewrite transport_b_f.
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - unfold DCM_associator_data. cbn.
      rewrite dispPostcompWithBinProductArrow.
      apply pathsinv0, transportf_comp_lemma.
      apply dispBinProductArrowUnique.
      + rewrite dispPrecompWithBinProductArrow.
        rewrite transport_f_b.
        etrans; [ apply mor_disp_transportf_postwhisker |].
        rewrite dispBinProductPr1Commutes.
        rewrite transport_f_b.
        apply pathsinv0, transportf_comp_lemma.
        rewrite assoc_disp.
        rewrite dispBinProductOfArrowsPr1.
        etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker].
        rewrite transport_b_f.
        etrans.
        2: { rewrite assoc_disp_var.
             rewrite dispBinProductOfArrowsPr1.
             rewrite transport_f_f.
             unfold transportb.
             rewrite mor_disp_transportf_prewhisker.
             rewrite transport_f_f.
             rewrite assoc_disp.
             rewrite transport_f_b.
             apply idpath.
        }
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      + etrans; [ apply mor_disp_transportf_postwhisker |].
        rewrite assoc_disp_var.
        rewrite dispBinProductPr2Commutes.
        rewrite transport_f_f.
        etrans; [apply maponpaths, mor_disp_transportf_prewhisker |].
        rewrite transport_f_f.
        rewrite dispPrecompWithBinProductArrow.
        rewrite transport_f_b.
        apply pathsinv0, transportf_comp_lemma.
        apply dispBinProductArrowUnique.
        * rewrite id_right_disp.
          rewrite transport_f_b.
          etrans; [ apply mor_disp_transportf_postwhisker |].
          apply pathsinv0, transportf_comp_lemma.
          rewrite dispBinProductPr1Commutes.
          apply pathsinv0, transportf_comp_lemma.
          rewrite assoc_disp.
          rewrite dispBinProductOfArrowsPr1.
          etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker].
          rewrite transport_b_f.
          apply transportf_comp_lemma.
          rewrite assoc_disp_var.
          rewrite dispBinProductOfArrowsPr2.
          rewrite id_right_disp.
          rewrite transport_b_b.
          etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_prewhisker].
          rewrite transport_f_f.
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
        * etrans; [ apply mor_disp_transportf_postwhisker |].
          apply pathsinv0, transportf_comp_lemma.
          rewrite assoc_disp_var.
          rewrite dispBinProductOfArrowsPr2.
          rewrite transport_f_b.
          apply transportf_comp_lemma.
          rewrite id_left_disp.
          etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
          rewrite id_right_disp.
          rewrite transport_f_b.
          rewrite dispBinProductPr2Commutes.
          rewrite transport_f_b.
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - unfold DCM_associator_data. cbn.
      rewrite dispPostcompWithBinProductArrow.
      apply pathsinv0, transportf_comp_lemma.
      apply dispBinProductArrowUnique.
      + rewrite dispPrecompWithBinProductArrow.
        rewrite transport_f_b.
        etrans; [ apply mor_disp_transportf_postwhisker |].
        rewrite dispBinProductPr1Commutes.
        rewrite transport_f_b.
        apply pathsinv0, transportf_comp_lemma.
        rewrite assoc_disp.
        rewrite dispBinProductOfArrowsPr1.
        etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker].
        rewrite transport_b_f.
        etrans.
        2: { rewrite assoc_disp_var.
             rewrite dispBinProductOfArrowsPr1.
             rewrite transport_f_f.
             unfold transportb.
             rewrite mor_disp_transportf_prewhisker.
             rewrite transport_f_f.
             rewrite id_right_disp.
             unfold transportb.
             rewrite mor_disp_transportf_prewhisker.
             rewrite transport_f_f.
             apply idpath.
        }
        apply pathsinv0, transportf_comp_lemma.
        rewrite assoc_disp_var.
        rewrite id_right_disp.
        unfold transportb.
        rewrite mor_disp_transportf_prewhisker.
        rewrite transport_f_f.
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        rewrite assoc_disp_var.
        rewrite dispBinProductPr2Commutes.
        rewrite transport_f_f.
        etrans; [apply maponpaths, mor_disp_transportf_prewhisker |].
        rewrite transport_f_f.
        rewrite dispPrecompWithBinProductArrow.
        rewrite transport_f_b.
        apply pathsinv0, transportf_comp_lemma.
        apply dispBinProductArrowUnique.
        * etrans; [apply mor_disp_transportf_postwhisker |].
          apply pathsinv0, transportf_comp_lemma.
          rewrite assoc_disp_var.
          rewrite dispBinProductOfArrowsPr1.
          etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_prewhisker].
          rewrite transport_f_f.
          apply transportf_comp_lemma.
          etrans.
          2: { rewrite assoc_disp.
               rewrite dispBinProductPr1Commutes.
               unfold transportb.
               rewrite mor_disp_transportf_postwhisker.
               rewrite transport_f_f.
               apply idpath.
          }
          apply pathsinv0, transportf_comp_lemma.
          etrans.
          2: { rewrite assoc_disp.
               rewrite dispBinProductOfArrowsPr1.
               apply maponpaths.
               apply pathsinv0, mor_disp_transportf_postwhisker.
          }
          rewrite transport_b_f.
          etrans.
          2: { rewrite assoc_disp_var.
               rewrite dispBinProductOfArrowsPr2.
               unfold transportb.
               rewrite mor_disp_transportf_prewhisker.
               rewrite transport_f_f.
               rewrite assoc_disp.
               rewrite transport_f_f.
               rewrite transport_f_b.
               apply idpath.
          }
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
        * etrans; [apply mor_disp_transportf_postwhisker |].
          apply pathsinv0, transportf_comp_lemma.
          rewrite assoc_disp_var.
          do 2 rewrite dispBinProductOfArrowsPr2.
          rewrite transport_f_b.
          rewrite id_right_disp.
          rewrite transport_f_b.
          apply transportf_comp_lemma.
          etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
          rewrite id_right_disp.
          etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_prewhisker].
          rewrite dispBinProductPr2Commutes.
          rewrite transport_f_f.
          rewrite transport_f_b.
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - unfold DCM_associator_data, DCM_associatorinv_data. cbn.
      etrans.
      { apply pathsinv0. simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _).
        + change (αinv^{M}_{ x, y, z} · α^{M}_{ x, y, z} · BinProductPr1 C (CP x (y ⊗_{M} z)) = BinProductPr1 C (CP x (y ⊗_{M} z))).
it thus appears as intermediary result in Lemma CartesianMonoidalCategoriesWhiskered.associator_law_from_binprod, but we reprove it here, analogously with the three other goals of this kind to come
          cbn.
          rewrite <- assoc.
          rewrite BinProductPr1Commutes.
          rewrite assoc.
          rewrite BinProductPr1Commutes.
          apply BinProductPr1Commutes.
        + rewrite assoc_disp_var.
          rewrite dispBinProductPr1Commutes.
          etrans; [apply maponpaths, mor_disp_transportf_prewhisker |].
          rewrite transport_f_f.
          apply pathsinv0, transportf_comp_lemma.
          rewrite assoc_disp.
          rewrite dispBinProductPr1Commutes.
          unfold transportb.
          rewrite mor_disp_transportf_postwhisker.
          rewrite dispBinProductPr1Commutes.
          rewrite transport_f_f.
          rewrite transport_f_b.
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
        + change( αinv^{M}_{ x, y, z} · α^{M}_{ x, y, z} · BinProductPr2 C (CP x (y ⊗_{M} z)) = BinProductPr2 C (CP x (y ⊗_{M} z))).
          cbn.
          rewrite <- assoc.
          rewrite BinProductPr2Commutes.
          rewrite precompWithBinProductArrow.
          rewrite BinProductPr2Commutes.
          rewrite assoc.
          rewrite BinProductPr1Commutes.
          rewrite BinProductPr2Commutes.
          apply pathsinv0, BinProductArrowUnique; apply idpath.
        + rewrite assoc_disp_var.
          rewrite dispBinProductPr2Commutes.
          etrans; [apply maponpaths, mor_disp_transportf_prewhisker |].
          rewrite transport_f_f.
          apply pathsinv0, transportf_comp_lemma.
          rewrite dispPrecompWithBinProductArrow.
          apply transportf_comp_lemma.
          apply dispBinProductArrowUnique.
          * etrans; [apply mor_disp_transportf_postwhisker |].
            apply transportf_comp_lemma.
            rewrite assoc_disp.
            rewrite dispBinProductPr1Commutes.
            etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker].
            rewrite dispBinProductPr2Commutes.
            rewrite transport_b_f.
            rewrite transport_f_b.
            apply transportf_comp_lemma.
            apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
          * etrans; [apply mor_disp_transportf_postwhisker |].
            apply transportf_comp_lemma.
            rewrite dispBinProductPr2Commutes.
            apply transportf_comp_lemma.
            apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      }
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - unfold DCM_associator_data, DCM_associatorinv_data. cbn.
      etrans.
      { apply pathsinv0. simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _).
        + change (α^{M}_{ x, y, z} · αinv^{M}_{ x, y, z} · BinProductPr1 C (CP (x ⊗_{M} y) z) = BinProductPr1 C (CP (x ⊗_{M} y) z)).
          cbn.
          rewrite <- assoc.
          rewrite BinProductPr1Commutes.
          rewrite precompWithBinProductArrow.
          apply pathsinv0, BinProductArrowUnique.
          * apply pathsinv0, BinProductPr1Commutes.
          * rewrite assoc.
            rewrite BinProductPr2Commutes.
            apply pathsinv0, BinProductPr1Commutes.
        + rewrite assoc_disp_var.
          rewrite dispBinProductPr1Commutes.
          apply pathsinv0, transportf_comp_lemma.
          etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
          rewrite dispPrecompWithBinProductArrow.
          rewrite transport_f_b.
          apply transportf_comp_lemma.
          apply dispBinProductArrowUnique.
          * etrans; [apply mor_disp_transportf_postwhisker |].
            apply transportf_comp_lemma.
            rewrite dispBinProductPr1Commutes.
            apply transportf_comp_lemma.
            apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
          * etrans; [apply mor_disp_transportf_postwhisker |].
            apply transportf_comp_lemma.
            rewrite assoc_disp.
            rewrite dispBinProductPr2Commutes.
            etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker].
            rewrite dispBinProductPr1Commutes.
            rewrite transport_b_f.
            rewrite transport_f_b.
            apply transportf_comp_lemma.
            apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
        + change (α^{M}_{ x, y, z} · αinv^{M}_{ x, y, z} · BinProductPr2 C (CP (x ⊗_{M} y) z) = BinProductPr2 C (CP (x ⊗_{M} y) z)).
          cbn.
          rewrite <- assoc.
          rewrite BinProductPr2Commutes.
          rewrite assoc.
          rewrite BinProductPr2Commutes.
          apply BinProductPr2Commutes.
        + rewrite assoc_disp_var.
          rewrite dispBinProductPr2Commutes.
          etrans; [apply maponpaths, mor_disp_transportf_prewhisker |].
          rewrite transport_f_f.
          apply pathsinv0, transportf_comp_lemma.
          rewrite assoc_disp.
          rewrite dispBinProductPr2Commutes.
          unfold transportb.
          rewrite mor_disp_transportf_postwhisker.
          rewrite dispBinProductPr2Commutes.
          rewrite transport_f_f.
          rewrite transport_f_b.
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      }
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.

  Lemma DCM_triangle_identity : disp_triangle_identity DCM_leftunitor_data DCM_rightunitor_data DCM_associator_data.
  Show proof.
    red; intros.
    cbn. unfold DCM_associator_data.
    rewrite dispPostcompWithBinProductArrow.
    apply pathsinv0, transportf_comp_lemma.
    apply dispBinProductArrowUnique.
    - etrans; [apply mor_disp_transportf_postwhisker |].
      apply pathsinv0, transportf_comp_lemma.
      etrans; [| apply pathsinv0, dispBinProductOfArrowsPr1].
      unfold DCM_rightunitor_data.
      rewrite assoc_disp_var.
      rewrite id_right_disp.
      rewrite transport_f_f.
      apply pathsinv0, transportf_comp_lemma.
      etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker].
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - etrans; [apply mor_disp_transportf_postwhisker |].
      apply pathsinv0, transportf_comp_lemma.
      etrans; [| apply pathsinv0, dispBinProductOfArrowsPr2].
      rewrite id_right_disp.
      unfold DCM_leftunitor_data.
      apply pathsinv0, transportf_comp_lemma.
      rewrite dispBinProductPr2Commutes.
      rewrite transport_f_b.
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.

  Lemma DCM_pentagon_identity : disp_pentagon_identity DCM_associator_data.
  Show proof.
    red; intros.
    unfold DCM_associator_data. cbn.
    etrans; [apply assoc_disp_var |].
    apply pathsinv0, transportf_comp_lemma.
    etrans.
    2: { rewrite dispPostcompWithBinProductArrow.
         rewrite dispPrecompWithBinProductArrow.
         unfold transportb.
         apply pathsinv0, mor_disp_transportf_prewhisker.
    }
    etrans; [| apply maponpaths, pathsinv0, dispPrecompWithBinProductArrow].
    rewrite transport_f_b.
    apply pathsinv0, transportf_comp_lemma.
    etrans; [| apply pathsinv0, dispPrecompWithBinProductArrow].
    apply transportf_comp_lemma.
    apply dispBinProductArrowUnique.
    - etrans; [apply mor_disp_transportf_postwhisker |].
      apply pathsinv0, transportf_comp_lemma.
      etrans.
      2: { rewrite dispBinProductPr1Commutes.
           apply maponpaths.
           rewrite id_right_disp.
           unfold transportb.
           rewrite mor_disp_transportf_prewhisker.
           apply maponpaths.
           rewrite assoc_disp.
           apply maponpaths.
           rewrite dispBinProductOfArrowsPr1.
           unfold transportb.
           rewrite mor_disp_transportf_postwhisker.
           apply maponpaths.
           rewrite assoc_disp_var.
           rewrite dispBinProductPr1Commutes.
           unfold transportb.
           rewrite mor_disp_transportf_prewhisker.
           rewrite assoc_disp.
           rewrite transport_f_f.
           rewrite transport_f_b.
           apply idpath.
      }
      rewrite transport_b_f.
      rewrite transport_f_b.
      do 2 rewrite transport_f_f.
      apply pathsinv0, transportf_comp_lemma.
      etrans.
      2: { rewrite assoc_disp.
           apply maponpaths.
           rewrite dispBinProductPr1Commutes.
           unfold transportb.
           rewrite mor_disp_transportf_postwhisker.
           apply idpath.
      }
      rewrite transport_b_f.
      apply transportf_comp_lemma.
      apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
    - etrans; [apply mor_disp_transportf_postwhisker |].
      apply pathsinv0, transportf_comp_lemma.
      etrans.
      2: { rewrite dispBinProductPr2Commutes.
           apply maponpaths.
           rewrite mor_disp_transportf_prewhisker.
           apply maponpaths.
           apply pathsinv0, dispPrecompWithBinProductArrow.
      }
      rewrite transport_b_f.
      rewrite transport_f_b.
      apply transportf_comp_lemma.
      apply dispBinProductArrowUnique.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        apply pathsinv0, transportf_comp_lemma.
        etrans.
        2: { rewrite dispPrecompWithBinProductArrow.
             unfold transportb.
             rewrite mor_disp_transportf_postwhisker.
             apply maponpaths.
             rewrite dispBinProductPr1Commutes.
             apply maponpaths.
             rewrite assoc_disp.
             apply maponpaths.
             rewrite dispBinProductPr1Commutes.
             unfold transportb.
             rewrite mor_disp_transportf_postwhisker.
             apply idpath.
        }
        do 2 rewrite transport_f_b.
        rewrite transport_f_f.
        apply pathsinv0, transportf_comp_lemma.
        etrans.
        2: { apply maponpaths. rewrite assoc_disp.
             apply maponpaths.
             rewrite dispBinProductPr1Commutes.
             unfold transportb.
             rewrite mor_disp_transportf_postwhisker.
             apply idpath.
        }
        etrans.
        2: { rewrite transport_b_f.
             rewrite mor_disp_transportf_prewhisker.
             apply maponpaths.
             rewrite assoc_disp.
             apply maponpaths.
             rewrite assoc_disp.
             rewrite dispBinProductOfArrowsPr1.
             unfold transportb.
             rewrite mor_disp_transportf_postwhisker.
             rewrite assoc_disp_var.
             rewrite transport_f_f.
             apply maponpaths.
             rewrite mor_disp_transportf_postwhisker.
             apply maponpaths.
             rewrite assoc_disp_var.
             apply maponpaths.
             apply maponpaths.
             rewrite assoc_disp.
             rewrite dispBinProductPr2Commutes.
             unfold transportb.
             rewrite mor_disp_transportf_postwhisker.
             rewrite dispBinProductPr1Commutes.
             rewrite transport_f_f.
             rewrite transport_f_b.
             apply idpath.
        }
        rewrite transport_f_b.
        rewrite mor_disp_transportf_prewhisker.
        do 4 rewrite transport_f_f.
        apply transportf_comp_lemma.
        rewrite assoc_disp.
        apply transportf_comp_lemma.
        apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
      + etrans; [apply mor_disp_transportf_postwhisker |].
        apply pathsinv0, transportf_comp_lemma.
        etrans.
        2: { rewrite dispPrecompWithBinProductArrow.
             unfold transportb.
             rewrite mor_disp_transportf_postwhisker.
             apply maponpaths.
             rewrite dispBinProductPr2Commutes.
             apply maponpaths.
             rewrite dispBinProductPr2Commutes.
             apply idpath.
        }
        do 2 rewrite transport_f_b.
        apply transportf_comp_lemma.
        apply dispBinProductArrowUnique.
        * rewrite mor_disp_transportf_postwhisker.
          apply pathsinv0, transportf_comp_lemma.
          etrans.
          2: { rewrite assoc_disp_var.
               apply maponpaths.
               apply maponpaths.
               rewrite assoc_disp_var.
               rewrite dispBinProductPr1Commutes.
               unfold transportb.
               rewrite mor_disp_transportf_prewhisker.
               rewrite transport_f_f.
               rewrite assoc_disp.
               rewrite dispBinProductPr1Commutes.
               unfold transportb.
               rewrite mor_disp_transportf_postwhisker.
               do 2 rewrite transport_f_f.
               apply idpath.
          }
          etrans.
          2: { rewrite mor_disp_transportf_prewhisker.
               rewrite transport_f_f.
               apply idpath. }
          apply transportf_comp_lemma.
          etrans.
          2: { apply maponpaths.
               rewrite assoc_disp_var.
               apply idpath. }
          etrans.
          2: { rewrite mor_disp_transportf_prewhisker.
               apply maponpaths.
               rewrite assoc_disp.
               rewrite dispBinProductOfArrowsPr1.
               unfold transportb.
               rewrite mor_disp_transportf_postwhisker.
               rewrite transport_f_f.
               apply maponpaths.
               rewrite assoc_disp_var.
               do 2 apply maponpaths.
               rewrite assoc_disp.
               rewrite dispBinProductPr2Commutes.
               unfold transportb.
               rewrite mor_disp_transportf_postwhisker.
               rewrite transport_f_f.
               rewrite dispBinProductPr2Commutes.
               rewrite transport_f_b.
               apply idpath.
          }
          rewrite mor_disp_transportf_prewhisker.
          do 3 rewrite transport_f_f.
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
        * rewrite mor_disp_transportf_postwhisker.
          apply pathsinv0, transportf_comp_lemma.
          etrans.
          2: { rewrite assoc_disp_var.
               apply maponpaths.
               apply maponpaths.
               rewrite assoc_disp_var.
               rewrite dispBinProductPr2Commutes.
               unfold transportb.
               rewrite mor_disp_transportf_prewhisker.
               rewrite transport_f_f.
               rewrite dispBinProductPr2Commutes.
               rewrite transport_f_b.
               apply idpath.
          }
          rewrite mor_disp_transportf_prewhisker.
          rewrite transport_f_f.
          apply transportf_comp_lemma.
          etrans.
          2: { rewrite dispBinProductOfArrowsPr2.
               rewrite id_right_disp.
               rewrite transport_b_b.
               apply idpath. }
          apply transportf_comp_lemma.
          apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.

  Lemma DCM_laws : disp_monoidal_laws DCM_data.
  Show proof.
    exists DCM_leftunitor_law.
    exists DCM_rightunitor_law.
    exists DCM_associator_law.
    exists DCM_triangle_identity.
    exact DCM_pentagon_identity.

  Definition displayedcartesianmonoidalcat: disp_monoidal D M := DCM_data ,, DCM_laws.
End FixADisplayedCategory.