Stack semantics of type theory

MaRDI QIDQ5144677zbMATH OpenFDO

Authors Thierry Coquand, Bassel Mannaa, Fabian Ruch

Publication date 19 January 2021

Full work available at URL https://arxiv.org/abs/1701.02571, http://dl.acm.org/citation.cfm?id=3330065

Mathematics Subject Classification ID

Type theory (03B38) Axiom of choice and related propositions (03E25) Metamathematics of constructive systems (03F50)

Recommendations

• The simplicial model of univalent foundations (after Voevodsky)
• A generalization of the Takeuti-Gandy interpretation
• scientific article; zbMATH DE number 6694181
• Partial univalence in n-truncated type theory
• Univalent semantics of constructive type theories

Cited in

(13)

• Formally computing with the non-computable
• scientific article; zbMATH DE number 2172969 (Why is no real title available?)
• Higher order functions and Brouwer's thesis
• Cubical methods in homotopy type theory and univalent foundations
• The Scott model of PCF in univalent type theory
• Synthetic topology in Homotopy Type Theory for probabilistic programming
• Partiality and Container Monads
• Constructive sheaf models of type theory
• Models of Type Theory Based on Moore Paths
• Bicategorical type theory: semantics and syntax
• Semantics for two-dimensional type theory
• Open bar -- a Brouwerian intuitionistic logic with a pinch of excluded middle
• Strict universes for Grothendieck topoi

This page was built for publication: Stack semantics of type theory

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