redefine Bifunctor

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.
@@ -127,10 +127,14 @@ 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)).
+  intros A B f C D g.
+  intros x.
+  strip_truncations; cbn.
+  pose proof (bifunctor_coh (Ext : AbGroup^op -> AbGroup -> pType) f g (tr x)) as X.
+  cbn in X.
+  exact X.
 Defined.
 
 (** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)
@@ -139,10 +143,10 @@ Definition abses_pushout_ext `{Univalence}
   : GroupHomomorphism (ab_hom A G) (ab_ext B G).
 Proof.
   snrapply Build_GroupHomomorphism.
-  1: exact (fun f => fmap01 (A:=AbGroup^op) Ext' _ f (tr E)).
+  1: exact (fun f => fmap (Ext' (_ : AbGroup^op)) f (tr E)).
   intros f g; cbn.
   nrapply (ap tr).
-  exact (baer_sum_distributive_pushouts f g).
+  exact (baer_sum_distributive_pushouts (E:=E) f g).
 Defined.
 
 (** ** Extensions ending in a projective are trivial *)

theories/Algebra/AbSES/SixTerm.v

@@ -98,7 +98,8 @@ Proof.
       destruct g as [g k].
     exists g.
     apply path_sigma_hprop; cbn.
-    exact k^.
+    elim k^. 
+    by apply equiv_path_grouphomomorphism.
 Defined.
 
 (** *** Exactness of [ab_hom A G -> Ext1 B G -> Ext1 E G]. *)

theories/Homotopy/Join/Core.v

@@ -562,16 +562,14 @@ Section FunctorJoin.
 
   Global Instance is0bifunctor_join : Is0Bifunctor Join.
   Proof.
-    rapply Build_Is0Bifunctor'.
     apply Build_Is0Functor.
     intros A B [f g].
     exact (functor_join f g).
   Defined.
 
   Global Instance is1bifunctor_join : Is1Bifunctor Join.
   Proof.
-    snrapply Build_Is1Bifunctor'.
-    nrapply Build_Is1Functor.
+    snrapply Build_Is1Functor.
     - intros A B f g [p q].
       exact (functor2_join p q).
     - intros A; exact functor_join_idmap.

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 *)

theories/Homotopy/Smash.v

@@ -353,15 +353,13 @@ Defined.
 
 Global Instance is0bifunctor_smash : Is0Bifunctor Smash.
 Proof.
-  rapply Build_Is0Bifunctor'.
   nrapply Build_Is0Functor.
   intros [X Y] [A B] [f g].
   exact (functor_smash f g).
 Defined.
 
 Global Instance is1bifunctor_smash : Is1Bifunctor Smash.
 Proof.
-  snrapply Build_Is1Bifunctor'.
   snrapply Build_Is1Functor.
   - intros [X Y] [A B] [f g] [h i] [p q].
     exact (functor_smash_homotopic p q).