Defined equalizers and coequalizers of semigroups and pullbacks of sets.

Author: wkolowski

Category/Monoidal.v

@@ -6,7 +6,7 @@ Set Implicit Arguments.
 
 Class Monoidal : Type :=
 {
-  cat : Cat;
+  cat :> Cat;
   tensor : Bifunctor cat cat cat;
   tensor_unit : Ob cat;
   associator : forall X Y Z : Ob cat, Hom (biob (biob X Y) Z) (biob X (biob Y Z));

Instances/Setoid/Sgr.v

@@ -512,4 +512,176 @@ Proof.
     + now apply HB.
     + change {| hd := h; tl := Some t; |} with (@op (Sgr_coproduct A B) (Cons h None) t).
       now rewrite (@pres_op _ _ h1), (@pres_op _ _ h2), IHt; destruct h; rewrite ?HA, ?HB.
+Defined.
+
+#[refine]
+#[export]
+Instance Sgr_equalizer {A B : Sgr} (f g : SgrHom A B) : Sgr :=
+{
+  setoid := CoqSetoid_equalizer f g;
+}.
+Proof.
+  - cbn; intros [x Hx] [y Hy].
+    exists (op x y).
+    now rewrite !pres_op, Hx, Hy.
+  - intros [a1 H1] [a2 H2] Heq1 [a3 H3] [a4 H4] Heq2; cbn in *.
+    now rewrite Heq1, Heq2.
+  - intros [x Hx] [y Hy] [z Hz]; cbn in *.
+    now rewrite assoc.
+Defined.
+
+#[refine]
+#[export]
+Instance Sgr_equalize {A B : Sgr} (f g : SgrHom A B) : SgrHom (Sgr_equalizer f g) A :=
+{
+  setoidHom := CoqSetoid_equalize f g;
+}.
+Proof.
+  now intros [x Hx] [y Hy]; cbn.
+Defined.
+
+#[export]
+#[refine]
+Instance Sgr_factorize
+  {A B : Sgr} {f g : SgrHom A B}
+  {E' : Sgr} (e' : Hom E' A) (Heq : (e' .> f) == (e' .> g))
+  : SgrHom E' (Sgr_equalizer f g) :=
+{
+  setoidHom := CoqSetoid_factorize e' Heq;
+}.
+Proof.
+  now cbn; intros; rewrite pres_op.
+Defined.
+
+#[refine]
+#[export]
+Instance HasEqualizers_Sgr : HasEqualizers SgrCat :=
+{
+  equalizer := @Sgr_equalizer;
+  equalize := @Sgr_equalize;
+  factorize := @Sgr_factorize;
+}.
+Proof.
+  split; cbn.
+  - now intros [x H]; cbn.
+  - easy.
+  - easy.
+Defined.
+
+Inductive Sgr_coeq_equiv {A B : Sgr} (f g : SgrHom A B) : B -> B -> Prop :=
+| SgrCE_quot : forall a : A, Sgr_coeq_equiv f g (f a) (g a)
+| SgrCE_op   :
+  forall {l1 r1 l2 r2 : B},
+    Sgr_coeq_equiv f g l1 l2 ->
+    Sgr_coeq_equiv f g r1 r2 ->
+      Sgr_coeq_equiv f g (op l1 r1) (op l2 r2)
+| SgrCE_refl : forall {b1 b2 : B}, b1 == b2 -> Sgr_coeq_equiv f g b1 b2
+| SgrCE_sym  :
+  forall {b1 b2 : B}, Sgr_coeq_equiv f g b1 b2 -> Sgr_coeq_equiv f g b2 b1
+| SgrCE_trans :
+  forall {b1 b2 b3 : B},
+    Sgr_coeq_equiv f g b1 b2 ->
+    Sgr_coeq_equiv f g b2 b3 ->
+      Sgr_coeq_equiv f g b1 b3.
+
+#[export] Hint Constructors Sgr_coeq_equiv : core.
+
+#[refine]
+#[export]
+Instance Sgr_coequalizer_Setoid {A B : Sgr} (f g : SgrHom A B) : Setoid' :=
+{
+  carrier := B;
+  Setoids.setoid :=
+  {|
+    equiv := Sgr_coeq_equiv f g;
+  |};
+}.
+Proof.
+  split; red.
+  - now constructor.
+  - now apply SgrCE_sym.
+  - now intros; apply SgrCE_trans with y.
+Defined.
+
+#[refine]
+#[export]
+Instance Sgr_coequalizer {A B : Sgr} (f g : SgrHom A B) : Sgr :=
+{
+  setoid := Sgr_coequalizer_Setoid f g;
+  op := op;
+}.
+Proof.
+  - intros x1 x2 H12 x3 x4 H34; cbn in *.
+    now constructor.
+  - cbn; intros.
+    apply SgrCE_refl.
+    now rewrite assoc.
+Defined.
+
+#[refine]
+#[export]
+Instance Sgr_coequalize' {A B : Sgr} (f g : SgrHom A B) : SetoidHom B (Sgr_coequalizer f g) :=
+{
+  func := fun b => b;
+}.
+Proof.
+  intros b1 b2 Heq; cbn.
+  now constructor.
+Defined.
+
+#[refine]
+#[export]
+Instance Sgr_coequalize {A B : Sgr} (f g : SgrHom A B) : SgrHom B (Sgr_coequalizer f g) :=
+{
+  setoidHom := Sgr_coequalize' f g;
+}.
+Proof.
+  now constructor; cbn.
+Defined.
+
+#[export]
+#[refine]
+Instance Sgr_cofactorize'
+  {A B : Sgr} {f g : Hom A B}
+  {Q : Sgr} (q : Hom B Q) (Heq : f .> q == g .> q)
+  : SetoidHom (Sgr_coequalizer f g) Q :=
+{
+  func := q;
+}.
+Proof.
+  intros x y H. cbn in *.
+  induction H.
+  - easy.
+  - now rewrite !pres_op, IHSgr_coeq_equiv1, IHSgr_coeq_equiv2.
+  - now rewrite H.
+  - now symmetry.
+  - now transitivity (q b2).
+Defined.
+
+#[export]
+#[refine]
+Instance Sgr_cofactorize
+  {A B : Sgr} {f g : Hom A B}
+  {Q : Sgr} (q : Hom B Q) (Heq : f .> q == g .> q)
+  : SgrHom (Sgr_coequalizer f g) Q :=
+{
+  setoidHom := Sgr_cofactorize' Heq;
+}.
+Proof.
+  now cbn; intros; rewrite pres_op.
+Defined.
+
+#[refine]
+#[export]
+Instance HasCoequalizers_Sgr : HasCoequalizers SgrCat :=
+{
+  coequalizer := @Sgr_coequalizer;
+  coequalize := @Sgr_coequalize;
+  cofactorize := @Sgr_cofactorize;
+}.
+Proof.
+  split; cbn.
+  - now constructor.
+  - easy.
+  - easy.
 Defined.

Instances/Setoids.v

@@ -1,7 +1,7 @@
 From Cat Require Export Cat.
 From Cat Require Import Category.CartesianClosed.
 From Cat.Universal Require Export
-  Initial Terminal Product Coproduct Equalizer Coequalizer Exponential
+  Initial Terminal Product Coproduct Equalizer Coequalizer Pullback Pushout Exponential
   IndexedProduct IndexedCoproduct.
 
 Set Implicit Arguments.
@@ -288,8 +288,8 @@ Proof. now setoid. Defined.
 
 #[export]
 Program Instance CoqSetoid_factorize
-  {X Y : Setoid'} (f g : SetoidHom X Y)
-  (E' : Setoid') (e' : SetoidHom E' X) (H : forall x : E', f (e' x) == g (e' x))
+  {X Y : Setoid'} {f g : SetoidHom X Y}
+  {E' : Setoid'} (e' : SetoidHom E' X) (Heq : forall x : E', f (e' x) == g (e' x))
   : SetoidHom E' (CoqSetoid_equalizer f g) :=
 {
   func := fun x => e' x
@@ -517,4 +517,88 @@ Instance CoqSetoid_CartesianClosed : CartesianClosed CoqSetoid :=
   HasTerm_CartesianClosed := HasTerm_CoqSetoid;
   HasProducts_CartesianClosed := HasProducts_CoqSetoid;
   HasExponentials_CartesianClosed := HasExponentials_CoqSetoid;
-}.
+}.
+
+Record CoqSetoid_pullback'
+  {A B X : Setoid'} (f : SetoidHom A X) (g : SetoidHom B X) : Type := triple
+{
+  pullL : A;
+  pullR : B;
+  ok : f pullL == g pullR;
+}.
+
+Arguments triple {A B X f g} _ _ _.
+Arguments pullL  {A B X f g} _.
+Arguments pullR  {A B X f g} _.
+Arguments ok     {A B X f g} _.
+
+#[refine]
+#[export]
+Instance CoqSetoid_pullback
+  {A B X : Setoid'} (f : SetoidHom A X) (g : SetoidHom B X) : Setoid' :=
+{
+  carrier := CoqSetoid_pullback' f g;
+}.
+Proof.
+  unshelve esplit.
+  - refine (fun x y => pullL x == pullL y /\ pullR x == pullR y).
+  - split; red.
+    + easy.
+    + easy.
+    + now intros x y z [-> ->] [-> ->].
+Defined.
+
+#[refine]
+#[export]
+Instance CoqSetoid_pullL
+  {A B X : Setoid'} (f : SetoidHom A X) (g : SetoidHom B X)
+  : SetoidHom (CoqSetoid_pullback f g) A :=
+{
+  func := pullL
+}.
+Proof.
+  now intros x y [H _]; cbn.
+Defined.
+
+#[refine]
+#[export]
+Instance CoqSetoid_pullR
+  {A B X : Setoid'} (f : SetoidHom A X) (g : SetoidHom B X)
+  : SetoidHom (CoqSetoid_pullback f g) B :=
+{
+  func := pullR;
+}.
+Proof.
+  now intros x y [_ H]; cbn.
+Defined.
+
+#[refine]
+#[export]
+Instance CoqSetoid_triple
+  {A B X : Setoid'} (f : SetoidHom A X) (g : SetoidHom B X)
+  {Γ : Setoid'} (a : SetoidHom Γ A) (b : SetoidHom Γ B) (Heq : forall x : Γ, f (a x) == g (b x))
+  : SetoidHom Γ (CoqSetoid_pullback f g) :=
+{
+   func := fun x => triple (a x) (b x) (Heq x);
+}.
+Proof.
+  intros x y H; cbn.
+  now rewrite H.
+Defined.
+
+#[refine]
+#[export]
+Instance HasPullbacks_CoqSetoid : HasPullbacks CoqSetoid :=
+{
+  pullback := @CoqSetoid_pullback;
+  pullL := @CoqSetoid_pullL;
+  pullR := @CoqSetoid_pullR;
+  triple := @CoqSetoid_triple;
+}.
+Proof.
+  split; cbn.
+  - now apply ok.
+  - easy.
+  - easy.
+  - easy.
+Defined.

README.md

@@ -19,6 +19,7 @@
   - equalizers and coequalizers
   - pullbacks and pushouts
   - exponentials
+
   The definitions are quite far from what you can find in a typical textbook a- they are equational and stated in a way that strongly resembles the rules of type theory (formation, introduction, elimination, computation and uniqueness), but with the uniqueness rules being "symmetric".
 
   This is one of my greatest accomplishments — after changing, improving and correcting the definitions a gazillion times I'm starting to be pretty sure that they are correct and convenient. However, they're not perfect yet: there are issues with coherence conditions.

Universal/Equalizer.v

@@ -118,7 +118,7 @@ Proof.
   exists (factorize2 E1 equalize1 ok).
   repeat split.
   - exists (factorize1 E2 equalize2 ok).
-    now rewrite equiv_equalizer', equiv_equalizer', !comp_assoc, !factorize_equalize, !comp_id_l.
+    now rewrite !equiv_equalizer', !comp_assoc, !factorize_equalize, !comp_id_l.
   - now rewrite factorize_equalize.
   - now intros y [_ ?]; rewrite equiv_equalizer', factorize_equalize.
 Qed.
@@ -150,7 +150,8 @@ Qed.
 Lemma isEqualizer_equiv_factorize :
   forall
     (E : Ob C) (equalize : Hom E X)
-    (factorize1 factorize2 : forall (E' : Ob C) (e' : Hom E' X), e' .> f == e' .> g -> Hom E' E),
+    (factorize1 factorize2 :
+      forall (E' : Ob C) (e' : Hom E' X), e' .> f == e' .> g -> Hom E' E),
       isEqualizer C f g E equalize factorize1 ->
       isEqualizer C f g E equalize factorize2 ->
         forall (E' : Ob C) (e' : Hom E' X) (H : e' .> f == e' .> g),
@@ -187,6 +188,6 @@ Class HasEqualizers (C : Cat) : Type :=
       isEqualizer C f g (equalizer f g) (equalize f g) (@factorize _ _ f g)
 }.
 
-Arguments equalizer     [C _ X Y] _ _.
-Arguments equalize    [C _ X Y] _ _.
+Arguments equalizer [C _ X Y] _ _.
+Arguments equalize  [C _ X Y] _ _.
 Arguments factorize [C _ X Y f g E'] _ _.