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

Finitary Higher Inductive Types in the Groupoid Model

Authors

Peter Dybjer, Hugo Moeneclaey
Type: Article
Publication Date: 2018-04-01
Citations: 24
DOI: https://doi.org/10.1016/j.entcs.2018.03.019

Abstract

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.

Locations

  • Chalmers Research (Chalmers University of Technology)
    View PDF
  • Electronic Notes in Theoretical Computer Science
    View

Ask a Question About This Paper

Summary

Login to see paper summary

Constructing Higher Inductive Types as Groupoid Quotients

2020-05-26
Niels van der Weide
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 … 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.
View PDF Chat

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

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

Computational Higher Type Theory IV: Inductive Types

2018-01-01
Evan Cavallo , Robert Harper
This is the fourth in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type … This is the fourth in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type systems supporting a general schema of indexed cubical inductive types whose constructors may take dimension parameters and have a specified boundary. Using this schema, we are able to specify and implement many of the higher inductive types which have been postulated in homotopy type theory, including homotopy pushouts, the torus, $W$-quotients, truncations, arbitrary localizations. By including indexed inductive types, we enable the definition of identity types. The addition of higher inductive types makes computational higher type theory a model of homotopy type theory, capable of interpreting almost all of the constructions in the HoTT Book (with the exception of inductive-inductive types). This is the first such model with an explicit canonicity theorem, which specifies the canonical values of higher inductive types and confirms that every term in an inductive type evaluates to such a value.

Functions out of Higher Truncations

2015-07-04
Paolo Capriotti , Nicolai Kraus , Andrea Vezzosi
In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and … In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B which are constant on all (n+1)-st loop spaces. We give one elementary proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct set-based representations of 1-types, as long as they have braided loop spaces. The main result with one of its proofs and the application have been formalised in Agda.

Functions out of Higher Truncations

2015-07-04
Paolo Capriotti , Nicolai Kraus , Andrea Vezzosi
In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) is often useful if one does not care about the higher structure of … In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B that are constant on all (n+1)-st loop spaces. We give one elementary proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct set-based representations of 1-types, as long as they have braided loop spaces. The main result with one of its proofs and the application have been formalised in Agda.

Chapter 4: Finite Theories on Two Types

1980-01-01
Jens Erik Fenstad

Functions out of Higher Truncations

2015-01-01
Paolo Capriotti , Nicolai Kraus , Andrea Vezzosi
In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and … In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B which are constant on all (n+1)-st loop spaces. We give one "elementary" proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct "set-based" representations of 1-types, as long as they have "braided" loop spaces. The main result with one of its proofs and the application have been formalised in Agda.
View PDF Chat

The Theory of an Arbitrary Higher $λ$-Model

2021-01-01
Daniel O. Martínez-Rivillas , Ruy J. G. B. de Queiroz
One takes advantage of some basic properties of every homotopic $\lambda$-model (e.g.\ extensional Kan complex) to explore the higher $\beta\eta$-conversions, which would correspond to proofs of equality between terms of … One takes advantage of some basic properties of every homotopic $\lambda$-model (e.g.\ extensional Kan complex) to explore the higher $\beta\eta$-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher $\lambda$-terms, whose equality rules would be contained in the theory of any $\lambda$-homotopic model.
View PDF Chat

Higher inductive types in Homotopy Type Theory: applications and theory

2016-04-01
Fredrik Nordvall Forsberg

Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory

2018-10-11
Dominik Kirst , Gert Smolka

A simple type theory without platonic domains

1984-08-01
Charles S. Chihara

The Theory of an Arbitrary Higher \(\lambda\)-Model

2023-04-25
Daniel O. Martínez-Rivillas , Ruy J. G. B. de Queiroz
One takes advantage of some basic properties of every homotopic \(\lambda\)-model (e.g. extensional Kan complex) to explore the higher \(\beta\eta\)-conversions, which would correspond to proofs of equality between terms of … One takes advantage of some basic properties of every homotopic \(\lambda\)-model (e.g. extensional Kan complex) to explore the higher \(\beta\eta\)-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher \(\lambda\)-terms, whose equality rules would be contained in the theory of any \(\lambda\)-homotopic model.
View PDF Chat

