Brouwer's fixed-point theorem in real-cohesive homotopy type theory
From MaRDI portal
Publication:4640312
DOI10.1017/S0960129517000147zbMath1390.03014arXiv1509.07584MaRDI QIDQ4640312
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
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