wildcat: binary products

theories/Algebra/Groups/FreeProduct.v

@@ -4,6 +4,7 @@ Require Import Spaces.List.
 Require Import Colimits.Pushout.
 Require Import Truncations.Core Truncations.SeparatedTrunc.
 Require Import Algebra.Groups.Group.
+Require Import WildCat.
 
 Local Open Scope list_scope.
 Local Open Scope mc_scope.
@@ -679,6 +680,8 @@ Section FreeProduct.
 
 End FreeProduct.
 
+Arguments amal_eta {G H K f g} x.
+
 Definition FreeProduct (G H : Group) : Group
   := AmalgamatedFreeProduct grp_trivial G H (grp_trivial_rec _) (grp_trivial_rec _).
 
@@ -709,3 +712,31 @@ Proof.
   apply tr.
   refine (grp_homo_unit _ @ (grp_homo_unit _)^).
 Defined.
+
+(** The freeproduct is the coproduct in the category of groups. *)
+Global Instance hasbinarycoproducts : HasBinaryCoproducts Group.
+Proof.
+  snrapply Build_HasBinaryCoproducts.
+  intros G H.
+  snrapply Build_BinaryCoproduct.
+  - exact (FreeProduct G H).
+  - exact freeproduct_inl.
+  - exact freeproduct_inr.
+  - exact (FreeProduct_rec G H).
+  - intros Z f g x; simpl.
+    rapply right_identity.
+  - intros Z f g x; simpl.
+    rapply right_identity.
+  - intros Z f g p q.
+    srapply amal_type_ind_hprop; simpl.
+    intros w.
+    induction w as [|gh].
+    1: exact (grp_homo_unit _ @ (grp_homo_unit _)^).
+    Local Notation "[ x ]" := (cons x nil).
+    change (f (amal_eta [gh] * amal_eta w) = g (amal_eta [gh] * amal_eta w)).
+    refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
+    f_ap; clear IHw w.
+    destruct gh as [g' | h].
+    + exact (p g').
+    + exact (q h).
+Defined.

theories/Algebra/Groups/Group.v

@@ -711,6 +711,24 @@ Global Instance issurj_grp_prod_pr2 {G H : Group}
   : IsSurjection (@grp_prod_pr2 G H)
   := issurj_retr grp_prod_inr (fun _ => idpath).
 
+Global Instance hasbinaryproducts_group : HasBinaryProducts Group.
+Proof.
+  snrapply Build_HasBinaryProducts.
+  intros G H.
+  snrapply Build_BinaryProduct.
+  - exact (grp_prod G H).
+  - exact grp_prod_pr1.
+  - exact grp_prod_pr2.
+  - intros K.
+    exact grp_prod_corec.
+  - intros K f g.
+    exact (Id _).
+  - intros K f g.
+    exact (Id _).
+  - intros K f g p q a.
+    exact (path_prod' (p a) (q a)).
+Defined.
+
 (** *** Properties of maps to and from the trivial group *)
 
 Global Instance isinitial_grp_trivial : IsInitial grp_trivial.

theories/Homotopy/Wedge.v

@@ -1,6 +1,7 @@
-Require Import Basics.
+Require Import Basics Types.Paths.
 Require Import Pointed.Core.
 Require Import Colimits.Pushout.
+Require Import WildCat.
 
 (* Here we define the Wedge sum of two pointed types *)
 
@@ -11,9 +12,93 @@ Definition Wedge (X Y : pType) : pType
 
 Notation "X \/ Y" := (Wedge X Y) : pointed_scope.
 
+Definition wedge_inl {X Y} : X $-> X \/ Y.
+Proof.
+  snrapply Build_pMap.
+  - exact (fun x => pushl x).
+  - reflexivity.
+Defined.
+
+Definition wedge_inr {X Y} : Y $-> X \/ Y.
+Proof.
+  snrapply Build_pMap.
+  - exact (fun x => pushr x).
+  - symmetry.
+    by rapply pglue.
+Defined.
+
 Definition wglue {X Y : pType}
   : pushl (point X) = (pushr (point Y) : X \/ Y) := pglue tt.
 
+Definition wedge_rec {X Y Z : pType} (f : X $-> Z) (g : Y $-> Z)
+  : X \/ Y $-> Z.
+Proof.
+  snrapply Build_pMap.
+  - snrapply Pushout_rec.
+    + exact f.
+    + exact g.
+    + by pelim f g.
+  - exact (point_eq f).
+Defined.
+
 Definition wedge_incl {X Y : pType} : X \/ Y -> X * Y :=
  Pushout_rec _ (fun x => (x, point Y)) (fun y => (point X, y)) 
   (fun _ : Unit => idpath).
+
+(** 1-universal property of wedge. *)
+(** TODO: remove rewrites. For some reason pelim is not able to immediately abstract the goal so some shuffling around is necessery. *)
+Lemma wedge_up X Y Z (f g : X \/ Y $-> Z)
+  : f $o wedge_inl $== g $o wedge_inl
+  -> f $o wedge_inr $== g $o wedge_inr
+  -> f $== g.
+Proof.
+  intros p q.
+  snrapply Build_pHomotopy.
+  - snrapply (Pushout_ind _ p q).
+    intros [].
+    simpl.
+    refine (transport_paths_FlFr _ _ @ _).
+    refine (concat_pp_p _ _ _ @ _).
+    apply moveR_Vp.
+    refine (whiskerR (dpoint_eq p) _ @ _).
+    refine (_ @ whiskerL _ (dpoint_eq q)^).
+    clear p q.
+    simpl.
+    apply moveL_Mp.
+    rewrite ? ap_V.
+    rewrite ? inv_pp.
+    hott_simpl.
+  - simpl; pelim p q.
+    hott_simpl.
+Defined.
+
+Global Instance hasbinarycoproducts : HasBinaryCoproducts pType.
+Proof.
+  snrapply Build_HasBinaryCoproducts.
+  intros X Y.
+  snrapply Build_BinaryCoproduct.
+  - exact (X \/ Y).
+  - exact wedge_inl.
+  - exact wedge_inr.
+  - intros Z f g.
+    by apply wedge_rec.
+  - intros Z f g.
+    snrapply Build_pHomotopy.
+    1: reflexivity.
+    by simpl; pelim f.
+  - intros Z f g.
+    snrapply Build_pHomotopy.
+    1: reflexivity.
+    simpl.
+    apply moveL_pV.
+    apply moveL_pM.
+    refine (_ @ (ap_V _ (pglue tt))^).
+    apply moveR_Mp.
+    apply moveL_pV.
+    apply moveR_Vp.
+    refine (Pushout_rec_beta_pglue _ f g _ _  @ _).
+    simpl.  
+    by pelim f g.
+  - intros Z f g p q.
+    by apply wedge_up.
+Defined.

theories/Pointed/Core.v

@@ -627,6 +627,38 @@ Proof.
   + intros. reflexivity.
 Defined.
 
+(** pType has binary products *)
+Global Instance hasbinaryproducts_ptype : HasBinaryProducts pType.
+Proof.
+  snrapply Build_HasBinaryProducts.
+  intros X Y.
+  snrapply Build_BinaryProduct.
+  - exact (X * Y).
+  - exact pfst.
+  - exact psnd.
+  - intros Z f g.
+    snrapply Build_pMap.
+    1: exact (fun w => (f w, g w)).
+    apply path_prod'; cbn; apply point_eq.
+  - intros Z f g.
+    snrapply Build_pHomotopy.
+    1: reflexivity.
+    by pelim f g.
+  - intros Z f g.
+    snrapply Build_pHomotopy.
+    1: reflexivity.
+    by pelim f g.
+  - intros Z f g p q.
+    simpl.
+    snrapply Build_pHomotopy.
+    { intros a.
+      apply path_prod'; cbn.
+      - exact (p a).
+      - exact (q a). }
+    simpl.
+    by pelim p q f g.
+Defined.
+
 (** Some higher homotopies *)
 
 (** Horizontal composition of homotopies. *)

theories/WildCat.v

@@ -12,6 +12,8 @@ Require Export WildCat.Square.
 Require Export WildCat.PointedCat.
 Require Export WildCat.Bifunctor.
 Require Export WildCat.Monoidal.
+Require Export WildCat.Products.
+Require Export WildCat.Coproducts.
 
 (* See also contrib/SetoidRewrite.v for tools that can be used for rewriting in wild categories. *)
 

theories/WildCat/Coproducts.v

@@ -0,0 +1,151 @@
+Require Import Basics EquivGpd Types.Prod Types.Sum.
+Require Import WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite WildCat.Products.
+
+(** * Categories with coproducts *)
+
+Class BinaryCoproduct (A : Type) `{Is1Cat A} (x y : A) := Build_BinaryCoproduct' {
+  prod_co_coprod :: BinaryProduct (x : A^op) y
+}.
+
+Arguments Build_BinaryCoproduct' {_ _ _ _ _ x y} _.
+Arguments BinaryCoproduct {A _ _ _ _} x y.
+
+Definition cat_coprod {A : Type}  `{Is1Cat  A} (x y : A) `{!BinaryCoproduct x y} : A
+  := cat_prod (x : A^op) y.
+
+Definition cat_inl {A : Type} `{Is1Cat A} {x y : A} `{!BinaryCoproduct x y} : x $-> cat_coprod x y.
+Proof.
+  change (cat_prod (x : A^op) y $-> x).
+  exact cat_pr1.
+Defined.
+
+Definition cat_inr {A : Type} `{Is1Cat A} {x y : A} `{!BinaryCoproduct x y} : y $-> cat_coprod x y.
+Proof.
+  change (cat_prod (x : A^op) y $-> y).
+  exact cat_pr2.
+Defined.
+
+Definition Build_BinaryCoproduct {A : Type} `{Is1Cat A} {x y : A}
+  (cat_coprod : A) (cat_inl : x $-> cat_coprod) (cat_inr : y $-> cat_coprod)
+  (cat_coprod_rec : forall z : A, (x $-> z) -> (y $-> z) -> cat_coprod $-> z)
+  (cat_coprod_beta_inl : forall z (f : x $-> z) (g : y $-> z), cat_coprod_rec z f g $o cat_inl $== f)
+  (cat_coprod_beta_inr : forall z (f : x $-> z) (g : y $-> z), cat_coprod_rec z f g $o cat_inr $== g)
+  (cat_coprod_in_eta : forall z (f g : cat_coprod $-> z), f $o cat_inl $== g $o cat_inl -> f $o cat_inr $== g $o cat_inr -> f $== g)
+  : BinaryCoproduct x y
+  := Build_BinaryCoproduct'
+    (Build_BinaryProduct
+      (cat_coprod : A^op)
+      cat_inl
+      cat_inr
+      cat_coprod_rec
+      cat_coprod_beta_inl
+      cat_coprod_beta_inr
+      cat_coprod_in_eta).
+
+Section Lemmata.
+
+  Context {A : Type} {x y z : A} `{BinaryCoproduct _ x y}.
+
+  Definition cate_cat_coprod_rec_inv
+    : (opyon_0gpd (cat_coprod x y) z)
+    $<~> prod_0gpd (opyon_0gpd x z) (opyon_0gpd y z)
+    := @cate_cat_prod_corec_inv A^op x y _ _ _ _ _ _.
+
+  Definition cate_cat_coprod_rec
+    : prod_0gpd (opyon_0gpd x z) (opyon_0gpd y z)
+    $<~> (opyon_0gpd (cat_coprod x y) z)
+    := @cate_cat_prod_corec A^op x y _ _ _ _ _ _.
+
+  Definition cat_coprod_rec (f : x $-> z) (g : y $-> z) : cat_coprod x y $-> z
+    := @cat_prod_corec A^op x y _ _ _ _ _ _ f g.
+
+  Definition cat_coprod_beta_inl (f : x $-> z) (g : y $-> z)
+    : cat_coprod_rec f g $o cat_inl $== f
+    := @cat_prod_beta_pr1 A^op x y _ _ _ _ _ _ f g.
+
+  Definition cat_coprod_beta_inr (f : x $-> z) (g : y $-> z)
+    : cat_coprod_rec f g $o cat_inr $== g
+    := @cat_prod_beta_pr2 A^op x y _ _ _ _ _ _ f g.
+
+  Definition cat_coprod_eta (f : cat_coprod x y $-> z)
+    : cat_coprod_rec (f $o cat_inl) (f $o cat_inr) $== f
+    := @cat_prod_eta A^op x y _ _ _ _ _ _ f.
+
+  (* TODO: decompose and move *)
+  Local Instance is0functor_coprod_0gpd_helper
+    : Is0Functor (fun z : A => prod_0gpd (opyon_0gpd x z) (opyon_0gpd y z)).
+  Proof.
+    snrapply Build_Is0Functor.
+    intros a b f.
+    snrapply Build_Morphism_0Gpd.
+    - intros [g g'].
+      exact (f $o g, f $o g').
+    - snrapply Build_Is0Functor.
+      intros [g g'] [h h'] [p q].
+      split.
+      + exact (f $@L p).
+      + exact (f $@L q).
+  Defined.
+
+  (* TODO: decompose and move *)
+  Local Instance is1functor_coprod_0gpd_helper
+    : Is1Functor (fun z : A => prod_0gpd (opyon_0gpd x z) (opyon_0gpd y z)).
+  Proof.
+    snrapply Build_Is1Functor.
+    - intros a b f g p [r_fst r_snd].
+      cbn; split.
+      + refine (_ $@R _).
+        apply p.
+      + refine (_ $@R _).
+        apply p.
+    - intros a [r_fst r_snd].
+      split; apply cat_idl.
+    - intros a b c f g [r_fst r_snd].
+      split; apply cat_assoc.
+  Defined.
+
+  Definition natequiv_cat_coprod_rec_inv
+    : NatEquiv (opyon_0gpd (cat_coprod x y)) (fun z => prod_0gpd (opyon_0gpd x z) (opyon_0gpd y z))
+    := @natequiv_cat_prod_corec_inv A^op x y _ _ _ _ _.
+
+  Definition cat_coprod_rec_eta {f f' : x $-> z} {g g' : y $-> z}
+    : f $== f' -> g $== g' -> cat_coprod_rec f g $== cat_coprod_rec f' g'
+    := @cat_prod_corec_eta A^op x y _ _ _ _ _ _ f f' g g'.
+
+  Definition cat_coprod_in_eta {f f' : cat_coprod x y $-> z}
+    : f $o cat_inl $== f' $o cat_inl -> f $o cat_inr $== f' $o cat_inr -> f $== f'
+    := @cat_prod_pr_eta A^op x y _ _ _ _ _ _ f f'.
+
+End Lemmata.
+
+(** *** Cateogires with binary coproducts *)
+
+Class HasBinaryCoproducts (A : Type) `{Is1Cat A} := {
+  binary_coproducts :: forall x y : A, BinaryCoproduct x y;
+}.
+
+(** *** Coproduct functor *)
+
+(** TODO: The functoriality argument doesn't follow definitionally from the functoriality of [cat_prod], however after some modification it is close. We need to use appropriate lemmas for opposite functors. *) 
+
+(** *** Coproducts in Type *)
+
+(** [Type] has all binary coproducts *)
+Global Instance hasbinarycoproducts_type : HasBinaryCoproducts Type.
+Proof.
+  snrapply Build_HasBinaryCoproducts.
+  intros X Y.
+  snrapply Build_BinaryCoproduct.
+  - exact (X + Y).
+  - exact inl.
+  - exact inr.
+  - intros Z f g.
+    intros [x | y].
+    + exact (f x).
+    + exact (g y).
+  - reflexivity.
+  - reflexivity.
+  - intros Z f g p q [x | y].
+    + exact (p x).
+    + exact (q y).
+Defined.