On Church’s thesis in cubical assemblies

DOI10.1017/S0960129522000068MaRDI QIDQ5055494

Taichi Uemura, Andrew Swan

Publication date: 9 December 2022

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

Full work available at URL: https://arxiv.org/abs/1905.03014

zbMATH Keywords

realizabilityhomotopy type theorycubical sets

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (3)

Cubical methods in homotopy type theory and univalent foundations ⋮ Synthetic topology in Homotopy Type Theory for probabilistic programming ⋮ Univalent polymorphism

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Realizability. An introduction to its categorical side
• Constructivism in mathematics. An introduction. Volume II
• Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
• Univalent polymorphism
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Internal type theory
• Propositions as [Types]
• Constructive sheaf models of type theory
• Partial Elements and Recursion via Dominances in Univalent Type Theory.
• On Higher Inductive Types in Cubical Type Theory
• Modalities in homotopy type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Types for Proofs and Programs
• On the interpretation of intuitionistic number theory

This page was built for publication: On Church’s thesis in cubical assemblies