# Abstract

## 1. History of Type Systems

The history of Type Theory take its root MLTT paper ^{1}.
The the Type Theory was fixed with Id types, W, Nat, List types were added ^{2}.
The type checker of single axiom system with Pi types only was given in CoC paper ^{3}.

**[1]**. P.Martin-Löf. An Intuitionistic Theory of Types, 1972.
**[2]**. P.Martin-Löf. Intuitionistic Type Theory, 1984.
**[3]**. T.Coquand. The Calculus of Constructions, 1988.
**[4]**. T.Streicher. The Groupoid Interpretation of Type Theory, 1996.
**[5]**. H.Barendregt. Lambda Calculus With Types, 2010.
**[6]**. S.Awodey et all. Homotopy Type Theory, 2014.
**[7]**. A.Mortberg. Cubical Type Theory, 2017.

Then Voevodsky presented HTS without a computational semantics of univalence axiom. This later was fixed by Mortberg et all in cubicaltt.

## Cubical Syntax

The 10 lines BNF declares syntax that covers: 1) MLTT as pi, sigma and path types; 2) inductive types case analisys; and 3) simple module system. This system is enough to encode core cubical base library.

```
0 := #empty
brs := 0 + cobrs
app := exp exp
id := [ #nat ]
ids := [ id ]
codec := def dec
dec := 0 + codec
```

```
imp := [ import id ]
tele := 0 + cotele
cotele := ( exp : exp ) tele
sum := 0 + id tele + id tele | sum
br := ids -> exp
mod := module id where imp def
cobrs := | br brs
```

```
def := data id tele = sum + id tele : exp = exp + id tele : exp where def
exp := cotele * exp + cotele -> exp + exp -> exp + app + ( exp ) + id +
split cobrs + exp.1 + exp.2 + \ cotele -> exp
```

## Infinity Language

The idea of Infinity Langauge is a unified layered type checker. We select 5 levels of type checker awareness from pure type systems up to homotopy calculus.

```
data lang
= PTS (_: pts)
| SIGMA (_: exists)
| ID (_: identity)
| INDUCTION (_: ind)
| HTS (_: hts)
```

## Dependent Type Theory

```
data pts
= star (n: nat)
| var (x: name) (l: nat)
| pi (x: name) (l: nat) (d c: lang)
| lambda (x: name) (l: nat) (d c: lang)
| app (f a: lang)
```

```
data exists
= sigma (n: name) (a b: lang)
| pair (a b: lang)
| fst (p: lang)
| snd (p: lang)
```

The categorical methods for lambda calculus and category theory in general could be found in the following works:

**[11]**. S.MacLane. Categories for the Working Mathematician.
**[12]**. W.Lawvere. Conceptual Mathematics, 1997.
**[13]**. B.Jacobs. Fibrations with indeterminates, 1994.
**[14]**. P.Curien. Category theory: a programming language-oriented introduction, 2008.

## Contextual Categories

Categories with Families is a categorical semantics of dependent type theory that nowadays formulated as cubical sets or as presheaf model of type theory.

**[20]**. P.Dybjer. The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories -- an Intuitionistic Perspective.
**[21]**. P.Clairambault. From Categories with Families to Locally Cartesian Closed Categories.
**[22]**. P.Dybjer. On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory.
**[23]**. R.A.G.Seely. Locally cartesian closed categories and type theory.
**[24]**. M.Hofmann. Revisiting the categorical interpretation of dependent type theory.
**[25]**. S.Castellan. Dependent type theory as the initial category with families.
**[26]**. P.Dybjer. Internal Type Theory.
**[27]**. V.Voevodsky. A C-system defined by a universe category.

## Identity Types

```
data identity
= id (a b: lang)
| idpair (a b: lang)
| idelim (a b c d e: lang)
```

**[30]**. E.Bishop. Foundations of Constructive Analysis, 1967.
**[31]**. B.Nordström. Programming in Martin-Löf’s Type Theory.
**[32]**. B.Jacobs. Structural induction and coinduction in a fibrational setting, 1997.
**[33]**. G.Barthe, V.Capretta. Setoids in type theory, 2003.
**[34]**. M.Sozeau. Internalizing Intensional Type Theory, 2013.
**[35]**. V.Voevodsky. Identity types in the C-systems defined by a universe category, 2015.
**[36]**. L.de Moura. Congruence Closure in Intensional Type Theory, 2016.

## Inductive Types

The further development of induction^{5} inside MLTT provers led
to the theory of polynomial functors and well-founded trees^{4},
known in programming languages as inductive types with data
and record core primitives of type checker. In fact recursive inductive
types^{3} could be encoded in PTS using non-recursive representation
Berarducci^{1} or Categorical^{6} encoding.

```
data tele (A: U) = emp | tel (n: name) (b: A) (t: tele A)
data branch (A: U) = br (n: name) (args: list name) (term: A)
data label (A: U) = lab (n: name) (t: tele A)
data ind
= data_ (n: name) (t: tele lang) (labels: list (label lang))
| case (n: name) (t: lang) (branches: list (branch lang))
| ctor (n: name) (args: list lang)
```

The non-well-founded trees or infinite coinductive trees^{6,8}
are useful for modeling infinite process running which is part
of Milner's Pi-calculus. Coinductive streams are part of any MLTT base library.

**[40]**. A.Berarducci. Automatic Synthesis of Typed Lambda-Programs, 1985.
**[41]**. F.Pfenning. Inductively defined types in the CoC, 1989.
**[42]**. P.Wadler. Recursive types for free, 1990.
**[43]**. N.Gambino. Wellfounded Trees and Dependent Polynomial Functors, 1995.
**[44]**. P.Dybjer. Inductive Famalies, 1997.
**[45]**. B.Jacobs. (Co)Algebras and (Co)Induction, 1997.
**[46]**. V.Vene. Categorical programming with (co)inductive types.
**[47]**. H.Geuvers. Dependent (Co)Inductive Types are Fibrational Dialgebras, 2015.

## Higher Inductive Types

The fundamental development of equality inside MLTT
provers led us to the notion of ∞-groupoid^{2} as spaces.
In this was Path identity type appeared in the core
of type checker along with de Morgan algebra on
built-in interval type. Glue, unglue composition
and fill operations are also needed in the core
for the univalence computability^{8}.

```
data hts
= path (a b: lang)
| path_lam (n: name) (a b: lang)
| path_app (f: name) (a b: lang)
| comp_ (a b: lang)
| fill_ (a b c: lang)
| glue_ (a b c: lang)
| glue_elem (a b: lang)
| unglue_elem (a b: lang)
```

**[50]**. T.Streicher. A groupoid model refutes UIP, 1994.
**[51]**. B.Jacobs. Categorical Logic and Type Theory, 1999.
**[52]**. S.Awodey. Homotopy Type Theory and Univalent Foundations, 2013.
**[53]**. S.Huber. A Cubical Type Theory, 2015.
**[54]**. A.Joyal. What is an elementary higher topos, 2014.
**[55]**. M.Shulman. Univalent Categories and the Rezk Completion, 2014.
**[56]**. A.Mortberg. Cubical Type Theory: a constructive univalence axiom, 2017.

## Universes

The universe system is completely described by the PTS SAR notation, given by Barendregt. Find more info in Axioms and Inference Rules of underlying Om intermediate language.

```
PTS : U
= (S: (n: nat) -> star n)
(A: (i: nat) -> type i (succ i))
(R: (i j: nat) -> pi i j (max i j)) * unit
```