Merge pull request #1952 from Alizter/bifunctor-redefin

redefine Bifunctor
HoTT · May 7, 2024 · 7c5ce31 · 7c5ce31
2 parents 72ced09 + f235f53
commit 7c5ce31
Show file tree

Hide file tree

Showing 11 changed files with 295 additions and 314 deletions.
diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v
@@ -92,13 +92,13 @@ Defined.
 Global Instance is0bifunctor_ab_hom `{Funext}
   : Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
 Proof.
-  rapply Build_Is0Bifunctor.
+  rapply Build_Is0Bifunctor''.
 Defined.
 
 Global Instance is1bifunctor_ab_hom `{Funext}
   : Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
 Proof.
-  nrapply Build_Is1Bifunctor.
+  nrapply Build_Is1Bifunctor''.
   1,2: exact _.
   intros A A' f B B' g phi; cbn.
   by apply equiv_path_grouphomomorphism.

diff --git a/theories/Algebra/AbSES/BaerSum.v b/theories/Algebra/AbSES/BaerSum.v
@@ -54,13 +54,13 @@ Defined.
 Global Instance is0bifunctor_abses' `{Univalence}
   : Is0Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
 Proof.
-  rapply Build_Is0Bifunctor.
+  rapply Build_Is0Bifunctor''.
 Defined.
 
 Global Instance is1bifunctor_abses' `{Univalence}
   : Is1Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
 Proof.
-  snrapply Build_Is1Bifunctor.
+  snrapply Build_Is1Bifunctor''.
   1,2: exact _.
   intros ? ? g ? ? f E; cbn.
   exact (abses_pushout_pullback_reorder E f g).
@@ -232,13 +232,13 @@ Defined.
 Global Instance is0bifunctor_abses `{Univalence}
   : Is0Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
 Proof.
-  rapply Build_Is0Bifunctor.
+  rapply Build_Is0Bifunctor''.
 Defined.
 
 Global Instance is1bifunctor_abses `{Univalence}
   : Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
 Proof.
-  snrapply Build_Is1Bifunctor.
+  snrapply Build_Is1Bifunctor''.
   1,2: exact _.
   intros ? ? f ? ? g.
   rapply hspace_phomotopy_from_homotopy.

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
@@ -63,9 +63,9 @@ Defined.
 
 (** ** The bifunctor [ab_ext] *)
 
-Definition ab_ext `{Univalence} (B A : AbGroup@{u}) : AbGroup.
+Definition ab_ext@{u v|u < v} `{Univalence} (B : AbGroup@{u}^op) (A : AbGroup@{u}) : AbGroup@{v}.
 Proof.
-  snrapply (Build_AbGroup (grp_ext B A)).
+  snrapply (Build_AbGroup (grp_ext@{u v} B A)).
   intros E F.
   strip_truncations; cbn.
   apply ap.
@@ -121,16 +121,16 @@ Defined.
 Global Instance is0bifunctor_abext `{Univalence}
   : Is0Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
-  rapply Build_Is0Bifunctor.
+  rapply Build_Is0Bifunctor''.
 Defined.
 
 Global Instance is1bifunctor_abext `{Univalence}
   : Is1Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
-  snrapply Build_Is1Bifunctor.
+  snrapply Build_Is1Bifunctor''.
   1,2: exact _.
   intros A B.
-  exact (bifunctor_isbifunctor (Ext : AbGroup^op -> AbGroup -> pType)).
+  exact (bifunctor_coh (Ext : AbGroup^op -> AbGroup -> pType)).
 Defined.
 
 (** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)

diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
@@ -562,7 +562,8 @@ Section FunctorJoin.
 
   Global Instance is0bifunctor_join : Is0Bifunctor Join.
   Proof.
-    rapply Build_Is0Bifunctor'.
+    snrapply Build_Is0Bifunctor'.
+    1,2: exact _.
     apply Build_Is0Functor.
     intros A B [f g].
     exact (functor_join f g).

diff --git a/theories/Homotopy/Join/JoinAssoc.v b/theories/Homotopy/Join/JoinAssoc.v
@@ -266,20 +266,7 @@ Proof.
   - intros A B C.
     apply join_assoc.
   - intros [[A B] C] [[A' B'] C'] [[f g] h]; cbn.
-    (* This is awkward because Monoidal.v works with a tensor that is separately a functor in each variable. *)
-    intro x.
-    rhs_V nrapply functor_join_compose.
-    rhs_V nrapply functor2_join.
-    2: reflexivity.
-    2: nrapply functor_join_compose.
-    cbn.
-    rhs_V nrapply join_assoc_nat; cbn.
-    apply ap.
-    lhs_V nrapply functor_join_compose.
-    lhs_V nrapply functor_join_compose.
-    apply functor2_join.
-    1: reflexivity.
-    symmetry; nrapply functor_join_compose.
+    apply join_assoc_nat.
 Defined.
 
 (** ** The Triangle Law *)

diff --git a/theories/Homotopy/Smash.v b/theories/Homotopy/Smash.v
@@ -353,7 +353,8 @@ Defined.
 
 Global Instance is0bifunctor_smash : Is0Bifunctor Smash.
 Proof.
-  rapply Build_Is0Bifunctor'.
+  snrapply Build_Is0Bifunctor'.
+  1,2: exact _.
   nrapply Build_Is0Functor.
   intros [X Y] [A B] [f g].
   exact (functor_smash f g).