Skip to content

Commit 6a93fb9

Browse files
AlizterAlizter
authored
Merge pull request #1934 from jdchristensen/opposites-involutive
Trick to make Is1Cat definitionally involutive
2 parents 6cb7ba0 + 3f1c0b0 commit 6a93fb9

File tree

19 files changed

+156
-72
lines changed

19 files changed

+156
-72
lines changed

‎test/WildCat/Opposite.v‎

Lines changed: 18 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,22 @@
1-
From HoTT Require Import Basics WildCat.Core WildCat.Opposite.
1+
From HoTT Require Import Basics WildCat.Core WildCat.Opposite WildCat.Equiv.
22

3-
(* Opposites are (almost) definitionally involutive. *)
3+
(** * Opposites are definitionally involutive. *)
44

55
Definition test1 A : A = (A^op)^op :> Type := 1.
6-
Definition test2 A `{x : IsGraph A} : x = isgraph_op (A := A^op) := 1.
7-
Definition test3 A `{x : Is01Cat A} : x = is01cat_op (A := A^op) := 1.
8-
Definition test4 A `{x : Is2Graph A} : x = is2graph_op (A := A^op) := 1.
6+
Definition test2 A `{x : IsGraph A} : x = @isgraph_op A^op (@isgraph_op A x) := 1.
7+
Definition test3 A `{x : Is01Cat A} : x = @is01cat_op A^op _ (@is01cat_op A _ x) := 1.
8+
Definition test4 A `{x : Is2Graph A} : x = @is2graph_op A^op _ (@is2graph_op A _ x) := 1.
9+
Definition test5 A `{x : Is1Cat A} : x = @is1cat_op A^op _ _ _ (@is1cat_op A _ _ _ x) := 1.
910

10-
(** Is1Cat is not definitionally involutive. *)
11-
Fail Definition test4 A `{x : Is1Cat A} : x = is1cat_op (A := A^op) := 1.
11+
(** * [core] only partially commutes with taking the opposite category. *)
12+
Definition core1 A `{HasEquivs A} : (core A)^op = core A^op :> Type := 1.
13+
Definition core2 A `{HasEquivs A} : isgraph_op (A:=core A) = isgraph_core (A:=A^op) := 1.
14+
Definition core3 A `{HasEquivs A} : is01cat_op (A:=core A) = is01cat_core (A:=A^op) := 1.
15+
Definition core4 A `{HasEquivs A} : is2graph_op (A:=core A) = is2graph_core (A:=A^op) := 1.
16+
17+
(** This also passes, but we comment it out as it is slow. When uncommented, to save time, we end with [Admitted.] instead of [Defined.] *)
18+
(*
19+
Definition core5 A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op).
20+
Time reflexivity. (* ~6s *)
21+
Admitted.
22+
*)

‎theories/Algebra/AbSES/Core.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -275,7 +275,7 @@ Global Instance is2graph_abses
275275
Global Instance is1cat_abses {A B : AbGroup@{u}}
276276
: Is1Cat (AbSES B A).
277277
Proof.
278-
snrapply Build_Is1Cat.
278+
snrapply Build_Is1Cat'.
279279
1: intros ? ?; apply is01cat_abses_path_data.
280280
1: intros ? ?; apply is0gpd_abses_path_data.
281281
3-5: cbn; reflexivity.

‎theories/Algebra/Rings/Module.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -269,7 +269,7 @@ Global Instance is2graph_leftmodule {R : Ring} : Is2Graph (LeftModule R)
269269

270270
Global Instance is1cat_leftmodule {R : Ring} : Is1Cat (LeftModule R).
271271
Proof.
272-
snrapply Build_Is1Cat.
272+
snrapply Build_Is1Cat'.
273273
- intros M N; rapply is01cat_induced.
274274
- intros M N; rapply is0gpd_induced.
275275
- intros M N L h.

