Steve Awodey

Search for another author

Author Description

Ask a Question About This Mathematician

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01

Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more

Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.

View PDF Chat

Homotopy theoretic models of identity types

2008-07-14

Steve Awodey , Michael A. Warren

This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing … This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.

View PDF Chat

Structure in Mathematics and Logic: A Categorical Perspective

1996-09-01

Steve Awodey

Abstract A precise notion of ‘mathematical structure’ other than that given by model theory may prove fruitful in the philosophy of mathematics. It is shown how the language and methods … Abstract A precise notion of ‘mathematical structure’ other than that given by model theory may prove fruitful in the philosophy of mathematics. It is shown how the language and methods of category theory provide such a notion, having developed out of a structural approach in modern mathematical practice. As an example, it is then shown how the categorical notion of a topos provides a characterization of ‘logical structure’, and an alternative to the Pregean approach to logic which is continuous with the modern structural approach in mathematics.

An Answer to Hellman's Question: ‘Does Category Theory Provide a Framework for Mathematical Structuralism?’†

2004-02-01

Steve Awodey

Journal Article An Answer to Hellman's Question: 'Does Category Theory Provide a Framework for Mathematical Structuralism?'† Get access STEVE AWODEY STEVE AWODEY *Department of Philosophy, Princeton University, Princeton, N. J. … Journal Article An Answer to Hellman's Question: 'Does Category Theory Provide a Framework for Mathematical Structuralism?'† Get access STEVE AWODEY STEVE AWODEY *Department of Philosophy, Princeton University, Princeton, N. J. 08544-1006 U. S. [email protected] Search for other works by this author on: Oxford Academic Google Scholar Philosophia Mathematica, Volume 12, Issue 1, February 2004, Pages 54–64, https://doi.org/10.1093/philmat/12.1.54 Published: 01 February 2004

First-order logical duality

2012-11-26

Steve Awodey , Henrik Forssell

View PDF Chat

Natural models of homotopy type theory

2016-11-17

Steve Awodey

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 … 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.

View PDF Chat

Type Theory and Homotopy

2012-01-01

Steve Awodey

Inductive Types in Homotopy Type Theory

2012-06-01

Steve Awodey , Nicola Gambino , Kristina Sojakova

Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional … Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.

View PDF Chat

A cubical model of homotopy type theory

2018-08-10

Steve Awodey

View PDF Chat

Relating first-order set theories, toposes and categories of classes

2013-07-08

Steve Awodey , Carsten Butz , Alex Simpson +1 more

View PDF Chat

Voevodsky’s Univalence Axiom in Homotopy Type Theory

2013-09-11

Steve Awodey , Álvaro Pelayo , Michael A. Warren

In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir … In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky’s univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study. The Institute for Advanced Study in Princeton is hosting a special program during the academic year 2012-2013 on a new research theme that is based on recently discovered connections between homotopy theory, a branch of algebraic topology, and type theory, a branch of mathematical logic and theoretical computer science. In this brief paper our goal is to take a glance at these developments. For those readers who would like to learn more about them, we recommend a number of references throughout. Type theory was invented by Bertrand Russell [20], but it was first developed as a rigorous formal system by Alonzo Church [3, 4, 5]. It now has numerous applications in computer science, especially in the theory of programming languages [19]. Per Martin-Lof [15, 11, 13, 14], among others, developed a generalization of Church’s system which is now usually called dependent, constructive, or simply Martin-Lof type theory; this is the system that we consider here. It was originally intended as a rigorous framework for constructive mathematics. In type theory objects are classified using a primitive notion of type, similar to the data-types used in programming languages. And as in programming languages, these elaborately structured types can be used to express detailed specifications of the objects classified, giving rise to principles of reasoning about them. To take a simple example, the objects of a product type A × B are known to be of the form 〈a, b〉, and so one automatically knows how to form them and how to decompose them. This aspect of type

View PDF Chat

Type theory and homotopy

2010-01-01

Steve Awodey

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 … 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öf into homotopy theory, resulting in new examples of higher-dimensional categories.

Natural models of homotopy type theory

2014-06-12

Steve Awodey

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 … 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, 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.

Impredicative Encodings of (Higher) Inductive Types

2018-06-27

Steve Awodey , Jonas Frey , Sam Speight

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit … Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.

View PDF Chat

Topological completeness for higher-order logic

2000-09-01

Steve Awodey , Carsten Butz

Abstract Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces—so-called “topological semantics”. The first is … Abstract Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces—so-called “topological semantics”. The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.

View PDF Chat

A Brief Introduction to Algebraic Set Theory

2008-09-01

Steve Awodey

Abstract This brief article is intended to introduce the reader to the field of algebraic set theory, in which models of set theory of a new and fascinating kind are … Abstract This brief article is intended to introduce the reader to the field of algebraic set theory, in which models of set theory of a new and fascinating kind are determined algebraically. The method is quite robust, applying to various classical, intuitionistic, and constructive set theories. Under this scheme some familiar set theoretic properties are related to algebraic ones, while others result from logical constraints. Conventional elementary set theories are complete with respect to algebraic models, which arise in a variety of ways, such as topologically, type-theoretically, and through variation. Many previous results from topos theory involving realizability, permutation, and sheaf models of set theory are subsumed, and the prospects for further such unification seem bright.

