A generalization of the Takeuti-Gandy interpretation
From MaRDI portal
Publication:5740650
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
- scientific article; zbMATH DE number 3291139 (Why is no real title available?)
- 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
- 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)- Normalization by Evaluation for Typed Weak lambda-Reduction
- Refinement by Interpretation in a General Setting
- Homotopical patch theory
- A Kripke model for simplicial sets
- Stack semantics of type theory
- A dependently-typed construction of semi-simplicial types
- The generalised type-theoretic interpretation of constructive set theory
- 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)