‎theories/Algebra/Universal/Homomorphism.v‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,7 @@ Global Instance is1cat_strong_algebra `{Funext} (σ : Signature)
190190
Proof.
191191
rapply Build_Is1Cat_Strong.
192192
- intros. apply assoc_homomorphism_compose.
193+
- intros. symmetry; apply assoc_homomorphism_compose.
193194
- intros. apply left_id_homomorphism_compose.
194195
- intros. apply right_id_homomorphism_compose.
195196
Defined.

‎theories/Homotopy/SuccessorStructure.v‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -217,7 +217,8 @@ Defined.
217217

218218
Global Instance is1cat_ss : Is1Cat SuccStr.
219219
Proof.
220-
srapply Build_Is1Cat.
220+
snrapply Build_Is1Cat'.
221+
1,2: exact _.
221222
- intros X Y Z g.
222223
snrapply Build_Is0Functor.
223224
intros f h p.

‎theories/Pointed/Core.v‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -570,7 +570,8 @@ Defined.
570570
(** pType is a 1-coherent 1-category *)
571571
Global Instance is1cat_ptype : Is1Cat pType.
572572
Proof.
573-
econstructor.
573+
snrapply Build_Is1Cat'.
574+
1, 2: exact _.
574575
- intros A B C h; rapply Build_Is0Functor.
575576
intros f g p; cbn.
576577
apply pmap_postwhisker; assumption.
@@ -602,7 +603,8 @@ Definition path_zero_morphism_pconst (A B : pType)
602603
(** pForall is a 1-category *)
603604
Global Instance is1cat_pforall (A : pType) (P : pFam A) : Is1Cat (pForall A P) | 10.
604605
Proof.
605-
econstructor.
606+
snrapply Build_Is1Cat'.
607+
1, 2: exact _.
606608
- intros f g h p; rapply Build_Is0Functor.
607609
intros q r s. exact (phomotopy_postwhisker s p).
608610
- intros f g h p; rapply Build_Is0Functor.

‎theories/WildCat/Core.v‎

Lines changed: 22 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,8 @@ Class Is1Cat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
102102
is0functor_precomp : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f) ;
103103
cat_assoc : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
104104
(h $o g) $o f $== h $o (g $o f);
105+
cat_assoc_opp : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
106+
h $o (g $o f) $== (h $o g) $o f;
105107
cat_idl : forall (a b : A) (f : a $-> b), Id b $o f $== f;
106108
cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f;
107109
}.
@@ -111,13 +113,23 @@ Global Existing Instance is0gpd_hom.
111113
Global Existing Instance is0functor_postcomp.
112114
Global Existing Instance is0functor_precomp.
113115
Arguments cat_assoc {_ _ _ _ _ _ _ _ _} f g h.
116+
Arguments cat_assoc_opp {_ _ _ _ _ _ _ _ _} f g h.
114117
Arguments cat_idl {_ _ _ _ _ _ _} f.
115118
Arguments cat_idr {_ _ _ _ _ _ _} f.
116119

117-
Definition cat_assoc_opp {A : Type} `{Is1Cat A}
118-
{a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
119-
: h $o (g $o f) $== (h $o g) $o f
120-
:= (cat_assoc f g h)^$.
120+
(** An alternate constructor that doesn't require the proof of [cat_assoc_opp]. This can be used for defining examples of wild categories, but shouldn't be used for the general theory of wild categories. *)
121+
Definition Build_Is1Cat' (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A}
122+
(is01cat_hom : forall a b : A, Is01Cat (a $-> b))
123+
(is0gpd_hom : forall a b : A, Is0Gpd (a $-> b))
124+
(is0functor_postcomp : forall (a b c : A) (g : b $-> c), Is0Functor (cat_postcomp a g))
125+
(is0functor_precomp : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f))
126+
(cat_assoc : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
127+
h $o g $o f $== h $o (g $o f))
128+
(cat_idl : forall (a b : A) (f : a $-> b), Id b $o f $== f)
129+
(cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f)
130+
: Is1Cat A
131+
:= Build_Is1Cat A _ _ _ is01cat_hom is0gpd_hom is0functor_postcomp is0functor_precomp
132+
cat_assoc (fun a b c d f g h => (cat_assoc a b c d f g h)^$) cat_idl cat_idr.
121133

