Types are weak ω -groupoids

Authors

Benno van den Berg, Richard Garner

Type: Article

Publication Date: 2010-10-12

Citations: 120

DOI: https://doi.org/10.1112/plms/pdq026

View Ask PDF

Abstract

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.

Locations

Proceedings of the London Mathematical Society
View
arXiv (Cornell University)
View PDF
DataCite API
View

Ask a Question About This Paper

Summary

Monoidal weak ω-categories as models of a type theory

2022-06-27

Thibaut Benjamin

Abstract Weak $\omega$ -categories are notoriously difficult to define because of the very intricate nature of their axioms. Various approaches have been explored based on different shapes given to the … Abstract Weak $\omega$ -categories are notoriously difficult to define because of the very intricate nature of their axioms. Various approaches have been explored based on different shapes given to the cells. Interestingly, homotopy type theory encompasses a definition of weak $\omega$ -groupoid in a globular setting, since every type carries such a structure. Starting from this remark, Brunerie could extract this definition of globular weak $\omega$ -groupoids, formulated as a type theory. By refining its rules, Finster and Mimram have then defined a type theory called $\mathsf{CaTT}$ , whose models are weak $\omega$ -categories. Here, we generalize this approach to monoidal weak $\omega$ -categories. Based on the principle that they should be equivalent to weak $\omega$ -categories with only one 0-cell, we are able to derive a type theory $\mathsf{MCaTT}$ whose models are monoidal weak $\omega$ -categories. This requires changing the rules of the theory in order to encode the information carried by the unique 0-cell. The correctness of the resulting type theory is shown by defining a pair of translations between our type theory $\mathsf{MCaTT}$ and the type theory $\mathsf{CaTT}$ . Our main contribution is to show that these translations relate the models of our type theory to the models of the type theory $\mathsf{CaTT}$ consisting of $\omega$ -categories with only one 0-cell by analyzing in details how the notion of models interact with the structural rules of both type theories.

Weak ω-Categories from Intensional Type Theory

2009-01-01

Peter LeFanu Lumsdaine

The strict 𝜔-groupoid interpretation of type theory

2011-09-07

Michael A. Warren

Hofmann and Streicher showed that there is a model of the intensional form of Martin-Lof’s type theory obtained by interpreting closed types as groupoids. We show that there is also … Hofmann and Streicher showed that there is a model of the intensional form of Martin-Lof’s type theory obtained by interpreting closed types as groupoids. We show that there is also a model when closed types are interpreted as strict ω-groupoids. The nonderivability of various truncation and uniqueness principles in intensional type theory is then an immediate consequence. In the process of constructing the interpretation we develop some ω-categorical machinery including a version of the Grothendieck construction for strict ω-categories.

Chat View PDF

Modelling Martin Löf Type Theory in Categories

2010-11-12

F. Lamarche

Polynomial functors and W-types for groupoids

2018-09-01

Jakob Vidmar

This thesis contributes to the semantics of Martin-Lof type theory and the theory of polynomial functors. We do so by investigating polynomial functors on the category of groupoids and their … This thesis contributes to the semantics of Martin-Lof type theory and the theory of polynomial functors. We do so by investigating polynomial functors on the category of groupoids and their initial algebras, known as W-types. We consider several versions of polynomial functors: both simple and dependent, associated to either split, cloven or general fibrations. Our main results show the existence of W-types and their pullback stability in a variety of situations. These results are obtained working constructively, ie avoiding the use of excluded middle, the axiom of choice, power set axiom, ordinal iteration. We also extend the theory of natural models, by defining a version of them for Martin-Lof type theories where eta-equality holds up to propositional, and not definitional equality.

Weak omega-categories from intensional type theory

2010-09-17

Peter LeFanu Lumsdaine

We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. … We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.

Chat View PDF

Modeling Martin-Löf type theory in categories

2013-09-04

F. Lamarche

We present a model of Martin-Löf type theory that includes both dependent products and the identity type. It is based on the category of small categories, with cloven Grothendieck bifibrations … We present a model of Martin-Löf type theory that includes both dependent products and the identity type. It is based on the category of small categories, with cloven Grothendieck bifibrations used to model dependent types. The identity type is modeled by a path functor that seems to have independent interest from the point of view of homotopy theory. We briefly describe this modelʼs strengths and limitations.

