SU\G(𝔸)/K·U
Sign Up for free Log In

Constructing Higher Inductive Types as Groupoid Quotients

Authors

Niels van der Weide
Type: Article
Publication Date: 2020-05-26
Citations: 1
DOI: https://doi.org/10.1145/3373718.3394803

Abstract

In this paper, we show that all finitary 1-truncated higher inductive types (HITs) can be constructed from the groupoid quotient. We start by defining internally a notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. We finish by constructing a biinitial object in the bicategory of algebras in groupoids. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.

Locations

  • arXiv (Cornell University)
    View PDF
  • Radboud Repository (Radboud University)
    View PDF

Ask a Question About This Paper

Summary

Login to see paper summary

Constructing Higher Inductive Types as Groupoid Quotients

2021-01-01
Niccolò Veltri , Niels van der Weide
In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. … In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.

Constructing Higher Inductive Types as Groupoid Quotients

2021-04-22
Niccolò Veltri , Niels van der Weide
In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. … In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.
View PDF Chat

Higher inductive types in $(\infty,1)$-categories

2024-10-23
Taichi Uemura
We propose a definition of higher inductive types in $(\infty,1)$-categories with finite limits. We show that the $(\infty,1)$-category of $(\infty,1)$-categories with higher inductive types is finitarily presentable. In particular, the … We propose a definition of higher inductive types in $(\infty,1)$-categories with finite limits. We show that the $(\infty,1)$-category of $(\infty,1)$-categories with higher inductive types is finitarily presentable. In particular, the initial $(\infty,1)$-category with higher inductive types exists. We prove a form of canonicity: the global section functor for the initial $(\infty,1)$-category with higher inductive types preserves higher inductive types.
View PDF Chat

Finitary Higher Inductive Types in the Groupoid Model

2018-04-01
Peter Dybjer , Hugo Moeneclaey
A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces … A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces too. We restrict attention to finitary higher inductive types and present general schemata for the types of their point, path, and surface constructors. We also derive the elimination and equality rules from the types of constructors for 1-hits and 2-hits. Moreover, we construct a groupoid model for dependent type theory with 2-hits and point out that we obtain a setoid model for dependent type theory with 1-hits by truncating the groupoid model.
View PDF Chat

Type-Theoretic Signatures for Algebraic Theories and Inductive Types

2022-01-01
András Kovács
Summary of Thesis This thesis develops the usage of certain type theories as specification languages for algebraic theories and inductive types. We observe that the expressive power of dependent type … Summary of Thesis This thesis develops the usage of certain type theories as specification languages for algebraic theories and inductive types. We observe that the expressive power of dependent type theories proves useful in the specification of more complicated algebraic theories. In the thesis, we describe three type theories where each typing context can be viewed as an algebraic signature, specifying sorts, operations and equations. These signatures are useful in broader mathematical contexts, but we are also concerned with potential implementation in proof assistants. In Chapter 3, we describe a way to use two-level type theory as a metalanguage for developing semantics of algebraic signatures. This makes it possible to work in a concise internal notation of a type theory, and at the same time build semantics internally to arbitrary structured categories. For example, the signature for natural number objects can be interpreted in any category with finite products. In Chapter 4, we describe finitary quotient inductive-inductive (FQII) signatures. Most type theories themselves can be specified with FQII signatures. We build a structured category of algebras for each signature, where equivalence of initiality and induction can be shown. We additionally present term algebra constructions, constructions of left adjoint functors of signature morphisms, and we describe a way to use self-describing signatures to minimize necessary metatheoretic assumptions. In Chapter 5, we describe infinitary quotient inductive-inductive signatures. These allow specification of infinitely branching trees as initial algebras. We adapt the semantics from the previous chapter. We also revisit term models, left adjoints of signature morphisms and self-description of signatures. We also describe how to build semantics of signatures internally to the theory of signatures itself, which yields numerous ways to build new signatures from existing ones. In Chapter 6, we describe higher inductive-inductive signatures. These differ from previous semantics mostly in that their intended semantics is in homotopy type theory, and allows higher-dimensional equalities. In this more general setting we only consider enough semantics to compute notions of initiality and induction for each signature.
View PDF Chat

A Whirlwind Tour of the World of $(\infty,1)$-categories

