Significant progress on biproducts.

Author: wkolowski

Cat.v

@@ -303,6 +303,17 @@ Definition isAut' {C : Cat} {A : Ob C} (f : Hom A A) : Type :=
 
 #[global] Hint Unfold isEndo isMono isEpi isBi isSec isRet isIso isAut : core.
 
+(** Constant, coconstant and zero morphisms *)
+
+Definition isConstant {C : Cat} {A B : Ob C} (f : Hom A B) : Prop :=
+  forall (X : Ob C) (h1 h2 : Hom X A), h1 .> f == h2 .> f.
+
+Definition isCoconstant {C : Cat} {A B : Ob C} (f : Hom A B) : Prop :=
+  forall (X : Ob C) (h1 h2 : Hom B X), f .> h1 == f .> h2.
+
+Definition isZeroMor {C : Cat} {A B : Ob C} (f : Hom A B) : Prop :=
+  isConstant f /\ isCoconstant f.
+
 (** *** Duality and subsumption *)
 
 Lemma isMono_Dual :

Instances/AbGrp.v

@@ -156,6 +156,8 @@ Proof.
   - now apply HasProducts_AbGrp.
   - now apply HasCoproducts_AbGrp.
   - now cbn.
+  - now cbn.
+  - now cbn.
 Defined.
 
 #[refine]

Instances/CMon.v

@@ -203,6 +203,8 @@ Proof.
   - now apply HasProducts_CMon.
   - now apply HasCoproducts_CMon.
   - now cbn.
+  - now cbn.
+  - now cbn.
 Defined.
 
 #[refine]

Instances/FunCat.v

@@ -1,6 +1,7 @@
 From Cat Require Import Cat.
 From Cat.Universal Require Import
-  Initial Terminal Product Coproduct Biproduct Equalizer Coequalizer Pullback Pushout Exponential.
+  Initial Terminal Product Coproduct Biproduct
+  Equalizer Coequalizer Pullback Pushout Exponential.
 From Cat.Universal Require Import Duality.
 
 Set Implicit Arguments.
@@ -244,7 +245,8 @@ Defined.
 
 #[refine]
 #[export]