Weakly invertible cells in a weak $ω$-category

2023-01-01

Soichiro Fujii , Keisuke Hoshino , Yuki Maehara

We study weakly invertible cells in weak $ω$-categories in the sense of Leinster, adopting Cheng's coinductive definition of weak invertibility. We show that weakly invertible cells in a weak $ω$-category … We study weakly invertible cells in weak $ω$-categories in the sense of Leinster, adopting Cheng's coinductive definition of weak invertibility. We show that weakly invertible cells in a weak $ω$-category are closed under globular pasting. Using this, we generalise elementary properties of weakly invertible cells known to hold in strict $ω$-categories to weak $ω$-categories, and show that every weak $ω$-category has a largest weak $ω$-subgroupoid.

Chat View PDF

Weakly invertible cells in a weak $\omega$-category

2024-11-16

Keisuke Hoshino , Soichiro Fujii , Yuki Maehara

We study weakly invertible cells in weak ω-categories in the sense of Batanin-Leinster, adopting the coinductive definition of weak invertibility.We show that weakly invertible cells in a weak ω-category are … We study weakly invertible cells in weak ω-categories in the sense of Batanin-Leinster, adopting the coinductive definition of weak invertibility.We show that weakly invertible cells in a weak ω-category are closed under globular pasting.Using this, we generalise elementary properties of weakly invertible cells known to hold in strict ω-categories to weak ω-categories, and show that every weak ω-category has a largest weak ω-subgroupoid.

The homotopy theory of type theories

2018-08-30

Krzysztof Kapulkin , Peter LeFanu Lumsdaine

Chat View PDF

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.

Chat View PDF

A Type Theory for Strictly Unital ∞-Categories.

2020-01-01

Eric Finster , David Reutter , Jamie Vicary

Other definitions of weak n-category

2004-07-22

Tom Leinster

The definition of weak n-category studied in the previous chapter is, of course, just one of a host of proposed definitions. Ten of them were described in my (2001b) survey, … The definition of weak n-category studied in the previous chapter is, of course, just one of a host of proposed definitions. Ten of them were described in my (2001b) survey, all except one in formal, precise terms. However, the format of that paper did not allow for serious discussion of the interrelationships, and one might get the impression from it that the ten definitions embodied eight or so completely different approaches to the subject.

An inductive model structure for strict ∞-categories

2024-12-01

Simon Henry , Félix Loubaton

The homotopy theory of type theories

2016-01-01

Chris Kapulkin , Peter LeFanu Lumsdaine

We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is … We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor $\mathrm{Cl}_\infty$ from there to the $\infty$-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.

Chat View PDF

The homotopy theory of type theories

2016-09-30

Chris Kapulkin , Peter LeFanu Lumsdaine

Chat View PDF

Topological and simplicial models of identity types

2010-01-01

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.

Chat View PDF

Axioms for Modelling Cubical Type Theory in a Topos

2017-01-01

Ian Orton , Andrew M. Pitts

The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object $I$ in a topos to give such a path-based … The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object $I$ in a topos to give such a path-based model of type theory in which paths are just functions with domain $I$. Cohen, Coquand, Huber and M\"ortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)

Chat View PDF

Models of Martin-L\"of type theory from algebraic weak factorisation systems

2019-06-04

Nicola Gambino , Marco Federico Larrea

We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Lof type theory. This is done by showing that the comprehension category associated … We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Lof type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal fibrations

Chat View PDF

A Type-Theoretical Definition of Weak {\omega}-Categories

2017-06-09

Eric Finster , Samuel Mimram

We introduce a dependent type theory whose models are weak {\omega}-categories, generalizing Brunerie's definition of {\omega}-groupoids. Our type theory is based on the definition of {\omega}-categories given by Maltsiniotis, himself … We introduce a dependent type theory whose models are weak {\omega}-categories, generalizing Brunerie's definition of {\omega}-groupoids. Our type theory is based on the definition of {\omega}-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of {\omega}-groupoids. In this setup, {\omega}-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an {\omega}-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.