View PDF Chat

Homotopy-Initial Algebras in Type Theory

2017-01-30

Steve Awodey , Nicola Gambino , Kristina Sojakova

We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a … We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition that replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterizes the types that are equivalent to W-types as homotopy-initial algebras.

View PDF Chat

Relating First-Order Set Theories and Elementary Toposes

2007-09-01

Steve Awodey , Carsten Butz , Alex Simpson +1 more

Abstract We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our … Abstract We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo–Fraenkel set theory (IZF).

View PDF Chat

Lawvere–Tierney sheaves in Algebraic Set Theory

2009-06-16

Steve Awodey , Nicola Gambino , Peter LeFanu Lumsdaine +1 more

We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that … We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we consider sheaves as determined by Lawvere-Tierney coverages, rather than by Grothendieck coverages, and assume only a weakening of the axioms for small maps originally introduced by Joyal and Moerdijk, thus subsuming the existing topos-theoretic results.

View PDF Chat

Sheaf representation for topoi

2000-01-01

Steve Awodey

Carnap’s quest for analyticity: the <i>Studies in Semantics</i>

2007-12-20

Steve Awodey

Carnap's project to construct a comprehensive language of science, which occupied his attention from about 1935 to 1945, was centered on his search for a satisfactory definition of logical truth, … Carnap's project to construct a comprehensive language of science, which occupied his attention from about 1935 to 1945, was centered on his search for a satisfactory definition of logical truth, or analyticity. The need for such a definition grew out of the logical syntax program he had first conceived in early 1931, which dropped the conception of meaning of Wittgenstein's Tractatus (1922) and instead applied the metalinguistic methods of Hilbert, Tarski, and Gödel to the scientific language as a whole.

Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory

2011-09-04

Steve Awodey , Richard Garner , Per Martin-Löf +1 more

Over the past few years it has become apparent that there is a surprising and deep connection between constructive logic and higherdimensional structures in algebraic topology and category theory, in … Over the past few years it has become apparent that there is a surprising and deep connection between constructive logic and higherdimensional structures in algebraic topology and category theory, in the form of an interpretation of the dependent type theory of Per Martin-Löf into classical homotopy theory. The interpretation results in a bridge between the worlds of constructive and classical mathematics which promises to shed new light on both. This mini-workshop brought together researchers in logic, topology, and cognate fields in order to explore both theoretical and practical ramifications of this discovery.

View PDF Chat

Topological Completeness for Higher-Order Logic

1997-01-21

Steve Awodey , Carsten Butz

Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces - so-called "topological semantics". The first … Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces - so-called "topological semantics". The first is classical higher order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.

View PDF Chat

Topological Completeness for Higher-Order Logic

1997-07-24

Steve Awodey , Carsten Butz

Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces---so-called ``topological semantics''. The first is classical … Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces---so-called ``topological semantics''. The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.

Univalence as a principle of logic

2018-06-30

Steve Awodey

Inductive types in homotopy type theory

2012-01-18

Steve Awodey , Nicola Gambino , Kristina Sojakova

From Sets to Types, to Categories, to Sets

2011-01-01

Steve Awodey

View PDF Chat

A cubical model of homotopy type theory

2016-07-21

Steve Awodey

We construct an algebraic weak factorization system $(L, R)$ on the cartesian cubical sets, in which the canonical path object factorization $A \to A^I \to A\times A$ induced by the … We construct an algebraic weak factorization system $(L, R)$ on the cartesian cubical sets, in which the canonical path object factorization $A \to A^I \to A\times A$ induced by the 1-cube $I$ is an $L$-$R$ factorization for any $R$-object $A$.

Polynomial pseudomonads and dependent type theory

2018-01-01

Steve Awodey , Clive Newstead

We assemble polynomials in a locally cartesian closed category into a tricategory, allowing us to define the notion of a polynomial pseudomonad and polynomial pseudoalgebra. Working in the context of … We assemble polynomials in a locally cartesian closed category into a tricategory, allowing us to define the notion of a polynomial pseudomonad and polynomial pseudoalgebra. Working in the context of natural models of type theory, we prove that dependent type theories admitting a unit type and dependent sum types give rise to polynomial pseudomonads, and that those admitting dependent product types give rise to polynomial pseudoalgebras.

Sheaf Representations and Duality in Logic

2021-01-01

Steve Awodey

View PDF Chat

Kripke Semantics for Martin-L\"of's Extensional Type Theory

2011-09-27

Steve Awodey , Florian Rabe

It is well-known that simple type theory is complete with respect to non-standard set-valued models. Completeness for standard models only holds with respect to certain extended classes of models, e.g., … It is well-known that simple type theory is complete with respect to non-standard set-valued models. Completeness for standard models only holds with respect to certain extended classes of models, e.g., the class of cartesian closed categories. Similarly, dependent type theory is complete for locally cartesian closed categories. However, it is usually difficult to establish the coherence of interpretations of dependent type theory, i.e., to show that the interpretations of equal expressions are indeed equal. Several classes of models have been used to remedy this problem. We contribute to this investigation by giving a semantics that is standard, coherent, and sufficiently general for completeness while remaining relatively easy to compute with. Our models interpret types of Martin-L\"of's extensional dependent type theory as sets indexed over posets or, equivalently, as fibrations over posets. This semantics can be seen as a generalization to dependent type theory of the interpretation of intuitionistic first-order logic in Kripke models. This yields a simple coherent model theory, with respect to which simple and dependent type theory are sound and complete.

