Intuitionistic Type Theory

Abstract

Type theory is a formal framework in mathematical logic and computer science where every term is assigned a type. It serves as a foundation for mathematics, an alternative to set theory, and the theoretical basis for functional programming languages and proof assistants.

Definition

A type system consists of a set of rules for assigning a type to terms. Formally, we express that a term $t$ has type $A$ under a context $Γ$ using the typing judgment $Γ ⊢ t : A$ .

Core Concepts

Basic Types and Constructors

Most type theories include base types (e.g., $N$ ) and type constructors:

Function types: $A \to B$ represents functions from $A$ to $B$ .
Product types: $A \times B$ represents pairs $(a, b)$ .
Sum types: $A + B$ represents disjoint unions.

Dependent Types

In dependent type theory, types may depend on terms. This is essential for representing mathematical predicates:

Pi-types: Dependent function types $(x : A) \to B (x)$ .
Sigma-types: Dependent pair types $Σ x : A . B (x)$ .

The Curry-Howard Correspondence

This principle establishes a structural isomorphism between logic and type theory. Propositions are treated as types, and proofs are treated as programs.

Logic	Type Theory
Proposition	Type
Proof	Term/Program
Implication	Function type
Conjunction	Product type
Disjunction	Sum type

See Curry-Howard Correspondence for details.

Notable Type Theories

Intuitionistic Type Theory (ITT)

Developed by Per Martin-Löf, ITT introduces a predicative foundation for constructive mathematics based on the internal meaning of intuitionistic logic.

Intensional vs Extensional

Type Theory: Does not include Equality Reflection or Uniqueness of Identity Proofs
Extensional Type Theory: Includes Equality Reflection and Axiom K

Calculus of Constructions (CoC)

A higher-order typed lambda calculus that forms the basis of the Coq proof assistant. It extends the Lambda Cube to its most expressive vertex.

Homotopy Type Theory (HoTT)

Homotopy Type Theory interprets types as spaces and identity types as paths. It introduces the Univalence Axiom, stating that equivalent types are equal.

Cubical Type Theory

Cubical Type Theory adds computational content to the univalence axiom, making HoTT constructive with canonical forms.

Other Variants

Observational Type Theory: Observational equality
Higher Observational Type Theory: Extension with higher structures
Setoid Type Theory: Types equipped with equivalence relations
Directed Type Theory: Types with directional structure
Geometric Type Theory: Geometric foundations
Partiality in Type Theory: Handling partial functions

Models

Presheaf Model of Type Theory: Presheaves as models
Categorical Model of Homotopy Type Theory: Infinity-topoi models
Sheaf Model: Sheaf-theoretic interpretations

Key Concepts

Inductive Type: Types defined by constructors
Higher Inductive Type: Inductive types with path constructors
Universe: Types of types
Substitution: Term replacement
Context: Variable environments
Type Judgement: Basic assertions in type theory
Eliminator: Recursion principles for types
Eta Rule: Definitional extensionality
Function Extensionality: Extensionality for functions
Identity Type: Identity types in Homotopy Type Theory
Univalence Principle: Equivalence is equality

History

The formal development of type theory spans over a century, evolving from a tool for resolving logical paradoxes to a constructive foundation for mathematics and computer science.

Ramified Type Theory (1908): Proposed by Bertrand Russell in Mathematical Logic as Based on the Theory of Types to resolve Russell’s Paradox and the Burali-Forti paradox. It introduced a hierarchy of types and orders to prevent circular definitions by enforcing the vicious circle principle.
Simply-Typed Lambda Calculus (1940): Alonzo Church simplified Russell’s system by combining it with the $λ$ -calculus. This formulation focused on the functional relationship between types rather than the complex ramified hierarchy.
The Curry-Howard Correspondence (1950s–1960s): Observations by Haskell Curry and William Howard revealed a structural correspondence between intuitionistic logic and typed calculi. This established that a proposition is a type and a proof is a program.
Intuitionistic Type Theory (1970s–1980s): Per Martin-Löf developed a predicative, dependent type theory intended as a foundation for constructive mathematics. This system introduced Pi-types, Sigma-types, and the identity type.
Calculus of Constructions (1980s): Thierry Coquand and Gérard Huet extended the Lambda Cube to include higher-order polymorphism and dependency, forming the basis for the Coq proof assistant.
Homotopy Type Theory (2000s–2010s): Vladimir Voevodsky and Steve Awodey independently recognized the connection between identity types and path spaces in algebraic topology. This led to the Univalence Principle, treating types as $\infty$ -groupoids.

References

church1940-simple-types howard1980-curry-howard coquand1988 russell1908-type-theory martin-lof1984-mltt nordstrom-petersson-smith1990-mltt hott2013-book sorensen2006-curry-howard

Type Theory where all types are constructive.

A kind of type theory without:

See also

Source

https://www.youtube.com/watch?v=u92V0OMgvhM&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z