scholarly journals Natural models of homotopy type theory

2016 ◽  
Vol 28 (2) ◽  
pp. 241-286 ◽  
Author(s):  
STEVE AWODEY
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Homotopy Theory ◽  
Inference Rules ◽  
Basic System ◽  
Homotopy Type Theory ◽  
Algebraic Formulation

The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π and intensional identity types Id, as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: They should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.

scholarly journals Introduction – from type theory and homotopy theory to univalent foundations

2015 ◽  
Vol 25 (5) ◽  
pp. 1005-1009
Author(s):  
STEVE AWODEY ◽  
NICOLA GAMBINO ◽  
ERIK PALMGREN
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Homotopy Theory ◽  
Foundations Of Mathematics ◽  
Special Issue ◽  
Research Papers ◽  
Homotopy Type Theory ◽  
Main Ideas ◽  
Univalent Foundations

We give an overview of the main ideas involved in the development of homotopy type theory and the univalent foundations of Mathematics programme. This serves as a background for the research papers published in the special issue.

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

2017 ◽  
Vol 28 (6) ◽  
pp. 856-941 ◽  
Author(s):  
MICHAEL SHULMAN
Keyword(s):  
Fixed Point ◽  
Fixed Point Theorem ◽  
Point Theorem ◽  
Homotopy Type ◽  
Algebraic Topology ◽  
Type Theory ◽  
Homotopy Theory ◽  
Homotopy Type Theory ◽  
Brouwer’S Fixed Point Theorem ◽  
Brouwer's Fixed Point Theorem

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 judgemental 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 ∞-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 Brouwer's fixed-point theorem.

scholarly journals Homotopical patch theory

2016 ◽  
Vol 26 ◽  
Author(s):  
CARLO ANGIULI ◽  
EDWARD MOREHOUSE ◽  
DANIEL R. LICATA ◽  
ROBERT HARPER
Keyword(s):  
Control Systems ◽  
Homotopy Type ◽  
Category Theory ◽  
Type Theory ◽  
Homotopy Theory ◽  
New Class ◽  
Homotopy Type Theory ◽  
Inductive Type ◽  
Higher Category Theory ◽  
Inductive Types

AbstractHomotopy type theory is an extension of Martin-Löf type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type is proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches—syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.

scholarly journals Homotopy type-theoretic interpretations of constructive set theories

2019 ◽  
pp. 1-32
Author(s):  
Cesare Gallozzi
Keyword(s):  
Comparative Analysis ◽  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Axiom Of Choice ◽  
Homotopy Type Theory ◽  
Constructive Set Theory

Abstract We introduce a family of (k, h)-interpretations for 2 ≤ k ≤ ∞ and 1 ≤ h ≤ ∞ of constructive set theory into type theory, in which sets and formulas are interpreted as types of homotopy level k and h, respectively. Depending on the values of the parameters k and h, we are able to interpret different theories, like Aczel’s CZF and Myhill’s CST. We also define a proposition-as-hproposition interpretation in the context of logic-enriched type theories. The rest of the paper is devoted to characterising and analysing the interpretations considered. The formulas valid in the prop-as-hprop interpretation are characterised in terms of the axiom of unique choice. We also analyse the interpretations of CST into homotopy type theory, providing a comparative analysis with Aczel’s interpretation. This is done by formulating in a logic-enriched type theory the key principles used in the proofs of the two interpretations. Finally, we characterise a class of sentences valid in the (k, ∞)-interpretations in terms of the ΠΣ axiom of choice.

scholarly journals Reviving the Philosophy of Geometry

2018 ◽  
Author(s):  
David Corfield
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Great Part ◽  
Mathematical Physics ◽  
Relevant Today ◽  
Homotopy Type Theory ◽  
Philosophical Account ◽  
Hard Times ◽  
Anglophone World

In the Anglophone world, the philosophical treatment of geometry has fallen on hard times. This chapter argues that philosophy can come to a better understanding of mathematics by providing an account of modern geometry, including its development of new forms of space, both for mathematical physics and for arithmetic. It returns to the discussions of Weyl and Cassirer on geometry whose concerns are very much relevant today. A way of encompassing a great part of modern geometry via homotopy toposes is discussed, along with the `cohesive’ variant of their internal language, known as `homotopy type theory’. With these tools in place, we can now start to see what an adequate philosophical account of current geometry might look like.

Homotopy Types

2020 ◽  
pp. 77-106
Author(s):  
David Corfield
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Definite Descriptions ◽  
Homotopy Types ◽  
Homotopy Type Theory

A further innovation is the introduction of an intensional type theory. Here one need not reduce equivalence to mere identity. How two entities are the same tells us more than whether they are the same. This is explained by the homotopical aspect of HoTT, where types are taken to resemble spaces of points, paths, paths between paths, and so on. This allows us to rethink Russell’s definite descriptions. Mathematicians use a ‘generalized the’ in situations where it appears that they might be talking about a multiplicity of instances, but there is essentially a unique instance. Taken together with the ‘univalence axiom’ there results a language in which anything that can be said of a type can be said of an equivalent type. This allows homotopy type theory to become the language of choice for a structuralist, avoiding the need for any kind of abstraction away from multiple instantiations.

Sign in / Sign up

Export Citation Format

Share Document