Chat View PDF

Homotopical inverse diagrams in categories with attributes

2020-09-09

Krzysztof Kapulkin , Peter LeFanu Lumsdaine

Chat View PDF

Could ∞-Category Theory Be Taught to Undergraduates?

2023-04-13

Emily Riehl

Weak omega-categories from intensional type theory

2010-09-17

Peter LeFanu Lumsdaine

Chat View PDF

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.

Chat View PDF

A Cubical Language for Bishop Sets

2022-03-29

Jonathan Sterling , Carlo Angiuli , Daniel Gratzer

We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity … We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) using Artin gluing.

Chat View PDF

A rewriting coherence theorem with applications in homotopy type theory

2022-08-01

Nicolai Kraus , Jakob von Raumer

Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. … Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. This higher structure can be captured by finding a homotopy basis for the rewriting system. We show that the basic notions of confluence and wellfoundedness are sufficient to recursively build such a homotopy basis, with a construction reminiscent of an argument by Craig C. Squier. We then go on to translate this construction to the setting of homotopy type theory, where managing equalities between paths is important in order to construct functions which are coherent with respect to higher dimensions. Eventually, we apply the result to approximate a series of open questions in homotopy type theory, such as the characterisation of the homotopy groups of the free group on a set and the pushout of 1-types. This paper expands on our previous conference contribution "Coherence via Wellfoundedness" (arXiv:2001.07655) by laying out the construction in the language of higher-dimensional rewriting.

Chat View PDF

Homotopy Type Theory: The Logic of Space

2021-03-22

Michael Shulman

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

Chat View PDF

Homotopy-Theoretic Models of Type Theory

2011-01-01

Peter Arndt , Krzysztof Kapulkin

Chat View PDF

Martin-Löf complexes

2013-05-22

Steve Awodey , Pieter Hofstra , Michael A. Warren

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.

Chat View PDF

Types Are Internal ∞-Groupoids

2021-06-29

Eric Finster , Antoine Allioux , Matthieu Sozeau

By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode … By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of ∞-groupoid internal to type theory and we prove that the type of such ∞-groupoids is equivalent to the universe of types. That is, every type admits the structure of an ∞-groupoid internally, and this structure is unique.

Chat View PDF

Univalence in Higher Category Theory

2021-01-01

Nima Rasekh

Univalence was first defined in the setting of homotopy type theory by Voevodsky, who also (along with Kapulkin and Lumsdaine) adapted it to a model categorical setting, which was subsequently … Univalence was first defined in the setting of homotopy type theory by Voevodsky, who also (along with Kapulkin and Lumsdaine) adapted it to a model categorical setting, which was subsequently generalized to locally Cartesian closed presentable $\infty$-categories by Gepner and Kock. These definitions were used to characterize various $\infty$-categories as models of type theories. We give a definition for univalent morphisms in finitely complete $\infty$-categories that generalizes the aforementioned definitions and completely focuses on the $\infty$-categorical aspects, characterizing it via representability of certain functors, which should remind the reader of concepts such as adjunctions or limits. We then prove that in a locally Cartesian closed $\infty$-category (that is not necessarily presentable) univalence of a morphism is equivalent to the completeness of a certain Segal object we construct out of the morphism, characterizing univalence via internal $\infty$-categories, which had been considered in a strict setting by Stenzel. We use these results to study the connection between univalence and elementary topos theory. We also study univalent morphisms in the category of groups, the $\infty$-category of $\infty$-categories, and pointed $\infty$-categories.

Chat View PDF

From dependent type theory to higher algebraic structures

2021-01-01

Chaitanya Leena Subramaniam

