diff --git a/manual/templates/plain.tree b/manual/templates/plain.tree new file mode 100644 index 00000000..a29ce570 --- /dev/null +++ b/manual/templates/plain.tree @@ -0,0 +1 @@ +\import{prelude} diff --git a/manual/theme/style.css b/manual/theme/style.css index a2d4c4e3..8b818807 100644 --- a/manual/theme/style.css +++ b/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; } diff --git a/manual/trees/0001.tree b/manual/trees/0001.tree index 38184706..520c6463 100644 --- a/manual/trees/0001.tree +++ b/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} diff --git a/manual/trees/002A.tree b/manual/trees/002A.tree index ed3c99ba..4f361d28 100644 --- a/manual/trees/002A.tree +++ b/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} diff --git a/manual/trees/002D.tree b/manual/trees/002D.tree index 573fc285..40798388 100644 --- a/manual/trees/002D.tree +++ b/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.”)} diff --git a/manual/trees/002I.tree b/manual/trees/002I.tree index 52503dc9..5cda7e57 100644 --- a/manual/trees/002I.tree +++ b/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.} diff --git a/manual/trees/002K.tree b/manual/trees/002K.tree new file mode 100644 index 00000000..ee89c2f7 --- /dev/null +++ b/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}.} diff --git a/manual/trees/002L.tree b/manual/trees/002L.tree new file mode 100644 index 00000000..fd8a811c --- /dev/null +++ b/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”.} diff --git a/manual/trees/002M.tree b/manual/trees/002M.tree new file mode 100644 index 00000000..d6d861ee --- /dev/null +++ b/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} diff --git a/manual/trees/002N.tree b/manual/trees/002N.tree new file mode 100644 index 00000000..d7b77e2f --- /dev/null +++ b/manual/trees/002N.tree @@ -0,0 +1 @@ +\title{The basic judgments of geometric type theory}