Related papers: Introduction to Homotopy Type Theory
The purpose of this survey article is to introduce the reader to a connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Martin-L\"of into…
When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties…
This is the first installment of a series of papers whose aim is to lay a foundation for homotopy probability theory by establishing its basic principles and practices. The notion of a homotopy probability space is an enrichment of the…
Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-L\"of's meaning explanations for constructive type theory define the concept of a type in…
We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional equality relation enforces…
We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky's univalent foundations. We observe for the first…
The usual homogeneous form of equality type in Martin-L\"of Type Theory contains identifications between elements of the same type. By contrast, the heterogeneous form of equality contains identifications between elements of possibly…
Homotopy Type Theory with a univalent universe $\,\mathcal{U}_0$ is interpreted at the strength of finite order arithmetic. We eliminate Grothendieck universes, avoid the axiom of replacement, and bound all uses of separation.
Covering spaces are a fundamental tool in algebraic topology because of the close relationship they bear with the fundamental groups of spaces. Indeed, they are in correspondence with the subgroups of the fundamental group: this is known as…
We provide a treatment of isomorphism within a set-theoretic formulation of dependent type theory. Type expressions are assigned their natural set-theoretic compositional meaning. Types are divided into small and large types --- sets and…
This is an introduction to the study of abstract homotopy theory by means of model categories and $(\infty,1)$-categories. The only prerequisites are very basic general topology and abstract algebra. None categorical background is needed.…
One of the prime motivation for topology was Homotopy theory, which captures the general idea of a continuous transformation between two entities, which may be spaces or maps. In later decades, an algebraic formulation of topology was…
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…
This book introduces a new context for global homotopy theory, i.e., equivariant homotopy theory with universal symmetries. Many important equivariant theories naturally exist not just for a particular group, but in a uniform way for all…
A typoid is a type equipped with an equivalence relation, such that the terms of equivalence between the terms of the type satisfy certain conditions, with respect to a given equivalence relation between them, that generalise the properties…
In this text we expose basic cases of some fundamental ideas and methods of topology. Namely, of homotopy, degree, fundamental group, covering, Whitehead invariant, etc. This is done by considering the elementary example: closed polygonal…
We construct a univalent universe in the sense of Voevodsky in some suitable model categories for homotopy types (obtained from Grothendieck's theory of test categories). In practice, this means for instance that, appart from the homotopy…
We define and develop two-level type theory (2LTT), a version of Martin-L\"of type theory which combines two different type theories. We refer to them as the inner and the outer type theory. In our case of interest, the inner theory is…
Category theory provides a means through which many far-ranging fields of mathematics can be related by their similar structure. In a paper by Robinson [2], this interconnectivity afforded by categorical perspectives allowed for the…
A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative…