Manual updates for current Coln

manual/templates/plain.tree

@@ -0,0 +1 @@
+\import{prelude}

manual/theme/style.css

@@ -85,10 +85,15 @@ h6 {
   margin-bottom: 0;
 }
 
-h5,
-h6,
 p {
   margin-top: 0;
+  margin-bottom: 0;
+}
+
+section.block > details {
+  > :not(:first-child)+* {
+    margin-top: 1rem;
+  }
 }
 
 h1,
@@ -263,6 +268,12 @@ section .block[data-taxon] details>summary>header>h1 {
   font-size: 12pt;
 }
 
+section .block[data-taxon] {
+    border-left-style: solid;
+    border-width: 2px;
+    border-radius: 0px;
+}
+
 span.taxon {
   color: #444;
   font-weight: bolder;
@@ -298,7 +309,8 @@ section.block>details {
 
 
 section.block>details[open] {
-  margin-bottom: 1em;
+    /* border-right: 1px; */
+  margin-bottom: 0;
 }
 
 

manual/trees/0001.tree

@@ -1,7 +1,5 @@
 \title{Coln manual}
 
-\p{Coln is a database with an expressive language for schemas, queries, and migrations. This document forms the manual for Coln.}
-
 \transclude{002H}
 \transclude{0002}
 \transclude{000K}

manual/trees/002A.tree

@@ -7,17 +7,9 @@
 
 \p{Following the principles of this manual, this is \em{not} a mathematical paper; there will be a more formal account of this type theory, but that is in progress. Rather, this is a conceptual account that makes reference to mathematics.}
 
-\p{In [The Elephant](johnstone-2002-sketches), Johnstone makes the following definitions for “theory”; we call this an \em{elephant theory} in order to distinguish it from other notions of theory we might consider.}
+\transclude{002M}
 
-\transclude{002C}
-
-\transclude{002E}
-
-\transclude{002F}
-
-\transclude{002D}
-
-\transclude{002G}
+\transclude{002N}
 
 \transclude{002I}
 

manual/trees/002D.tree

@@ -2,14 +2,6 @@
 \taxon{Definition}
 \import{prelude}
 
-\p{\defcase{Geometric theories} may be consicely defined as the elephant theories built up via a sequence of [product-inserter-equifier limits](pie-limit) starting from the object classifier.}
-
-\p{We expand this to give more intuition.}
-
-\p{If #{T} is a theory, a \defcase{simple functional extension} of #{T} is another theory #{T'} given as the \em{inserter} of two geometric constructs #{F,G \colon T \to \bb{O}}. Intuitively, #{T'} is the theory given by freely adding a new morphism between the “objects” #{F} and #{G}.}
-
-\p{If #{T} is a theory, a \defcase{simple equational extension} of #{T} is another theory #{T'} given as the \em{equifier} of two indexed natural transformations #{\alpha, \beta \colon F \Rightarrow G}, where #{F} and #{G} are geometric constructs. Intuitively, #{T'} is the theory given by adding a new equality between morphisms of “objects”.}
-
-\p{A \defcase{geometric theory} is a theory built up by a finite sequence #{T_0,\ldots,T_n} of simple functional extensions and simple equational extensions starting from #{T_0 = \bb{O}^m} for some finite #{m}.}
+\p{A \defcase{geometric theory} is an elephant theory built up by a finite sequence #{T_0,\ldots,T_n} of [simple functional extensions](002K) and [simple equational extensions](002L) starting from #{T_0 = \bb{O}^m} for some finite #{m}.}
 
 \p{(See [Elephant](johnstone-2002-sketches) Definition 4.2.7, note that Johnstone gives a slightly different definition, using \em{simple geometric quotients} in place of simple equational extensions, which use inverters instead of equifiers. The name “simple equational extension” is not known to us to be previously used, but it follows the schema of “simple functional extension.”)}

manual/trees/002I.tree

@@ -6,10 +6,10 @@
 
 \p{Intuitively, #{\ms{Ty}(\Gamma)} is “elephant theories relative to #{\Gamma}.” This is because #{\groth \Gamma} is the category of topoi equipped with a model of #{\Gamma}; if #{\Gamma} were a geometric theory then #{\groth \Gamma} would be equivalent to #{\ms{BTop}/\mc{S}[\Gamma]}.}
 
-\p{Then define #{\ms{Tm} \colon (\groth \ms{Ty})\op \to \ms{Set}} by letting #{\ms{Tm}(\Gamma, A)} be the set of \em{sections} of #{A}. A section #{a} is a natural assignment of #{a(\mc{E}, M) \colon A(\mc{E}, M)} for #{(\mc{E},M) \in \groth \Gamma}.}
+\p{Then define #{\ms{Tm} \colon (\groth \ms{Ty})\op \to \ms{SET}} by letting #{\ms{Tm}(\Gamma, A)} be the set of \em{sections} of #{A}. A section #{a} is a natural assignment of #{a(\mc{E}, M) \colon A(\mc{E}, M)} for #{(\mc{E},M) \in \groth \Gamma}.}
 
 \p{Context extension is given in the following way. Suppose that #{\Gamma \colon (\ms{BTop}/\mc{S})\op \to \ms{Cat}} is a context and #{A \colon \ms{Ty}(\Gamma)}. Then #{\Gamma \ext A \colon (\ms{BTop}/\mc{S})\op \to \ms{Cat}} is defined by #{(\Gamma \ext A)(\mc{E}) = (M \colon \Gamma(\mc{E})) \times A(\mc{E},M)}.}
 
-\p{Then finally we have weakening and the variable rule given by the first and second projections out of #{\Gamma \ext A}.}
+\p{Weakening and the variable rule are by the first and second projections out of #{\Gamma \ext A}.}
 
 \p{Note that even though topoi and elephant theories are non-trivially 2-categorical, #{(\ms{ElTh},\ms{Ty},\ms{Tm})} forms nevertheless a strict (albeit quite large) category with families.}

manual/trees/002K.tree

@@ -0,0 +1,5 @@
+\title{Simple functional extension}
+\taxon{Definition}
+\import{prelude}
+
+\p{If #{T} is a theory, a \defcase{simple functional extension} of #{T} is another theory #{T'} given as the \em{inserter} of two geometric constructs #{F,G \colon T \to \bb{O}}. Intuitively, #{T'} is the theory given by freely adding a new morphism between the “objects” #{F} and #{G}.}

manual/trees/002L.tree

@@ -0,0 +1,5 @@
+\title{Simple equational extension}
+\import{prelude}
+\taxon{Definition}
+
+\p{If #{T} is a theory, a \defcase{simple equational extension} of #{T} is another theory #{T'} given as the \em{equifier} of two indexed natural transformations #{\alpha, \beta \colon F \Rightarrow G}, where #{F} and #{G} are geometric constructs. Intuitively, #{T'} is the theory given by adding a new equality between morphisms of “objects”.}

manual/trees/002M.tree

@@ -0,0 +1,17 @@
+\title{A refresher on geometric theories}
+
+\p{In this section, we briefly review the approach to geometric theories followed in [The Elephant](johnstone-2002-sketches).}
+
+\transclude{002C}
+
+\transclude{002E}
+
+\transclude{002F}
+
+\transclude{002K}
+
+\transclude{002L}
+
+\transclude{002D}
+
+\transclude{002G}

manual/trees/002N.tree

@@ -0,0 +1 @@
+\title{The basic judgments of geometric type theory}