A Note on LEO-II and the Basic Fragment of Simple Type Theory

2009-01-01
Christoph Benzmüller

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

Strongly determined types

1999-08-01
А. А. Иванов , Dugald Macpherson

On Higher Inductive Types in Cubical Type Theory

2018-02-04
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.

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

On Higher Inductive Types in Cubical Type Theory

2018-01-01
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

A General Syntax for Nonrecursive Higher Inductive Types.

2020-01-01
Marco Girardi , Roberto Zunino , Marco Benini

Finite sets in homotopy type theory

2018-01-08
Dan Frumin , Herman Geuvers , Léon Gondelman +1 more
We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. … We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.
View PDF Chat

Computational Higher Type Theory IV: Inductive Types

2018-01-01
Evan Cavallo , Robert Harper
This is the fourth in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type … This is the fourth in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type systems supporting a general schema of indexed cubical inductive types whose constructors may take dimension parameters and have a specified boundary. Using this schema, we are able to specify and implement many of the higher inductive types which have been postulated in homotopy type theory, including homotopy pushouts, the torus, $W$-quotients, truncations, arbitrary localizations. By including indexed inductive types, we enable the definition of identity types. The addition of higher inductive types makes computational higher type theory a model of homotopy type theory, capable of interpreting almost all of the constructions in the HoTT Book (with the exception of inductive-inductive types). This is the first such model with an explicit canonicity theorem, which specifies the canonical values of higher inductive types and confirms that every term in an inductive type evaluates to such a value.

Normalization by gluing for free λ-theories

2018-01-01
Jonathan Sterling , Bas Spitters
The connection between normalization by evaluation, logical predicates and semantic gluing constructions is a matter of folklore, worked out in varying degrees within the literature. In this note, we present … The connection between normalization by evaluation, logical predicates and semantic gluing constructions is a matter of folklore, worked out in varying degrees within the literature. In this note, we present an elementary version of the gluing technique which corresponds closely with both semantic normalization proofs and the syntactic normalization by evaluation.

Quotients, inductive types, and quotient inductive types

2022-06-07
Marcelo Fiore , Andrew M. Pitts , S. C. Steenkamp
This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories … This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.
View PDF Chat

Quotient Inductive-Inductive Types

2018-01-01
Thorsten Altenkirch , Paolo Capriotti , Gabe Dijkstra +2 more
View PDF Chat

Bicategories in Univalent Foundations

2019-03-04
Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 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 univalent bicategories, we develop the notion of `displayed bicategories', an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-category is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

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

Finite sets in homotopy type theory

2017-12-22
Dan Frumin , Herman Geuvers , Léon Gondelman +1 more
We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. … We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.
View PDF Chat

Bicategories in univalent foundations

2021-11-01
Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 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 univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.
View PDF Chat

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

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

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

Code Generation for Higher Inductive Types

2019-01-01
Paventhan Vivekanandan
View PDF Chat

Normalization by gluing for free {\lambda}-theories

2018-09-23
Jonathan Sterling , Bas Spitters
The connection between normalization by evaluation, logical predicates and semantic gluing constructions is a matter of folklore, worked out in varying degrees within the literature. In this note, we present … The connection between normalization by evaluation, logical predicates and semantic gluing constructions is a matter of folklore, worked out in varying degrees within the literature. In this note, we present an elementary version of the gluing technique which corresponds closely with both semantic normalization proofs and the syntactic normalization by evaluation.

Constructing Higher Inductive Types as Groupoid Quotients

2020-05-26
Niels van der Weide
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 … 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.
View PDF Chat

Constructing Infinitary Quotient-Inductive Types

2020-01-01
Marcelo Fiore , Andrew M. Pitts , S. C. Steenkamp
Abstract This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types … Abstract This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the combination of inductive-inductive definitions involving strictly positive occurrences of Hofmann-style quotient types, and Abel’s size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of our encoding of QW-types. The development is formalized using the Agda theorem prover.
View PDF Chat

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

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

Internal type theory

1996-01-01
Peter Dybjer

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>

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