Documentation

variable

\[ \frac {\Gamma (x) = \tau} {\color{darkblue}\Gamma \vdash \color{darkgreen}x \Rightarrow \color{darkred}\tau} \;\mathrm{V{\scriptstyle AR}} \]

annotated term

\[\frac {\color{darkblue}\Gamma \vdash \color{darkgreen}\rho \Leftarrow \color{darkred}{\sigma} \qquad \rho \leadsto \tau} {\color{darkblue}\Gamma \vdash \color{darkgreen}{x : \rho} \Rightarrow \color{darkred}\tau } \;\mathrm{A{\scriptstyle NN}} \]

dependent function space

\[\frac {\color{darkblue}\Gamma \vdash \color{darkgreen}{\rho} \Rightarrow \color{darkred}s \qquad \rho \leadsto \tau \qquad \color{darkblue}{\Gamma, x : \tau} \vdash \color{darkgreen}{\rho'} \Rightarrow \color{darkred}{s'} \qquad (s,s',s'') \in \mathcal{R} } {\color{darkblue}\Gamma \vdash \color{darkgreen}{\prod (x : \rho) \to \rho'} \Rightarrow \color{darkred}{s''} } \;\mathsf{Pi} \]

application

\[\frac {\color{darkblue}\Gamma \vdash \color{darkgreen}{e} \Rightarrow \color{darkred}{\prod (x : \tau) \to \tau'} \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}{e'} \Leftarrow \color{darkred}\tau \qquad \tau'[x \mapsto e'] \leadsto \tau'' } {\color{darkblue}\Gamma \vdash \color{darkgreen}{e\, e'} \Rightarrow \color{darkred}{\tau''} } \;\mathrm{A{\scriptstyle PP}} \]

sort

\[\frac {s : s' \in \mathcal{A}} {\color{darkblue}\Gamma \vdash \color{darkgreen}s \Rightarrow \color{darkred}{s'} } \;\mathrm{A{\scriptstyle XIOM}} \]

Dependent pair

\[\frac {\color{darkblue}\Gamma \vdash \color{darkgreen}{\rho} \Rightarrow \color{darkred}s \qquad \rho \leadsto \tau \qquad \color{darkblue}{\Gamma, x : \tau} \vdash \color{darkgreen}{\rho'} \Rightarrow \color{darkred}{s'} \qquad (s,s',s'') \in \mathcal{R} } {\color{darkblue}\Gamma \vdash \color{darkgreen}{\sum (x : \rho) \to \rho'} \Rightarrow \color{darkred}{s''} } \;\mathsf{Sigma} \]

Propositional equality

\[\frac {\color{darkblue}\Gamma \vdash \color{darkgreen}{\rho} \Rightarrow \color{darkred}{s} \qquad \rho \leadsto \tau \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}{x} \Leftarrow \color{darkred}{\tau} \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}{y} \Leftarrow \color{darkred}{\tau} } {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{Eq}\;\rho\;x\;y} \Rightarrow \color{darkred}{s} } \;\mathsf{Eq} \]

J-rule. Propositional equality elimination.

\[\frac {\array{ \color{darkblue}\Gamma \vdash \color{darkgreen}{a} \Rightarrow \color{darkred}{s} \qquad s \in \mathcal{S} \cr \color{darkblue}{\Gamma, x : A, y : A, z : \mathsf{Eq}\,a\,x\,y} \vdash \color{darkgreen}{P} \Rightarrow \color{darkred}{s'} \qquad s' \in \mathcal{S} \cr \color{darkblue}{\Gamma, q : A} \vdash \color{darkgreen}{r} \Leftarrow \color{darkred}{P [ x \mapsto q; y \mapsto q; z \mapsto \mathsf{refl}]} \cr \color{darkblue}{\Gamma} \vdash \color{darkgreen}{u} \Leftarrow \color{darkred}{a} \qquad \color{darkblue}{\Gamma} \vdash \color{darkgreen}{v} \Leftarrow \color{darkred}{a} \qquad \color{darkblue}{\Gamma} \vdash \color{darkgreen}{w} \Leftarrow \color{darkred}{\mathsf{Eq}\,A\,u\,v} }} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{J}\;a\;(\lambda\,x\,y\,z \to c)\;(\lambda\,q \to r)\;u\,v\,w} \Rightarrow \color{darkred}{P [ x \mapsto u; y \mapsto v; z \mapsto w]} } \;\mathsf{J} \]

