make opposite Is1Natural definitionally involutive

test/WildCat/Opposite.v

@@ -35,8 +35,14 @@ Definition test9 A B C (F : A -> B -> C) `{x : Is1Bifunctor A B C 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. *)
+Definition test10 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. *)
+Definition test11 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.

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.
@@ -409,7 +409,7 @@ Proof.
   intros [alpha nat].
   snrapply Build_NatTrans.
   - exact (alpha o equiv_prod_symm _ _).
-  - snrapply Build_Is1Natural'.
+  - snrapply Build_Is1Natural.
     intros [b a] [b' a'] [g f].
     exact (nat (a, b) (a', b') (f, g)).
 Defined.

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.

theories/WildCat/NatTrans.v

@@ -57,30 +57,36 @@ Class Is1Natural {A B : Type} `{IsGraph A, Is1Cat B}
   (F : A -> B) `{!Is0Functor F} (G : A -> B) `{!Is0Functor G}
   (alpha : F $=> G) := Build_Is1Natural' {
   isnat {a a'} (f : a $-> a') : alpha a' $o fmap F f $== fmap G f $o alpha a;
+  (** We also include the transposed naturality square in the definition so that opposite natural transformations are definitionally involutive. In most cases, this will be constructed to be the inverse of the [isnat] field. *)
+  isnat_tr {a a'} (f : a $-> a') : fmap G f $o alpha a $== alpha a' $o fmap F f;
 }.
 
 Arguments Is1Natural {A B} {isgraph_A}
   {isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B}
   F {is0functor_F} G {is0functor_G} alpha : rename.
 Arguments isnat {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.
+Arguments isnat_tr {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.
 
 (** We coerce naturality proofs to their naturality square as the [isnat] projection can be unwieldy in certain situations where the transformation is difficult to write down. This allows for the naturality proof to be used directly. *)
 Coercion isnat : Is1Natural >-> Funclass.
 
-(** TODO: make this part of the data for definitional involution of op *)
-(** The transposed natural square. *)
-Definition isnat_tr {A B : Type} `{IsGraph A} `{Is1Cat B}
-  {F : A -> B} `{!Is0Functor F} {G : A -> B} `{!Is0Functor G}
-  (alpha : F $=> G) `{!Is1Natural F G alpha} {a a' : A} (f : a $-> a')
-  : fmap G f $o alpha a $== alpha a' $o fmap F f
-  := (isnat alpha f)^$.
+Definition Build_Is1Natural {A B : Type} `{IsGraph A} `{Is1Cat B}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G} (alpha : F $=> G)
+  (isnat : forall a a' (f : a $-> a'), alpha a' $o fmap F f $== fmap G f $o alpha a)
+  : Is1Natural F G alpha.
+Proof.
+  snrapply Build_Is1Natural'.
+  - exact isnat.
+  - intros a a' f.
+    exact (isnat a a' f)^$.
+Defined.
 
 (** The identity transformation is 1-natural. *)
 Global Instance is1natural_id {A B : Type} `{IsGraph A} `{Is1Cat B}
   (F : A -> B) `{!Is0Functor F}
   : Is1Natural F F (trans_id F).
 Proof.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros a b f; cbn.
   refine (cat_idl _ $@ (cat_idr _)^$).
 Defined.
@@ -92,7 +98,7 @@ Global Instance is1natural_comp {A B : Type} `{IsGraph A} `{Is1Cat B}
   (alpha : F $=> G) `{!Is1Natural F G alpha}
   : Is1Natural F K (trans_comp gamma alpha).
 Proof.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros a b f; unfold trans_comp; cbn.
   refine (cat_assoc _ _ _ $@ (_ $@L isnat alpha f) $@ _).
   refine (cat_assoc_opp _ _ _ $@ (isnat gamma f $@R _) $@ _).
@@ -105,7 +111,7 @@ Global Instance is1natural_prewhisker {A B C : Type} {F G : B -> C} (K : A -> B)
   (gamma : F $=> G) `{L : !Is1Natural F G gamma}
   : Is1Natural (F o K) (G o K) (trans_prewhisker gamma K).
 Proof.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros x y f; unfold trans_prewhisker; cbn.
   exact (isnat gamma _).
 Defined.
@@ -117,7 +123,7 @@ Global Instance is1natural_postwhisker {A B C : Type} {F G : A -> B} (K : B -> C
   (gamma : F $=> G) `{L : !Is1Natural F G gamma}
   : Is1Natural (K o F) (K o G) (trans_postwhisker K gamma).
 Proof.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros x y f; unfold trans_postwhisker; cbn.
   refine (_^$ $@ _ $@ _).
   1,3: rapply fmap_comp.
@@ -132,7 +138,7 @@ Definition is1natural_homotopic {A B : Type} `{Is01Cat A} `{Is1Cat B}
   (p : forall a, alpha a $== gamma a)
   : Is1Natural F G alpha.
 Proof.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros a b f.
   exact ((p b $@R _) $@ isnat gamma f $@ (_ $@L (p a)^$)).
 Defined.
@@ -145,8 +151,10 @@ Global Instance is1natural_op A B `{Is01Cat A} `{Is1Cat B}
 Proof.
   unfold op.
   snrapply Build_Is1Natural'.
-  intros a b f.
-  srapply isnat_tr.
+  - intros a b f.
+    by snrapply isnat_tr.
+  - intros a b f.
+    by snrapply isnat.
 Defined.
 
 (** ** Natural transformations *)
@@ -250,7 +258,7 @@ Proof.
   snrapply Build_NatEquiv.
   - intro a.
     refine (Build_CatEquiv (alpha a)).
-  - snrapply Build_Is1Natural'.
+  - snrapply Build_Is1Natural.
     intros a a' f.
     refine (cate_buildequiv_fun _ $@R _ $@ _ $@ (_ $@L cate_buildequiv_fun _)^$).
     apply (isnat alpha).
@@ -301,7 +309,7 @@ Proof.
   intros [alpha I].
   snrapply Build_NatEquiv.
   1: intro a; symmetry; apply alpha.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros X Y f.
   apply vinverse, I.
 Defined.
@@ -315,7 +323,7 @@ Definition natequiv_functor_assoc_ff_f {A B C D : Type}
 Proof.
   snrapply Build_NatEquiv.
   1: intro; reflexivity.
-  snrapply Build_Is1Natural'.
+  snrapply Build_Is1Natural.
   intros X Y f.
   refine (cat_prewhisker (id_cate_fun _) _ $@ cat_idl _ $@ _^$).
   refine (cat_postwhisker _ (id_cate_fun _) $@ cat_idr _).

theories/WildCat/Paths.v

@@ -80,25 +80,25 @@ Proof.
   - intros a b c q r s t h g.
     exact (concat_whisker q r s t h g)^.
   - intros a b c d q r.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros s t h.
     apply concat_p_pp_nat_r.
   - intros a b c d q r.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros s t h.
     apply concat_p_pp_nat_m.
   - intros a b c d q r.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros s t h.
     apply concat_p_pp_nat_l.
   - intros a b.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros p q h; cbn.
     apply moveL_Mp.
     lhs nrapply concat_p_pp.
     exact (whiskerR_p1 h).
   - intros a b.
-    snrapply Build_Is1Natural'.
+    snrapply Build_Is1Natural.
     intros p q h.
     apply moveL_Mp.
     lhs rapply concat_p_pp.