Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userModalities in homotopy type theory
144
0
0.0
(
0
)
Added by
Bas Spitters
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a localization higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
rate research
Read More
Doctrines are categorical structures very apt to study logics of different nature within a unified environment: the 2-category Dtn of doctrines. Modal interior operators are characterised as particular adjoints in the 2-category Dtn. We show that they can be constructed from comonads in Dtn as well as from adjunctions in it, and the two constructions compare. Finally we show the amount of information lost in the passage from a comonad, or from an adjunction, to the modal interior operator. The basis for the present work is provided by some seminal work of John Power.
We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of adjoint logic in which the discretization and codiscretization modalities are characterized using a judgmental formalism of crisp variables. This yields type theories that we call spatial and cohesive, in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the fundamental $infty$-groupoid or shape), disentangling the identifications of Homotopy Type Theory from the continuous paths of topology. In a further refinement called real-cohesion, the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwers fixed-point theorem.
We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Lof type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces for Mathematics and Physics (ed. Gabriel Catren and Mathieu Anel).
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in quantum gauge field theory. This is a brief survey of work by the authors developed in detail elsewhere.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
