Refactor scopes

docs/src/api.md

@@ -11,7 +11,7 @@ Modules = [
   GATlab.Syntax,
   GATlab.Syntax.Scopes,
   GATlab.Syntax.GATs,
-  GATlab.Syntax.Presentations,
+  GATlab.Syntax.GATContexts,
   GATlab.Syntax.ExprInterop,
   GATlab.Syntax.TheoryInterface,
 ]

docs/src/concepts/theories.md

@@ -2,33 +2,8 @@
 
 A theory in GATlab consists of two parts.
 
-1. A Julia value of type `Theory` that describes the theory.
+1. A Julia value of type `GAT` that describes the theory.
 2. A module named by the theory with various Julia types that give us handles
 for metaprogramming.
 
-These metaprogramming types include:
 
-- A singleton struct named `Th` and subtyping `AbstractTheory` that has an
-   overload of `gettheory` on it returning the Julia value from 1. This is used
-   to pass around the entire theory at the type level.
-- A singleton struct for each type constructor and term constructor in the
-   theory. These are used in place of `Lvl` in types, so that backtraces are
-   more readable.
-
-Example:
-
-```julia
-module Category
-using GATlab.Theories
-
-struct Th <: AbstractTheory end
-
-Theories.gettheory(::Th) = ...
-
-struct Ob <: TypCon{1} end
-struct Hom <: TypCon{2} end
-
-struct compose <: TrmCon{3} end
-...
-end
-```

docs/src/stdlib.md

@@ -5,7 +5,7 @@
 Our friend `ThCategory` is the main theory in this module.
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThCategory
+GATlab.Stdlib.StdTheories.ThCategory
 ```
 
 You can specialize a theory by adding more axioms. In this case we can specialize the theory of categories to that of thin category by adding the axiom that two morphisms are equal if they have the same domain and codomain.
@@ -15,33 +15,30 @@ thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThThinCategory
+GATlab.Stdlib.StdTheories.ThThinCategory
 ```
 ### Category Building Blocks
 The remaining theories in this module are not necessarily useful, but go to show demonstrate the theory hierarchy can be built up in small increments.
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThClass
+GATlab.Stdlib.StdTheories.ThClass
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThLawlessCat
+GATlab.Stdlib.StdTheories.ThLawlessCat
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThAscCat
+GATlab.Stdlib.StdTheories.ThAscCat
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThIdLawlessCat
+GATlab.Stdlib.StdTheories.ThIdLawlessCat
 ```
 
 ```@autodocs
 Modules = [GATlab.Stdlib,
   GATlab.Stdlib.StdTheories,
-  GATlab.Stdlib.StdTheories.Algebra,
-  GATlab.Stdlib.StdTheories.Monoidal,
-  GATlab.Stdlib.StdTheories.Naturals,
   GATlab.Stdlib.StdModels,
   GATlab.Stdlib.StdModels.FinSets,
   ]