View PDF Chat

Continuity and Logical Completeness: An Application of Sheaf Theory and Topoi

2006-01-01

Steve Awodey

Homotopy type theory

2015-01-28

Steve Awodey , Robert Harper

Homotopy type theory is a recently-developed unification of previously disparate frameworks, which can serve to advance the project of formalizing and mechanizing mathematics. One framework is based on a computational … Homotopy type theory is a recently-developed unification of previously disparate frameworks, which can serve to advance the project of formalizing and mechanizing mathematics. One framework is based on a computational conception of the type of a construction, the other is based on a homotopical conception of the homotopy type of a space. The computational notion of type has its origins in Brouwer's program of intuitionism, and Church's λ-calculus, both of which sought to ground mathematics in computation (one would say "algorithm" these days). The homotopical notion comes from Grothendieck's late conception of homotopy types of spaces as represented by ∞-groupoids [Grothendieck 1983]. The computational perspective was developed most fully by Per Martin-Löf, leading in particular to his Intuitionistic Theory of Types [Martin-Löf and Sambin 1984], on which the formal system of homotopy type theory is based. The connection to homotopy theory was first hinted at in the groupoid interpretation of Hofmann and Streicher [Hofmann and Streicher 1994; 1995]. It was then made explicit by several researchers, roughly simultaneously. The connection was clinched by Voevodsky's introduction of the univalence axiom , which is motivated by the homotopical interpretation, and which relates type equality to homotopy equivalence [Kapulkin et al. 2012; Awodey et al. 2013].

View PDF Chat

Peter T. Johnstone. Sketches of an elephant: a topos theory compendium. Oxford Logic Guides, vols. 43, 44. Oxford University Press, Oxford, 2002, xxii + 1160 pp.

2005-03-01

Steve Awodey

An abstract is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content. An abstract is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.

Scheme representation for first-order logic

2018-01-23

Steve Awodey , Spencer Breiner

My research concerns a construction of "logical schemes," geometric entities which represent logical theories in much the same way that algebraic schemes represent rings. These involve two components: a semantic … My research concerns a construction of "logical schemes," geometric entities which represent logical theories in much the same way that algebraic schemes represent rings. These involve two components: a semantic spectral space and a syntactic structure sheaf. As in the algebraic case, we can recover a theory from its scheme representation (up to a conservative completion) and the structure sheaf is local in a certain logical sense. From these ane pieces we can build up a 2-category of logical schemes which share some of the nice properties of algebraic schemes.

View PDF Chat

Structuralism, Invariance, and Univalence

2018-01-18

Steve Awodey

The recent discovery of an interpretation of constructive type theory into abstract homotopy theory suggests a new approach to the foundations of mathematics with intrinsic geometric content and a computational … The recent discovery of an interpretation of constructive type theory into abstract homotopy theory suggests a new approach to the foundations of mathematics with intrinsic geometric content and a computational implementation. Voevodsky has proposed such a program, including a new axiom with both geometric and logical significance: the univalence axiom. It captures the familiar aspect of informal mathematical practice according to which one can identify isomorphic objects. This powerful addition to homotopy type theory gives the new system of foundations a distinctly structural character.

View PDF Chat

Kripke Semantics for Martin-Löf’s Extensional Type Theory

2009-01-01

Steve Awodey , Florian Rabe

View PDF Chat

Martin-L\"of Complexes

2009-06-24

Steve Awodey , Pieter Hofstra , Michael A. Warren

In this paper we define Martin-Lof complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional … In this paper we define Martin-Lof complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional Martin-Lof type theory. We then study the resulting categories of algebras for several theories. Our principal result is that there exists a cofibrantly generated Quillen model structure on the category of 1-truncated Martin-Lof complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-Lof complexes are a model of homotopy 1-types.

Martin-Löf complexes

2013-05-22

Steve Awodey , Pieter Hofstra , Michael A. Warren

Ultrasheaves and Double Negation

2004-10-01

Steve Awodey , Jonas Eliasson

Moerdijk has introduced a topos of sheaves on a category of filters. Following his suggestion, we prove that its double negation subtopos is the topos of sheaves on the subcategory … Moerdijk has introduced a topos of sheaves on a category of filters. Following his suggestion, we prove that its double negation subtopos is the topos of sheaves on the subcategory of ultrafilters—the ultrasheaves. We then use this result to establish a double negation translation of results between the topos of ultrasheaves and the topos on filters.

View PDF Chat

Impredicative Encodings of (Higher) Inductive Types

2018-01-01

Steve Awodey , Jonas Frey , Sam Speight

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit … Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit dependent eliminators. To recover {\eta} and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.

View PDF Chat

Natural Models of Homotopy Type Theory (Abstract)

2013-01-01

Steve Awodey

Voevodsky's Univalence Axiom in homotopy type theory

2013-02-19

Steve Awodey , Álvaro Pelayo , Michael A. Warren

Kripke-Joyal forcing for type theory and uniform fibrations

2021-01-01

Steve Awodey , Nicola Gambino , Sina Hazratpour

We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way … We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.

View PDF Chat

On Hofmann-Streicher universes

2022-01-01

Steve Awodey

We have another look at the construction by Hofmann and Streicher of a universe $(U,{\mathsf{E}l})$ for the interpretation of Martin-L\"of type theory in a presheaf category $\psh{\C}$. It turns out … We have another look at the construction by Hofmann and Streicher of a universe $(U,{\mathsf{E}l})$ for the interpretation of Martin-L\"of type theory in a presheaf category $\psh{\C}$. It turns out that $(U,{\mathsf{E}l})$ can be described as the \emph{categorical nerve} of the classifier $\dot{\Set}^{\mathsf{op}} \to \op{\Set}$ for discrete fibrations in $\Cat$, where the nerve functor is right adjoint to the so-called ``Grothendieck construction'' taking a presheaf $P : \op{\C}\to\Set$ to its category of elements $\int_\C P$. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.

View PDF Chat

A proposition is the (homotopy) type of its proofs

2017-01-01

Steve Awodey

An introduction and survey of homotopy type theory in honor of W.W. Tait. An introduction and survey of homotopy type theory in honor of W.W. Tait.

View PDF Chat

A proposition is the (homotopy) type of its proofs

2017-01-08

Steve Awodey

Martin-Löf Complexes

2009-06-25

Steve Awodey , Pieter Hofstra , Michael A. Warren

Abstract In this paper we define Martin-Lof complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of … Abstract In this paper we define Martin-Lof complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional Martin-Lof type theory. We then study the resulting categories of algebras for several theories. Our principal result is that there exists a cofibrantly generated Quillen model structure on the category of 1-truncated Martin-Lof complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-Lof complexes are a model of homotopy 1-types.

Scheme representation for first-order logic

2013-01-01

Steve Awodey , Spencer Breiner

In this work, we present a construction of \logical schemes, geometric entities which represent logical theories in much the same way that algebraic schemes represent rings. These also involve two … In this work, we present a construction of \logical schemes, geometric entities which represent logical theories in much the same way that algebraic schemes represent rings. These also involve two components: a semantic spectral space and a syntactic structure sheaf. As in the algebraic case, we can recover a theory from its scheme representation (up to a conservative completion) and the structure sheaf is local in a certain logical sense. From these ane pieces we can build up a 2-category of logical schemes which share some of the nice properties of algebraic schemes. The \logical spectrum of a

Sheaf Representations and Duality in Logic

2020-01-01

Steve Awodey

The fundamental duality theories relating algebra and geometry that were discovered in the mid-20th century can also be applied to logic via its algebraization under categorical logic. They thereby result … The fundamental duality theories relating algebra and geometry that were discovered in the mid-20th century can also be applied to logic via its algebraization under categorical logic. They thereby result in known and new completeness theorems. This idea can be taken even further via what is sometimes called ``categorification'' to establish a new connection between logic and geometry, a glimpse of which can also be had in topos theory.

On Hofmann–Streicher universes

2024-09-19

Steve Awodey

Abstract We take another look at the construction by Hofmann and Streicher of a universe $(U,{\mathcal{E}l})$ for the interpretation of Martin-Löf type theory in a presheaf category $[{{{\mathbb{C}}}^{\textrm{op}}},\textsf{Set}]$ . It … Abstract We take another look at the construction by Hofmann and Streicher of a universe $(U,{\mathcal{E}l})$ for the interpretation of Martin-Löf type theory in a presheaf category $[{{{\mathbb{C}}}^{\textrm{op}}},\textsf{Set}]$ . It turns out that $(U,{\mathcal{E}l})$ can be described as the nerve of the classifier $\dot{{\textsf{Set}}}^{\textsf{op}} \rightarrow{{\textsf{Set}}}^{\textsf{op}}$ for discrete fibrations in $\textsf{Cat}$ , where the nerve functor is right adjoint to the so-called “Grothendieck construction” taking a presheaf $P :{{{\mathbb{C}}}^{\textrm{op}}}\rightarrow{\textsf{Set}}$ to its category of elements $\int _{\mathbb{C}} P$ . We also consider change of base for such universes, as well as universes of structured families, such as fibrations.

Kripke-Joyal forcing for type theory and uniform fibrations

2024-07-31

Steve Awodey , Nicola Gambino , Sina Hazratpour

Abstract We introduce a new method for precisely relating algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise … Abstract We introduce a new method for precisely relating algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.

View PDF Chat

The equivariant model structure on cartesian cubical sets

2024-06-26

Steve Awodey , Evan Cavallo , Thierry Coquand +2 more

We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over … We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over the cartesian cube category, a well-behaved Eilenberg-Zilber category. The key innovation is an additional equivariance condition in the specification of the cubical Kan fibrations, which can be described as the pullback of an interval-based class of uniform fibrations in the category of symmetric sequences of cubical sets. The main technical results in the development of our model have been formalized in a computer proof assistant.

