Brouwer's fixed-point theorem in real-cohesive homotopy type theory

DOI10.1017/S0960129517000147zbMath1390.03014arXiv1509.07584MaRDI QIDQ4640312

Michael Shulman

Publication date: 17 May 2018

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

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

zbMATH Keywords

homotopy type theoryBrouwer's fixed-point theorem

Mathematics Subject Classification ID

Related Items (26)

Modalities in homotopy type theory ⋮ Adjoint Logic with a 2-Category of Modes ⋮ Synthetic topology in Homotopy Type Theory for probabilistic programming ⋮ A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types ⋮ Constructive sheaf models of type theory ⋮ Normalization by evaluation for modal dependent type theory ⋮ Strange new universes: Proof assistants and synthetic foundations ⋮ A general framework for the semantics of type theory ⋮ Two-level type theory and applications ⋮ UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC ⋮ Semantical analysis of contextual types ⋮ Univalent foundations as structuralist foundations ⋮ Unnamed Item ⋮ A type theory for synthetic $\infty$-categories ⋮ Characterizations of modalities and lex modalities ⋮ Indexed type theories ⋮ Unnamed Item ⋮ Good Fibrations through the Modal Prism ⋮ An introduction to univalent foundations for mathematicians ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Modal dependent type theory and dependent right adjoints ⋮ Real ADE-equivariant (co)homotopy and super M-branes ⋮ Unnamed Item ⋮ Modal descent

Uses Software

• HoTT
• GitHub
• MathOverflow

Cites Work

• On the homotopy type of higher orbifolds and Haefliger classifying spaces
• The intrinsic topology of Martin-Löf universes
• Univalence in locally Cartesian closed categories
• Metric spaces in synthetic topology
• A constructive and functorial embedding of locally compact metric spaces into locales
• Constructivism in mathematics. An introduction. Volume II
• Calculus. III: Taylor series
• Elementary axioms for local maps of toposes
• A judgmental reconstruction of modal logic
• The Local Universes Model
• Convenient categories of smooth spaces
• A lambda calculus for real analysis
• Homotopy theoretic models of identity types
• On a Topological Topos
• Eilenberg-MacLane spaces in homotopy type theory
• Constructions with Non-Recursive Higher Inductive Types
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Adjoint Logic with a 2-Category of Modes
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Resolution of the uniform lower bound problem in constructive analysis
• Higher Topos Theory (AM-170)
• Universal homotopy theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Brouwer's fixed-point theorem in real-cohesive homotopy type theory