2013-01-01
Omar Antolín Camarena
This introduction to higher category theory is intended to a give the reader an intuition for what $(\infty,1)$-categories are, when they are an appropriate tool, how they fit into the … This introduction to higher category theory is intended to a give the reader an intuition for what $(\infty,1)$-categories are, when they are an appropriate tool, how they fit into the landscape of higher category, how concepts from ordinary category theory generalize to this new setting, and what uses people have put the theory to. It is a rough guide to a vast terrain, focuses on ideas and motivation, omits almost all proofs and technical details, and provides many references.

Large and Infinitary Quotient Inductive-Inductive Types

2020-05-26
András Kovács , Ambrus Kaposi
Quotient inductive-inductive types (QIITs) are generalized inductive types which allow sorts to be indexed over previously declared sorts, and allow usage of equality constructors. QIITs are especially useful for algebraic … Quotient inductive-inductive types (QIITs) are generalized inductive types which allow sorts to be indexed over previously declared sorts, and allow usage of equality constructors. QIITs are especially useful for algebraic descriptions of type theories and constructive definitions of real, ordinal and surreal numbers. We develop new metatheory for large QIITs, large elimination, recursive equations and infinitary constructors. As in prior work, we describe QIITs using a type theory where each context represents a QIIT signature. However, in our case the theory of signatures can also describe its own signature, modulo universe sizes. We bootstrap the model theory of signatures using self-description and a Church-coded notion of signature, without using complicated raw syntax or assuming an existing internal QIIT of signatures. We give semantics to described QIITs by modeling each signature as a finitely complete CwF (category with families) of algebras. Compared to the case of finitary QIITs, we additionally need to show invariance under algebra isomorphisms in the semantics. We do this by modeling signature types as isofibrations. Finally, we show by a term model construction that every QIIT is constructible from the syntax of the theory of signatures.
View PDF Chat

Squiggoling with Bialgebras: Recursion Schemes from Comonads Revisited

2013-05-30
Ralf Hinze , Nicolas Wu

Signatures and Induction Principles for Higher Inductive-Inductive Types

2019-01-01
Ambrus Kaposi , András Kovács
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed … Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.
View PDF Chat

An inductive model structure for strict ∞-categories

2024-12-01
Simon Henry , Félix Loubaton

Functors with Initial Algebras or Terminal Coalgebras

2025-01-30

One-sorted algebraic categories

2010-11-18
J. Adámek , Jir̆ı́ Rosický , E. M. Vitale
A summary 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. A summary 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.

CATEGORIES OF ALGEBRAS

2002-10-01

Cartesian closure — Higher types in categories

1986-01-01
Axel Poigné

Ranges of functors in algebra

2018-01-01
Friedrich Wehrung

Universal Algebra in UniMath

2021-01-01
Gianluca Amato , Marco Maggesi , Cosimo Perini Brogi
We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to implement term algebras … We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories, and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic.
View PDF Chat

Higher theories of algebraic structures