View PDF Chat

Cartesian cubical model categories

2023-01-01

Steve Awodey

The category of Cartesian cubical sets is introduced and endowed with a Quillen model structure using ideas coming from recent constructions of cubical systems of univalent type theory. The category of Cartesian cubical sets is introduced and endowed with a Quillen model structure using ideas coming from recent constructions of cubical systems of univalent type theory.

View PDF Chat

On Hofmann-Streicher universes

2022-01-01

Steve Awodey

View PDF Chat

Sheaf Representations and Duality in Logic

2021-01-01

Steve Awodey

View PDF Chat

Kripke-Joyal forcing for type theory and uniform fibrations

2021-01-01

Steve Awodey , Nicola Gambino , Sina Hazratpour

View PDF Chat

Sheaf Representations and Duality in Logic

2020-01-01

Steve Awodey

A cubical model of homotopy type theory

2018-08-10

Steve Awodey

View PDF Chat

Univalence as a principle of logic

2018-06-30

Steve Awodey

Impredicative Encodings of (Higher) Inductive Types

2018-06-27

Steve Awodey , Jonas Frey , Sam Speight

View PDF Chat

Scheme representation for first-order logic

2018-01-23

Steve Awodey , Spencer Breiner

View PDF Chat

Structuralism, Invariance, and Univalence

2018-01-18

Steve Awodey

View PDF Chat

Polynomial pseudomonads and dependent type theory

2018-01-01

Steve Awodey , Clive Newstead

Impredicative Encodings of (Higher) Inductive Types

2018-01-01

Steve Awodey , Jonas Frey , Sam Speight

View PDF Chat

Homotopy-Initial Algebras in Type Theory

2017-01-30

Steve Awodey , Nicola Gambino , Kristina Sojakova

View PDF Chat

A proposition is the (homotopy) type of its proofs

2017-01-08

Steve Awodey

A proposition is the (homotopy) type of its proofs

2017-01-01

Steve Awodey

An introduction and survey of homotopy type theory in honor of W.W. Tait. An introduction and survey of homotopy type theory in honor of W.W. Tait.

View PDF Chat

Natural models of homotopy type theory

2016-11-17

Steve Awodey

View PDF Chat

A cubical model of homotopy type theory

2016-07-21

Steve Awodey

A cubical model of homotopy type theory

2016-01-01

Steve Awodey

View PDF Chat

Homotopy-initial algebras in type theory

2015-04-21

Steve Awodey , Nicola Gambino , Kristina Sojakova

We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a … We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.

Introduction – from type theory and homotopy theory to univalent foundations

2015-03-10

Steve Awodey , Nicola Gambino , Erik Palmgren

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 … 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.

View PDF Chat

Homotopy type theory

2015-01-28

Steve Awodey , Robert Harper

View PDF Chat

Homotopy-initial algebras in type theory

2015-01-01

Steve Awodey , Nicola Gambino , Kristina Sojakova

We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a … We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.

View PDF Chat

Natural models of homotopy type theory

2014-06-12

Steve Awodey

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 … 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, 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.

Natural models of homotopy type theory

2014-01-01

Steve Awodey

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 … 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, 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.

View PDF Chat

Topos Semantics for Higher-Order Modal Logic

2014-01-01

Steve Awodey , Kohei Kishida , Hans-Christoph Kotzsch

We define the notion of a model of higher-order modal logic in an arbitrary elementary topos $\mathcal{E}$. In contrast to the well-known interpretation of (non-modal) higher-order logic, the type of … We define the notion of a model of higher-order modal logic in an arbitrary elementary topos $\mathcal{E}$. In contrast to the well-known interpretation of (non-modal) higher-order logic, the type of propositions is not interpreted by the subobject classifier $\Omega_{\mathcal{E}}$, but rather by a suitable complete Heyting algebra $H$. The canonical map relating $H$ and $\Omega_{\mathcal{E}}$ both serves to interpret equality and provides a modal operator on $H$ in the form of a comonad. Examples of such structures arise from surjective geometric morphisms $f : \mathcal{F} \to \mathcal{E}$, where $H = f_\ast \Omega_{\mathcal{F}}$. The logic differs from non-modal higher-order logic in that the principles of functional and propositional extensionality are no longer valid but may be replaced by modalized versions. The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modal logic are subsumed by this notion.

View PDF Chat

Voevodsky’s Univalence Axiom in Homotopy Type Theory

2013-09-11

Steve Awodey , Álvaro Pelayo , Michael A. Warren

View PDF Chat

Relating first-order set theories, toposes and categories of classes

2013-07-08

Steve Awodey , Carsten Butz , Alex Simpson +1 more

View PDF Chat

Martin-Löf complexes

2013-05-22

Steve Awodey , Pieter Hofstra , Michael A. Warren

Voevodsky's Univalence Axiom in homotopy type theory

2013-02-19

Steve Awodey , Álvaro Pelayo , Michael A. Warren

Natural Models of Homotopy Type Theory (Abstract)

2013-01-01

Steve Awodey

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01

Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more

View PDF Chat

Scheme representation for first-order logic

2013-01-01

Steve Awodey , Spencer Breiner

Voevodsky's Univalence Axiom in homotopy type theory