Tautology.

\[\frac {} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\top} \Rightarrow \color{darkred}\star} \]

Tautology witness.

\[\frac {} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{I}} \Rightarrow \color{darkred}\top} \]

Contradiction.

\[\frac {} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\bot} \Rightarrow \color{darkred}\star} \]

Booleans

\[\frac {} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathbb{B}} \Rightarrow \color{darkred}\star } \]

True.

\[\frac {} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{True}} \Rightarrow \color{darkred}{\mathbb{B}} } \]

False.

\[\frac {} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{False}} \Rightarrow \color{darkred}{\mathbb{B}} } \]

Boolean elimination.

Note: \(\mathbb{B}\mathsf{-elim}\) is universe-polymorphic.

\[ \frac {\array{ \color{darkblue}{\Gamma, x : \mathbb{B}} \vdash \color{darkgreen}P \Rightarrow \color{darkred}{s} \qquad (\star, s, s') \in \mathcal{R} \cr P[x \mapsto \mathsf{True}] \leadsto \tau \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}t \Leftarrow \color{darkred}{\tau} \cr P[x \mapsto \mathsf{False}] \leadsto \tau' \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}f \Leftarrow \color{darkred}{\tau'} \cr \color{darkblue}\Gamma \vdash \color{darkgreen}b \Leftarrow \color{darkred}{\mathbb{B}} \qquad P[x \mapsto b] \leadsto \sigma }} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathbb{B}\mathsf{-elim}\,(\lambda\, x \to P) \,t\,f\,b} \Rightarrow \color{darkred}{\sigma} } \]

Boolean conjunction, and.

\[ \frac {\array{ \color{darkblue}\Gamma \vdash \color{darkgreen}x \Leftarrow \color{darkred}{\mathbb{B}} \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}y \Leftarrow \color{darkred}{\mathbb{B}} }} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathbb{B}\mathsf{-and}\,x\,y} \Rightarrow \color{darkred}{\mathbb{B}} } \]

Natural numbers.

\[\frac {\star \in \mathcal{S}} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathbb{N}} \Rightarrow \color{darkred}\star } \]

Zero.

\[\frac {} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{Zero}} \Rightarrow \color{darkred}{\mathbb{N}} } \]

Successor

\[\frac {\color{darkbluw}\Gamma \vdash \color{darkgreen}{n} \Leftarrow \color{darkred}{\mathbb{N}} } {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{Succ}\,n} \Rightarrow \color{darkred}{\mathbb{N}} } \]

Natural numbers elimination.

Here we have to assume the target sort (or parametrise further!).

\[ \frac {\array{ \color{darkblue}{\Gamma, x : \mathbb{N}} \vdash \color{darkgreen}P \Leftarrow \color{darkred}{s} \qquad (\star, s, s') \in \mathcal{R} \cr P[x \mapsto \mathsf{Zero}] \leadsto \tau \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}z \Leftarrow \color{darkred}{\tau} \cr \prod (l : \mathbb{N}) \to P[x \mapsto l] \to P[x \mapsto \mathsf{Succ}\,l] \leadsto \tau' \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}s \Leftarrow \color{darkred}{\tau'} \cr \color{darkblue}\Gamma \vdash \color{darkgreen}n \Leftarrow \color{darkred}{\mathbb{N}} \qquad P[x \mapsto n] \leadsto \sigma }} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathbb{N}\mathsf{-elim}\,(\lambda\, x \to p)\,z\,s\,n} \Rightarrow \color{darkred}{\sigma} } \]

Natural number addition, plus.

\[ \frac {\array{ \color{darkblue}\Gamma \vdash \color{darkgreen}x \Leftarrow \color{darkred}{\mathbb{N}} \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}y \Leftarrow \color{darkred}{\mathbb{N}} }} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathbb{N}\mathsf{-plus}\,x\,y} \Rightarrow \color{darkred}{\mathbb{N}} } \]

Natural number addition, times.

\[ \frac {\array{ \color{darkblue}\Gamma \vdash \color{darkgreen}x \Leftarrow \color{darkred}{\mathbb{N}} \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}y \Leftarrow \color{darkred}{\mathbb{N}} }} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathbb{N}\mathsf{-times}\,x\,y} \Rightarrow \color{darkred}{\mathbb{N}} } \]

