Skip to content

Make DisplayedCartesianMonoidalCategoriesWhiskered fit the style #30

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: issue1576forbifunctors
Choose a base branch
from
Open

Make DisplayedCartesianMonoidalCategoriesWhiskered fit the style #30

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2c4a9ac
Small change
nmvdw Oct 27, 2022
e459db9
Make the file fit the style
nmvdw Oct 27, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 4 additions & 8 deletions UniMath/CategoryTheory/Monoidal/DisplayedCartesianMonoidalCategoriesWhiskered.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,8 @@ Require Import UniMath.CategoryTheory.Monoidal.DisplayedMonoidalWhiskered.

Require Import UniMath.CategoryTheory.Monoidal.CartesianMonoidalCategoriesWhiskered.

Require Export UniMath.Tactics.EnsureStructuredProofs.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Expand Down Expand Up @@ -277,8 +279,6 @@ Section FixADisplayedCategory.
- exact DCM_associatorinv_data.
Defined.

Set Default Goal Selector "1".

Lemma DCM_leftunitor_law : disp_leftunitor_law DCM_leftunitor_data DCM_leftunitorinv_data.
Proof.
split; [| split]; try red; intros.
Expand All @@ -297,9 +297,8 @@ Set Default Goal Selector "1".
(* eapply (pathscomp0(b:=?[sh1])).
Show sh1. *)
etrans.
2: { simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). shelve. (* creates one shelved goal *)
2: { refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). (* creates one shelved goal *)
+ apply dispTerminalArrowEq. (* resolves the shelved goal *)
+ shelve. (* creates one shelved goal *)
+ rewrite assoc_disp_var.
rewrite dispBinProductPr2Commutes.
apply pathsinv0, transportf_comp_lemma.
Expand Down Expand Up @@ -329,7 +328,7 @@ Set Default Goal Selector "1".
- cbn. unfold DCM_rightunitorinv_data, DCM_rightunitor_data.
apply pathsinv0.
etrans.
2: { simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). shelve. (* creates one shelved goal *)
2: { refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). (* creates one shelved goal *)
(* Show shH1. *)
+ rewrite assoc_disp_var.
rewrite dispBinProductPr1Commutes.
Expand All @@ -339,7 +338,6 @@ Set Default Goal Selector "1".
rewrite transport_f_b.
apply transportf_comp_lemma.
apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
+ shelve. (* creates one shelved goal *)
+ apply dispTerminalArrowEq. (* resolves second shelved goal *)
(* Show shH1. *)
}
Expand All @@ -349,8 +347,6 @@ Set Default Goal Selector "1".
rewrite <- assoc. rewrite BinProductPr1Commutes. apply id_right.
Qed.

Export Set Default Goal Selector "!".

Lemma DCM_associator_law : disp_associator_law DCM_associator_data DCM_associatorinv_data.
Proof.
repeat split; try red; intros.
Expand Down