The first part of this dissertation defines "dependently typed algebraic theories", which are a strict subclass of the generalised algebraic theories (GATs) of Cartmell. We characterise dependently typed algebraic theories … The first part of this dissertation defines "dependently typed algebraic theories", which are a strict subclass of the generalised algebraic theories (GATs) of Cartmell. We characterise dependently typed algebraic theories as finitary monads on certain presheaf categories, generalising a well-known result due to Lawvere, Bénabou and Linton for ordinary multisorted algebraic theories. We use this to recognise dependently typed algebraic theories for a number of classes of algebraic structures, such as small categories, n-categories, strict and weak omega-categories, planar coloured operads and opetopic sets. We then show that every locally finitely presentable category is the category of models of some dependently typed algebraic theory. Thus, with respect to their Set-models, these theories are just as expressive as GATs, essentially algebraic theories and finite limit sketches. However, dependently typed algebraic theories admit a good definition of homotopy-models in spaces, via a left Bousfield localisation of a global model structure on simplicial presheaves. Some cases, such as certain "idempotent opetopic theories", have a rigidification theorem relating homotopy-models and (strict) simplicial models. The second part of this dissertation concerns localisations of presentable $(\infty,1)$-categories. We give a definition of "pre-modulator", and show that every accessible orthogonal factorisation system on a presentable $(\infty,1)$-category can be generated from a pre-modulator by iterating a plus-construction resembling that of sheafification. We give definitions of "modulator" and "left-exact modulator", and prove that they correspond to those factorisation systems that are modalities and left-exact modalities respectively. Thus every left-exact localisation of an $\infty$-topos is obtained by iterating the plus-construction associated to a left-exact modulator.

Chat View PDF

2-Dimensional Directed Dependent Type Theory

2011-01-01

Daniel R. Licata , Robert Harper

The groupoid interpretation of dependent type theory given by Hofmann and Streicher associates to each closed type a category whose objects represent the elements of that type and whose maps … The groupoid interpretation of dependent type theory given by Hofmann and Streicher associates to each closed type a category whose objects represent the elements of that type and whose maps represent proofs of equality of elements. The categorial structure ensures that equality is reflexive (identity maps) and transitive (closure under composition); the groupoid structure, which demands that every map be invertible, ensures symmetry. Families of types are interpreted as functors; the action on maps (equality proofs) ensures that families respect equality of elements of the index type. The functorial action of a type family is computationally non-trivial in the case that the groupoid associated to the index type is non-trivial. For example, one may identity elements of a universe of sets up to isomorphism, in which case the action of a family of types indexed by sets must respect set isomorphism. The groupoid interpretation is 2-dimensional in that the coherence requirements on proofs of equality are required to hold “on the nose”, rather than up to higher dimensional equivalences. Recent work by Awodey and Lumsdaine, Voevodsky, and others extends the groupoid interpretation to higher dimensions, exposing close correspondences between type theory, higher-dimensional category theory, and homotopy theory. In this paper we consider another generalization of the groupoid interpretation that relaxes the symmetry requirement on proofs of “equivalence” to obtain a directed notion of transformation between elements of a type. Closed types may then be interpreted as categories, and families as functors that extend transformations on indices to transformations between families. Relaxing symmetry requires a reformulation of type theory to make the variances of type families explicit. The types themselves must be reinterpreted to take account of variance; for example, a type is contravariant in its domain, but covariant in its range. Whereas in symmetric type theory proofs of equivalence can be internalized using the Martin-Lof identity type, in directed type theory the two-dimensional structure must be made explicit at the judgemental level. The resulting 2-dimensional directed dependent type theory, or 2DTT, is validated by an interpretation into the strict 2-categoryCat of categories, functors, and natural transformations, generalizing the groupoid interpretation. We conjecture that 2DTT can be given semantics in a broad class of 2-categories, and can be extended to make the higher dimensional structure explicit. We illustrate the use of 2DTT for writing dependently typed programs over representations of syntax and logical systems.

Abstraction, equality and univalence

2023-07-30

Gabriel Catren

We shall propose a conceptual-oriented discussion of the so-called Univalent Foundations Program, that is, of Martin-Löf type theory enriched with a homotopic interpretation, together with the univalence axiom proposed by … We shall propose a conceptual-oriented discussion of the so-called Univalent Foundations Program, that is, of Martin-Löf type theory enriched with a homotopic interpretation, together with the univalence axiom proposed by Voevodsky. We shall argue that the type-theoretic notion of propositional equality encodes the notion of indiscernibility, we shall address the homotopic interpretation of Martin-Löf type theory, and we shall analyse whether Leibniz's principle of the identity of indiscernibles holds or not in Univalent Foundations. We shall finally argue that univalence can be understood as a particular implementation of a constructive notion of abstraction that resolves Fregean abstraction. This article is part of the theme issue 'Identity, individuality and indistinguishability in physics and mathematics'.

