Change the name of files in Cat

Changes the name files in Cat, e.g., Cat_Initial -> Initial. This is more standard compared to the rest of the development.
amintimany · Apr 29, 2016 · 51b97bd · 51b97bd
1 parent 463eed5
commit 51b97bd
Show file tree

Hide file tree

Showing 15 changed files with 27 additions and 25 deletions.
diff --git a/Adjunction/AFT/Commas_Complete/Commas_Equalizer.v b/Adjunction/AFT/Commas_Complete/Commas_Equalizer.v
@@ -16,7 +16,7 @@ Require Import
         Basic_Cons.Limits
 .
 Require Import Archetypal.Discr.Discr.
-Require Import Cat.Cat_Terminal.
+Require Import Cat.Terminal.
 
 (** We show that if C is a complete category and G : C –≻ D preserves limits,
 then every comma category (Comma (Func_From_SingletonCat x) G) for (x : D) has

diff --git a/Adjunction/AFT/Commas_Complete/Commas_GenProd.v b/Adjunction/AFT/Commas_Complete/Commas_GenProd.v
@@ -16,7 +16,7 @@ Require Import
         Basic_Cons.Limits
 .
 Require Import Archetypal.Discr.Discr.
-Require Import Cat.Cat_Terminal.
+Require Import Cat.Terminal.
 
 (** We show that if C is a complete category and G : C –≻ D preserves limits,
 then every comma category (Comma (Func_From_SingletonCat x) G) for (x : D) has

diff --git a/Adjunction/Adj_Facts.v b/Adjunction/Adj_Facts.v
@@ -2,12 +2,14 @@ Require Import Essentials.Notations.
 Require Import Essentials.Types.
 Require Import Essentials.Facts_Tactics.
 Require Import Category.Main.
-Require Import Ext_Cons.Prod_Cat.Prod_Cat Ext_Cons.Prod_Cat.Nat_Facts Ext_Cons.Prod_Cat.Operations.
+Require Import Ext_Cons.Prod_Cat.Prod_Cat Ext_Cons.Prod_Cat.Nat_Facts
+        Ext_Cons.Prod_Cat.Operations.
 Require Import Functor.Main.
-Require Import Functor.Representable.Hom_Func Functor.Representable.Hom_Func_Prop.
+Require Import Functor.Representable.Hom_Func
+        Functor.Representable.Hom_Func_Prop.
 Require Import NatTrans.Main.
 Require Import Adjunction.Adjunction Adjunction.Duality.
-Require Import Cat.Cat Cat.Cat_Exponential Cat.Cat_Exponential_Facts.
+Require Import Cat.Cat Cat.Exponential Cat.Exponential_Facts.
 Require Import Yoneda.Yoneda.
 Require Import Functor.Functor_Extender.
 

diff --git a/Basic_Cons/Limits.v b/Basic_Cons/Limits.v
@@ -5,7 +5,7 @@ Require Import Category.Main.
 Require Import Functor.Main.
 Require Import Limits.Limit.
 Require Import Archetypal.Discr.Discr.
-Require Import Cat.Cat_Terminal.
+Require Import Cat.Terminal.
 Require Import
         Basic_Cons.Terminal
         Basic_Cons.Product

diff --git a/Cat/Cat_CCC.v → Cat/CCC.v b/Cat/Cat_CCC.v → Cat/CCC.v
@@ -4,9 +4,9 @@ Require Import Basic_Cons.CCC.
 
 Require Export Cat.Cat.
 
-Require Export Cat.Cat_Terminal.
-Require Export Cat.Cat_Product.
-Require Export Cat.Cat_Exponential.
+Require Export Cat.Terminal.
+Require Export Cat.Product.
+Require Export Cat.Exponential.
 
 Program Instance Cat_CCC : CCC Cat.
 

diff --git a/Cat/Cat_Exponential.v → Cat/Exponential.v b/Cat/Cat_Exponential.v → Cat/Exponential.v
@@ -8,7 +8,7 @@ Require Import Ext_Cons.Prod_Cat.Prod_Cat Ext_Cons.Prod_Cat.Operations.
 Require Import Basic_Cons.Product.
 Require Import Basic_Cons.Exponential.
 Require Import NatTrans.NatTrans NatTrans.Func_Cat.
-Require Import Cat.Cat_Product.
+Require Import Cat.Product.
 
 (** The exponential in cat is jsut the functor category. *)
 

diff --git a/Cat/Cat_Exponential_Facts.v → Cat/Exponential_Facts.v b/Cat/Cat_Exponential_Facts.v → Cat/Exponential_Facts.v
@@ -8,7 +8,7 @@ Require Import Ext_Cons.Prod_Cat.Prod_Cat Ext_Cons.Prod_Cat.Operations.
 Require Import Basic_Cons.Product.
 Require Import Basic_Cons.Exponential.
 Require Import NatTrans.NatTrans NatTrans.Func_Cat NatTrans.NatIso.
-Require Import Cat.Cat_Product Cat.Cat_Exponential.
+Require Import Cat.Product Cat.Exponential.
 
 (** Facts about exponentials in Cat. *)
 

diff --git a/Cat/Facts.v b/Cat/Facts.v
@@ -1,5 +1,5 @@
-Require Export Cat_Initial.
-Require Export Cat_Terminal.
-Require Export Cat_Product.
-Require Export Cat_Exponential.
-Require Export Cat_CCC.
+Require Export Cat.Initial.
+Require Export Cat.Terminal.
+Require Export Cat.Product.
+Require Export Cat.Exponential.
+Require Export Cat.CCC.
diff --git a/Cat/Cat_Initial.v → Cat/Initial.v b/Cat/Cat_Initial.v → Cat/Initial.v
diff --git a/Cat/Cat_Product.v → Cat/Product.v b/Cat/Cat_Product.v → Cat/Product.v
diff --git a/Cat/Cat_Terminal.v → Cat/Terminal.v b/Cat/Cat_Terminal.v → Cat/Terminal.v
diff --git a/Limits/Isomorphic_Cat.v b/Limits/Isomorphic_Cat.v
@@ -3,7 +3,7 @@ Require Import Essentials.Types.
 Require Import Essentials.Facts_Tactics.
 Require Import Category.Main.
 Require Import Functor.Main.
-Require Import Cat.Cat Cat.Cat_Terminal.
+Require Import Cat.Cat Cat.Terminal.
 Require Import Limits.Limit.
 Require Import KanExt.LocalFacts.From_Iso_Cat.
 Require Import Cat.Cat_Iso.

diff --git a/Limits/Limit.v b/Limits/Limit.v
@@ -9,7 +9,7 @@ Require Import Coq_Cats.Type_Cat.Card_Restriction.
 Require Export NatTrans.NatTrans NatTrans.Operations.
 Require Export KanExt.Local KanExt.Global KanExt.GlobalDuality
         KanExt.GlobaltoLocal KanExt.LocaltoGlobal KanExt.LocalFacts.Main.
-Require Export Cat.Cat_Terminal.
+Require Export Cat.Terminal.
 
 Local Open Scope functor_scope.
 

diff --git a/Limits/Pointwise.v b/Limits/Pointwise.v
@@ -11,7 +11,7 @@ Require Import KanExt.Pointwise.
 Require Import Ext_Cons.Prod_Cat.Prod_Cat Ext_Cons.Prod_Cat.Operations.
 Require Import Coq_Cats.Type_Cat.Type_Cat.
 Require Import NatTrans.Main.
-Require Import Cat.Cat_Terminal.
+Require Import Cat.Terminal.
 Require Import Functor.Representable.Representable.
 
 Local Open Scope functor_scope.

diff --git a/_CoqProject b/_CoqProject
@@ -80,12 +80,12 @@ Algebras/Main.v
 
 #Cat:
 Cat/Cat.v
-Cat/Cat_Initial.v
-Cat/Cat_Terminal.v
-Cat/Cat_Product.v
-Cat/Cat_Exponential.v
-Cat/Cat_Exponential_Facts.v
-Cat/Cat_CCC.v
+Cat/Initial.v
+Cat/Terminal.v
+Cat/Product.v
+Cat/Exponential.v
+Cat/Exponential_Facts.v
+Cat/CCC.v
 Cat/Facts.v
 Cat/Cat_Iso.v