Towards Univalent Construction Calculus
Modern constructive Martin-Löf Type Theories (MLTTs) are exceptionally expressive and convenient languages for mathematical reasoning.
By “modern” let us mean MLTTs featuring the empty type 𝟘, the unit type 𝟙 inhabited solely by the symbol 𝟘, the type 𝔹 (bit or boolean type) inhabited by the symbols 𝟘 and 𝟙, and a cumulative hierarchy of univalent universes (types containing symbols for other types) closed under forming quotient inductive-inductive types (QIITs), dependent product types “∀(x : X) Y” and identity types “x = y”:
```
𝟘 ⊃ 𝟙 ⊃ 𝔹 ⊃ 𝓤 ⊃ 𝓤⁺ ⊃ 𝓤⁺⁺ ⊃ ···,
𝟘 : 𝟙 : 𝔹 : 𝓤 : 𝓤⁺ : 𝓤⁺⁺ : ···,
```
Such theories support a huge repertoire of value types, here's a list of some random examples:
- Natural numbers `ℕ`;
- Finite lists of integer Numbers (`List[ℤ]`);
- Sequences of rational numbers (`Seq[ℚ]`);
- Countable subsets of real numbers (`CSet[ℝ]`);
- Turing-complete computations yielding a complex number if they halt (`℧(ℂ)`).
Types `P` satisfying `∀(x y : P) x = y` are called propositional and enjoy propositional resizing, i.e. once it is proven that a type `P : 𝓤⁺ⁿ` is propositional, it is guaranteed to have an isomorphic copy in the smallest open universe U. Predicates and relations on value types can be represented propositional types and composed by conjunction, disjunction, implication, negation as well as quantifiers `∀(x : X) P(x)` (a special case of the dependent product) and `∃(x : X) P(x)` (can be defined as a QIIT) in a way faithfully representing higher-order intuitionistic logic with equality. Proofs and mathematical constructions can be represented as terms of the theory. Univalence allows transporting proofs and constructions along isomorphism and equivalences of mathematical structures and induces the natural extensional notion of identifiability (equality, isomorphy, equivalence, etc.) for propositions, functions, conductive types, and all sorts of mathematical structures such as groups, rings, categories, and topological spaces. Constructiveness means that proofs can be algorithmically verified and terms of closed inductive types like 𝔹 or ℕ can be algorithmically evaluated to a fixed bit value or numerical value respectively. [Footnote: Constructive type theories are thus abstruse programming languages capable to express both total and Turing-complete computations, without being able to specify their operational behavior and effectively control their computational complexity. It is possible to extend it to a genuine programming language by introducing linear types, but that's another story.]
What can we wish more?
Well, there is an expressivity problem: in pure MLTT it is not possible to define generic type formers such as `List[T]` or `Group[T]` (type of group structures on the carrier type `T`) for _all_ types. Similarly, it is not possible to provide generic proofs for all groups `G` or all categories `T`. It is only possible to do so for U-small types, groups, and categories for any given universe U. And if we want to use only the formal language to formulate the propositions, this expressivity problem is not a negligible one. The classical set theory ZFC has exactly the same expressivity problem which is solved by its conservative extension NBG, the von Neumann-Bernays-Gödel theory, where one can reason not only about sets but also about classes, like for example the pure class of all groups.
Our endeavor is to extend a modern Martin-Löf Type Theory to a variant of Construction Calculus solving this issue. As it will turn out, solving this issue also solves a seemingly unrelated issue: it paves the way for non-constructive reasoning (double negation elimination and optionally, the Axiom of Choice) in a computationally sound way[Heberlin'12].
Recall, that in NBG every set is also a class, and a class is a set precisely if it is contained in another set. We'll introduce a notion of signature so that every type is a signature, but a signature is a type only if it belongs to a universe (another type). While values have types, parameters and parametric constructions have signatures. The signature * stands for “type”, that can be understood as a kind of ideal limit of the universe hierarchy `U ⊃ U¹ ⊃ U² ⊃ ···` that lives outside of the realm of types in contrary to the universes `Uⁿ` themselves.
The type former `List[T : *]` has a parameter `T` of signature `*` and has the signature `List : * -> *` itself. Parametric constructions and theorems also have signatures instead of types. As an example of a parametric construction, consider the polymorphic identity function `id[T : *] := (\x : T => x)`. It has the signature `id : ∀(T : *) (T -> T)`. An imaginary theorem `Thm₁[Carrier : *, g : Group[Carrier]] : ...` proven for all groups would have the signature `Thm₁ : ∀(Carrier : *, G : Group) ...`.
Now let us introduce the notion of parametric dependency formally.
Definition 1 (Parametric dependence, syntactic definition)
A function is said to be parametric in `T` if it never uses `T` in its body.
Example 1
```
id(T : *): T -> T
(x : T) => x
```
Example 2
```
reverse(T : *): List[T] -> List[T]
# reverses the list
```
Parameters are only allowed to be used generically in parameters of input and output types.
Non-example 1
```
idU(T : 𝓤)
T
```
Here, the argument `T` is used in the body, it is namely returned as-is. That's an example of non-parametric dependence.
Definition 2 (Generic dependence, syntactic definition)
A function is said to be generic in `x` if it never inspects `x`, i.e. never uses an eliminator on it. It may however return its argument as is, apply any constructors or other generic functions. In case all constructors of the types involved are injective, generic functions are guaranteed to be injective.
Non-example 2
```
is-nonzero(n : Nat): 𝔹
Zero => 𝟙
Succ(n : Nat) => 𝟘
```
Example 3
```
add-two(n : Nat): Nat
Succ(Succ(n))
```
Example 4
```
pack-into-singleton-list(n : Nat): List[Nat]
NonEmptyList(head: n, tail: EmptyList)
```
Example 5
```
idU(T : 𝓤)
T
```
The function `idU` depends on `T` generically, but not parametrically as we have underlined in Non-Example 1.
Since in MLTT, universes do not have eliminators, all functions are guaranteed to depend on their typal arguments generically.
(TBC)
By “modern” let us mean MLTTs featuring the empty type 𝟘, the unit type 𝟙 inhabited solely by the symbol 𝟘, the type 𝔹 (bit or boolean type) inhabited by the symbols 𝟘 and 𝟙, and a cumulative hierarchy of univalent universes (types containing symbols for other types) closed under forming quotient inductive-inductive types (QIITs), dependent product types “∀(x : X) Y” and identity types “x = y”:
```
𝟘 ⊃ 𝟙 ⊃ 𝔹 ⊃ 𝓤 ⊃ 𝓤⁺ ⊃ 𝓤⁺⁺ ⊃ ···,
𝟘 : 𝟙 : 𝔹 : 𝓤 : 𝓤⁺ : 𝓤⁺⁺ : ···,
```
Such theories support a huge repertoire of value types, here's a list of some random examples:
- Natural numbers `ℕ`;
- Finite lists of integer Numbers (`List[ℤ]`);
- Sequences of rational numbers (`Seq[ℚ]`);
- Countable subsets of real numbers (`CSet[ℝ]`);
- Turing-complete computations yielding a complex number if they halt (`℧(ℂ)`).
Types `P` satisfying `∀(x y : P) x = y` are called propositional and enjoy propositional resizing, i.e. once it is proven that a type `P : 𝓤⁺ⁿ` is propositional, it is guaranteed to have an isomorphic copy in the smallest open universe U. Predicates and relations on value types can be represented propositional types and composed by conjunction, disjunction, implication, negation as well as quantifiers `∀(x : X) P(x)` (a special case of the dependent product) and `∃(x : X) P(x)` (can be defined as a QIIT) in a way faithfully representing higher-order intuitionistic logic with equality. Proofs and mathematical constructions can be represented as terms of the theory. Univalence allows transporting proofs and constructions along isomorphism and equivalences of mathematical structures and induces the natural extensional notion of identifiability (equality, isomorphy, equivalence, etc.) for propositions, functions, conductive types, and all sorts of mathematical structures such as groups, rings, categories, and topological spaces. Constructiveness means that proofs can be algorithmically verified and terms of closed inductive types like 𝔹 or ℕ can be algorithmically evaluated to a fixed bit value or numerical value respectively. [Footnote: Constructive type theories are thus abstruse programming languages capable to express both total and Turing-complete computations, without being able to specify their operational behavior and effectively control their computational complexity. It is possible to extend it to a genuine programming language by introducing linear types, but that's another story.]
What can we wish more?
Well, there is an expressivity problem: in pure MLTT it is not possible to define generic type formers such as `List[T]` or `Group[T]` (type of group structures on the carrier type `T`) for _all_ types. Similarly, it is not possible to provide generic proofs for all groups `G` or all categories `T`. It is only possible to do so for U-small types, groups, and categories for any given universe U. And if we want to use only the formal language to formulate the propositions, this expressivity problem is not a negligible one. The classical set theory ZFC has exactly the same expressivity problem which is solved by its conservative extension NBG, the von Neumann-Bernays-Gödel theory, where one can reason not only about sets but also about classes, like for example the pure class of all groups.
Our endeavor is to extend a modern Martin-Löf Type Theory to a variant of Construction Calculus solving this issue. As it will turn out, solving this issue also solves a seemingly unrelated issue: it paves the way for non-constructive reasoning (double negation elimination and optionally, the Axiom of Choice) in a computationally sound way[Heberlin'12].
Recall, that in NBG every set is also a class, and a class is a set precisely if it is contained in another set. We'll introduce a notion of signature so that every type is a signature, but a signature is a type only if it belongs to a universe (another type). While values have types, parameters and parametric constructions have signatures. The signature * stands for “type”, that can be understood as a kind of ideal limit of the universe hierarchy `U ⊃ U¹ ⊃ U² ⊃ ···` that lives outside of the realm of types in contrary to the universes `Uⁿ` themselves.
The type former `List[T : *]` has a parameter `T` of signature `*` and has the signature `List : * -> *` itself. Parametric constructions and theorems also have signatures instead of types. As an example of a parametric construction, consider the polymorphic identity function `id[T : *] := (\x : T => x)`. It has the signature `id : ∀(T : *) (T -> T)`. An imaginary theorem `Thm₁[Carrier : *, g : Group[Carrier]] : ...` proven for all groups would have the signature `Thm₁ : ∀(Carrier : *, G : Group) ...`.
Now let us introduce the notion of parametric dependency formally.
Definition 1 (Parametric dependence, syntactic definition)
A function is said to be parametric in `T` if it never uses `T` in its body.
Example 1
```
id(T : *): T -> T
(x : T) => x
```
Example 2
```
reverse(T : *): List[T] -> List[T]
# reverses the list
```
Parameters are only allowed to be used generically in parameters of input and output types.
Non-example 1
```
idU(T : 𝓤)
T
```
Here, the argument `T` is used in the body, it is namely returned as-is. That's an example of non-parametric dependence.
Definition 2 (Generic dependence, syntactic definition)
A function is said to be generic in `x` if it never inspects `x`, i.e. never uses an eliminator on it. It may however return its argument as is, apply any constructors or other generic functions. In case all constructors of the types involved are injective, generic functions are guaranteed to be injective.
Non-example 2
```
is-nonzero(n : Nat): 𝔹
Zero => 𝟙
Succ(n : Nat) => 𝟘
```
Example 3
```
add-two(n : Nat): Nat
Succ(Succ(n))
```
Example 4
```
pack-into-singleton-list(n : Nat): List[Nat]
NonEmptyList(head: n, tail: EmptyList)
```
Example 5
```
idU(T : 𝓤)
T
```
The function `idU` depends on `T` generically, but not parametrically as we have underlined in Non-Example 1.
Since in MLTT, universes do not have eliminators, all functions are guaranteed to depend on their typal arguments generically.
(TBC)