Intuitionistic Type Theory¶
A constructive dependent type-theory family that treats propositions as types and proofs as terms governed by explicit formation, use, and computation rules.
Core Idea¶
Intuitionistic type theory is a family of constructive dependent type calculi in which propositions can be read as types and proofs as terms inhabiting them. Judgments say when a type or term is valid under assumptions. Dependent products (\(\Pi\)) represent function-like evidence across inputs; dependent sums (\(\Sigma\)) package a witness with its evidence. Formation, introduction, elimination and computation rules link statements, constructions and their use. Particular equality and universe rules vary across formulations.[ref-9d5f58f91a7f][ref-6564075999bd]
Scope of Application¶
Martin-Löf's internal choice construction uses a term in a dependent product of sums to extract a choice function and evidence about it. In programming, Agda's length-indexed vectors and matrices illustrate ITT-derived dependent typing: an index appears in the type of the program object. Agda adds features and is not identical to the original calculus.[ref-9d5f58f91a7f][ref-f4d67dfdb6e7][^ref-6564075999bd]
Clarity¶
A proposition is not the same thing as a judgment asserting it, and a judgment is not the same as a term that inhabits the proposition-as-type. An existential inhabitant in this constructive reading contains a witness. Merely annotating a classical truth assertion with the word “proof” does not supply one.[^ref-9d5f58f91a7f]
Manages Complexity¶
The calculus organizes propositions, evidence, specifications and programs through typed judgments and coordinated constructor/eliminator rules. A dependent sum exposes a witness pair; a dependent product exposes a function-like term. In an implemented language, an index such as vector length can move a constraint from an informal comment into a checking obligation, without guaranteeing that every proof is practically executable.[ref-9d5f58f91a7f][ref-f4d67dfdb6e7]
Abstract Reasoning¶
Given an inhabitant of \(\Pi_{x:A}\Sigma_{y:B(x)}C(x,y)\), apply it to an input \(x\), then project the witness \(y\) and evidence of \(C(x,y)\). Repeating that operation constructs a choice function. The inference depends on the actual dependent-type rules; a bare English claim of existence does not suffice. A migrated proof must be checked against the equality and universe rules of its target formulation.[ref-9d5f58f91a7f][ref-6564075999bd]
Knowledge Transfer¶
The choice proof and an Agda length-indexed program share context, dependent type, inhabiting term and rules for using it. What transfers is the constructive, type-governed pattern. Their full calculi need not be identical, and generic type theory need not have the same dependent witness interpretation.[ref-9d5f58f91a7f][ref-f4d67dfdb6e7][^ref-6564075999bd]
[^ref-9d5f58f91a7f]: Per Martin-Löf, Intuitionistic Type Theory, notes by Giovanni Sambin (Bibliopolis, 1984; retypeset online), pp. 2–28. [^ref-f4d67dfdb6e7]: Agda documentation, “What is Agda?”, Agda 2.9.0. [^ref-6564075999bd]: Stanford Encyclopedia of Philosophy, “Intuitionistic Type Theory.”
Relationships to Other Abstractions¶
Current abstraction Intuitionistic Type Theory Domain-specific
Parents (1) — more general patterns this builds on
-
Intuitionistic Type Theory is a kind of Type theory Domain-specific
Intuitionistic type theory is a constructive dependent specialization of type theory.
Hierarchy path (1) — routes to 1 parentless root
- Intuitionistic Type Theory → Type theory → Classification
Neighborhood in Abstraction Space¶
Intuitionistic Type Theory sits in a moderately populated region (40th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.
Family — Type Systems & Functional Constructs (18 abstractions)
Nearest neighbors
- Constructive Logic — 0.88
- Simply typed lambda calculus — 0.88
- Categorial Grammar — 0.87
- Propositional logic — 0.87
- Proof calculus — 0.87
Computed from structural-signature embeddings · 2026-10-08