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 (ITT), in the Martin-Löf tradition, is a family of constructive dependent type calculi in which a proposition can be read as a type and a proof as a term inhabiting it. A judgment establishes that a term has a type under specified assumptions. A dependent type may vary with an input term; a dependent product (\(\Pi\)) expresses function-like evidence across inputs, while a dependent sum (\(\Sigma\)) packages a witness with evidence about it. Formation, introduction, elimination and computation/equality rules connect what may be stated, how evidence is built, how it is used and how the result reduces.[1]
This is a family, not one immutable axiom list. Martin-Löf's lectures specify a particular system; later implementations such as Agda inherit constructive dependent typing while adding language features. Equality and universe rules differ across formulations. Those variants cannot be collapsed into a universal claim about decidable checking or one exact proof calculus.[1][2][3]
Structural Signature¶
Sig role-phrases: contextual judgment → proposition-as-type → constructed inhabitant → dependent former → introduction/elimination/computation rule.
- Judgments in context: formation and term-in-type assertions are derived under explicit assumptions. Without this validity relation, a purported proof term is only syntax.[1]
- Proof-bearing terms: an inhabited proposition-as-type has constructed evidence. A bare external assertion of truth does not supply the same object.[1]
- Dependent formers: \(\Pi\) and \(\Sigma\) allow the output type to depend on an input; their terms respectively act like dependent functions and witness–evidence pairs. Removing dependence leaves a simpler constructive typed calculus, not this scoped family.[1]
- Coordinated rules: each chosen former comes with rules for its formation, introduction, elimination and computation/equality. Exact equality and universe rules are variant-dependent, but an uninterpreted type name alone does not provide the constructive operation.[1][2]
What It Is Not¶
It is not all type theory. A simply typed or industrial type system may classify program terms without interpreting propositions as proof-inhabited types or providing dependent products and sums. It is not classical truth-value semantics with a proof annotation pasted on: an existential inhabitant must contain a witness in the constructive reading. Nor is every ITT an exact copy of Agda; Agda adds practical language features to an ITT-derived basis.[1][3][2]
ITT is also not a refinement type: a predicate that narrows a host programming type need not provide constructive dependent proof terms. Nor is ITT a blanket promise that every proof runs as useful software, every equality is decidable or every variant admits the same universe structure. Such claims depend on the selected calculus and its computation and equality rules.[2]
Scope of Application¶
In constructive mathematics, Martin-Löf derives a form of the axiom of choice internally from a term of dependent-product-of-sums type: projections extract a choice function and its accompanying evidence. This uses the witness-bearing interpretation of \(\Sigma\) rather than asserting the existence of a function by an external classical rule.[1]
In dependently typed programming, official Agda documentation illustrates vectors indexed by their length and matrices whose dimensions appear in types. A program inhabiting such a type carries a machine-checkable structural specification. Agda is an implementation descended from the tradition, not a claim that its full feature set was present in the 1984 lectures.[3][2]
Clarity¶
Separate proposition, judgment and proof term. The proposition is what can be inhabited; the judgment records a formal claim such as a term having that type; the term is the constructed evidence. Martin-Löf explicitly distinguishes propositions from judgments. Conflating them hides whether an existential statement has an actual witness or has only been asserted true.[1]
Also separate judgmental computation from variants of propositional equality. A reduction rule can explain what an eliminator computes on an introduced term without determining every identity-type or extensionality principle in later systems.[1][2]
Manages Complexity¶
Instead of treating a theorem, its proof, a program and its specification as unrelated objects, the calculus organizes them through typed judgments and a small set of constructor/eliminator rules. For a dependent sum, the essential interface is a pair plus projections; for a dependent product, it is a function-like term plus application. This does not erase the proof's detail: it specifies where the witness and evidence must reside.[1]
In Agda's vector example, length is an index in the type rather than an informal comment beside an ordinary list. That can move a dimension mismatch into a type-checking obligation, although actual checking and execution still depend on the implemented language and chosen definitions.[3]
Abstract Reasoning¶
Suppose a term has type \(\Pi_{x:A}\Sigma_{y:B(x)}C(x,y)\). Given an \(x:A\), apply the term to get a pair: a \(y:B(x)\) and evidence of \(C(x,y)\). Projecting first components for each input constructs a function choosing \(y\); projecting the second components verifies its required property. Martin-Löf's choice construction makes this reasoning explicit. The inference relies on the dependent formers and their elimination rules, not just the English sentence “for every input there exists an output.”[1]
Conversely, seeing a type annotation alone does not justify extracting a witness. Ask which judgment establishes the inhabitant and which eliminator exposes it. If no such term/rule exists, the constructive conclusion has not been demonstrated.[1]
Knowledge Transfer¶
The mathematical choice argument and an Agda vector program share the roles context / dependent proposition-or-specification / inhabitant / rules of use. In the first, the inhabitant packages witnesses and proof obligations; in the second, a program is checked against an index-sensitive type. The transfer is the constructive rule pattern, not identity of their full calculi or the assertion that every mathematical theorem is executable.[1][3][2]
When carrying an argument between formulations, recheck equality, universes and available type formers. The original lecture system and Agda have related foundations but different language provisions; a proof relying on a later extension does not automatically inhabit the earlier system.[1][2]
Examples¶
Internal choice construction. Mapped back: context = a family of inputs and witness types; dependent formers = product of sums; term = a proof giving a witness-plus-evidence for each input; rules = product application and sum projections extract a function and verification. Martin-Löf gives this as a worked construction, not merely a slogan that proofs are programs.[1]
Length-indexed vectors in Agda. Mapped back: context = element type and natural-number length; dependent type = Vec A n, varying with \(n\); term = a vector-producing program checked at that index; rules = typed constructors/functions and computation in Agda's implementation. The official documentation also describes length-indexed matrices. These are an implementation-level instance of the dependent constructive pattern, with Agda-specific details outside the minimal ITT core.[3][2]
Structural Tensions¶
Expressive dependency versus tractable judgmental equality. More type-level dependence can state exact index-sensitive obligations, but every added former or equality rule needs a computation and checking account. Restricting the language can make checking easier to specify while losing desired statements; adding principles can express more while obliging a new metatheoretic check rather than inheriting one universal decidability claim. Diagnostic: Which rules permit the proposed dependency, and what equality procedure validates its inhabitants in this formulation?[1][2]
Witness content versus proof reuse. Requiring a \(\Sigma\) inhabitant lets an eliminator recover a witness and evidence, as in the internal choice construction. That gain has a cost: a classical existential argument that supplies no such inhabitant cannot simply be imported as a constructive proof. Relaxing the witness demand admits a broader style of assertion but forfeits the same extraction inference. Diagnostic: Does this argument actually construct a term whose projections deliver the claimed witness and property?[1]
Shared core versus implementation-specific power. Using Agda's added programming conveniences can shorten a development and provide richer implementations, but a proof that relies on an extension need not be valid in the earlier lecture calculus. Staying within a common \(\Pi\)/\(\Sigma\) fragment supports portability but may require a more explicit encoding or omit a desired feature. Diagnostic: Which type formers, equality rules and universes does the argument require in both systems?[1][2][3]
Structural–Framed Character¶
Evaluative weight. Constructive witness requirements are logical validity conditions within the chosen calculus, not an ethical preference; whether they are desirable for a project depends on proof and programming goals. Human-practice dependence. People choose syntax, axioms and implementations, but after those are specified, judgments follow formal rules rather than convention alone.[1]
Institutional origin. Martin-Löf's lectures and proof-assistant development supply a historical lineage, yet a term is not ITT merely because it appears in Agda or an institution uses it. Vocabulary travel. “Type,” “proof” and “program” cross logic and computing literally when the inhabitant interpretation is preserved; borrowing those words for organizational categories is only analogy.[1][3]
Import versus recognition. A new formalism counts by its constructive judgments, dependent formers and coordinated rules, even if it has a new name. Conversely, calling a classical annotation language “intuitionistic” does not establish witness-bearing inhabitants. Its character: predominantly structural within formal logic and programming, but still domain-bound by typed judgments and constructive proof rules.[1][2]
Structural Core vs. Domain Accent¶
Portable skeleton. The immediate live genus is Type theory: both use formal judgments assigning terms to types. A more portable idea—requiring a constructed witness before treating a claim as established—may be a future-prime candidate, but this wave does not establish its substrate independence or add a prime edge. Live Verification checks an object against a specification and is a useful comparison, not the genus of ITT; an individual proof or check does not itself constitute a type calculus.[1]
Domain-bound mechanism. ITT adds the propositions-as-types inhabitant reading and dependent \(\Pi\)/\(\Sigma\) constructors with coordinated formation, introduction, elimination and computation rules. These formal resources explain why a constructive existential carries a witness and why the internal choice term can be projected. Exact equality/universe choices remain formulation-specific.[1][2]
Why not prime. The prospective witness-before-assertion skeleton might travel to evidence practices elsewhere, but the literal ITT identity depends on types, terms, judgments, dependent constructors and reduction. Importing its words into an unrelated workflow would not yield an ITT calculus. The live Type Theory parent is itself domain-specific; no existing prime is being claimed as this entry's parent.
Instantiates / Related Primes¶
This entry is a kind of Type theory.
The proposed typed edge is strict subsumption under Type theory; it is not yet a canonical DAG relation. ITT instantiates generic term/type judgments while imposing a constructive dependent interpretation. Live Proof is related as what an inhabitant can realize, not as the necessary genus. Agda is an implementation neighbor rather than an exact synonym.[1][3]
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.The live Type Theory identity assigns terms to types through formal judgments. This family retains that relation and adds constructive proof-as-inhabitant interpretation, dependent families and coordinated rules for their construction, use and computation.
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
Not to Be Confused With¶
Generic type theory may lack constructive dependent proof terms. Simply typed lambda calculus lacks dependence of a type on a term. Agda is a later programming/proof environment with its own extensions. Classical existential reasoning can establish a proposition without furnishing the particular witness term demanded by an internal \(\Sigma\) proof. Intensional/extensional identity distinguishes formulations; neither label alone defines the entire ITT family.[1][2][3]
References¶
[1] Per Martin-Löf, Intuitionistic Type Theory, notes by Giovanni Sambin of Padua 1980 lectures (Bibliopolis, 1984; retypeset online), “Propositions and judgements,” pp. 2–12; “General remarks on the rules,” p. 13; dependent product and sum chapters, pp. 13–26; “The axiom of choice,” pp. 27–28. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v ↩w ↩x ↩y ↩z
[2] Stanford Encyclopedia of Philosophy, “Intuitionistic Type Theory,” introduction and discussion of Martin-Löf formulations and Agda. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n
[3] Agda documentation, “What is Agda?”, Agda 2.9.0, introductory dependent-functions and length-indexed vector/matrix examples. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j