2013-01-01

Steve Awodey , Álvaro Pelayo , Michael A. Warren

View PDF Chat

First-order logical duality

2012-11-26

Steve Awodey , Henrik Forssell

View PDF Chat

Inductive Types in Homotopy Type Theory

2012-06-01

Steve Awodey , Nicola Gambino , Kristina Sojakova

View PDF Chat

Inductive types in homotopy type theory

2012-01-18

Steve Awodey , Nicola Gambino , Kristina Sojakova

Type Theory and Homotopy

2012-01-01

Steve Awodey

Inductive types in homotopy type theory

2012-01-01

Steve Awodey , Nicola Gambino , Kristina Sojakova

Homotopy type theory is an interpretation of Martin-Löf's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional … Homotopy type theory is an interpretation of Martin-Löf's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.

Kripke Semantics for Martin-L\"of's Extensional Type Theory

2011-09-27

Steve Awodey , Florian Rabe

View PDF Chat

Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory

2011-09-04

Steve Awodey , Richard Garner , Per Martin-Löf +1 more

View PDF Chat

From Sets to Types, to Categories, to Sets

2011-01-01

Steve Awodey

View PDF Chat

Type theory and homotopy

2010-01-01

Steve Awodey

Martin-Löf Complexes

2009-06-25

Steve Awodey , Pieter Hofstra , Michael A. Warren

Martin-L\"of Complexes

2009-06-24

Steve Awodey , Pieter Hofstra , Michael A. Warren

Lawvere–Tierney sheaves in Algebraic Set Theory

2009-06-16

Steve Awodey , Nicola Gambino , Peter LeFanu Lumsdaine +1 more

View PDF Chat

Martin-Löf Complexes

2009-01-01

Steve Awodey , Pieter Hofstra , Michael A. Warren

In this paper we define Martin-Löf complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional … In this paper we define Martin-Löf complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional Martin-Löf type theory. We then study the resulting categories of algebras for several theories. Our principal result is that there exists a cofibrantly generated Quillen model structure on the category of 1-truncated Martin-Löf complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-Löf complexes are a model of homotopy 1-types.

Kripke Semantics for Martin-Löf’s Extensional Type Theory

2009-01-01

Steve Awodey , Florian Rabe

View PDF Chat

Coauthor	Papers Together
Nicola Gambino	11
Michael A. Warren	9
Kristina Sojakova	7
Carsten Butz	6
Pieter Hofstra	5
Álvaro Pelayo	4
Vladimir Voevodsky	2
Per Martin-Löf	2
Sam Speight	2
Richard Garner	2
Sina Hazratpour	2
Alex Simpson	2
Spencer Breiner	2
Peter LeFanu Lumsdaine	2
Emily Riehl	2
Erik Palmgren	2
Thomas Streicher	2
Robert Harper	2
Thierry Coquand	2
Jonas Frey	2
Florian Rabe	2
Martı́n Hötzel Escardó	1
Peter Aczel	1
Peter Dybjer	1
Thorsten Altenkirch	1
Michael Nahas	1
Hugo Herbelin	1
Philip Scott	1
Kuen-Bang Hou	1
Matthieu Sozeau	1
Michael Shulman	1
Andrej Bauer	1
Henrik Forssell	1
André Joyal	1
Georges Gonthier	1
Guillaume Brunerie	1
Carlo Angiuli	1
Egbert Rijke	1
Zhaohui Luo	1
Nuo Li	1
Martin Hofmann	1
Christian Sattler	1
Robert L. Constable	1
Cyril Cohen	1
Dana Scott	1
M.A. Warren	1
Sergei Soloviev	1
Pierre-Louis Curien	1
Thomas Hales	1
Bruno Barras	1

Homotopy theoretic models of identity types

2008-07-14

Steve Awodey , Michael A. Warren

View PDF Chat

Sheaves in Geometry and Logic

1994-01-01

Saunders Mac Lane , Ieke Moerdijk

Types are weak <i>ω</i> -groupoids

2010-10-12

Benno van den Berg , Richard Garner

We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower … We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.

View PDF Chat

The identity type weak factorisation system

2008-09-03

Nicola Gambino , Richard Garner

View PDF Chat

On the interpretation of type theory in locally cartesian closed categories

1995-01-01

Martin Hofmann

Topological and Simplicial Models of Identity Types

2012-01-01

Benno van den Berg , Richard Garner

In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do … In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren [2009], which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorization system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a slightly richer structure, which we call a homotopy-theoretic model of identity types , and to prove that this is sufficient for a sound interpretation. Now, although both Top and SSet are categories endowed with a weak factorization system---and indeed, an entire Quillen model structure---exhibiting the additional structure required for a homotopy-theoretic model is quite hard to do. However, the categories we are interested in share a number of common features, and abstracting these leads us to introduce the notion of a path object category . This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the construction of homotopy-theoretic models. Now by exhibiting suitable path object structures on Top and SSet , we endow those categories with the structure of a homotopy-theoretic model and, in this way, obtain the desired topological and simplicial models of identity types.

View PDF Chat

Locally cartesian closed categories and type theory

1984-01-01

R. A. G. Seely

