Homotopy Type Theory

The Univalent Foundations Program. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics.

Type

Book

Intellectual base

Review or monograph

Year

2013

Link

https://homotopytypetheory.org/book/

Cited by

3 citations across 3 artifacts.

Domain-specific

• Extensionality
  • Extensionality identifies objects solely by equality of their extensions rather than by how they are described or constructed.
• Transport of Structure
  • Univalence and the structure identity principle connect equivalence with identity and explain why equivalent structured objects support coherent transport.
• Type System
  • Programming languages — the home turf, spanning the whole expressiveness frontier: C's coarse primitives, Java's nominal class hierarchy, ML/Haskell parametric polymorphism, Rust's linear/affine ownership, Liquid Haskell's SMT-checked refinements, and Coq/Agda/Lean/Idris dependent types. Static analysis and verification — refinement types, session types for concurrent protocols, and linear/affine types for resource use that turn correctness proofs into type checks. Schema and serialization languages — JSON Schema, XML Schema, Protocol Buffers, and Avro impose a type discipline on interchange formats. Database schemas — column types, constraints, and referential integrity form a type system over relational data. Type theory and proof assistants — Martin-Löf type theory, the calculus of constructions, and homotopy type theory turn the type system, via Curry-Howard, into a foundation for mathematics where checking is proof verification

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Registry ID ref:c8f065cf5c29 · see in the full table