View on GitHub

Andromeda 1

Type theory with equality reflection

$\newcommand{\G}{\Gamma}$ $\newcommand{\D}{\Delta}$ $\newcommand{\tyA}{A}$ $\newcommand{\tyB}{B}$ $\newcommand{\x}{x}$ $\newcommand{\y}{y}$ $\newcommand{\z}{z}$ $\newcommand{\e}{e}$ $\newcommand{\bnf}{\ \mathrel{ {\colon}{\colon}{=}}\ }$ $\newcommand{\bnfor}{\ \mid\ \ }$ $\newcommand{\ctxempty}{\bullet}$ $\newcommand{\ctxextend}[3]{#1,\, #2\, {\colon}\, #3}$ $\newcommand{\Type}{\mathsf{Type}} % The type of all types$ $\newcommand{\Prod}[2]{\mathop{\textstyle\prod_{(#1 {\colon} #2)}}}$ $\newcommand{\lam}[3]{\lambda #1 {\colon} #2.{#3}\,.\,}$ $\newcommand{\app}[5]{#1\mathbin{@^{#2{\colon}#3.#4}} #5}$ $\newcommand{\abst}[2]{[#1 \,.\, #2]}$ $\newcommand{\ascribe}[2]{#1 \,{\colon}\, #2}$ $\newcommand{\JuEqual}[3]{\mathsf{Eq}_{ #1 }( #2, #3 )}$ $\newcommand{\juRefl}[1]{\mathsf{refl}_{#1}\ }$ $\newcommand{\isctx}[1]{#1\ \mathsf{ctx}}$ $\newcommand{\istype}[2]{\isterm{#1}{#2}{\Type}}$ $\newcommand{\isterm}[3]{#1 \vdash\,#2\,:\,#3}$ $\newcommand{\eqctx}[2]{#1 \equiv_{\mathsf{ctx}} #2}$ $\newcommand{\eqtype}[3]{\eqterm{#1}{#2}{#3}{\Type}}$ $\newcommand{\eqterm}[4]{#1 \vdash #2 \equiv #3 : #4}$ $\newcommand{\infer}[2]{\frac{\displaystyle #1}{\displaystyle #2}}$ $\newcommand{\subst}[3]{#1[#3/#2]}$

Type theory with equality reflection

We give here the rules of type theory that is implemented in Andromeda. The rules are simplified with respect to the implementation in the following ways:

  1. In Andromeda each subexpression carries an explicit set of variables on which it depends. We call these assumptions tags. This is necessary to recover the strengthening rule (because of equality reflection it may happen that the well-formedness of a term relies on an assumption which is not recorded in the term).

  2. The typing context is not a list but rather a directed graph whose vertices are the context entries and whose edges are dependencies between context entries (they edges are recoverable from the assumption tags).

  3. The actual rules implemented by the nucleus perform a context join. This is best illustrated with an example. The introduction rule for equality types ty-eq is here stated as

    but is implemented as

    where the join $\G \bowtie \D$ is computed as the union of (directed graphs representing) context $\G$ and $\D$. The join operation may fail if there is a variable appears in $\G$ and $\D$ with different types.

    TODO: Explain precisely how the context joins work and what properties they have.

Unlike in traditional type theory the terms are explicitly tagged with typing information. For instance, a $\lambda$-abstraction is tagged with both the doman and the codomain.

Syntax

Terms $\e$ and types $\tyA$, $\tyB$:

$\Type$ universe
$\Prod{x}{\tyA} \tyB$ product
$\JuEqual{\tyA}{\e_1}{\e_2}$ equality type
$\x$ variable
$\lam{\x}{\tyA}{\tyB} \e$ $\lambda$-abstraction
$\app{\e_1}{\x}{\tyA}{\tyB}{\e_2}$ application
$\juRefl{\tyA} \e$ reflexivity

Contexts $\G$:

$\ctxempty$ empty context
$\ctxextend{\G}{\x}{\tyA}$ context $\G$ extended with $\x : \tyA$

Judgments

$\isctx{\G}$ $\G$ is a well formed context
$\isterm{\G}{\e}{\tyA}$ $\e$ is a well formed term of type $\tyA$ in context $\G$
$\eqterm{\G}{\e_1}{\e_2}{\tyA}$ $e_1$ and $e_2$ are equal terms of type $\tyA$ in context
$\eqctx{\G}{\D}$ $\G$ and $\D$ are equal contexts

Judgment: $\isctx{\G}$

ctx-empty
ctx-extend

Here $\mathsf{dom}(\G)$ is the set of all variables that are declared in $\G$, i.e.:

Judgment: $\eqctx{\G}{\D}$

eq-ctx-empty
eq-ctx-extend
ctx-term-conv
ctx-eq-conv

Judgment: $\isterm{\G}{\e}{\tyA}$

General rules

term-conv
term-var

Universe

ty-type

Products

ty-prod
term-abs
term-app

Equality type

ty-eq
term-refl

Equality

General rules

eq-refl
eq-sym
eq-trans
eq-conv

Remark: in the presence of eq-reflection (see below) the rules eq-conv, eq-sym and eq-trans are derivable using term-conv and congruence rules.

Computations

prod-beta

Reflection and extensionality

eq-reflection
eq-ext
prod-ext

Congruences

Type formers
congr-prod
congr-eq
Products
congr-lambda
congr-apply
Equality types
congr-refl

TODO: Substitution.