It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/ A are cartesian … It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/ A are cartesian closed. In such a category, the notion of a ‘generalized set’, for example an ‘ A -indexed set’, is represented by a morphism B → A of C, i.e. by an object of C/ A . The point about such a category C is that C is a C-indexed category, and more, is a hyper-doctrine, so that it has a full first order logic associated with it. This logic has some peculiar aspects. For instance, the types are the objects of C and the terms are the morphisms of C. For a given type A , the predicates with a free variable of type A are morphisms into A , and ‘proofs’ are morphisms over A . We see here a certain ‘ambiguity’ between the notions of type, predicate, and term, of object and proof: a term of type A is a morphism into A , which is a predicate over A ; a morphism 1 → A can be viewed either as an object of type A or as a proof of the proposition A .

Weak ω-Categories from Intensional Type Theory

2009-01-01

Peter LeFanu Lumsdaine

Type theories, toposes and constructive set theory: predicative aspects of AST

2002-04-01

Ieke Moerdijk , Erik Palmgren

View PDF Chat

Wellfounded trees in categories

2000-07-01

Ieke Moerdijk , Erik Palmgren

An extension of the Galois theory of Grothendieck

1984-01-01

André Joyal , Myles Tierney

A model of type theory in cubical sets

2014-01-01

M Bezem , Thierry Coquand , Simon Huber

We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types … We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.

Type Theory and Homotopy

2012-01-01

Steve Awodey

Inductive Types in Homotopy Type Theory

2012-06-01

Steve Awodey , Nicola Gambino , Kristina Sojakova

View PDF Chat

Toposes as homotopy groupoids

1990-03-01

André Joyal , Ieke Moerdijk

View PDF Chat

Strong stacks and classifying spaces

1991-01-01

André Joyal , Myles Tierney

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-06-01

Daniel R. Licata , Michael Shulman

Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new … Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.

View PDF Chat

Polynomial functors and polynomial monads

2012-09-06

Nicola Gambino , Joachim Kock

We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. … We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.

View PDF Chat

Understanding the Small Object Argument

2008-04-03

Richard Garner

View PDF Chat

Sheaf representation for topoi

2000-01-01

Steve Awodey

The petit topos of globular sets

2000-12-01

Ross Street

Higher Operads, Higher Categories

2004-07-22

Tom Leinster

Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical … Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical physics, logic, and theoretical computer science. The heart of this book is the language of generalized operads. This is as natural and transparent a language for higher category theory as the language of sheaves is for algebraic geometry, or vector spaces for linear algebra. It is introduced carefully, then used to give simple descriptions of a variety of higher categorical structures. In particular, one possible definition of n-category is discussed in detail, and some common aspects of other possible definitions are established. This is the first book on the subject and lays its foundations. It will appeal to both graduate students and established researchers who wish to become acquainted with this modern branch of mathematics.

View PDF Chat

The Simplicial Model of Univalent Foundations (after Voevodsky)

2012-11-12

Chris Kapulkin , Peter LeFanu Lumsdaine

We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Lof type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

Topological and simplicial models of identity types

2010-07-27

Benno van den Berg , Richard Garner

In this paper we construct new categorical models for the identity types of Martin-L\of type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do … In this paper we construct new categorical models for the identity types of Martin-L\of type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren, which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorisation system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a slightly richer structure---which we call a homotopy-theoretic model of identity types---and to prove that this is sufficient for a sound interpretation. Now, although both Top and SSet are categories endowed with a weak factorisation system---and indeed, an entire Quillen model structure---exhibiting the additional structure required for a homotopy-theoretic model is quite hard to do. However, the categories we are interested in share a number of common features, and abstracting away from these leads us to introduce the notion of a path object category. This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the construction of homotopy-theoretic models. Now by exhibiting suitable path object structures on Top and SSet, we endow those categories with the structure of a homotopy-theoretic model: and in this way, obtain the desired topological and simplicial models of identity types.

Two-dimensional models of type theory

2009-07-02

Richard Garner

We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories. We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.

View PDF Chat

Relating First-Order Set Theories and Elementary Toposes

2007-09-01

Steve Awodey , Carsten Butz , Alex Simpson +1 more

View PDF Chat

Representing topoi by topological groupoids

1998-09-01

Carsten Butz , Ieke Moerdijk

View PDF Chat

First-order logical duality

2012-11-26

Steve Awodey , Henrik Forssell

View PDF Chat

Monoidal Globular Categories As a Natural Environment for the Theory of Weakn-Categories

1998-06-01

Michael Batanin

An experimental library of formalized Mathematics based on the univalent foundations

2015-01-20

Vladimir Voevodsky

This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started … This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).

View PDF Chat

Categories for the Working Mathematician

1971-01-01

Saunders Mac Lane

View PDF Chat

Wellfounded Trees and Dependent Polynomial Functors

2004-01-01

Nicola Gambino , Martin Hyland

View PDF Chat

La logique des topos

1981-03-01

