make opposite Is1Natural definitionally involutive

test/WildCat/Opposite.v

@@ -1,42 +1,72 @@
 From HoTT Require Import Basics WildCat.Core WildCat.Opposite WildCat.Equiv
-  WildCat.NatTrans WildCat.Bifunctor.
+  WildCat.NatTrans WildCat.Bifunctor WildCat.Monoidal.
 
 (** Opposites are definitionally involutive. *)
-Definition test1 A : A = (A^op)^op :> Type := 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.
+Succeed Definition t A : A = (A^op)^op :> Type := 1.
+Succeed Definition t A `{x : IsGraph A} : x = @isgraph_op A^op (@isgraph_op A x) := 1.
+Succeed Definition t A `{x : Is01Cat A} : x = @is01cat_op A^op _ (@is01cat_op A _ x) := 1.
+Succeed Definition t A `{x : Is2Graph A} : x = @is2graph_op A^op _ (@is2graph_op A _ x) := 1.
+Succeed Definition t A `{x : Is1Cat A} : x = @is1cat_op A^op _ _ _ (@is1cat_op A _ _ _ x) := 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.
+Succeed Definition t A `{HasEquivs A} : (core A)^op = core A^op :> Type := 1.
+Succeed Definition t A `{HasEquivs A} : isgraph_op (A:=core A) = isgraph_core (A:=A^op) := 1.
+Succeed Definition t A `{HasEquivs A} : is01cat_op (A:=core A) = is01cat_core (A:=A^op) := 1.
+Succeed Definition t A `{HasEquivs A} : is2graph_op (A:=core A) = is2graph_core (A:=A^op) := 1.
 
 (** The Opaque line reduces the time from 0.3s to 0.07s. *)
 Opaque compose_catie_isretr.
-Definition core5 A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op) := 1.
+Succeed Definition t A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op) := 1.
 
 (** Opposite functors are definitionally involutive. *)
-Definition test6 A B (F : A -> B) `{x : Is0Functor A B F}
+Succeed Definition t A B (F : A -> B) `{x : Is0Functor A B F}
   : @is0functor_op _ _ F _ _ (@is0functor_op _ _ F _ _ x) = x
   := 1.
-Definition test7 A B (F : A -> B) `{x : Is1Functor A B F}
+Succeed Definition t A B (F : A -> B) `{x : Is1Functor A B F}
   : @is1functor_op _ _ F _ _ _ _ _ _ _ _ _ (@is1functor_op _ _ F _ _ _ _ _ _ _ _ _ x) = x
   := 1.
 
 (** Opposite bifunctors are definitionally involutive. *)
-Definition test8 A B C (F : A -> B -> C) `{x : Is0Bifunctor A B C F}
+Succeed Definition t A B C (F : A -> B -> C) `{x : Is0Bifunctor A B C F}
   : @is0bifunctor_op _ _ _ F _ _ _ (@is0bifunctor_op _ _ _ F _ _ _ x) = x
   := 1.
-Definition test9 A B C (F : A -> B -> C) `{x : Is1Bifunctor A B C F}
+Succeed Definition t A B C (F : A -> B -> C) `{x : Is1Bifunctor A B C F}
   : @is1bifunctor_op _ _ _ F _ _ _ _ _ _ _ _ _ _ _ _ _
     (@is1bifunctor_op _ _ _ F _ _ _ _ _ _ _ _ _ _ _ _ _ x) = x
   := 1.
 
-(** Opposite natural transformations are *not* definitionally involutive. *)
-Fail Definition test10 A `{Is01Cat A} B `{Is1Cat B} (F G : A -> B)
+(** Opposite natural transformations are definitionally involutive. *)
+Succeed Definition t A `{Is01Cat A} B `{Is1Cat B} (F G : A -> B)
   `{!Is0Functor F, !Is0Functor G} (n : NatTrans F G)
   : nattrans_op (nattrans_op n) = n
   := 1.
+
+(** Opposite natural equivalences are definitionally involutive. *)
+Succeed Definition t A `{Is01Cat A} B `{HasEquivs B} (F G : A -> B)
+  `{!Is0Functor F, !Is0Functor G} (n : NatEquiv F G)
+  : natequiv_op (natequiv_op n) = n
+  := 1.
+
+(** Opposite left unitors are *not* definitionally involutive. *)
+Fail Definition t A `{HasEquivs A} (unit : A)
+  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : LeftUnitor F unit)
+  : @left_unitor_op _ _ _ _ _ _ F unit _ _ (@left_unitor_op _ _ _ _ _ _ F unit _ _ a) = a
+  := 1.
+
+(** Opposite right unitors are *not* definitionally involutive. *)
+Fail Definition t A `{HasEquivs A} (unit : A)
+  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : RightUnitor F unit)
+  : @right_unitor_op _ _ _ _ _ _ F unit _ _ (@right_unitor_op _ _ _ _ _ _ F unit _ _ a) = a
+  := 1.
+
+(** Opposite associators are *not* definitionally involutive. *)
+Fail Definition t A `{HasEquivs A}
+  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : Associator F)
+  : @associator_op _ _ _ _ _ _ F _ _ (@associator_op _ _ _ _ _ _ F _ _ a) = a
+  := 1.
+
+(** Opposite braidings are definitionally involutive. *)
+Succeed Definition t A `{HasEquivs A}
+  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : Braiding F)
+  : @braiding_op _ _ _ _ _ _ _ _ (@braiding_op _ _ _ _ _ _ _ _ a) = a
+  := 1.

