A generalization of the Takeuti-Gandy interpretation

DOI10.1017/S0960129514000504MaRDI QIDQ5740650zbMATH OpenFDO

Authors Bruno Barras, Thierry Coquand, Simon Huber

Publication date 27 July 2016

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Categorical logic, topoi (03G30)

Recommendations

• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• scientific article; zbMATH DE number 2079044
• The simplicial model of univalent foundations (after Voevodsky)
• Revisiting the categorical interpretation of dependent type theory
• The generalised type-theoretic interpretation of constructive set theory

Cites work

• A course in constructive algebra
• A formulation of the simple theory of types
• Constructivism in mathematics. An introduction. Volume I
• Homotopy theoretic models of identity types
• scientific article; zbMATH DE number 3291139 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• L.J.E. Brouwer : Topologie et constructivisme
• Logical relations and the typed λ-calculus
• On the axiom of extensionality – Part I
• Proof-relevance of families of setoids and identity in type theory

Cited in

(8)

• A Kripke model for simplicial sets
• Refinement by Interpretation in a General Setting
• Normalization by Evaluation for Typed Weak lambda-Reduction
• Stack semantics of type theory
• Homotopical patch theory
• The generalised type-theoretic interpretation of constructive set theory
• A dependently-typed construction of semi-simplicial types
• Towards a constructive simplicial model of Univalent Foundations

This page was built for publication: A generalization of the Takeuti-Gandy interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740650)