André Boileau , André Joyal

Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de: (1) La géométrie … Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de: (1) La géométrie algébrique sous la forme élaborée par Grothendieck. (2) La logique formelle. Le point de contact s'est effectué aux environs de 1970 par W. Lawvere et M. Tierney et l'instrument de rapprochement a été la théorie des catégories, plus particulièrement la théorie des faisceaux. Depuis ce moment, une dialectique incessante imprime un mouvement dynamique à toute une série de recherches qui visent à rapprocher les méthodes suivantes: (1) Mathématique intuitionniste. (2) Forcing de Cohen et Robinson. (3) Logique algébrique. (4) Géométrie algébrique. (5) Géométrie différentielle et analytique. (6) Topologie algébrique: cohomologie, homotopie. (7) Théorie de Galois. Certains rapprochements sont dans un stade avancé, d'autres encore embryonnaires: (6) ↔ (3). La structure centrale qui joue le rôle d'élément provocateur et unificateur est celle de topos. Avant d'être axiomatisée par Lawvere, celle-ci a été étudiée systématiquement par l'école de Grothendieck (voir [1]) et c'est dans le contexte de la géométrie algébrique qu'elle fit son apparition. Dans cet article nous utiliserons cependant la définition de Lawvere telle qu'améliorée par Mikkelsen [12] et Kock [8]. Le but de ce travail est de présenter une version (au sens de la logique formelle) du concept de topos et d'examiner brièvement les rapports entre la théorie des topos, la logique et les mathématiques. Cette version a déjà été exposée par l'un des auteurs lors du Séminaire de Mathématiques Supérieures de l'Université de Montréal, à l'été 1974. Depuis elle a fait l'objet d'une thèse où elle a été améliorée et sa cohérence vérifiée [2]. Des systèmes différents ont été proposés simultanément par Fourman [4] et Coste [3].

Homotopical Algebra

1967-01-01

Daniel Quillen

View PDF Chat

The Frobenius condition, right properness, and uniform fibrations

2017-03-01

Nicola Gambino , Christian Sattler

We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can … We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can be thought of as (uniform) fibrations and that satisfy the (functorial) Frobenius condition. As applications, we obtain a new proof that the Quillen model structure for Kan complexes is right proper, avoiding entirely the use of topological realization and minimal fibrations, and we solve an open problem in the study of Voevodsky's simplicial model of type theory, proving a constructive version of the preservation of Kan fibrations by pushforward along Kan fibrations. Our results also subsume and extend work by Coquand and others on cubical sets.

View PDF Chat

Internal type theory

1996-01-01

Peter Dybjer

Varieties of Cubical Sets

2017-01-01

Ulrik Buchholtz , Edward Morehouse

Quasi-categories and Kan complexes

2002-11-01

André Joyal

Sheaves and logic

1979-01-01

Michael Fourman , Dana Scott

Higher Topos Theory (AM-170)

2009-12-31

Jacob Lurie

Higher category theory is generally regarded as technical and forbidding, but part of it is considerably more tractable: the theory of infinity-categories, higher categories in which all higher morphisms are … Higher category theory is generally regarded as technical and forbidding, but part of it is considerably more tractable: the theory of infinity-categories, higher categories in which all higher morphisms are assumed to be invertible. In Higher Topos Theory , Jacob Lurie presents the foundations of this theory, using the language of weak Kan complexes introduced by Boardman and Vogt, and shows how existing theorems in algebraic topology can be reformulated and generalized in the theory's new language. The result is a powerful theory with applications in many areas of mathematics. The book's first five chapters give an exposition of the theory of infinity-categories that emphasizes their role as a generalization of ordinary categories. Many of the fundamental ideas from classical category theory are generalized to the infinity-categorical setting, such as limits and colimits, adjoint functors, ind-objects and pro-objects, locally accessible and presentable categories, Grothendieck fibrations, presheaves, and Yoneda's lemma. A sixth chapter presents an infinity-categorical version of the theory of Grothendieck topoi, introducing the notion of an infinity-topos, an infinity-category that resembles the infinity-category of topological spaces in the sense that it satisfies certain axioms that codify some of the basic principles of algebraic topology. A seventh and final chapter presents applications that illustrate connections between the theory of higher topoi and ideas from classical topology.

Type theory and homotopy

2010-01-01

Steve Awodey

Univalence in Simplicial Sets

2012-01-01

Chris Kapulkin , Peter LeFanu Lumsdaine , Vladimir Voevodsky

We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations. We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.

Two Sheaf Representations of Elementary Toposes.

1982-01-01

J. Lambek , Ieke Moerdijk

A1-homotopy theory of schemes

1999-12-01

Fabien Morel , Vladimir Voevodsky

View PDF Chat

Higher Inductive Types as Homotopy-Initial Algebras

2014-12-19

Kristina Sojakova

Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these … Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs.

View PDF Chat

THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS

2014-01-01

Krzysztof Kapulkin , Peter LeFanu Lumsdaine , Vladimir Voevodsky

In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique … In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique for constructing models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan bration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Univalent Foundations are at least as consistent as ZFC with two inaccessible cardinals.

Constructions of factorization systems in categories

1977-01-01

A. K. Bousfield

Bernays–Gödel type theory

2002-12-30

Carsten Butz

On the strength of dependent products in the type theory of Martin-Löf

2009-02-02

Richard Garner

View PDF Chat

Natural models of homotopy type theory

2014-06-12

Steve Awodey

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 … 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, 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.