Chat View PDF

Martin-Löf identity types in C-systems

2023-07-31

Vladimir Voevodsky

Abstract This paper continues a series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of … Abstract This paper continues a series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of the identity types in the intensional Martin-Löf type theories on the C-systems that arise from universe categories. In the first part of the paper we develop constructions that produce interpretations of these rules from certain structures on universe categories while in the second we study the functoriality of these constructions with respect to functors of universe categories. The results of the first part of the paper play a crucial role in the construction of the univalent model of type theory in simplicial sets.

Chat View PDF

A notion of homotopy for the effective topos

2014-11-17

Jaap van Oosten

We define a notion of homotopy in the effective topos. We define a notion of homotopy in the effective topos.

Chat View PDF

Martin-Lof identity types in the C-systems defined by a universe category

2015-01-01

Vladimir Voevodsky

This paper continues the series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of the … This paper continues the series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of the identity types in the intensional Martin-Lof type theories on the C-systems that arise from universe categories. In the first part of the paper we develop constructions that produce interpretations of these rules from certain structures on universe categories while in the second we study the functoriality of these constructions with respect to functors of universe categories. The results of the first part of the paper play a crucial role in the construction of the univalent model of type theory in simplicial sets.

Chat View PDF

Algebraic models of homotopy types and the homotopy hypothesis

2016-01-01

Simon Henry

We introduce and study a notion of cylinder coherator similar to the notion of Grothendieck coherator which define more flexible notion of weak infinity groupoids. We show that each such … We introduce and study a notion of cylinder coherator similar to the notion of Grothendieck coherator which define more flexible notion of weak infinity groupoids. We show that each such cylinder coherator produces a combinatorial semi-model category of weak infinity groupoids, whose objects are all fibrant and which is in a precise sense "freely generated by an object". We show that all those semi model categories are Quillen equivalent together and Quillen to the model category of spaces. A general procedure is given to produce such coherator, and several explicit examples are presented: one which is simplicial in nature and allows the comparison to the model category for spaces. A second example can be describe as the category of globular sets endowed with "all the operations that can be defined within a weak type theory". This second notion seem to provide a definition of weak infinity groupoids which can be defined internally within type theory and which is classically equivalent to homotopy types. Finally, the category of Grothendieck infinity groupoids for a fixed Grothendieck coherator would be an example of this formalism under a seemingly simple conjecture whose validity is shown to imply Grothendieck homotopy hypothesis. This conjecture seem to sum up what needs to be proved at a technical level to ensure that the theory of Grothendieck weak infinity groupoid is well behaved.

Chat View PDF

Foundations of Algebraic Theories and Higher Dimensional Categories

2019-01-01

Soichiro Fujii

Universal algebra uniformly captures various algebraic structures, by expressing them as equational theories or abstract clones. The ubiquity of algebraic structures in mathematics and related fields has given rise to … Universal algebra uniformly captures various algebraic structures, by expressing them as equational theories or abstract clones. The ubiquity of algebraic structures in mathematics and related fields has given rise to several variants of universal algebra, such as symmetric operads, non-symmetric operads, generalised operads, and monads. These variants of universal algebra are called notions of algebraic theory. In the first part of this thesis, we develop a unified framework for notions of algebraic theory which includes all of the above examples. Our key observation is that each notion of algebraic theory can be identified with a monoidal category, in such a way that theories correspond to monoid objects therein. We introduce a categorical structure called metamodel, which underlies the definition of models of theories. We also consider morphisms between notions of algebraic theory, which are a monoidal version of profunctors. Every strong monoidal functor gives rise to an adjoint pair of such morphisms, and provides a uniform way to establish isomorphisms between categories of models in different notions of algebraic theory. A general structure-semantics adjointness result and a double categorical universal property of categories of models are also shown. In the second part of this thesis, we shift from the general study of algebraic structures, and focus on a particular algebraic structure: higher dimensional categories. Among several existing definitions of higher dimensional categories, we choose to look at the one proposed by Batanin and later refined by Leinster. We show that the notion of extensive category plays a central role in Batanin and Leinster's definition. Using this, we generalise their definition by allowing enrichment over any locally presentable extensive category.

