A coherence theorem for Martin-Löf's type theory

DOI10.1017/S0956796898003153zbMath0917.03028OpenAlexW2102861499MaRDI QIDQ4236885

Michael Hedberg

Publication date: 15 July 1999

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796898003153

zbMATH Keywords

coherencecategory-theoretical propertiesidentity proofsinductive equalityinitial category structurekernel fragment of Martin-Löf's type theorytypes with decidable identities

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)

Related Items (16)

Unnamed Item ⋮ Unnamed Item ⋮ Regular language representations in the constructive type theory of Coq ⋮ Unnamed Item ⋮ Constructing a small category of setoids ⋮ Homotopy type theory in Lean ⋮ Unnamed Item ⋮ Proof-relevance of families of setoids and identity in type theory ⋮ Univalence for inverse diagrams and homotopy canonicity ⋮ Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory ⋮ From Sets to Bits in Coq ⋮ Isomorphism is equality ⋮ Two-Way Automata in Coq ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

Uses Software

• ALF

This page was built for publication: A coherence theorem for Martin-Löf's type theory