# Article

## Introduction

The idea of Infinity Langauge came from the needs of unification and arranging different calculuses as extensions to the core of the language with dependent types (or MLTT core). While been working on distributed systems, data storages and stream processing, the core two languages: pi-calculus and stream calculus discovered to be connected and being driven by a language with quantifiers as primitives. So we started to look forward to a unified type checker.

## Layered Core

## Pure Type System

From the time Coquand at all discovered Calculus of Constructions^{6},
and Barendregt^{7} systemized its variations, a Pure Type System
theory was developed. It is known also as Single Axiom System
with only Pi-Type of MLTT^{2}, representing Functional Completeness^{3}.

`data O`_{1} = U : nat → O_{1}
| Var: Ident → O_{1}
| App: O_{1} → O_{1} → O_{1}
| Lambda: Binder → O_{1} → O_{1} → O_{1}
| Arrow: O_{1} → O_{1} → O_{1}
| Pi: name → O_{1} → O_{1} → O_{1}

1. S.MacLane. Categories for the Working Mathematician

2. P.Martin-Löf. An Intuitionistic Theory of Types. 1972

3. B.Jacobs. Fibrations with indeterminates. 1994

4. W.Lawvere. Conceptual Mathematics. 1997

5. P.Curien. Category theory: a programming language-oriented introduction. 2008

6. T.Coquand. The Calculus of Constructions. 1988

7. H.Barendregt. Lambda Calculus With Types. 2010

## Contextual Completness

The basic Core primitive which is needed for proving things is MLTT Sigma-Type, representing Contextual Completeness. This is needed for building Sigma pairs which are curried records. Usually, type checkers called Pi-Sigma provers as it contains PTS enriched with Sigma primitive.

`data O`_{2} = O_{1}
| Sigma: name → O_{2} → O_{2} → O_{2}
| Pair: O_{2} → O_{2} → O_{2}
| Fst: O_{2} → O_{2}
| Snd: O_{2} → O_{2}

## Identity Types

`data O`_{3} = O_{2}
| Id: O_{3} → O_{3} → O_{3}
| IdPair: O_{3} → O_{3} → O_{3}
| IdJ: O_{3} → O_{3} → O_{3} → O_{3} → O_{3} → O_{3}

1. E.Bishop. Foundations of Constructive Analysis. 1967

2. T.Streicher, M.Hofmann. The groupoid interpretation of type theory. 1996

3. G.Barthe, V.Capretta. Setoids in type theory. 2003

4. M.Sozeau. Internalizing Intensional Type Theory 2013

5. V.Voevodsky. Identity types in the C-systems defined by a universe category. 2015

6. D.Selsam,L.de Moura. Congruence Closure in Intensional Type Theory. 2016

## (Co)-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) = empty | tel: name → A → tele A
data branch (A: U) = br: name → list name → A
data label (A: U) = lab: name → tele A
data O
```_{4} = O_{3}
| Sum: name → tele → list (label O_{4})
| Split: name → list (branch O_{4})
| Ctor: name → list O_{4}

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.

1. A.Berarducci. Automatic Synthesis of Typed Lambda-Programs. 1985

2. F.Pfenning. Inductively defined types in the CoC. 1989

3. P.Wadler. Recursive types for free. 1990

4. N.Gambino. Wellfounded Trees and Dependent Polynomial Functors. 1995

5. P.Dybjer. Inductive Famalies. 1997

6. B.Jacobs. (Co)Algebras and (Co)Induction. 1997

7. V.Vene. Categorical programming with (co)inductive types

8. 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^{7}.

`data O`_{5} = O_{4}
| Path: O_{5} → O_{5} → O_{4}
| PathLam: Binder → O_{5} → O_{5} → O_{5}
| PathApp: O_{5} → Formula → O_{5} → O_{5}
| Comp: O_{5} → O_{5} → O_{5}
| Fill: O_{5} → O_{5} → O_{5}
| Glue: O_{5} → O_{5} → O_{5}
| GlueElem: O_{5} → O_{5} → O_{5}
| UnGlueElem: O_{5} → O_{5} → O_{5}

1. T.Streicher. A groupoid model refutes UIP. 1994

2. T.Streicher. The Groupoid Interpretation. 1996

3. B.Jacobs. Categorical Logic and Type Theory. 1999

4. S.Awodey. Homotopy Type Theory and Univalent Foundations. 2013

5. S.Huber. A Cubical Type Theory. 2015

6. A.Joyal. What is an elementary higher topos. 2014

7. 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.

```
record PTS: * :=
(S: ∀ (n: nat) → star n)
(A: ∀ (i: nat) → type i (succ i))
(R: ∀ (i: nat) → ∀ (j: nat)
→ pi i j (max i j))
```