From 1b97296cb4e043ed6ba8e200bcfc36bd60e602a9 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Mon, 27 Apr 2026 09:55:11 +0100
Subject: Move type theory into readme

---
 README.md | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 66 insertions(+), 1 deletion(-)

(limited to 'README.md')

diff --git a/README.md b/README.md
index 79b66c0..fafec00 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,71 @@
 # Makkai
 
-TODO
+A simple type theory.
+
+## Judgements
+- `C ctx` means `C` is a context.
+- `C ⊢ X set` means `X` is a set in context `C`.
+- `C ⊢ m : X` means `m` is a match of set `X`.
+- `C ⊢ S signature` means `S` is a signature in context `C`.
+- `C ⊢ I :: S` means `I` is an instance of signature `S`.
+
+Contexts are built by extension with either kind of binding:
+- `· ctx`.
+- `C, x : X` ctx, when `C ⊢ X set`.
+- `C, i :: S` ctx, when `C ⊢ S signature`.
+
+Everywhere below, `...` ranges over a finite (possibly zero) index, and the labels `xi`, `si`, `vi` are assumed distinct within any single list.
+
+## The set layer
+
+### Built-Ins
+For each `B ∈ { Nat, Int, Float, Str }`:
+- **Formation.** `C ⊢ B set`.
+- **Intro.** Literals of the appropriate form match the corresponding built-in (e.g. `C ⊢ 7 : Nat`).
+
+### Variables
+- `C ⊢ x : X` when `x : X` is in `C`.
+
+### Records
+- **Formation.** `C ⊢ record { .x0 : X0, ..., .xn : Xn } set` when `C ⊢ X0 set`, `C, x0 : X0 ⊢ X1 set`, ..., `C, x0 : X0, ..., xn-1 : Xn-1 ⊢ Xn set`.
+- **Intro.** `C ⊢ { .x0 = m0, ..., .xn = mn } : record { .x0 : X0, ..., .xn : Xn }` when `C ⊢ m0 : X0`, `C ⊢ m1 : X1[m0/x0]`, ..., `C ⊢ mn : Xn[m0/x0, ..., mn-1/xn-1]`.
+- **Elim.** `C ⊢ m.xi : Xi[m.x0/x0, ..., m.xi-1/xi-1]` when `C ⊢ m : record { .x0 : X0, ..., .xn : Xn }`.
+- **β.** `{ ..., .xi = mi, ... }.xi=mi`.
+- **η.** `m=record { .x0=m.x0, ..., .xn=m.xn }` when `m : record { ... }`.
+
+### Variants
+- **Formation.** `C ⊢ variant { v0. : X0 | ... | vn. : Xn } set` when each `C ⊢ Xi set`.
+- **Intro.** `C ⊢ vi.(m) : variant { v0. : X0 | ... | vn. : Xn }` when `C ⊢ m : Xi`.
+- **Elim.** `C ⊢ case m of { v0.x0 => n0 | ... | vn.xn => nn } : X` when `C ⊢ m : variant { v0. : X0 | ... | vn. : Xn }` and, for each `i`, `C, xi : Xi ⊢ ni : X`.
+- **β.** `case vi.(m) of { ... | vi.xi => ni | ... }=ni[m/xi]`.
+- **η.** `m=case m of { v0.x0 => v0.(x0) | ... | vn.xn => vn.(xn) }` when `m : variant { ... }`.
+
+## The signature layer
+
+### Theory
+- **Formation.** `C ⊢ theory { .s0 :: S0, ..., .sn :: Sn } signature` when `C ⊢ S0 signature`, `C, s0 :: S0 ⊢ S1 signature`, ..., `C, s0 :: S0, ..., sn-1 :: Sn-1 ⊢ Sn signature`.
+- **Intro.** `C ⊢ { .s0 = I0, ..., .sn = In } :: theory { .s0 :: S0, ..., .sn :: Sn }` when `C ⊢ I0 :: S0`, `C ⊢ I1 :: S1[I0/s0]`, ..., `C ⊢ In :: Sn[I0/s0, ..., In-1/sn-1]`.
+- **Elim.** `C ⊢ I.si :: Si[I.s0/s0, ..., I.si-1/si-1]` when `C ⊢ I :: theory { .s0 :: S0, ..., .sn :: Sn }`.
+- **β.** `{ ..., .si=Ii, ... }.si=Ii`.
+- **η.** `I={ .s0=I.s0, ..., .sn=I.sn }` when `I :: theory { ... }`.
+
+### Variables
+- `C ⊢ i :: S` when `i :: S` is in `C`.
+
+## The interface between signatures and sets
+
+### The signature `Set`
+- **Formation.** `C ⊢ Set signature`.
+- **Intro.** `C ⊢ X :: Set` when `C ⊢ X set`.
+- **Elim.** `C ⊢ set-of(I) set` when `C ⊢ I :: Set`.
+- **β.** `set-of(X)=X` when `X :: Set` arises from `C ⊢ X set`.
+- **η.** `I=set-of(I)` viewed as an instance, when `I :: Set`.
+
+### Extension signatures
+- **Formation.** `C ⊢ (x: X) -> S signature` when `C ⊢ X set` and `C, x : X ⊢ S signature`.
+- **Intro.** `C ⊢ for (y: X). I :: (x: X) -> S` when `C, y : X ⊢ I :: S[y/x]`.
+- **β.** `(for (x: X). I)(y)=I[y/x]`.
+- **η.** `I=for (x: X). I(x)` when x is not free in I.
 
 # License
 
-- 
cgit v1.3.1