Manual updates for current Coln

flake.nix

@@ -3,12 +3,17 @@
     nixpkgs.url = "github:NixOS/nixpkgs/nixos-26.05";
     flake-utils.url = "github:numtide/flake-utils";
     rust-overlay.url = "github:oxalica/rust-overlay";
+    bib2forester = {
+      url = "github:olynch/bib2forester";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
   };
   outputs =
     inputs@{
       self,
       nixpkgs,
       rust-overlay,
+      bib2forester,
       ...
     }:
     inputs.flake-utils.lib.eachSystem [ "x86_64-linux" ] (
@@ -171,6 +176,7 @@
         devShells.default = pkgs.mkShell {
           name = "coln";
           buildInputs = with pkgs; [
+            bib2forester.packages."${system}".default
             cabal-install
             cabal2nix
             coln-manual-dev

manual/templates/plain.tree

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

manual/theme/javascript-source/forester.js

@@ -10,7 +10,7 @@ function partition(array, isValid) {
 }
 
 window.addEventListener("load", (event) => {
- autoRenderMath(document.body)
+    autoRenderMath(document.body, { fleqn: true })
 
  const openAllDetailsAbove = elt => {
   while (elt != null) {

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/0028.tree

@@ -16,7 +16,7 @@
 
 \p{The reason type theory may be usefully applied to propositional logic because all of the connectives of propositional logic (and, or, not, forall, exists, etc.) satisfy universal properties; this is the same as the reason why type theory may be applied to any other area.}
 
-\p{The way that type theory may be applied to a particular area is via the development of \em{a particular} type theory. Confusion between type theory as a subject and the concept of \em{a type theory} as a mathematical object is an unfortunate side effect of the nomenclature, because “ breaks with the convention that in group theory, we study groups, in field theory we study fields, or in category theory we study categories.} 
+\p{The way that type theory may be applied to a particular area is via the development of \em{a particular} type theory. Confusion between type theory as a subject and the concept of \em{a type theory} as a mathematical object is an unfortunate side effect of the nomenclature, because the use of “type theory” to describe the field breaks with the convention that in group theory, we study groups, in field theory we study fields, or in category theory we study categories. However, in type theory, we study type theories.} 
 
 \p{A particular type theory is merely a syntactic formalization of some collection of universal properties, consisting of a collection of \em{rules} by which we judge that a certain piece of syntax is \em{well-typed}. The beauty of universal properties is that each universal property is quite self-contained, so a type theory may be designed by systematically observing which universal properties the objects of interest support, and then adding the standard type-theoretic rules for those universal properties to one's type theory.}
 

manual/trees/002A.tree

@@ -7,20 +7,10 @@
 
 \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{002N}
 
-\transclude{002E}
-
-\transclude{002F}
-
-\transclude{002D}
-
-\transclude{002G}
-
-\transclude{002I}
-
-\p{The remainder of this section is simply an investigation of what type formers are supported in #{\ms{ElTh}}.}
+\transclude{002S}
 
 \transclude{002J}

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/002J.tree

@@ -1 +1,6 @@
-\date{2026-05-27T09:54:56Z}
+\import{prelude}
+\title{Type formers}
+
+\p{One of the nice things about categorical semantics is that once we have fixed the basic structure (the category with families), the type theory essentially writes itself, in the sense that we may just look through various standard type formers and ask whether or not the semantics has the relevant universal property or not.}
+
+\transclude{002V}

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,15 @@
+\title{Types and terms}
+\import{prelude}
+
+\p{In this section, we build a [category with families](cwf) #{\mb{E}} out of elephant theories, which gives the semantics of types and terms in our type theory.}
+
+\p{Categories with families have many parts; we build up the structure in sections. We follow [Kovacs](kovacs-2022-typetheoretic) in presenting a category with families as a model of a GAT. As we give the semantics for each part of the GAT, we write out the relevant part of the signature with a \check next to it to signify that that part of the GAT is defined.}
+
+\transclude{002O}
+
+\transclude{002P}
+
+\transclude{002Q}
+
+\transclude{002R}
+

manual/trees/002O.tree

@@ -0,0 +1,13 @@
+\import{prelude}
+\title{Category structure of #{\mb{E}}}
+
+\p{The category for #{\mb{E}} is just the category of [elephant theories](002C), where the morphisms are 2-natural transformations.}
+
+##{\begin{align*}
+&\ms{Con} \colon \ms{Type} \quad \check \\
+&\ms{Sub} \colon \ms{Con} \to \ms{Con} \to \ms{Type} \quad \check
+\end{align*}}
+
+\p{We omit some parts of the GAT signature; for instance here we omit the parts which declare that #{\ms{Con}} and #{\ms{Sub}} form a category. We refer to this category overall as #{\bb{C}_{\mb{E}}}.}
+
+\p{This category has a terminal object given by the functor constant at #{1}, the terminal category; we refer to this by #{\cdot} in light of its role as the empty context.}

manual/trees/002P.tree

@@ -0,0 +1,14 @@
+\import{prelude}
+\title{Types in #{\mb{E}}}
+
+\p{Given a context #{\Gamma}, a type in #{\Gamma} is a 2-functor #{A \colon \left(\groth \Gamma\right)\op \to \ms{CAT}}.}
+
+##{\ms{Ty} \colon \ms{Con} \to \ms{Type} \quad \check}
+
+\p{Note that #{\ms{Ty}\,\cdot} is again just the type of elephant theories.}
+
+\p{In general, #{\groth \Gamma} is the 2-category of topoi equipped with a model of #{\Gamma}. In the case that #{\Gamma} is a geometric theory, this is equivalent to elephant theories where #{\ms{BTop}/\ms{S}} is replaced with the #{\ms{BTop}/\ms{S}[\Gamma]}, where #{\ms{S}[\Gamma]} is the classifying topos for #{\Gamma}. Thus, #{\ms{Ty}\,\Gamma} can be thought of as the collection of elephant theories relative to #{\Gamma}.}
+
+\p{It is not hard to see that #{\ms{Ty}} forms a presheaf over #{\bb{C}_{\mb{E}}} because we can apply the Grothendieck construction to the 2-natural transformation #{\gamma \colon \Delta \To \Gamma} to get #{\groth \gamma \colon \groth \Delta \to \groth \Gamma}, and then precomposition with #{\groth \gamma} gives us the required map from #{\ms{Ty}\,\Gamma} to #{\ms{Ty}\,\Delta}.}
+
+##{{-}[-] \colon \{\Delta\;\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to (\ms{Sub}\,\Delta\,\Gamma) \to \ms{Ty}\,\Delta \quad \check}

manual/trees/002Q.tree

@@ -0,0 +1,19 @@
+\import{prelude}
+\title{Terms in #{\mb{E}}}
+
+\p{Given a context #{\Gamma} and a type #{A \colon \left(\groth \Gamma\right)\op \to \ms{CAT}}, a term #{a} of type #{A} is a 2-section of #{A}.}
+
+##{\ms{Tm} \colon (\Gamma \colon \ms{Con}) \to \ms{Ty}\,\Gamma \to \ms{Type} \quad \check}
+
+\p{The categorical way to define “2-section” would be as a strict 2-functor #{a \colon \groth \Gamma \to \groth A} that is a strict section of the projection. A more type-theoretic way to define “2-section” would be to say a 2-section is a map #{a \colon \left((\mc{E},M) \colon \groth \Gamma\right) \to A(\mc{E},M)} such that #{a(\mc{E},M)} is 2-functorial in #{\mc{E}} and #{M}.}
+
+\p{Given #{\gamma \colon \Delta \To \Gamma}, we may define #{a[\gamma] \colon \ms{Tm}\,\Delta\,(A[\gamma])} by}
+
+##{a[\gamma]\,\left((\mc{E}, M) \colon \groth \Delta \right) = a(\mc{E}, \gamma_{\mc{E}}(M)) \colon ({A[\gamma]}(\mc{E}, M) = A(\mc{E}, \gamma_{\mc{E}}(M)))}
+
+\p{This turns #{\ms{Tm}} into an indexed presheaf over #{\ms{Ty}}.}
+
+##{\begin{align*}
+  &{-}[-] \colon \{\Delta\;\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \\
+  &\quad \ms{Tm}\,\Gamma\,A \to (\gamma \colon \Delta \To \Gamma) \to \ms{Tm}\,\Delta\,(A[\gamma]) \quad \check
+\end{align*}}

manual/trees/002R.tree

@@ -0,0 +1,28 @@
+\import{prelude}
+\title{Context extension in #{\mb{E}}}
+
+\p{Given a context #{\Gamma} and type #{A}, we define the context extension #{\Gamma \ext A} by}
+
+##{(\Gamma \ext A)(\mc{E} \colon \ms{BTop}/\mc{S}) = (M \colon \Gamma(\mc{E})) \times A(\mc{E},M)}
+
+\p{extended suitably to produce a category, and to be 2-functorial.}
+
+##{{-}\ext{-} \colon (\Gamma \colon \ms{Con}) \to \ms{Ty}\,\Gamma \to \ms{Con} \quad \check}
+
+\p{We then have the weakening substitution given by first projection and the variable rule given by second projection.}
+
+##{\begin{align*}
+&\ms{p} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to (\Gamma \ext A \To \Gamma) \quad \check \\
+&\ms{q} \colon \{\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \ms{Tm}\,(\Gamma \ext A)\,(A[\ms{p}]) \quad \check
+\end{align*}}
+
+\p{Finally, context comprehension is defined by pairing.}
+
+##{\begin{align*}
+  &({-},{-}) \colon \{\Delta\;\Gamma \colon \ms{Con}\} \to \{A \colon \ms{Ty}\,\Gamma\} \to \\
+  &\quad (\gamma \colon \Delta \To \Gamma) \to \ms{Tm}\,\Delta\,(A[\gamma]) \to (\Delta \To \Gamma \ext A) \quad \check
+\end{align*}}
+
+\p{Weakening/variable and context comprehension then can be used to form an isomorphism:}
+
+##{(\Delta \Rightarrow \Gamma \ext A) \cong (\gamma \colon \Delta \Rightarrow \Gamma) \times \ms{Tm}\,\Delta\,(A[\gamma]) \quad \check}

manual/trees/002S.tree

@@ -0,0 +1,12 @@
+\title{Levels and universes}
+\import{prelude}
+
+\p{The basic structure of types and terms works for general elephant theories, but we are most concerned with geometric theories. To handle this, we introduce judgments inspired by the approach to levels and universes introduced by Jon Sterling in [[sterling-2025-fuss-free]].}
+
+\p{Note that Jon uses this for levels in MLTT, where the type theory “at each level” is essentially the same. However, in our use of levels, different rules in the type theory will only apply at certain levels.}
+
+\transclude{002U}
+
+\transclude{002T}
+
+\transclude{002W}

manual/trees/002T.tree

@@ -0,0 +1,16 @@
+\title{Geometric theories}
+\import{prelude}
+
+\p{We introduce a judgment on types capturing when an elephant theory is a geometric theory. Confusingly enough, in Coln we call these types \defcase{theories}; general types (elephant theories) are called top-level types.}
+
+##{\ms{IsTheory} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop}}
+
+\p{A proof of #{\ms{IsTheory}\,A} is a construction of #{A} as a sequence of simple functional and simple equational extensions of the object classifier, establishing it as a [geometric theory](002D). As #{\ms{IsTheory}\,A} is a proposition, we propositionally truncate the type of such constructions.}
+
+##{\ms{IsTheory} \colon \{\Gamma \colon \ms{Con}\} \to \ms{Ty}\,\Gamma \to \ms{Prop} \quad \check}
+
+\p{We can then internalize this into a universe. The universe #{\ms{Theory} \colon \ms{Ty}\,\cdot} sends a topos #{\mc{E}} to the category of geometric theories #{A \colon \ms{BTop}/\mc{E} \to \ms{CAT}}.}
+
+##{\ms{Tm}\,\Gamma\,\ms{Theory} \cong (A \colon \ms{Ty}\,\Gamma) \times \ms{IsTheory}\,A \quad \check}
+
+\p{This is the shakiest part of the semantics for this type theory; it may be that non-strictness or size issues make this universe infeasible. However, this can be fixed by moving to a two-level type theory. “Presheaves over elephant theories” seems a bit absurd though, so hopefully this can work out as is.}