Hadron type.

In physics, quarks combine to form composite particles called hadrons. In our type system(s) quark combine to form types. Hadrons are finite sets (enumerations).

We call single quark hadrons atoms. This is not true in physics, but we do get lisp-like atoms this way; i.e. things which are equal to itself only. But we agree with modern physics: atoms are not indivisible.

\[\frac {\star \in \mathcal{S}} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\{\overline{:\!\!q}\}} \Rightarrow \color{darkred}\star } \]

Quark elimination.

The rule is not the same as in PiSigma label (which influenced quark design). There the rule is checkable, but we have to provide a motive.

Note: here we infer the type of hadron from the match clauses. That way we get exhautivity check.

The real reason for the quark name is because \(\mathbb{Q}\) is better supported in fonts, than e.g. \(\mathbb{L}\).

\[ \frac {\array{ \color{darkblue}{\Gamma, x : \{\overline{:\!\!q}\}} \vdash \color{darkgreen}P \Rightarrow \color{darkred}{s} \qquad (\star, s, s') \in \mathcal{R} \cr P[x \mapsto :\!\!q_i] \leadsto \tau_i \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}{u_i} \Leftarrow \color{darkred}{\tau_i} \cr \color{darkblue}\Gamma \vdash \color{darkgreen}t \Leftarrow \color{darkred}{\{\overline{:\!\!q}\}} \qquad P[x \mapsto t] \leadsto \sigma }} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathbb{Q}\mathsf{-elim}\,(\lambda\, x \to P)\;\{\overline{:\!\!q \longrightarrow u}\}\;t} \Rightarrow \color{darkred}{\sigma} } \]

Inferrable terms

\[\frac {\color{darkblue}\Gamma \vdash \color{darkgreen}x \Rightarrow \color{darkred}{\tau'} \qquad \tau \equiv \tau' } {\color{darkblue}\Gamma \vdash \color{darkgreen}x \Leftarrow \color{darkred}\tau } \;\mathrm{C{\scriptstyle HK}} \]

Lambda abstraction

\[\frac {\color{darkblue}{\Gamma, x : \tau} \vdash \color{darkgreen}{e} \Leftarrow \color{darkred}{\tau'}} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\lambda\, x \to e} \Leftarrow \color{darkred}{\prod (x : \tau) \to \tau'}} \;\mathrm{L{\scriptstyle AM}} \]

Dependent pair

\[\frac {\color{darkblue}\Gamma \vdash \color{darkgreen}{x} \Leftarrow \color{darkred}{\tau} \qquad \color{darkblue}\Gamma \vdash \color{darkgreen}{y} \Leftarrow \color{darkred}{\tau' [ x \mapsto \tau} ] } {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{pair}\;x\;y} \Leftarrow \color{darkred}{\sum (x : \tau) \to \tau'}} \]

Dependent pattern match

match p (x y -> b) ~ (x y -> b) (fst p) (snd p)

\[\frac { \color{darkblue}\Gamma \vdash \color{darkgreen}p \Rightarrow \color{darkred}{\sum (z : \tau) \to \tau'} \qquad \color{darkblue}{\Gamma, x : \tau, y : \tau' [z \mapsto x]} \vdash b \Leftarrow \color{darkred}{\tau''} } {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{match}\;p\;(\lambda\, x\, y \to b)} \Leftarrow \color{darkred}{\tau''}} \]

Witness or propositional equality

\[\frac {x \equiv y} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{refl}} \Leftarrow \color{darkred}{\mathsf{Eq}\;\tau\;x\;y}} \]

Ex falso quodlibet.

\[\frac {\color{darkblue}\Gamma \vdash \color{darkgreen}{x} \Leftarrow \color{darkred}\bot} {\color{darkblue}\Gamma \vdash \color{darkgreen}{\mathsf{absurd}\;x} \Leftarrow \color{darkred}{\tau}} \]

Single quark.

Compare to Booleans: TermTrue and TermFalse. Here we don't know the type of hadron a quark belongs to, we must check it; On the other hand, Boolean literals are inferrable.

Quarks are prefixed with a colon, to syntatically distinguish them.

\[\frac {:\!\!x \in \overline{:\!\!q}} {\color{darkblue}\Gamma \vdash \color{darkgreen}{:\!\!x} \Leftarrow \color{darkred}{\{\overline{:\!\!q}\}} } \]