Chat View PDF

Segal-type models of higher categories

2017-01-01

Simona Paoli

Higher category theory is an exceedingly active area of research, whose rapid growth has been driven by its penetration into a diverse range of scientific fields. Its influence extends through … Higher category theory is an exceedingly active area of research, whose rapid growth has been driven by its penetration into a diverse range of scientific fields. Its influence extends through key mathematical disciplines, notably homotopy theory, algebraic geometry and algebra, mathematical physics, to encompass important applications in logic, computer science and beyond. Higher categories provide a unifying language whose greatest strength lies in its ability to bridge between diverse areas and uncover novel applications. In this foundational work we introduce a new approach to higher categories. It builds upon the theory of iterated internal categories, one of the simplest possible higher categorical structures available, by adopting a novel and remarkably simple "weak globularity" postulate and demonstrating that the resulting model provides a fully general theory of weak n-categories. The latter are among the most complex of the higher structures, and are crucial for applications. We show that this new model of "weakly globular n-fold categories" is suitably equivalent to the well studied model of weak n-categories due to Tamsamani and Simpson.

Chat View PDF

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.

Chat View PDF

Joyal's Conjecture in Homotopy Type Theory

2014-09-22

Krzysztof Kapulkin

Joyal's Conjecture asserts, in a mathematically precise way, that Martin--Lof dependent type theory gives rise to locally cartesian closed quasicategories. We prove this conjecture. Joyal's Conjecture asserts, in a mathematically precise way, that Martin--Lof dependent type theory gives rise to locally cartesian closed quasicategories. We prove this conjecture.

Topological Quantum Gates in Homotopy Type Theory

2024-07-01

David Jaz Myers , Hisham Sati , Urs Schreiber

Canonicity of Weak ω-groupoid Laws Using Parametricity Theory

2014-10-01

Marc Lasson

We show that terms witnessing a groupoid law from the ω-groupoid structure of types are all propositionally equal. Our proof reduce this problem to the unicity of the canonical point … We show that terms witnessing a groupoid law from the ω-groupoid structure of types are all propositionally equal. Our proof reduce this problem to the unicity of the canonical point in the n-th loop space and conclude using Bernardy's parametricity theory for dependent types.

Eilenberg-MacLane spaces in homotopy type theory

2014-07-14

Daniel R. Licata , Eric Finster

Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs … Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopy-theoretic theorems, in a way that is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. In this paper, we give a computer-checked construction of Eilenberg-MacLane spaces. For an abelian group G, an Eilenberg-MacLane space K(G,n) is a space (type) whose nth homotopy group is G, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in G. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far.

Chat View PDF

Polynomials in homotopy type theory as a Kleisli category

2024-12-11

