Trick to make Is1Cat definitionally involutive

test/WildCat/Opposite.v

@@ -1,11 +1,22 @@
-From HoTT Require Import Basics WildCat.Core WildCat.Opposite.
+From HoTT Require Import Basics WildCat.Core WildCat.Opposite WildCat.Equiv.
 
-(* Opposites are (almost) definitionally involutive. *)
+(** * Opposites are definitionally involutive. *)
 
 Definition test1 A : A = (A^op)^op :> Type := 1.
-Definition test2 A `{x : IsGraph A} : x = isgraph_op (A := A^op) := 1.
-Definition test3 A `{x : Is01Cat A} : x = is01cat_op (A := A^op) := 1.
-Definition test4 A `{x : Is2Graph A} : x = is2graph_op (A := A^op) := 1.
+Definition test2 A `{x : IsGraph A} : x = @isgraph_op A^op (@isgraph_op A x) := 1.
+Definition test3 A `{x : Is01Cat A} : x = @is01cat_op A^op _ (@is01cat_op A _ x) := 1.
+Definition test4 A `{x : Is2Graph A} : x = @is2graph_op A^op _ (@is2graph_op A _ x) := 1.
+Definition test5 A `{x : Is1Cat A} : x = @is1cat_op A^op _ _ _ (@is1cat_op A _ _ _ x) := 1.
 
-(** Is1Cat is not definitionally involutive. *)
-Fail Definition test4 A `{x : Is1Cat A} : x = is1cat_op (A := A^op) := 1.
+(** * [core] only partially commutes with taking the opposite category. *)
+Definition core1 A `{HasEquivs A} : (core A)^op = core A^op :> Type := 1.
+Definition core2 A `{HasEquivs A} : isgraph_op (A:=core A) = isgraph_core (A:=A^op) := 1.
+Definition core3 A `{HasEquivs A} : is01cat_op (A:=core A) = is01cat_core (A:=A^op) := 1.
+Definition core4 A `{HasEquivs A} : is2graph_op (A:=core A) = is2graph_core (A:=A^op) := 1.
+
+(** This also passes, but we comment it out as it is slow.  When uncommented, to save time, we end with [Admitted.] instead of [Defined.] *)
+(*
+Definition core5 A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op).
+  Time reflexivity. (* ~6s *)
+Admitted.
+*)

theories/Algebra/AbSES/Core.v

@@ -275,7 +275,7 @@ Global Instance is2graph_abses
 Global Instance is1cat_abses {A B : AbGroup@{u}}
   : Is1Cat (AbSES B A).
 Proof.
-  snrapply Build_Is1Cat.
+  snrapply Build_Is1Cat'.
   1: intros ? ?; apply is01cat_abses_path_data.
   1: intros ? ?; apply is0gpd_abses_path_data.
   3-5: cbn; reflexivity.

theories/Algebra/Rings/Module.v

@@ -269,7 +269,7 @@ Global Instance is2graph_leftmodule {R : Ring} : Is2Graph (LeftModule R)
 
 Global Instance is1cat_leftmodule {R : Ring} : Is1Cat (LeftModule R).
 Proof.
-  snrapply Build_Is1Cat.
+  snrapply Build_Is1Cat'.
   - intros M N; rapply is01cat_induced.
   - intros M N; rapply is0gpd_induced.
   - intros M N L h.

theories/Algebra/Universal/Homomorphism.v

