Merge pull request #1886 from gio256/bifunctors

Update bifunctors

Author: jdchristensen

contrib/SetoidRewrite.v

@@ -71,7 +71,7 @@ Defined.
 
 Open Scope signatureT_scope.
 
-#[export] Instance symmetry_flip {A B: Type} {f : A -> B}
+#[export] Instance symmetry_flip {A B : Type} {f : A -> B}
   {R : Relation A} {R' : Relation B} `{Symmetric _ R}
   (H0 : CMorphisms.Proper (R ++> R') f)
   : CMorphisms.Proper (R --> R') f.
@@ -80,15 +80,15 @@ Proof.
   apply H0. unfold CRelationClasses.flip. symmetry. exact Rab.
 Defined.
 
-#[export] Instance symmetric_flip_snd {A B C: Type} {R : Relation A}
+#[export] Instance symmetric_flip_snd {A B C : Type} {R : Relation A}
   {R' : Relation B} {R'' : Relation C} `{Symmetric _ R'}
   (f : A -> B -> C) (H1 : CMorphisms.Proper (R ++> R' ++> R'') f)
   : CMorphisms.Proper (R ++> R' --> R'') f.
 Proof.
   intros a b Rab x y R'yx. apply H1; [ assumption | symmetry; assumption ].
 Defined.
 
-#[export] Instance IsProper_fmap {A B: Type} `{Is1Cat A}
+#[export] Instance IsProper_fmap {A B : Type} `{Is1Cat A}
   `{Is1Cat A} (F : A -> B) `{Is1Functor _ _ F} (a b : A)
   : CMorphisms.Proper (GpdHom ==> GpdHom) (@fmap _ _ _ _ F _ a b) := fun _ _ eq => fmap2 F eq.
 
@@ -99,7 +99,7 @@ Proof.
   intros f1 f2.
   apply (is0functor_postcomp a b c g ).
 Defined.
-                  
+
 #[export] Instance IsProper_catcomp {A : Type} `{Is1Cat A}
   {a b c : A}
   : CMorphisms.Proper (GpdHom ==> GpdHom ==> GpdHom)
@@ -111,45 +111,14 @@ Proof.
   exact eq_g.
 Defined.
 
-#[export] Instance gpd_hom_to_hom_proper {A B: Type} `{Is0Gpd A} 
+#[export] Instance gpd_hom_to_hom_proper {A B : Type} `{Is0Gpd A}
   {R : Relation B} (F : A -> B)
   `{CMorphisms.Proper _ (GpdHom ==> R) F}
   : CMorphisms.Proper (Hom ==> R) F.
 Proof.
   intros a b eq_ab; apply H2; exact eq_ab.
 Defined.
 
-#[export] Instance Is1Functor_uncurry_bifunctor {A B C : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C)
-  `{!IsBifunctor F}
-  `{forall a, Is1Functor (F a)}
-  `{forall b, Is1Functor (flip F b)}
-  : Is1Functor (uncurry F).
-Proof.
-  nrapply Build_Is1Functor.
-  - intros [a1 a2] [b1 b2] [f1 f2] [g1 g2] [eq_fg1 eq_fg2];
-      cbn in f1, f2, g1, g2, eq_fg1, eq_fg2. cbn.
-    rewrite eq_fg1, eq_fg2.
-    reflexivity.
-  - intros [a b]; cbn.
-    (* rewrite fmap_id generates an extra goal. Not sure how to get typeclass resolution to figure this out automatically. *)
-    rewrite (fmap_id _).
-    rewrite (fmap_id _).
-    rewrite cat_idl.
-    reflexivity.
-  - intros [a1 b1] [a2 b2] [a3 b3] [f1 f2] [g1 g2];
-      cbn in f1, f2, g1, g2.
-    cbn.
-    rewrite (fmap_comp _).
-    rewrite (fmap_comp _).
-    rewrite cat_assoc.
-    rewrite <- (cat_assoc _ (fmap (F a1) g2)).
-    rewrite <- (bifunctor_isbifunctor F f1 g2).
-    rewrite ! cat_assoc.
-    reflexivity.
-Defined.
-
 #[export] Instance gpd_hom_is_proper1 {A : Type} `{Is0Gpd A}
  : CMorphisms.Proper
      (Hom ==> Hom ==> CRelationClasses.arrow) Hom.
@@ -194,7 +163,7 @@ Defined.
 
 Proposition nat_equiv_faithful {A B : Type}
   {F G : A -> B} `{Is1Functor _ _ F}
-  `{!Is0Functor G, !Is1Functor G} 
+  `{!Is0Functor G, !Is1Functor G}
   `{!HasEquivs B} (tau : NatEquiv F G)
   : Faithful F -> Faithful G.
 Proof.

theories/Algebra/AbGroups/AbHom.v

@@ -63,11 +63,42 @@ Proof.
   by apply equiv_path_grouphomomorphism.
 Defined.
 
-Global Instance isbifunctor_ab_hom `{Funext}
-  : IsBifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
+Global Instance is1functor_ab_hom01 `{Funext} {A : Group^op}
+  : Is1Functor (ab_hom A).
 Proof.
-  snrapply Build_IsBifunctor.
-  1-2: exact _.
+  nrapply Build_Is1Functor.
+  - intros B B' f g p phi.
+    apply equiv_path_grouphomomorphism; intro a; cbn.
+    exact (p (phi a)).
+  - intros B phi.
+    by apply equiv_path_grouphomomorphism.
+  - intros B C D f g phi.
+    by apply equiv_path_grouphomomorphism.
+Defined.
+
+Global Instance is1functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
+  : Is1Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
+Proof.
+  nrapply Build_Is1Functor.
+  - intros A A' f g p phi.
+    apply equiv_path_grouphomomorphism; intro a; cbn.
+    exact (ap phi (p a)).
+  - intros A phi.
+    by apply equiv_path_grouphomomorphism.
+  - intros A C D f g phi.
+    by apply equiv_path_grouphomomorphism.
+Defined.
+
+Global Instance is0bifunctor_ab_hom `{Funext}
+  : Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
+Proof.
+  rapply Build_Is0Bifunctor.
+Defined.
+
+Global Instance is1bifunctor_ab_hom `{Funext}
+  : Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
+Proof.
+  rapply Build_Is1Bifunctor.
   intros A A' f B B' g phi; cbn.
   by apply equiv_path_grouphomomorphism.
 Defined.

theories/Algebra/AbSES/BaerSum.v

@@ -51,12 +51,19 @@ Proof.
   apply abses_pushout_pullback_reorder'.
 Defined.
 
-Global Instance isbifunctor_abses' `{Univalence}
-  : IsBifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
+Global Instance is0bifunctor_abses' `{Univalence}
+  : Is0Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
 Proof.
-  eapply Build_IsBifunctor.
+  rapply Build_Is0Bifunctor.
+Defined.
+
+Global Instance is1bifunctor_abses' `{Univalence}
+  : Is1Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
+Proof.
+  snrapply Build_Is1Bifunctor.
+  1,2: exact _.
   intros ? ? g ? ? f E; cbn.
-  apply abses_pushout_pullback_reorder.
+  exact (abses_pushout_pullback_reorder E f g).
 Defined.
 
 (** Given a short exact sequence [A -> E -> B] and maps [f : A -> A'], [g : B' -> B], we can change the order of pushing out along [f] and pulling back along [g]. *)
@@ -222,10 +229,17 @@ Proof.
   - intro; apply baer_sum_unit_r.
 Defined.
 
-Global Instance isbifunctor_abses `{Univalence}
-  : IsBifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
+Global Instance is0bifunctor_abses `{Univalence}
+  : Is0Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
+Proof.
+  rapply Build_Is0Bifunctor.
+Defined.
+
+Global Instance is1bifunctor_abses `{Univalence}
+  : Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
 Proof.
-  econstructor.
+  snrapply Build_Is1Bifunctor.
+  1,2: exact _.
   intros ? ? f ? ? g.
   rapply hspace_phomotopy_from_homotopy.
   1: apply ishspace_abses.

theories/Algebra/AbSES/Ext.v

@@ -2,7 +2,7 @@ Require Import Basics Types Truncations.Core.
 Require Import Pointed WildCat.
 Require Import Truncations.SeparatedTrunc.
 Require Import AbelianGroup AbHom AbProjective.
-Require Import AbSES.Pullback AbSES.BaerSum AbSES.Core.
+Require Import AbSES.Pullback AbSES.Pushout AbSES.BaerSum AbSES.Core.
 
 Local Open Scope mc_scope.
 Local Open Scope mc_add_scope.
@@ -11,6 +11,14 @@ Local Open Scope mc_add_scope.
 
 Definition Ext (B A : AbGroup@{u}) := pTr 0 (AbSES B A).
 
+Global Instance is0bifunctor_ext `{Univalence}
+  : Is0Bifunctor (Ext : AbGroup^op -> AbGroup -> pType)
+  := is0bifunctor_compose _ _ (bf:=is0bifunctor_abses).
+
+Global Instance is1bifunctor_ext `{Univalence}
+  : Is1Bifunctor (Ext : AbGroup^op -> AbGroup -> pType)
+  := is1bifunctor_compose _ _ (bf:=is1bifunctor_abses).
+
 (** An extension [E : AbSES B A] is trivial in [Ext B A] if and only if [E] merely splits. *)
 Proposition iff_ab_ext_trivial_split `{Univalence} {B A : AbGroup} (E : AbSES B A)
   : merely {s : GroupHomomorphism B E & (projection _) $o s == idmap}
@@ -24,9 +32,13 @@ Defined.
 
 Definition Ext' (B A : AbGroup@{u}) := Tr 0 (AbSES' B A).
 
-Global Instance isbifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
-  : IsBifunctor@{v v w u u v v} (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
-  := isbifunctor_compose _ _ (P:=isbifunctor_abses').
+Global Instance is0bifunctor_ext' `{Univalence}
+  : Is0Bifunctor (Ext' : AbGroup^op -> AbGroup -> Type)
+  := is0bifunctor_compose _ _ (bf:=is0bifunctor_abses').
+
+Global Instance is1bifunctor_ext' `{Univalence}
+  : Is1Bifunctor (Ext' : AbGroup^op -> AbGroup -> Type)
+  := is1bifunctor_compose _ _ (bf:=is1bifunctor_abses').
 
 (** [Ext B A] is an abelian group for any [A B : AbGroup]. The proof of commutativity is a bit faster if we separate out the proof that [Ext B A] is a group. *)
 Definition grp_ext `{Univalence} (B A : AbGroup@{u}) : Group.
@@ -60,39 +72,65 @@ Proof.
   apply baer_sum_commutative.
 Defined.
 
-Global Instance is01functor_ext `{Univalence} (B : AbGroup^op)
+Global Instance is0functor_abext01 `{Univalence} (B : AbGroup^op)
   : Is0Functor (ab_ext B).
 Proof.
   srapply Build_Is0Functor; intros ? ? f.
   snrapply Build_GroupHomomorphism.
-  1: exact (fmap01 (A:=AbGroup^op) Ext' B f).
+  1: exact (fmap (Ext B) f).
   rapply Trunc_ind; intro E0.
   rapply Trunc_ind; intro E1.
   apply (ap tr); cbn.
   apply baer_sum_pushout.
 Defined.
 
-Global Instance is10functor_ext `{Univalence} (A : AbGroup)
+Global Instance is0functor_abext10 `{Univalence} (A : AbGroup)
   : Is0Functor (fun B : AbGroup^op => ab_ext B A).
 Proof.
   srapply Build_Is0Functor; intros ? ? f; cbn.
   snrapply Build_GroupHomomorphism.
-  1: exact (fmap10 (A:=AbGroup^op) Ext' f A).
+  1: exact (fmap (fun (B : AbGroup^op) => Ext B A) f).
   rapply Trunc_ind; intro E0.
   rapply Trunc_ind; intro E1.
   apply (ap tr); cbn.
   apply baer_sum_pullback.
 Defined.
 
-Global Instance isbifunctor_ext `{Univalence}
-  : IsBifunctor (A:=AbGroup^op) ab_ext.
+Global Instance is1functor_abext01 `{Univalence} (B : AbGroup^op)
+  : Is1Functor (ab_ext B).
+Proof.
+  snrapply Build_Is1Functor.
+  - intros A C f g.
+    exact (fmap2 (Ext B)).
+  - exact (fmap_id (Ext B)).
+  - intros A C D.
+    exact (fmap_comp (Ext B)).
+Defined.
+
+Global Instance is1functor_abext10 `{Univalence} (A : AbGroup)
+  : Is1Functor (fun B : AbGroup^op => ab_ext B A).
+Proof.
+  snrapply Build_Is1Functor.
+  - intros B C f g.
+    exact (fmap2 (fun B : AbGroup^op => Ext B A)).
+  - exact (fmap_id (fun B : AbGroup^op => Ext B A)).
+  - intros B C D.
+    exact (fmap_comp (fun B : AbGroup^op => Ext B A)).
+Defined.
+
+Global Instance is0bifunctor_abext `{Univalence}
+  : Is0Bifunctor (A:=AbGroup^op) ab_ext.
+Proof.
+  rapply Build_Is0Bifunctor.
+Defined.
+
+Global Instance is1bifunctor_abext `{Univalence}
+  : Is1Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
-  snrapply Build_IsBifunctor.
+  snrapply Build_Is1Bifunctor.
   1,2: exact _.
-  intros B B' f A A' g.
-  rapply Trunc_ind; intro E.
-  apply (ap tr).
-  apply abses_pushout_pullback_reorder.
+  intros A B.
+  exact (bifunctor_isbifunctor (Ext : AbGroup^op -> AbGroup -> pType)).
 Defined.
 
 (** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)

theories/Homotopy/Join/Core.v

@@ -560,16 +560,23 @@ Section FunctorJoin.
   Definition equiv_functor_join {A B C D} (f : A <~> C) (g : B <~> D)
     : Join A B <~> Join C D := Build_Equiv _ _ (functor_join f g) _.
 
-  Global Instance isbifunctor_join : IsBifunctor Join.
-  Proof.
-    snrapply Build_IsBifunctor.
-    - intro A; snrapply Build_Is0Functor; intros B D g.
-      exact (functor_join idmap g).
-    - intro B; snrapply Build_Is0Functor; intros A C f.
-      exact (functor_join f idmap).
-    - intros A C f B D g x.
-      lhs_V nrapply functor_join_compose.
-      nrapply functor_join_compose.
+  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.
+    - intros A B f g [p q].
+      exact (functor2_join p q).
+    - intros A; exact functor_join_idmap.
+    - intros A B C [f g] [h k].
+      exact (functor_join_compose f g h k).
   Defined.
 
 End FunctorJoin.