Renamed CoqSet to SET, CoqSetoid to SETOID and CatCat to CAT.

Author: wkolowski

Cat.v

@@ -684,7 +684,7 @@ Defined.
 
 (** ** The category of setoids *)
 
-(** [CoqSetoid] corresponds to what most category theory textbooks call Set,
+(** [SETOID] corresponds to what most category theory textbooks call Set,
     the category of sets and functions.
 
     We need to use setoids instead of sets, because our categories have a
@@ -785,7 +785,7 @@ Proof. now setoid. Defined.
 
 #[refine]
 #[global]
-Instance CoqSetoid : Cat :=
+Instance SETOID : Cat :=
 {|
   Ob := Setoid';
   Hom := SetoidHom;
@@ -952,7 +952,7 @@ Defined.
 
 #[refine]
 #[export]
-Instance HomFunctor (C : Cat) (X : Ob C) : Functor C CoqSetoid :=
+Instance HomFunctor (C : Cat) (X : Ob C) : Functor C SETOID :=
 {
   fob := fun Y : Ob C => {| carrier := Hom X Y; setoid := HomSetoid X Y |}
 }.
@@ -991,7 +991,7 @@ Defined.
 
 #[refine]
 #[export]
-Instance HomContravariant (C : Cat) (X : Ob C) : Contravariant C CoqSetoid :=
+Instance HomContravariant (C : Cat) (X : Ob C) : Contravariant C SETOID :=
 {
   coob := fun Y : Ob C => {| carrier := Hom Y X; setoid := HomSetoid Y X |}
 }.
@@ -1157,7 +1157,7 @@ Defined.
 
 #[refine]
 #[export]
-Instance HomProfunctor (C : Cat) : Profunctor C C CoqSetoid :=
+Instance HomProfunctor (C : Cat) : Profunctor C C SETOID :=
 {
   diob := fun X Y : Ob C => {| carrier := Hom X Y; setoid := HomSetoid X Y |};
 }.
@@ -1371,8 +1371,8 @@ Proof.
   now exists (component β X).
 Qed.
 
-Definition representable {C : Cat} (X : Ob C) (F : Functor C CoqSetoid) : Type :=
+Definition representable {C : Cat} (X : Ob C) (F : Functor C SETOID) : Type :=
   {α : NatTrans F (HomFunctor C X) & natural_isomorphism α}.
 
-Definition corepresentable {C : Cat} (X : Ob C) (F : Functor (Dual C) CoqSetoid) : Type :=
+Definition corepresentable {C : Cat} (X : Ob C) (F : Functor (Dual C) SETOID) : Type :=
   {α : NatTrans F (HomFunctor (Dual C) X) & natural_isomorphism α}.

Category/Enriched.v

@@ -1,7 +1,7 @@
 From Cat Require Import Cat.
 From Cat.Category Require Import CartesianClosed Monoidal.
 From Cat.Universal Require Import Initial Terminal Product Coproduct.
-From Cat Require Import Instances.Setoids.
+From Cat Require Import Instances.SETOID.
 
 Class Enriched (V : Monoidal) : Type :=
 {
@@ -23,10 +23,10 @@ Class Enriched (V : Monoidal) : Type :=
 
 #[refine]
 #[export]
-Instance Enriched_CoqSetoid
-  : Enriched (Monoidal_HasTerm_HasProducts HasTerm_CoqSetoid HasProducts_CoqSetoid) :=
+Instance Enriched_SETOID
+  : Enriched (Monoidal_HasTerm_HasProducts HasTerm_SETOID HasProducts_SETOID) :=
 {
-  EOb := Ob CoqSetoid;
+  EOb := Ob SETOID;
   EHom := fun X Y =>
   {|
     carrier := @Hom _ X Y;

Instances/AbGrp.v

@@ -1,6 +1,6 @@
 From Cat Require Export Cat.
 From Cat.Universal Require Import Initial Terminal Zero Product Coproduct.
-From Cat.Instances Require Import Setoids Mon CMon Grp.
+From Cat.Instances Require Import SETOID Mon CMon Grp.
 
 Set Implicit Arguments.
 

Instances/CatCat.v renamed to Instances/CAT.v

@@ -1,6 +1,6 @@
 From Cat Require Export Cat.
 From Cat.Universal Require Import Initial Terminal Product Coproduct.
-From Cat Require Export Instances.Setoids.
+From Cat Require Export Instances.SETOID.
 
 Set Implicit Arguments.
 

Instances/Graph.v

@@ -1,6 +1,6 @@
 From Cat Require Export Cat.
 From Cat.Universal Require Import Initial Terminal Zero Product Coproduct.
-From Cat.Instances Require Import Setoids Mon.
+From Cat.Instances Require Import SETOID Mon.
 
 Set Implicit Arguments.
 

Instances/Grp.v

@@ -98,7 +98,7 @@ Proof. now lin. Defined.
 #[export]
 Instance Lin_Pros_product (X Y : Lin) : Pros :=
 {
-  carrier := CoqSetoid_product X Y;
+  carrier := SETOID_product X Y;
   leq := fun p1 p2 : X * Y =>
     fst p1 ≤ fst p2 /\ ~ fst p1 == fst p2
       \/
@@ -140,7 +140,7 @@ Defined.
 #[export]
 Instance Lin_Pros_coproduct (X Y : Lin) : Pros :=
 {
-  carrier := CoqSetoid_coproduct X Y;
+  carrier := SETOID_coproduct X Y;
   leq := fun p1 p2 : X + Y =>
     match p1, p2 with
     | inl x, inl x' => leq x x'

Instances/Lin.v

@@ -454,7 +454,7 @@ Defined.
 
 #[refine]
 #[export]
-Instance forgetful : Functor MonCat CoqSetoid :=
+Instance forgetful : Functor MonCat SETOID :=
 {
   fob := fun X : Mon => @setoid (sgr X);
   fmap := fun (A B : Mon) (f : Hom A B) => f;
@@ -468,7 +468,7 @@ Defined.
 Notation "'U'" := forgetful.
 
 Definition free_monoid
-  (X : Ob CoqSetoid) (M : Mon) (p : Hom X (fob U M)) : Prop :=
+  (X : Ob SETOID) (M : Mon) (p : Hom X (fob U M)) : Prop :=
     forall (N : Mon) (q : SetoidHom X (fob U N)),
       exists!! h : MonHom M N, q == p .> fmap U h.
 
@@ -494,7 +494,7 @@ Proof.
   all: now cbn; intros; lia.
 Defined.
 
-Definition MonListUnit_p : SetoidHom CoqSetoid_term MonListUnit.
+Definition MonListUnit_p : SetoidHom SETOID_term MonListUnit.
 Proof.
   exists (fun _ => 1).
   now proper.
@@ -503,10 +503,10 @@ Defined.
 Set Nested Proofs Allowed.
 
 Lemma free_monoid_MonListUnit :
-  @free_monoid CoqSetoid_term MonListUnit MonListUnit_p.
+  @free_monoid SETOID_term MonListUnit MonListUnit_p.
 Proof.
   unfold free_monoid. intros.
-  Definition f1 (N : Mon) (q : SetoidHom CoqSetoid_term (fob U N))
+  Definition f1 (N : Mon) (q : SetoidHom SETOID_term (fob U N))
     : SetoidHom MonListUnit N.
   Proof.
     exists (fix f (n : nat) : N :=
@@ -516,15 +516,15 @@ Proof.
       end).
     now proper; subst.
   Defined.
-  Definition f2 (N : Mon) (q : SetoidHom CoqSetoid_term (fob U N))
+  Definition f2 (N : Mon) (q : SetoidHom SETOID_term (fob U N))
     : SgrHom MonListUnit N.
   Proof.
     exists (f1 N q).
     induction x as [| x']; intros.
     - now cbn; rewrite neutr_l.
     - now cbn; rewrite <- assoc, -> IHx'.
   Defined.
-  Definition f3 (N : Mon) (q : SetoidHom CoqSetoid_term (fob U N))
+  Definition f3 (N : Mon) (q : SetoidHom SETOID_term (fob U N))
     : MonHom MonListUnit N.
   Proof.
     now exists (f2 N q).

Instances/Mon.v

@@ -1,6 +1,6 @@
 From Cat Require Export Cat.
 From Cat.Universal Require Export Initial Terminal Product Coproduct.
-From Cat Require Export Instances.Setoids.
+From Cat Require Export Instances.SETOID.
 
 Set Implicit Arguments.
 
@@ -123,14 +123,14 @@ Abort.
 #[export]
 Instance Pros_init : Pros :=
 {
-  carrier := CoqSetoid_init;
+  carrier := SETOID_init;
   leq := fun (x y : Empty_set) => match x with end
 }.
 Proof. all: easy. Defined.
 
 Definition Pros_create (X : Pros) : ProsHom Pros_init X.
 Proof.
-  now exists (CoqSetoid_create X).
+  now exists (SETOID_create X).
 Defined.
 
 #[refine]
@@ -155,14 +155,14 @@ Defined.
 #[export]
 Instance Pros_term : Pros :=
 {
-  carrier := CoqSetoid_term;
+  carrier := SETOID_term;
   leq := fun _ _ => True
 }.
 Proof. all: easy. Defined.
 
 Definition Pros_delete (X : Pros) : ProsHom X Pros_term.
 Proof.
-  now exists (CoqSetoid_delete X).
+  now exists (SETOID_delete X).
 Defined.
 
 #[refine]
@@ -178,7 +178,7 @@ Proof. easy. Defined.
 #[export]
 Instance Pros_product (X Y : Pros) : Pros :=
 {
-  carrier := CoqSetoid_product X Y;
+  carrier := SETOID_product X Y;
   leq := fun x y : X * Y => leq (fst x) (fst y) /\ leq (snd x) (snd y)
 }.
 Proof.
@@ -190,18 +190,18 @@ Defined.
 
 Definition Pros_outl (X Y : Pros) : ProsHom (Pros_product X Y) X.
 Proof.
-  now exists (CoqSetoid_outl X Y); cbn.
+  now exists (SETOID_outl X Y); cbn.
 Defined.
 
 Definition Pros_outr (X Y : Pros) : ProsHom (Pros_product X Y) Y.
 Proof.
-  now exists (CoqSetoid_outr X Y); cbn.
+  now exists (SETOID_outr X Y); cbn.
 Defined.
 
 Definition Pros_fpair
   {A B X : Pros} (f : ProsHom X A) (g : ProsHom X B) : ProsHom X (Pros_product A B).
 Proof.
-  exists (CoqSetoid_fpair f g).
+  exists (SETOID_fpair f g).
   now pros.
 Defined.
 
@@ -225,7 +225,7 @@ Defined.
 #[export]
 Instance Pros_coproduct (X Y : Pros) : Pros :=
 {
-  carrier := CoqSetoid_coproduct X Y;
+  carrier := SETOID_coproduct X Y;
   leq := fun a b : X + Y =>
     match a, b with
     | inl x, inl x' => x ≤ x'
@@ -242,18 +242,18 @@ Defined.
 
 Definition Pros_finl (X Y : Pros) : ProsHom X (Pros_coproduct X Y).
 Proof.
-  now exists (CoqSetoid_finl X Y).
+  now exists (SETOID_finl X Y).
 Defined.
 
 Definition Pros_finr (X Y : Pros) : ProsHom Y (Pros_coproduct X Y).
 Proof.
-  now exists (CoqSetoid_finr X Y).
+  now exists (SETOID_finr X Y).
 Defined.
 
 Definition Pros_copair
   (A B X : Pros) (f : ProsHom A X) (g : ProsHom B X) : ProsHom (Pros_coproduct A B) X.
 Proof.
-  exists (CoqSetoid_copair f g).
+  exists (SETOID_copair f g).
   now intros [] []; pros.
 Defined.
 

Instances/Pros.v

@@ -1,6 +1,6 @@
 From Cat Require Export Cat.
 From Cat.Universal Require Import Initial Terminal Zero Product Coproduct.
-From Cat Require Export Instances.Setoids.
+From Cat Require Export Instances.SETOID.
 
 Class SetoidRel (X Y : Setoid') : Type :=
 {
@@ -81,7 +81,7 @@ Proof. all: now rel. Defined.
 #[export]
 Program Instance HasInit_SetoidRel : HasInit SetoidRelCat :=
 {
-  init := CoqSetoid_init;
+  init := SETOID_init;
   create := fun X : Setoid' => {| rel := fun (e : Empty_set) _ => match e with end |}
 }.
 Next Obligation. easy. Defined.
@@ -90,7 +90,7 @@ Next Obligation. easy. Defined.
 #[export]
 Program Instance HasTerm_SetoidRel : HasTerm SetoidRelCat :=
 {
-  term := CoqSetoid_init;
+  term := SETOID_init;
   delete := fun X : Setoid' => {| rel := fun _ (e : Empty_set) => match e with end |}
 }.
 Next Obligation. easy. Defined.