2016-01-01
Takuo Matsuoka
The notion of (symmetric) coloured operad or "multicategory" can be obtained from the notion of commutative algebra through a certain general process which we call "theorization" (where our term comes … The notion of (symmetric) coloured operad or "multicategory" can be obtained from the notion of commutative algebra through a certain general process which we call "theorization" (where our term comes from an analogy with William Lawvere's notion of algebraic theory). By exploiting the inductivity in the structure of higher associativity, we obtain the notion of "$n$-theory" for every integer $n\ge 0$, which inductively "theorizes" $n$ times, the notion of commutative algebra. As a result, (coloured) morphism between $n$-theories is a "graded" and "enriched" generalization of ($n-1$)-theory. The inductive hierarchy of those "higher theories" extends in particular, the hierarchy of higher categories. Indeed, theorization turns out to produce more general kinds of structure than the process of categorification in the sense of Louis Crane does. In a part of low "theoretic" order of this hierarchy, graded and enriched $1$- and $0$-theories vastly generalize symmetric, braided, and many other kinds of enriched multicategories and their algebras in various places. We make various constructions of/with higher theories, and obtain some fundamental notions and facts. We also find iterated theorizations of more general kinds of algebraic structure including (coloured) properad of Bruno Vallette and various kinds of topological field theory (TFT). We show that a "TFT" in the extended context can reflect a datum of a very different type from a TFT in the conventional sense, despite close formal similarity of the notions. This work is intended to illustrate use of simple understanding of higher coherence for associativity.

A Note on Algebras of Finite Uniserial Type

1997-02-01
Klaus Bongartz

Globular Multicategories with Homomorphism Types

2020-01-01
Christopher J. Dean
We introduce a notion of globular multicategory with homomorphism types. These structures arise when organizing collections of "higher category-like" objects such as type theories with identity types. We show how … We introduce a notion of globular multicategory with homomorphism types. These structures arise when organizing collections of "higher category-like" objects such as type theories with identity types. We show how these globular multicategories can be used to construct various weak higher categorical structures of types and terms.
View PDF Chat

Higher Inductive Types as Homotopy-Initial Algebras

2014-02-04
Kristina Sojakova
Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs constructive type theory and abstract homotopy theory. We have a powerful interplay … Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs 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. A crucial ingredient in this new system are higher inductive types, which allow us to represent objects such as spheres, tori, pushouts, and quotients. We investigate a variant of higher inductive types whose computational behavior is determined up to a higher path. We show that in this setting, higher inductive types are characterized by the universal property of being a homotopy-initial algebra.

Constructing Higher Inductive Types as Groupoid Quotients

2021-04-22
Niccolò Veltri , Niels van der Weide
In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. … In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.
View PDF Chat

A Cubical Approach to Synthetic Homotopy Theory

2015-07-01
Daniel R. Licata , Guillaume Brunerie
Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe … Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe higher-dimensional paths.While some aspects of homotopy theory have been developed synthetically and formalized in proof assistants, some seemingly easy examples have proved difficult because the required manipulations of paths becomes complicated.In this paper, we describe a cubical approach to developing homotopy theory within type theory.The identity type is complemented with higher-dimensional cube types, such as a type of squares, dependent on four points and four lines, and a type of three-dimensional cubes, dependent on the boundary of a cube.Path-over-a-path types and higher generalizations are used to describe cubes in a fibration over a cube in the base.These higher-dimensional cube and path-over types can be defined from the usual identity type, but isolating them as independent conceptual abstractions has allowed for the formalization of some previously difficult examples.
View PDF Chat

The groupoid model refutes uniqueness of identity proofs

2002-12-17
Martin Hofmann , Thomas Streicher
We give a model of intensional Martin-Lof type theory based on groupoids and fibrations of groupoids in which identity types may contain two distinct elements which are not even prepositionally … We give a model of intensional Martin-Lof type theory based on groupoids and fibrations of groupoids in which identity types may contain two distinct elements which are not even prepositionally equal. This shows that the principle of uniqueness of identity proofs is not derivable in the syntax.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>

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

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

Univalent categories and the Rezk completion

2015-01-19
Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman
We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition … We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.
View PDF Chat

Two-dimensional monad theory

1989-07-01
Robert Blackwell , G. M. Kelly , John Power

A Coherent Approach to Pseudomonads

2000-06-01
Stephen Lack

Biequivalences in tricategories

2011-01-01
Nick Gurski
We show that every internal biequivalence in a tricategory T is part of a biadjoint biequivalence. We give two applications of this result, one for transporting monoidal structures and one … We show that every internal biequivalence in a tricategory T is part of a biadjoint biequivalence. We give two applications of this result, one for transporting monoidal structures and one for equipping a monoidal bicategory with invertible objects with a coherent choice of those inverses.

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.
View PDF Chat

Constructing the propositional truncation using non-recursive HITs

2016-01-12
Floris van Doorn
In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive … In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.
View PDF Chat

Constructions with Non-Recursive Higher Inductive Types

2016-07-05
Nicolai Kraus
Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to … Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify over elements or paths in H. The advantage of non-recursive HITs is that their elimination principles are easier to apply than those of general HITs.
View PDF Chat

The real projective spaces in homotopy type theory

2017-06-01
Ulrik Buchholtz , Egbert Rijke
Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about … Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> , as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">-1</sup> to be the empty type. In the inductive step, we take ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n+1</sup> to be the mapping cone of the projection map of the tautological bundle of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> , and we use its universal property and the univalence axiom to define the tautological bundle on ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n+1</sup> . By showing that the total space of the tautological bundle of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> is the n-sphere S <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> , we retrieve the classical description of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n+1</sup> as ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> with an (n + 1)-disk attached to it. The infinite dimensional real projective space ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">∞</sup> , defined as the sequential colimit of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(ℤ/2ℤ, 1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in homotopy type theory further illustrate the utility of homotopy type theory, including the interplay of type theoretic and homotopy theoretic ideas.
View PDF Chat

Displayed Categories

2017-01-01
Benedikt Ahrens , Peter LeFanu Lumsdaine
We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but … We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.
View PDF Chat

Finitary Higher Inductive Types in the Groupoid Model

2018-04-01
Peter Dybjer , Hugo Moeneclaey
A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces … A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces too. We restrict attention to finitary higher inductive types and present general schemata for the types of their point, path, and surface constructors. We also derive the elimination and equality rules from the types of constructors for 1-hits and 2-hits. Moreover, we construct a groupoid model for dependent type theory with 2-hits and point out that we obtain a setoid model for dependent type theory with 1-hits by truncating the groupoid model.
View PDF Chat

Univalent Higher Categories via Complete Semi-Segal Types

2018-01-07
Paolo Capriotti , Nicolai Kraus
Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (Ahrens … Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (Ahrens et al. 2015) solves this by considering only truncated types, and it roughly corresponds to an ordinary category. The drawback is that univalent categories fail to capture many naturally occurring structures, such as type universes or the type of univalent categories themselves. This stems from the fact that the natural notion of a category in homotopy type theory is not that of an ordinary, but rather a higher category.

Constructing quotient inductive-inductive types

2019-01-02
Ambrus Kaposi , András Kovács , Thorsten Altenkirch
Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In … Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher inductive-inductive type. An example of a QIIT is the well-typed (intrinsic) syntax of type theory quotiented by conversion. In this paper first we specify finitary QIITs using a domain-specific type theory which we call the theory of signatures. The syntax of the theory of signatures is given by a QIIT as well. Then, using this syntax we show that all specified QIITs exist and they have a dependent elimination principle. We also show that algebras of a signature form a category with families (CwF) and use the internal language of this CwF to show that dependent elimination is equivalent to initiality.
View PDF Chat

Higher inductive types in cubical computational type theory

2019-01-02
Evan Cavallo , Robert Harper
Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory … Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory does not specify the computational behavior of HITs. Computational interpretations have now been provided for univalence and specific HITs by way of cubical type theories, which use a judgmental infrastructure of dimension variables. We extend the cartesian cubical computational type theory introduced by Angiuli et al. with a schema for indexed cubical inductive types (CITs), an adaptation of higher inductive types to the cubical setting. In doing so, we isolate the canonical values of a cubical inductive type and prove a canonicity theorem with respect to these values.
View PDF Chat

Bicategories in Univalent Foundations

2019-06-01
Benedikt Ahrens , Dan Frumin , Marco Maggesi +1 more
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples … We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of those, we develop the notion of bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. To demonstrate the applicability of this notion, we prove several bicategories are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Our work is formalized in the UniMath library of univalent mathematics.

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

On Higher Inductive Types in Cubical Type Theory

2018-06-27
Thierry Coquand , Simon Huber , Anders Mörtberg
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly … Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.
View PDF Chat

Univalent higher categories via complete Semi-Segal types

2017-12-27
Paolo Capriotti , Nicolai Kraus
Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as … Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.) solves this by considering only truncated types, roughly corresponding to an ordinary category. This fails to capture many naturally occurring structures, stemming from the fact that the naturally occurring structures in homotopy type theory are not ordinary, but rather higher categories. Out of the large variety of approaches to higher category theory that mathematicians have proposed, we believe that, for type theory, the simplicial strategy is best suited. Work by Lurie and Harpaz motivates the following definition. Given the first ( n +3) levels of a semisimplicial type S , we can equip S with three properties: first, contractibility of the types of certain horn fillers; second, a completeness property; and third, a truncation condition. We call this a complete semi-Segal n -type . This is very similar to an earlier suggestion by Schreiber. The definition of a univalent (1-) category by Ahrens et al. can easily be extended or restricted to the definition of a univalent n -category (more precisely, ( n ,1)-category) for n ∈ {0,1,2}, and we show that the type of complete semi-Segal n -types is equivalent to the type of univalent n -categories in these cases. Thus, we believe that the notion of a complete semi-Segal n -type can be taken as the definition of a univalent n -category. We provide a formalisation in the proof assistant Agda using a completely explicit representation of semi-simplicial types for levels up to 4.
View PDF Chat

Cubical Type Theory: a constructive interpretation of the univalence axiom

2016-01-01
Cyril Cohen , Thierry Coquand , Simon Huber +1 more
This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in … This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.

The Integers as a Higher Inductive Type

2020-05-26
Thorsten Altenkirch , Luis Scoccola
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its … We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda.
View PDF Chat

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 simplicial model of Univalent Foundations (after Voevodsky)

2021-03-08
Krzysztof 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-Löf type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.
View PDF Chat

Studies in Logic and the Foundations of Mathematics

2008-01-01

A type-theoretical definition of weak ω-categories

2017-06-01
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.
View PDF Chat

π n (S n ) in Homotopy Type Theory

2013-01-01
Daniel R. Licata , Guillaume Brunerie