A coherence theorem for Martin-Löf's type theory
From MaRDI portal
Publication:4236885
DOI10.1017/S0956796898003153zbMath0917.03028OpenAlexW2102861499MaRDI QIDQ4236885
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
coherencecategory-theoretical propertiesidentity proofsinductive equalityinitial category structurekernel fragment of Martin-Löf's type theorytypes with decidable identities
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
This page was built for publication: A coherence theorem for Martin-Löf's type theory