theories/Homotopy/ClassifyingSpace.v

@@ -432,7 +432,7 @@ Definition natequiv_g_loops_bg `{Univalence}
 Proof.
   snrapply Build_NatEquiv.
   1: intros G; rapply pequiv_g_loops_bg.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros X Y f.
   symmetry.
   apply pbloop_natural.
@@ -534,7 +534,7 @@ Defined.
 Global Instance is1natural_grp_homo_pmap_bg_r {U : Univalence} (G : Group)
   : Is1Natural (opyon G) (opyon (B G) o B) (equiv_grp_homo_pmap_bg G).
 Proof.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros K H f h.
   apply path_hom.
   rapply (fmap_comp B h f).

theories/Homotopy/Join/Core.v

@@ -627,7 +627,7 @@ Section JoinSym.
       1, 2: apply joinrecdata_sym.
       1, 2: apply joinrecdata_sym_inv.
     (* Naturality: *)
-    - snrapply Build_Is1Natural'.
+    - snrapply Build_Is1Natural.
       intros P Q g f; simpl.
       bundle_joinrecpath.
       intros b a; simpl.
@@ -837,7 +837,7 @@ Section JoinEmpty.
   Proof.
     snrapply Build_NatEquiv.
     - apply equiv_join_empty_right.
-    - snrapply Build_Is1Natural'.
+    - snrapply Build_Is1Natural.
       intros A B f.
       cbn -[equiv_join_empty_right].
       snrapply Join_ind_FlFr.
@@ -851,7 +851,7 @@ Section JoinEmpty.
   Proof.
     snrapply Build_NatEquiv.
     - apply equiv_join_empty_left.
-    - snrapply Build_Is1Natural'.
+    - snrapply Build_Is1Natural.
       intros A B f x.
       cbn -[equiv_join_empty_right].
       rhs_V rapply (isnat_natequiv join_right_unitor).

theories/Homotopy/Join/JoinAssoc.v

@@ -60,7 +60,7 @@ Proof.
     1, 2: apply trijoinrecdata_twist.
     1, 2: apply trijoinrecdata_twist_inv.
   (* Naturality: *)
-  - snrapply Build_Is1Natural'.
+  - snrapply Build_Is1Natural.
     intros P Q g f; simpl.
     bundle_trijoinrecpath.
     all: intros; cbn.
@@ -265,7 +265,7 @@ Global Instance join_associator : Associator Join.
 Proof.
   snrapply Build_Associator; simpl.
   - exact join_assoc.
-  - snrapply Build_Is1Natural'.
+  - snrapply Build_Is1Natural.
     intros [[A B] C] [[A' B'] C'] [[f g] h]; cbn.
     apply join_assoc_nat.
 Defined.

theories/Pointed/Core.v

@@ -661,31 +661,31 @@ Proof.
       exact (concat_Ap q _)^.
     + by pelim p f g q h k.
   - intros A B C D f g.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros r1 r2 s1.
     srapply Build_pHomotopy.
     1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
     by pelim f g s1 r1 r2.
   - intros A B C D f g.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros r1 r2 s1.
     srapply Build_pHomotopy.
     1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
     by pelim f s1 r1 r2 g.
   - intros A B C D f g.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros r1 r2 s1.
     srapply Build_pHomotopy.
     1: cbn; exact (fun _ => concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).
     by pelim s1 r1 r2 f g.
   - intros A B.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros r1 r2 s1.
     srapply Build_pHomotopy.
     1: exact (fun _ => concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
     by pelim s1 r1 r2.
   - intros A B.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros r1 r2 s1.
     srapply Build_pHomotopy.
     1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
@@ -1069,7 +1069,7 @@ Lemma natequiv_pointify_r `{Funext} (A : Type)
 Proof.
   snrapply Build_NatEquiv.
   1: rapply equiv_pointify_map.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   cbv; reflexivity.
 Defined.
 

theories/Pointed/Loops.v