Elies Harington , Samuel Mimram

Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type … Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type theory, by Finster, Mimram, Lucas and Seiller, thus resulting in a cartesian closed bicategory. We refine and extend their work in multiple directions. We begin by generalizing the construction of the free symmetric monoid monad on types in order to handle arities in an arbitrary universe. Then, we extend this monad to the (wild) category of spans of types, and thus to a comonad by self-duality. Finally, we show that the resulting Kleisli category is equivalent to the traditional category of polynomials. This thus establishes polynomials as a (homotopical) model of linear logic. In fact, we explain that it is closely related to a bicategorical model of differential linear logic introduced by Melli\`es.

Chat View PDF

A type theory for synthetic ∞-categories

2017-12-22

Emily Riehl , Michael Shulman

We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe … We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define \emph{Segal types}, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define \emph{Rezk types}, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities --- a ``local univalence'' condition. And we define \emph{covariant fibrations}, which are type families varying functorially over a Segal type, and prove a ``dependent Yoneda lemma'' that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using ``extension types'' that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.

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.

Chat View PDF

Type Theory and Homotopy

2012-01-01

Steve Awodey

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

2016-07-05

Kuen-Bang Hou , Eric Finster , Daniel R. Licata +1 more

This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result … This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.

Chat View PDF

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.

Chat View PDF

Homotopical inverse diagrams in categories with attributes

2018-08-06

Chris Kapulkin , Peter LeFanu Lumsdaine

We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct … We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct the category with attributes $C^I$ of homotopical diagrams of shape $I$ in $C$ and Reedy types over these; and we show how various logical structure ($\Pi$-types, identity types, and so on) lifts from $C$ to $C^I$. This may be seen as providing a general class of diagram models of type theory. In a companion paper The homotopy theory of type theories (arXiv:1610.00037), we apply the present results to construct semi-model structures on categories of contextual categories.

Chat View PDF

Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory

2020-01-21

Nicolai Kraus , Jakob von Raumer

Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of … Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not necessarily closed. This paper derives a principle reminiscent of induction for cycles for the case that the graph is given as the symmetric closure of a locally confluent and (co-)well-founded relation. We show that, assuming the property in question is sufficiently nice, it is enough to prove it for the empty cycle and for cycles given by local confluence. Our motivation and application is in the field of homotopy type theory, which allows us to work with the higher-dimensional structures that appear in homotopy theory and in higher category theory, making coherence a central issue. This is in particular true for quotienting - a natural operation which gives a new type for any binary relation on a type and, in order to be well-behaved, cuts off higher structure (set-truncates). The latter makes it hard to characterise the type of maps from a quotient into a higher type, and several open problems stem from this difficulty. We prove our theorem on cycles in a type-theoretic setting and use it to show coherence conditions necessary to eliminate from set-quotients into 1-types, deriving approximations to open problems on free groups and pushouts. We have formalised the main result in the proof assistant Lean.

Chat View PDF

A type-theoretical definition of weak ω-categories

2017-06-20

Eric Finster , Samuel Mimram

We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself … We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of ω-groupoids. In this setup, ω-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an ω-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.

Path categories and propositional identity types

2016-04-20

Benno van den Berg

Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky's univalent foundations and the interpretation of Martin-Lof's identity types in Quillen model categories as … Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky's univalent foundations and the interpretation of Martin-Lof's identity types in Quillen model categories as some of the highlights. In this paper we establish a connection between a natural weakening of Martin-Lof's rules for the identity types which has been considered by Cohen, Coquand, Huber and Mortberg in their work on a constructive interpretation of the univalence axiom on the one hand, and the notion of a path category, a slight variation on the classic notion of a category of fibrant objects due to Brown. This involves showing that the syntactic category associated to a type theory with weak identity types carries the structure of a path category, strengthening earlier results by Avigad, Lumsdaine and Kapulkin. In this way we not only relate a well-known concept in homotopy theory with a natural concept in logic, but also provide a framework for further developments.

Chat View PDF

A homotopy-theoretic model of function extensionality in the effective topos.

2017-01-29

Daniil Frumin , Benno van den Berg

We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance. The … We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance. The advantage of this method is that it does not require the underlying topos to be cocomplete. The resulting model category structure gives rise to a model of homotopy type theory with identity types, $\Sigma$- and $\Pi$-types, and functional extensionality. We apply the method to the effective topos with the interval object $\nabla 2$. In the resulting model structure we identify uniform inhabited objects as contractible objects, and show that discrete objects are fibrant. Moreover, we show that the unit of the discrete reflection is a homotopy equivalence and the homotopy category of fibrant assemblies is equivalent to the category of modest sets. We compare our work with the path object category construction on the effective topos by Jaap van Oosten.

Chat View PDF

Coherence via Well-Foundedness

2020-05-26

Nicolai Kraus , Jakob von Raumer

Chat View PDF

A Type-Theoretical Definition of Weak {\omega}-Categories

2017-06-09

Eric Finster , Samuel Mimram

Chat View PDF

Globular weak ω-categories as models of a type theory

2021-07-17

Thibaut Benjamin , Eric Finster , Samuel Mimram

We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $\omega$-categories, following the idea that type theories can be considered as presentations … We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $\omega$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $\omega$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $\omega$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $\omega$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories

Chat View PDF

Basic concepts of enriched category theory

1982-01-01

G. M. Kelly

Received by the editors 2004-10-30. Transmitted by Steve Lack, Ross Street and RJ Wood. Reprint published on 2005-04-23. Several typographical errors corrected 2012-05-13. 2000 Mathematics Subject Classification: 18-02, 18D10, 18D20. Received by the editors 2004-10-30. Transmitted by Steve Lack, Ross Street and RJ Wood. Reprint published on 2005-04-23. Several typographical errors corrected 2012-05-13. 2000 Mathematics Subject Classification: 18-02, 18D10, 18D20.

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.

Chat View PDF

Weak ω-Categories from Intensional Type Theory

2009-01-01

Peter LeFanu Lumsdaine

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

1998-06-01

Michael Batanin

An ω-category with all Duals is an ω-groupoid

2007-07-31

Eugenia Cheng

Homotopy Theoretic Aspects of Constructive Type Theory

2008-01-01

Michael A. Warren

Connected limits, familial representability and Artin glueing

1995-12-01

A. Carboni , Peter Johnstone

We consider the following two properties of a functor F from a presheaf topos to the category of sets: (a) F preserves connected limits, and (b) the Artin glueing of … We consider the following two properties of a functor F from a presheaf topos to the category of sets: (a) F preserves connected limits, and (b) the Artin glueing of F is again a presheaf topos. We show that these two properties are in fact equivalent. In the process, we develop a general technique for associating categorical properties of a category obtained by Artin glueing with preservation properties of the functor along which the glueing takes place. We also give a syntactic characterization of those monads on Set whose functor parts have the above properties, and whose units and multiplications are cartesian natural transformations.

The identity type weak factorisation system

2008-09-03

Nicola Gambino , Richard Garner

Chat View PDF

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.

Chat View PDF

BASIC CONCEPTS OF ENRICHED CATEGORY THEORY (London Mathematical Society Lecture Note Series, 64)

1983-01-01

Peter Johnstone

By G. M. Kelly: pp. 245. £12.50. (Cambridge University Press, 1982.) By G. M. Kelly: pp. 245. £12.50. (Cambridge University Press, 1982.)

Operads in Higher-Dimensional Category Theory

2000-01-01

Tom Leinster

The purpose of this dissertation is to set up a theory of generalized operads and multicategories, and to use it as a language in which to propose a definition of … The purpose of this dissertation is to set up a theory of generalized operads and multicategories, and to use it as a language in which to propose a definition of weak n-category. Included is a full explanation of why the proposed definition of n-category is a reasonable one, and of what happens when n=2. Generalized operads and multicategories play other parts in higher-dimensional algebra too, some of which are outlined here: for instance, they can be used to simplify the opetopic approach to n-categories expounded by Baez, Dolan and others, and are a natural language in which to discuss enrichment of categorical structures.

Chat View PDF

A survey of definitions of -category.

2002-01-01

Tom Leinster

Many people have proposed definitions of ‘weak n-category’. Ten of them are presented here. Each definition is given in two pages, with a further two pages on what happens when … Many people have proposed definitions of ‘weak n-category’. Ten of them are presented here. Each definition is given in two pages, with a further two pages on what happens when n ≤ 2. The definitions can be read independently. Chatty bibliography follows.

A homotopy-theoretic universal property of Leinster's operad for weak ω-categories

2009-05-22

Richard Garner

Abstract We explain how any cofibrantly generated weak factorisation system on a category may be equipped with a universally and canonically determined choice of cofibrant replacement. We then apply this … Abstract We explain how any cofibrantly generated weak factorisation system on a category may be equipped with a universally and canonically determined choice of cofibrant replacement. We then apply this to the theory of weak ω-categories, showing that the universal and canonical cofibrant replacement of the operad for strict ω-categories is precisely Leinster's operad for weak ω-categories.

Chat View PDF

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.

Chat View PDF

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

Authors

Abstract

Locations

Ask a Question About This Paper

Summary