@@ -190,6 +190,7 @@ Global Instance is1cat_strong_algebra `{Funext} (σ : Signature)
 Proof.
   rapply Build_Is1Cat_Strong.
   - intros. apply assoc_homomorphism_compose.
+  - intros. symmetry; apply assoc_homomorphism_compose.
   - intros. apply left_id_homomorphism_compose.
   - intros. apply right_id_homomorphism_compose.
 Defined.

theories/Homotopy/SuccessorStructure.v

@@ -217,7 +217,8 @@ Defined.
 
 Global Instance is1cat_ss : Is1Cat SuccStr.
 Proof.
-  srapply Build_Is1Cat.
+  snrapply Build_Is1Cat'.
+  1,2: exact _.
   - intros X Y Z g.
     snrapply Build_Is0Functor.
     intros f h p.

theories/Pointed/Core.v

@@ -570,7 +570,8 @@ Defined.
 (** pType is a 1-coherent 1-category *)
 Global Instance is1cat_ptype : Is1Cat pType.
 Proof.
-  econstructor.
+  snrapply Build_Is1Cat'.
+  1, 2: exact _.
   - intros A B C h; rapply Build_Is0Functor.
     intros f g p; cbn.
     apply pmap_postwhisker; assumption.
@@ -602,7 +603,8 @@ Definition path_zero_morphism_pconst (A B : pType)
 (** pForall is a 1-category *)
 Global Instance is1cat_pforall (A : pType) (P : pFam A) : Is1Cat (pForall A P) | 10.
 Proof.
-  econstructor.
+  snrapply Build_Is1Cat'.
+  1, 2: exact _.
   - intros f g h p; rapply Build_Is0Functor.
     intros q r s. exact (phomotopy_postwhisker s p).
   - intros f g h p; rapply Build_Is0Functor.

theories/WildCat/Core.v

@@ -102,6 +102,8 @@ Class Is1Cat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
   is0functor_precomp : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f) ;
   cat_assoc : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
     (h $o g) $o f $== h $o (g $o f);
+  cat_assoc_opp : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
+    h $o (g $o f) $== (h $o g) $o f;
   cat_idl : forall (a b : A) (f : a $-> b), Id b $o f $== f;
   cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f;
 }.
@@ -111,13 +113,23 @@ Global Existing Instance is0gpd_hom.
 Global Existing Instance is0functor_postcomp.
 Global Existing Instance is0functor_precomp.
 Arguments cat_assoc {_ _ _ _ _ _ _ _ _} f g h.
+Arguments cat_assoc_opp {_ _ _ _ _ _ _ _ _} f g h.
 Arguments cat_idl {_ _ _ _ _ _ _} f.
 Arguments cat_idr {_ _ _ _ _ _ _} f.
 
-Definition cat_assoc_opp {A : Type} `{Is1Cat A}
-           {a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
-  : h $o (g $o f) $== (h $o g) $o f
-  := (cat_assoc f g h)^$.
+(** 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. *)
+Definition Build_Is1Cat' (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A}
+  (is01cat_hom : forall a b : A, Is01Cat (a $-> b))
+  (is0gpd_hom : forall a b : A, Is0Gpd (a $-> b))
+  (is0functor_postcomp : forall (a b c : A) (g : b $-> c), Is0Functor (cat_postcomp a g))
+  (is0functor_precomp : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f))
+  (cat_assoc : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
+      h $o g $o f $== h $o (g $o f))
+  (cat_idl : forall (a b : A) (f : a $-> b), Id b $o f $== f)
+  (cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f)
+  : Is1Cat A
+  := Build_Is1Cat A _ _ _ is01cat_hom is0gpd_hom is0functor_postcomp is0functor_precomp
+      cat_assoc (fun a b c d f g h => (cat_assoc a b c d f g h)^$) cat_idl cat_idr.
 
 (** Whiskering and horizontal composition of 2-cells. *)
 
