Extensional Constructs in Intensional Type Theory

DOI10.1007/978-1-4471-0963-1zbMath1411.03001OpenAlexW1481180394MaRDI QIDQ4632162

Martin Hofmann

Publication date: 26 April 2019

Full work available at URL: https://doi.org/10.1007/978-1-4471-0963-1

Mathematics Subject Classification ID

Theory of programming languages (68N15) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Related Items (19)

From type theory to setoids and back ⋮ Game semantics for dependent types ⋮ Quotienting the delay monad by weak bisimilarity ⋮ Elementary fibrations of enriched groupoids ⋮ On generalized algebraic theories and categories with families ⋮ A Comparison of Type Theory with Set Theory ⋮ The compatibility of the minimalist foundation with homotopy type theory ⋮ Unnamed Item ⋮ Constructions of categories of setoids from proof-irrelevant families ⋮ Exact completion of path categories and algebraic set theory. I: Exact completion of path categories ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ A computer-verified monadic functional implementation of the integral ⋮ A minimalist two-level foundation for constructive mathematics ⋮ Guarded cubical type theory ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Safe recursion with higher types and BCK-algebra ⋮ Wellfounded trees in categories ⋮ Containers: Constructing strictly positive types ⋮ The effective model structure and -groupoid objects

This page was built for publication: Extensional Constructs in Intensional Type Theory