# Makkai

A simple type theory.

## Motivation

There's a pleasant story here about categorical semantics in `Alg(Fam(Lex))^op`, but the real impetus for developing and implementing this particular fragment was the exercise: i had never implemented a dependent type theory before, and wanted to know whether i could deduce how to do so by trying. You, the reader, may be the judge of those efforts.

As a consequence, this code is 100% artisanal, hand-crafted, guaranteed-cruft-and-hacks human written (by me).

Credit goes to [David Jaz](https://www.davidjaz.com/) for developing the fragment and its semantics. Credit goes to me for introducing errors.

## Rust implementation

Usage `makkai [--debug] file1.makkai ... fileN.makkai`

See the [grammar](grammar.txt) for details, and the examples in `examples/`.

Note: the checker does not presently support η-equivalence in all cases and so has some known errors, and likely therefore, some unknown errors.

## 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 an element 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.

#### Instances via case analysis
A construction admitting an instance of any signature, given an element of a variant set and a branch for every tag.
- **Intro.** `C ⊢ case m of [ v0. x0 => I0 | ... | vn. xn => In ] :: S` when `C ⊢ S signature`, `C ⊢ m : variant [ v0. : X0 | ... | vn. : Xn ]`, and, for each `i`, `C, xi : Xi ⊢ Ii :: S`.
- **β.** `case vi. m of [ ... | vi. xi => Ii | ... ]=Ii[m/xi]`.

#### Lifted sets
- **Formation.** `C ⊢ <X> signature` when `C ⊢ X set`.
- **Intro.** `C ⊢ <m> :: <X>` when `C ⊢ m : X`.
- **Elim.** `C ⊢ element-of(I) : X` when `C ⊢ I :: <X>`.
- **β.** `element-of(<m>)=m` when `m : X`.
- **η.** `I=<element-of(I)>` when `I :: <X>`.

### Notes

There are no formal large eliminators, and as such we cannot perform case analysis on an element and produce varying set or signatures. However, the former construction may be losslessly encoded by detouring through instances-via-case-analysis and the signature `Set`. That is, `set-of(case m of [ ... | vi. xi => Xi :: Set | ... ])` is a set that varies depending on an element.

The signatures `Set` and `<_>` each give a full isomorphism between the corresponding set-layer and signature-layer notion (sets ~ instances of `Set`; elements of `X` ~ instances of `<X>`), via `set-of`/`element-of` respectively. These are parallel in some sense, and do not interact.

# License

Copyright tslil clingman 2026, this programme is free software and is made available under the terms of the GPL v3 or later. See LICENSE for details.