@@ -175,19 +187,18 @@ Class Is1Cat_Strong (A : Type)`{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
   cat_assoc_strong : forall (a b c d : A)
     (f : a $-> b) (g : b $-> c) (h : c $-> d),
     (h $o g) $o f = h $o (g $o f) ;
+  cat_assoc_opp_strong : forall (a b c d : A)
+    (f : a $-> b) (g : b $-> c) (h : c $-> d),
+    h $o (g $o f) = (h $o g) $o f ;
   cat_idl_strong : forall (a b : A) (f : a $-> b), Id b $o f = f ;
   cat_idr_strong : forall (a b : A) (f : a $-> b), f $o Id a = f ;
 }.
 
 Arguments cat_assoc_strong {_ _ _ _ _ _ _ _ _} f g h.
+Arguments cat_assoc_opp_strong {_ _ _ _ _ _ _ _ _} f g h.
 Arguments cat_idl_strong {_ _ _ _ _ _ _} f.
 Arguments cat_idr_strong {_ _ _ _ _ _ _} f.
 
-Definition cat_assoc_opp_strong {A : Type} `{Is1Cat_Strong A}
-           {a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
-  : h $o (g $o f) = (h $o g) $o f
-  := (cat_assoc_strong f g h)^.
-
 Global Instance is1cat_is1cat_strong (A : Type) `{Is1Cat_Strong A}
   : Is1Cat A | 1000.
 Proof.
@@ -198,6 +209,7 @@ Proof.
   - apply is0functor_postcomp_strong.
   - apply is0functor_precomp_strong.
   - intros; apply GpdHom_path, cat_assoc_strong.
+  - intros; apply GpdHom_path, cat_assoc_opp_strong.
   - intros; apply GpdHom_path, cat_idl_strong.
   - intros; apply GpdHom_path, cat_idr_strong.
 Defined.
@@ -247,6 +259,7 @@ Global Instance is1cat_strong_hasmorext {A : Type} `{HasMorExt A}
 Proof.
   rapply Build_Is1Cat_Strong; hnf; intros; apply path_hom.
   + apply cat_assoc.
+  + apply cat_assoc_opp.
   + apply cat_idl.
   + apply cat_idr.
 Defined.

theories/WildCat/Displayed.v

@@ -106,6 +106,11 @@ Class IsD1Cat {A : Type} `{Is1Cat A}
                (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
                DHom (cat_assoc f g h) ((h' $o' g') $o' f')
                (h' $o' (g' $o' f'));
+  dcat_assoc_opp : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
+               {a' : D a} {b' : D b} {c' : D c} {d' : D d}
+               (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
+               DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f'))
+               ((h' $o' g') $o' f');
   dcat_idl : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
              (f' : DHom f a' b'), DHom (cat_idl f) (DId b' $o' f') f';
   dcat_idr : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
@@ -117,13 +122,6 @@ Global Existing Instance isd0gpd_hom.
 Global Existing Instance isd0functor_postcomp.
 Global Existing Instance isd0functor_precomp.
 
-Definition dcat_assoc_opp {A : Type} {D : A -> Type} `{IsD1Cat A D}
-  {a b c d : A}  {f : a $-> b} {g : b $-> c} {h : c $-> d}
-  {a' : D a} {b' : D b} {c' : D c} {d' : D d}
-  (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d')
-  : DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f')) ((h' $o' g') $o' f')
-  := (dcat_assoc f' g' h')^$'.
-
 Definition dcat_postwhisker {A : Type} {D : A -> Type} `{IsD1Cat A D}
   {a b c : A} {f g : a $-> b} {h : b $-> c} {p : f $== g}
   {a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'}
@@ -234,6 +232,8 @@ Proof.
     exact (p $@R f; p' $@R' f').
   - intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].
     exact (cat_assoc f g h; dcat_assoc f' g' h').
+  - intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].
+    exact (cat_assoc_opp f g h; dcat_assoc_opp f' g' h').
   - intros [a a'] [b b'] [f f'].
     exact (cat_idl f; dcat_idl f').
   - intros [a a'] [b b'] [f f'].
@@ -275,6 +275,11 @@ Class IsD1Cat_Strong {A : Type} `{Is1Cat_Strong A}
                       (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
                       (transport (fun k => DHom k a' d') (cat_assoc_strong f g h)
                       ((h' $o' g') $o' f')) = h' $o' (g' $o' f');
+  dcat_assoc_opp_strong : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
+                      {a' : D a} {b' : D b} {c' : D c} {d' : D d}
+                      (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
+                      (transport (fun k => DHom k a' d') (cat_assoc_opp_strong f g h)
+                      (h' $o' (g' $o' f'))) = (h' $o' g') $o' f';
   dcat_idl_strong : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
                     (f' : DHom f a' b'),
                     (transport (fun k => DHom k a' b') (cat_idl_strong f)
@@ -290,6 +295,7 @@ Global Existing Instance isd0gpd_hom_strong.
 Global Existing Instance isd0functor_postcomp_strong.
 Global Existing Instance isd0functor_precomp_strong.
 
+(* 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:
 Definition dcat_assoc_opp_strong {A : Type} {D : A -> Type} `{IsD1Cat_Strong A D}
   {a b c d : A}  {f : a $-> b} {g : b $-> c} {h : c $-> d}
   {a' : D a} {b' : D b} {c' : D c} {d' : D d}
@@ -300,13 +306,16 @@ Proof.
   apply (moveR_transport_V (fun k => DHom k a' d') (cat_assoc_strong f g h) _ _).
   exact ((dcat_assoc_strong f' g' h')^).
 Defined.
+*)
 
 Global Instance isd1cat_isd1catstrong {A : Type} (D : A -> Type)
   `{IsD1Cat_Strong A D} : IsD1Cat D.
 Proof.
   srapply Build_IsD1Cat.
   - intros a b c d f g h a' b' c' d' f' g' h'.
     exact (DHom_path (cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
+  - intros a b c d f g h a' b' c' d' f' g' h'.
+    exact (DHom_path (cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
   - intros a b f a' b' f'.
     exact (DHom_path (cat_idl_strong f) (dcat_idl_strong f')).
   - intros a b f a' b' f'.
@@ -321,6 +330,9 @@ Proof.
   - intros aa' bb' cc' dd' [f f'] [g g'] [h h'].
     exact (path_sigma' _
             (cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
+  - intros aa' bb' cc' dd' [f f'] [g g'] [h h'].
+    exact (path_sigma' _
+            (cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
   - intros aa' bb' [f f'].
     exact (path_sigma' _ (cat_idl_strong f) (dcat_idl_strong f')).
   - intros aa' bb' [f f'].
@@ -506,6 +518,9 @@ Proof.
   - intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.
     intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].
     exact (dcat_assoc f1' f2' f3', dcat_assoc g1' g2' g3').
+  - intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.
+    intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].
+    exact (dcat_assoc_opp f1' f2' f3', dcat_assoc_opp g1' g2' g3').
   - intros ab1 ab2 fg ab1' ab2' [f' g'].
     exact (dcat_idl f', dcat_idl g').
   - intros ab1 ab2 fg ab1' ab2' [f' g'].

theories/WildCat/DisplayedEquiv.v

@@ -160,7 +160,7 @@ Defined.
 Global Instance dcatie_id {A} {D : A -> Type} `{DHasEquivs A D}
   {a : A} (a' : D a)
   : DCatIsEquiv (DId a')
-  := dcatie_adjointify (DId a') (DId a') (dcat_idl (DId a')) (dcat_idl (DId a')).
+  := dcatie_adjointify (DId a') (DId a') (dcat_idl (DId a')) (dcat_idr (DId a')).
 
 Definition did_cate {A} {D : A -> Type} `{DHasEquivs A D}
   {a : A} (a' : D a)
@@ -205,10 +205,10 @@ Proof.
     refine (_ $@L' (dcate_isretr _ $@R' _) $@' _).
     refine (_ $@L' dcat_idl _ $@' _).
     apply dcate_isretr.
-  - refine (dcat_assoc _ _ _ $@' _).
-    refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
-    refine (_ $@L' (dcate_issect _ $@R' _) $@' _).
-    refine (_ $@L' dcat_idl _ $@' _).
+  - refine (dcat_assoc_opp _ _ _ $@' _).
+    refine (dcat_assoc _ _ _ $@R' _ $@' _).
+    refine (((_ $@L' dcate_issect _) $@R' _) $@' _).
+    refine ((dcat_idr _ $@R' _) $@' _).
     apply dcate_issect.
 Defined.
 

theories/WildCat/Equiv.v

@@ -137,7 +137,7 @@ Defined.
 (** The identity morphism is an equivalence *)
 Global Instance catie_id {A} `{HasEquivs A} (a : A)
   : CatIsEquiv (Id a)
-  := catie_adjointify (Id a) (Id a) (cat_idl (Id a)) (cat_idl (Id a)).
+  := catie_adjointify (Id a) (Id a) (cat_idl (Id a)) (cat_idr (Id a)).
 
 Definition id_cate {A} `{HasEquivs A} (a : A)
   : a $<~> a
@@ -177,10 +177,10 @@ Proof.
     refine ((_ $@L (cate_isretr _ $@R _)) $@ _).
     refine ((_ $@L cat_idl _) $@ _).
     apply cate_isretr.
-  - refine (cat_assoc _ _ _ $@ _).
-    refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
-    refine ((_ $@L (cate_issect _ $@R _)) $@ _).
-    refine ((_ $@L cat_idl _) $@ _).
+  - refine (cat_assoc_opp _ _ _ $@ _).
+    refine ((cat_assoc _ _ _ $@R _) $@ _).
+    refine (((_ $@L cate_issect _) $@R _) $@ _).
+    refine ((cat_idr _ $@R _) $@ _).
     apply cate_issect.
 Defined.
 
@@ -226,6 +226,16 @@ Proof.
   - refine (_ $@L compose_cate_funinv g f).
 Defined.
 
+Definition compose_cate_assoc_opp {A} `{HasEquivs A}
+           {a b c d : A} (f : a $<~> b) (g : b $<~> c) (h : c $<~> d)
+  : cate_fun (h $oE (g $oE f)) $== cate_fun ((h $oE g) $oE f).
+Proof.
+  refine (compose_cate_fun h _ $@ _ $@ cat_assoc_opp f g h $@ _ $@
+                           compose_cate_funinv _ f).
+  - refine (_ $@L compose_cate_fun g f).
+  - refine (compose_cate_funinv h g $@R _).
+Defined.
+
 Definition compose_cate_idl {A} `{HasEquivs A}
            {a b : A} (f : a $<~> b)
   : cate_fun (id_cate b $oE f) $== cate_fun f.
@@ -559,6 +569,7 @@ Global Instance is1cat_core {A : Type} `{HasEquivs A}
 Proof.
   rapply Build_Is1Cat.
   - intros; apply compose_cate_assoc.
+  - intros; apply compose_cate_assoc_opp.
   - intros; apply compose_cate_idl.
   - intros; apply compose_cate_idr.
 Defined.

theories/WildCat/Forall.v

@@ -52,6 +52,7 @@ Proof.
     intros f g p a.
     exact (p a $@R h a).
   + intros w x y z f g h a; apply cat_assoc.
+  + intros w x y z f g h a; apply cat_assoc_opp.
   + intros x y f a; apply cat_idl.
   + intros x y f a; apply cat_idr.
 Defined.

theories/WildCat/FunctorCat.v

@@ -72,6 +72,8 @@ Proof.
     exact (f a $@R alpha a).
   - intros [F ?] [G ?] [K ?] [L ?] [alpha ?] [gamma ?] [phi ?] a; cbn.
     srapply cat_assoc.
+  - intros [F ?] [G ?] [K ?] [L ?] [alpha ?] [gamma ?] [phi ?] a; cbn.
+    srapply cat_assoc_opp.
   - intros [F ?] [G ?] [alpha ?] a; cbn.
     srapply cat_idl.
   - intros [F ?] [G ?] [alpha ?] a; cbn.

theories/WildCat/Induced.v

@@ -57,6 +57,7 @@ Section Induced_category.
     + rapply is0functor_postcomp.
     + rapply is0functor_precomp.
     + rapply cat_assoc.
+    + rapply cat_assoc_opp.
     + rapply cat_idl.
     + rapply cat_idr.
   Defined.