@@ -428,7 +428,7 @@ Defined.
 (** [loops_inv] is a natural transformation. *)
 Global Instance is1natural_loops_inv : Is1Natural loops loops loops_inv.
 Proof.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros A B f.
   srapply Build_pHomotopy.
   + intros p. refine (inv_Vp _ _ @ whiskerR _ (point_eq f) @ concat_pp_p _ _ _).

theories/Pointed/pSusp.v

@@ -292,7 +292,7 @@ Global Instance is1natural_loop_susp_adjoint_r `{Funext} (A : pType)
   : Is1Natural (opyon (psusp A)) (opyon A o loops)
       (loop_susp_adjoint A).
 Proof.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros B B' g f.
   refine ( _ @ cat_assoc_strong _ _ _).
   refine (ap (fun x => x o* loop_susp_unit A) _).

theories/WildCat/Adjoint.v

@@ -112,7 +112,7 @@ Section AdjunctionData.
   Proof.
     snrapply Build_NatEquiv.
     1: intros [x y]; exact (equiv_adjunction adj x y).
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros [a b] [a' b'] [f g] K.
     refine (_ @ ap (fun x : a $-> G b' => x $o f)
       (is1natural_equiv_adjunction_r adj a b b' g K)).
@@ -125,7 +125,7 @@ Section AdjunctionData.
     snrapply Build_NatTrans.
     { hnf. intros x.
       exact (equiv_adjunction adj x (F x) (Id _)). }
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros x x' f.
     apply GpdHom_path.
     refine (_^ @ _ @ _).
@@ -143,7 +143,7 @@ Section AdjunctionData.
     snrapply Build_NatTrans.
     { hnf. intros y.
       exact ((equiv_adjunction adj (G y) y)^-1 (Id _)). }
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros y y' f.
     apply GpdHom_path.
     refine (_^ @ _ @ _).
@@ -335,7 +335,7 @@ Proof.
   - snrapply Build_NatTrans.
     + intros K.
       exact (nattrans_prewhisker (adjunction_unit adj) K).
-    + snrapply Build_Is1Natural'.
+    + snrapply Build_Is1Natural.
       intros K K' θ j.
       apply GpdHom_path.
       refine (_ @ is1natural_natequiv (natequiv_inverse
@@ -348,7 +348,7 @@ Proof.
   - snrapply Build_NatTrans.
     + intros K.
       exact (nattrans_prewhisker (adjunction_counit adj) K).
-    + snrapply Build_Is1Natural'.
+    + snrapply Build_Is1Natural.
       intros K K' θ j.
       apply GpdHom_path.
       refine (_ @ is1natural_natequiv

theories/WildCat/Bifunctor.v

@@ -388,7 +388,7 @@ Global Instance is1natural_uncurry {A B C : Type}
   (nat_r : forall a, Is1Natural (F a) (G a) (fun y : B => alpha (a, y)))
   : Is1Natural (uncurry F) (uncurry G) alpha.
 Proof.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros [a b] [a' b'] [f f']; cbn in *.
   change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
   nrapply vconcatL.
@@ -406,12 +406,14 @@ Definition nattrans_flip {A B C : Type}
   : NatTrans (uncurry F) (uncurry G)
     -> NatTrans (uncurry (flip F)) (uncurry (flip G)).
 Proof.
-  intros [alpha nat].
+  intros alpha.
   snrapply Build_NatTrans.
   - exact (alpha o equiv_prod_symm _ _).
   - snrapply Build_Is1Natural'.
-    intros [b a] [b' a'] [g f].
-    exact (nat (a, b) (a', b') (f, g)).
+    + intros [b a] [b' a'] [g f].
+      exact (isnat (a:=(a, b)) (a':=(a', b')) alpha (f, g)).
+    + intros [b a] [b' a'] [g f].
+      exact (isnat_tr (a:=(a, b)) (a':=(a', b')) alpha (f, g)).
 Defined.
 
 (** ** Opposite Bifunctors *)

theories/WildCat/Monoidal.v

@@ -682,7 +682,7 @@ Section TwistConstruction.
   Proof.
     snrapply Build_Associator.
     - exact associator_twist'.
-    - snrapply Build_Is1Natural'.
+    - snrapply Build_Is1Natural.
       simpl; intros [[a b] c] [[a' b'] c'] [[f g] h]; simpl in f, g, h.
       (** To prove naturality it will be easier to reason about squares. *)
       change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
@@ -718,7 +718,7 @@ Section TwistConstruction.
     snrapply Build_NatEquiv'.
     - snrapply Build_NatTrans.
       + exact (fun a => right_unitor a $o braid cat_tensor_unit a).
-      + snrapply Build_Is1Natural'.
+      + snrapply Build_Is1Natural.
         intros a b f.
         change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
         nrapply vconcat.