122134
(** Whiskering and horizontal composition of 2-cells. *)
123135

@@ -175,19 +187,18 @@ Class Is1Cat_Strong (A : Type)`{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
175187
cat_assoc_strong : forall (a b c d : A)
176188
(f : a $-> b) (g : b $-> c) (h : c $-> d),
177189
(h $o g) $o f = h $o (g $o f) ;
190+
cat_assoc_opp_strong : forall (a b c d : A)
191+
(f : a $-> b) (g : b $-> c) (h : c $-> d),
192+
h $o (g $o f) = (h $o g) $o f ;
178193
cat_idl_strong : forall (a b : A) (f : a $-> b), Id b $o f = f ;
179194
cat_idr_strong : forall (a b : A) (f : a $-> b), f $o Id a = f ;
180195
}.
181196

182197
Arguments cat_assoc_strong {_ _ _ _ _ _ _ _ _} f g h.
198+
Arguments cat_assoc_opp_strong {_ _ _ _ _ _ _ _ _} f g h.
183199
Arguments cat_idl_strong {_ _ _ _ _ _ _} f.
184200
Arguments cat_idr_strong {_ _ _ _ _ _ _} f.
185201

186-
Definition cat_assoc_opp_strong {A : Type} `{Is1Cat_Strong A}
187-
{a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
188-
: h $o (g $o f) = (h $o g) $o f
189-
:= (cat_assoc_strong f g h)^.
190-
191202
Global Instance is1cat_is1cat_strong (A : Type) `{Is1Cat_Strong A}
192203
: Is1Cat A | 1000.
193204
Proof.
@@ -198,6 +209,7 @@ Proof.
198209
- apply is0functor_postcomp_strong.
199210
- apply is0functor_precomp_strong.
200211
- intros; apply GpdHom_path, cat_assoc_strong.
212+
- intros; apply GpdHom_path, cat_assoc_opp_strong.
201213
- intros; apply GpdHom_path, cat_idl_strong.
202214
- intros; apply GpdHom_path, cat_idr_strong.
203215
Defined.
@@ -247,6 +259,7 @@ Global Instance is1cat_strong_hasmorext {A : Type} `{HasMorExt A}
247259
Proof.
248260
rapply Build_Is1Cat_Strong; hnf; intros; apply path_hom.
249261
+ apply cat_assoc.
262+
+ apply cat_assoc_opp.
250263
+ apply cat_idl.
251264
+ apply cat_idr.
252265
Defined.

‎theories/WildCat/Displayed.v‎

Lines changed: 22 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,11 @@ Class IsD1Cat {A : Type} `{Is1Cat A}
106106
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
107107
DHom (cat_assoc f g h) ((h' $o' g') $o' f')
108108
(h' $o' (g' $o' f'));
109+
dcat_assoc_opp : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
110+
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
111+
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
112+
DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f'))
113+
((h' $o' g') $o' f');
109114
dcat_idl : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
110115
(f' : DHom f a' b'), DHom (cat_idl f) (DId b' $o' f') f';
111116
dcat_idr : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
@@ -117,13 +122,6 @@ Global Existing Instance isd0gpd_hom.
117122
Global Existing Instance isd0functor_postcomp.
118123
Global Existing Instance isd0functor_precomp.
119124

120-
Definition dcat_assoc_opp {A : Type} {D : A -> Type} `{IsD1Cat A D}
121-
{a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
122-
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
123-
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d')
124-
: DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f')) ((h' $o' g') $o' f')
125-
:= (dcat_assoc f' g' h')^$'.
126-
127125
Definition dcat_postwhisker {A : Type} {D : A -> Type} `{IsD1Cat A D}
128126
{a b c : A} {f g : a $-> b} {h : b $-> c} {p : f $== g}
129127
{a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'}
@@ -234,6 +232,8 @@ Proof.
234232
exact (p $@R f; p' $@R' f').
235233
- intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].
236234
exact (cat_assoc f g h; dcat_assoc f' g' h').
235+
- intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].
236+
exact (cat_assoc_opp f g h; dcat_assoc_opp f' g' h').
237237
- intros [a a'] [b b'] [f f'].
238238
exact (cat_idl f; dcat_idl f').
239239
- intros [a a'] [b b'] [f f'].
@@ -275,6 +275,11 @@ Class IsD1Cat_Strong {A : Type} `{Is1Cat_Strong A}
275275
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
276276
(transport (fun k => DHom k a' d') (cat_assoc_strong f g h)
277277
((h' $o' g') $o' f')) = h' $o' (g' $o' f');
278+
dcat_assoc_opp_strong : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
279+
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
280+
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
281+
(transport (fun k => DHom k a' d') (cat_assoc_opp_strong f g h)
282+
(h' $o' (g' $o' f'))) = (h' $o' g') $o' f';
278283
dcat_idl_strong : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
279284
(f' : DHom f a' b'),
280285
(transport (fun k => DHom k a' b') (cat_idl_strong f)
@@ -290,6 +295,7 @@ Global Existing Instance isd0gpd_hom_strong.
290295
Global Existing Instance isd0functor_postcomp_strong.
291296
Global Existing Instance isd0functor_precomp_strong.
292297

298+
(* If in the future we make a [Build_Is1Cat_Strong'] that lets the user omit the second proof of associativity, this shows how it can be recovered from the original proof:
293299
Definition dcat_assoc_opp_strong {A : Type} {D : A -> Type} `{IsD1Cat_Strong A D}
294300
{a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
295301
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
@@ -300,13 +306,16 @@ Proof.
300306
apply (moveR_transport_V (fun k => DHom k a' d') (cat_assoc_strong f g h) _ _).
301307
exact ((dcat_assoc_strong f' g' h')^).
302308
Defined.
309+
*)
303310

304311
Global Instance isd1cat_isd1catstrong {A : Type} (D : A -> Type)
305312
`{IsD1Cat_Strong A D} : IsD1Cat D.
306313
Proof.
307314
srapply Build_IsD1Cat.
308315
- intros a b c d f g h a' b' c' d' f' g' h'.
309316
exact (DHom_path (cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
317+
- intros a b c d f g h a' b' c' d' f' g' h'.
318+
exact (DHom_path (cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
310319
- intros a b f a' b' f'.
311320
exact (DHom_path (cat_idl_strong f) (dcat_idl_strong f')).
312321
- intros a b f a' b' f'.
@@ -321,6 +330,9 @@ Proof.
321330
- intros aa' bb' cc' dd' [f f'] [g g'] [h h'].
322331
exact (path_sigma' _
323332
(cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
333+
- intros aa' bb' cc' dd' [f f'] [g g'] [h h'].
334+
exact (path_sigma' _
335+
(cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
324336
- intros aa' bb' [f f'].
325337
exact (path_sigma' _ (cat_idl_strong f) (dcat_idl_strong f')).
326338
- intros aa' bb' [f f'].
@@ -506,6 +518,9 @@ Proof.
506518
- intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.
507519
intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].
508520
exact (dcat_assoc f1' f2' f3', dcat_assoc g1' g2' g3').
521+
- intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.
522+
intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].
523+
exact (dcat_assoc_opp f1' f2' f3', dcat_assoc_opp g1' g2' g3').
509524
- intros ab1 ab2 fg ab1' ab2' [f' g'].
510525
exact (dcat_idl f', dcat_idl g').
511526
- intros ab1 ab2 fg ab1' ab2' [f' g'].

‎theories/WildCat/DisplayedEquiv.v‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,7 @@ Defined.
160160
Global Instance dcatie_id {A} {D : A -> Type} `{DHasEquivs A D}
161161
{a : A} (a' : D a)
162162
: DCatIsEquiv (DId a')
163-
:= dcatie_adjointify (DId a') (DId a') (dcat_idl (DId a')) (dcat_idl (DId a')).
163+
:= dcatie_adjointify (DId a') (DId a') (dcat_idl (DId a')) (dcat_idr (DId a')).
164164

165165
Definition did_cate {A} {D : A -> Type} `{DHasEquivs A D}
166166
{a : A} (a' : D a)
@@ -205,10 +205,10 @@ Proof.
205205
refine (_ $@L' (dcate_isretr _ $@R' _) $@' _).
206206
refine (_ $@L' dcat_idl _ $@' _).
207207
apply dcate_isretr.
208-
- refine (dcat_assoc _ _ _ $@' _).
209-
refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
210-
refine (_ $@L' (dcate_issect _ $@R' _) $@' _).
211-
refine (_ $@L' dcat_idl _ $@' _).
208+
- refine (dcat_assoc_opp _ _ _ $@' _).
209+
refine (dcat_assoc _ _ _ $@R' _ $@' _).
210+
refine (((_ $@L' dcate_issect _) $@R' _) $@' _).
211+
refine ((dcat_idr _ $@R' _) $@' _).
212212
apply dcate_issect.
213213
Defined.
214214

‎theories/WildCat/Equiv.v‎

Lines changed: 16 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,7 @@ Defined.
137137
(** The identity morphism is an equivalence *)
138138
Global Instance catie_id {A} `{HasEquivs A} (a : A)
139139
: CatIsEquiv (Id a)
140-
:= catie_adjointify (Id a) (Id a) (cat_idl (Id a)) (cat_idl (Id a)).
140+
:= catie_adjointify (Id a) (Id a) (cat_idl (Id a)) (cat_idr (Id a)).
141141

142142
Definition id_cate {A} `{HasEquivs A} (a : A)
143143
: a $<~> a
@@ -177,10 +177,10 @@ Proof.
177177
refine ((_ $@L (cate_isretr _ $@R _)) $@ _).
178178
refine ((_ $@L cat_idl _) $@ _).
179179
apply cate_isretr.
180-
- refine (cat_assoc _ _ _ $@ _).
181-
refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
182-
refine ((_ $@L (cate_issect _ $@R _)) $@ _).
183-
refine ((_ $@L cat_idl _) $@ _).
180+
- refine (cat_assoc_opp _ _ _ $@ _).
181+
refine ((cat_assoc _ _ _ $@R _) $@ _).
182+
refine (((_ $@L cate_issect _) $@R _) $@ _).
183+
refine ((cat_idr _ $@R _) $@ _).
184184
apply cate_issect.
185185
Defined.
186186

@@ -226,6 +226,16 @@ Proof.
226226
- refine (_ $@L compose_cate_funinv g f).
227227
Defined.
228228

229+
Definition compose_cate_assoc_opp {A} `{HasEquivs A}
230+
{a b c d : A} (f : a $<~> b) (g : b $<~> c) (h : c $<~> d)
231+
: cate_fun (h $oE (g $oE f)) $== cate_fun ((h $oE g) $oE f).
232+
Proof.
233+
refine (compose_cate_fun h _ $@ _ $@ cat_assoc_opp f g h $@ _ $@
234+
compose_cate_funinv _ f).
235+
- refine (_ $@L compose_cate_fun g f).
236+
- refine (compose_cate_funinv h g $@R _).
237+
Defined.
238+
229239
Definition compose_cate_idl {A} `{HasEquivs A}
230240
{a b : A} (f : a $<~> b)
231241
: cate_fun (id_cate b $oE f) $== cate_fun f.
@@ -559,6 +569,7 @@ Global Instance is1cat_core {A : Type} `{HasEquivs A}
559569
Proof.
560570
rapply Build_Is1Cat.
561571
- intros; apply compose_cate_assoc.
572+
- intros; apply compose_cate_assoc_opp.
562573
- intros; apply compose_cate_idl.
563574
- intros; apply compose_cate_idr.
564575
Defined.

0 commit comments

Comments
 (0)