-Instance FunCat_biproduct {C D : Cat} {hb : HasBiproducts' D} (F G : Functor C D) : Functor C D :=
+Instance FunCat_biproduct
+  {C D : Cat} {hb : HasBiproducts' D} (F G : Functor C D) : Functor C D :=
 {
   fob  := fun X : Ob C => biproduct (fob F X) (fob G X);
   fmap := fun (X Y : Ob C) (f : Hom X Y) => fmap F f ×+' fmap G f
@@ -258,7 +260,8 @@ Defined.
 #[refine]
 #[export]
 Instance FunCat_bioutl
-  {C D : Cat} {hp : HasBiproducts' D} {F G : Functor C D} : NatTrans (FunCat_biproduct F G) F :=
+  {C D : Cat} {hp : HasBiproducts' D} {F G : Functor C D}
+  : NatTrans (FunCat_biproduct F G) F :=
 {
   component := fun _ : Ob C => bioutl
 }.
@@ -272,7 +275,8 @@ Defined.
 #[refine]
 #[export]
 Instance FunCat_bioutr
-  {C D : Cat} {hp : HasBiproducts' D} {F G : Functor C D} : NatTrans (FunCat_biproduct F G) G :=
+  {C D : Cat} {hp : HasBiproducts' D} {F G : Functor C D}
+  : NatTrans (FunCat_biproduct F G) G :=
 {
   component := fun _ : Ob C => bioutr
 }.
@@ -292,19 +296,18 @@ Instance FunCat_bipair
   component := fun X : Ob C => bipair (component α X) (component β X)
 }.
 Proof.
-  intros.
-  rewrite fpair_comp, <- !natural.
-  rewrite equiv_product', fpair_outl, fpair_outr.
-  Search bipair fmap. cbn.
-(*   rewrite equiv_product', !comp_assoc, fpair_outl, fpair_outr. cbn.
-  rewrite !copair_comp, binr_bioutl', binl_bioutr'.
-  rewrite !comp_assoc, binl_bioutl, binr_bioutr, !comp_id_r. *)
-Admitted.
+  intros X Y f; cbn.
+  rewrite equiv_product', !comp_assoc.
+  rewrite bicopair_bioutl, bicopair_bioutr.
+  rewrite fpair_outl, fpair_outr, <- !comp_assoc, fpair_outl, fpair_outr.
+  now rewrite !natural.
+Defined.
 
 #[refine]
 #[export]
 Instance FunCat_binl
-  {C D : Cat} {hp : HasBiproducts' D} {F G : Functor C D} : NatTrans F (FunCat_biproduct F G) :=
+  {C D : Cat} {hp : HasBiproducts' D} {F G : Functor C D}
+  : NatTrans F (FunCat_biproduct F G) :=
 {
   component := fun _ : Ob C => binl
 }.
@@ -315,7 +318,8 @@ Defined.
 #[refine]
 #[export]
 Instance FunCat_binr
-  {C D : Cat} {hp : HasBiproducts' D} {F G : Functor C D} : NatTrans G (FunCat_biproduct F G) :=
+  {C D : Cat} {hp : HasBiproducts' D} {F G : Functor C D}
+  : NatTrans G (FunCat_biproduct F G) :=
 {
   component := fun _ : Ob C => binr
 }.
@@ -352,14 +356,16 @@ Instance HasBiproducts_FunCat
 }.
 Proof.
   - split; cbn; intros.
-    + admit.
-    + admit.
+    + now rewrite fpair_outl.
+    + now rewrite fpair_outr.
     + now rewrite equiv_product', H, H0.
   - split; cbn; intros.
     + now rewrite finl_copair.
     + now rewrite finr_copair.
     + now rewrite equiv_coproduct', H, H0.
-  - cbn; intros. apply HasBiproducts'_ok.
+  - now cbn; intros F G X; apply binl_bioutl.
+  - now cbn; intros F G X; apply binr_bioutr.
+  - now cbn; intros; apply HasBiproducts'_ok.
 Defined.
 
 #[refine]

Instances/Rel.v

@@ -281,6 +281,12 @@ Instance HasBiproducts'_Rel : HasBiproducts' Rel :=
 Proof.
   - now apply HasProducts_Rel.
   - now apply HasCoproducts_Rel.
+  - intros A B a1 a2; cbn; split.
+    + now intros [[a | b] [H1 H2]]; [rewrite H1, H2 |].
+    + now intros Heq; exists (inl a2).
+  - intros A B b1 b2; cbn; split.
+    + now intros [[a | b] [H1 H2]]; [| rewrite H1, H2].
+    + now intros Heq; exists (inr b2).
   - intros A B [a1 | b1] [a2 | b2]; cbn.
     + now firstorder.
     + split; [| now firstorder].

Universal/Biproduct.v

@@ -17,7 +17,7 @@ Set Implicit Arguments.
 Class isBiproduct
   (C : Cat) {A B : Ob C}
   (P : Ob C) (outl : Hom P A) (outr : Hom P B) (finl : Hom A P) (finr : Hom B P)
-  (fpair : forall {X : Ob C} (f : Hom X A) (g : Hom X B), Hom X P)
+  (fpair  : forall {X : Ob C} (f : Hom X A) (g : Hom X B), Hom X P)
   (copair : forall {X : Ob C} (f : Hom A X) (g : Hom B X), Hom P X)
   : Prop :=
 {
@@ -56,17 +56,36 @@ Class HasBiproducts' (C : Cat) : Type :=
   binl     : forall {A B : Ob C}, Hom A (biproduct A B);
   binr     : forall {A B : Ob C}, Hom B (biproduct A B);
   bicopair : forall {A B : Ob C} {P : Ob C} (f : Hom A P) (g : Hom B P), Hom (biproduct A B) P;
-
   isCoproduct_HasBiproducts :>
     forall {A B : Ob C}, isCoproduct C (@biproduct A B) binl binr (@bicopair A B);
 
+  binl_bioutl :
+    forall {A B : Ob C},
+      @binl A B .> bioutl == id A;
+  binr_bioutr :
+    forall {A B : Ob C},
+      @binr A B .> bioutr == id B;
+
   HasBiproducts'_ok :
     forall {A B : Ob C},
       @bioutl A B .> @binl A B .> @bioutr A B .> @binr A B
         ==
       bioutr .> binr .> bioutl .> binl;
 }.
-    
+
+Definition zero {C : Cat} {hb : HasBiproducts' C} {A B : Ob C} : Hom A B :=
+  @binl _ _ A B .> bioutr.
+
+Definition bidiag {C : Cat} {hp : HasBiproducts' C} {A : Ob C} : Hom A (biproduct A A) :=
+  bipair (id A) (id A).
+
+Definition bicodiag {C : Cat} {hp : HasBiproducts' C} {A : Ob C} : Hom (biproduct A A) A :=
+  bicopair (id A) (id A).
+
+Definition biadd
+  {C : Cat} {hb : HasBiproducts' C}
+  {A B : Ob C} (f g : Hom A B) : Hom A B :=
+    bipair f g .> bicodiag.
 
 Section BiproductIdentities.
 
@@ -75,20 +94,16 @@ Context
   (hb : HasBiproducts' C)
   (A B : Ob C).
 
-Lemma binl_bioutl :
-  @binl _ _ A B .> bioutl == id A.
-Proof.
-Admitted.
-
-Lemma binr_bioutr :
-  @binr _ _ A B .> bioutr == id B.
-Proof.
-Admitted.
-
 Lemma binl_bioutr :
   forall {X : Ob C} (f : Hom B X),
     @binl _ _ A B .> bioutr .> f == @binl _ _ A X .> bioutr.
 Proof.
+  intros.
+  (* assert (
+    bioutr .> binr .> bioutl .> @binl _ _ A B .> bioutr .> f
+      ==
+    bioutr .> binr .> bioutl .> @binl _ _ A X .> bioutr).
+  ). *)
 Admitted.
 
 Lemma binl_bioutr' :
@@ -107,10 +122,63 @@ Lemma binr_bioutl' :
   forall {X : Ob C} (f : Hom X B),
     f .> @binr _ _ A B .> bioutl == @binr _ _ A X .> bioutl.
 Proof.
+  intros.
+  assert (H1 : isConstant (@binr _ _ A B .> bioutl)) by admit.
+  assert (H2 : isCoconstant (@binr _ _ A B .> bioutl)) by admit.
+  unfold isConstant, isCoconstant in H1, H2.
 Admitted.
 
 End BiproductIdentities.
 
+Section MoreBiproductIdentities.
+
+Context
+  (C : Cat)
+  (hb : HasBiproducts' C)
+  (A B : Ob C).
+
+Lemma binl_bipair :
+  forall {A' B' : Ob C} (f : Hom A A') (g : Hom B B'),
+    binl .> bipair (bioutl .> f) (bioutr .> g) == f .> binl.
+Proof.
+  intros.
+  rewrite equiv_product', !comp_assoc, fpair_outl, fpair_outr.
+  rewrite binl_bioutl, <- !comp_assoc, binl_bioutl, comp_id_l, comp_id_r.
+  now rewrite binl_bioutr, binl_bioutr'.
+Qed.
+
+Lemma binr_bipair :
+  forall {A' B' : Ob C} (f : Hom A A') (g : Hom B B'),
+    binr .> bipair (bioutl .> f) (bioutr .> g) == g .> binr.
+Proof.
+  intros.
+  rewrite equiv_product', !comp_assoc, fpair_outl, fpair_outr.
+  rewrite binr_bioutr, <- !comp_assoc, binr_bioutr, comp_id_l, comp_id_r.
+  now rewrite binr_bioutl, binr_bioutl'.
+Qed.
+
+Lemma bicopair_bioutl :
+  forall {A' B' : Ob C} (f : Hom A A') (g : Hom B B'),
+    bicopair (f .> binl) (g .> binr) .> bioutl == bioutl .> f.
+Proof.
+  intros.
+  rewrite equiv_coproduct', <- !comp_assoc, finl_copair, finr_copair.
+  rewrite binr_bioutl, binr_bioutl'.
+  now rewrite binl_bioutl, comp_assoc, binl_bioutl, comp_id_l, comp_id_r.
+Defined.
+
+Lemma bicopair_bioutr :
+  forall {A' B' : Ob C} (f : Hom A A') (g : Hom B B'),
+    bicopair (f .> binl) (g .> binr) .> bioutr == bioutr .> g.
+Proof.
+  intros.
+  rewrite equiv_coproduct', <- !comp_assoc, finl_copair, finr_copair.
+  rewrite binl_bioutr, binl_bioutr'.
+  now rewrite binr_bioutr, comp_assoc, binr_bioutr, comp_id_l, comp_id_r.
+Defined.
+
+End MoreBiproductIdentities.
+
 #[refine]
 #[export]
 Instance BiproductBifunctor' {C : Cat} {hp : HasBiproducts' C} : Bifunctor C C C :=

Universal/Coproduct.v

@@ -353,6 +353,9 @@ Proof.
   now apply isIso_associator.
 Defined.
 
+Definition codiag {C : Cat} {hp : HasCoproducts C} {A : Ob C} : Hom (coproduct A A) A :=
+  copair (id A) (id A).
+
 #[refine]
 #[export]
 Instance CoproductBifunctor {C : Cat} {hp : HasCoproducts C} : Bifunctor C C C :=

Universal/Product.v

@@ -249,8 +249,7 @@ Lemma fpair_comp' :
     (A B Γ A' B' : Ob C) (a : Hom Γ A) (b : Hom Γ B) (h1 : Hom A A') (h2 : Hom B B'),
       fpair a b .> fpair (outl .> h1) (outr .> h2) == fpair (a .> h1) (b .> h2).
 Proof.
-  intros; rewrite equiv_product'.
-  now rewrite !comp_assoc, !fpair_outl, !fpair_outr, <- !comp_assoc, fpair_outl, fpair_outr.
+  now intros; rewrite fpair_comp, <- !comp_assoc, fpair_outl, fpair_outr.
 Qed.
 
 Lemma fpair_comp_id :
@@ -347,6 +346,9 @@ Proof.
   - now apply unassociator_associator.
 Defined.
 
+Definition diag {C : Cat} {hp : HasProducts C} {A : Ob C} : Hom A (product A A) :=
+  fpair (id A) (id A).
+
 #[refine]
 #[export]
 Instance ProductBifunctor {C : Cat} {hp : HasProducts C} : Bifunctor C C C :=