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

Author Description

Login to generate an author description

Ask a Question About This Mathematician

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

Internalizing representation independence with univalence

2021-01-04
Carlo Angiuli , Evan Cavallo , Anders Mörtberg +1 more
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our … In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.
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.

Unifying Cubical Models of Univalent Type Theory

2020-01-01
Evan Cavallo , Anders Mörtberg , Andrew Swan
We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is … We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.

Internal Parametricity for Cubical Type Theory

2020-05-01
Evan Cavallo , Robert Harper
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, … We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, and we give an account of the identity extension lemma for internal parametricity.

The RedPRL Proof Assistant (Invited Paper)

2018-07-03
Carlo Angiuli , Evan Cavallo , Kuen-Bang Hou +2 more
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, … RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory, allowing an extensional, proof-irrelevant notion of exact equality to coexist with a higher-dimensional proof-relevant notion of paths.
View PDF Chat

Internal Parametricity for Cubical Type Theory

2021-11-03
Evan Cavallo , Robert Harper
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, … We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, observe how cubical equality regularizes parametric type theory, and examine the similarities and discrepancies between cubical and parametric type theory, which are closely related. We also abstract a formal interface to the computational interpretation and show that this also has a presheaf model.
View PDF Chat

Modalities and Parametric Adjoints

2022-03-29
Daniel Gratzer , Evan Cavallo , G. A. Kavvos +2 more
Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and … Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and that it cannot serve as an internal language. We resolve these problems by assuming that the modal context operator is a parametric right adjoint. We show that this hitherto unrecognized structure is common. Based on these discoveries we present a new well-behaved Fitch-style multimodal type theory, which can be used as an internal language. Finally, we apply this syntax to guarded recursion and parametricity.
View PDF Chat

Parametric Cubical Type Theory

2019-01-01
Evan Cavallo , Robert Harper
We exhibit a computational type theory which combines the higher-dimensional structure of cartesian cubical type theory with the internal parametricity primitives of parametric type theory, drawing out the similarities and … We exhibit a computational type theory which combines the higher-dimensional structure of cartesian cubical type theory with the internal parametricity primitives of parametric type theory, drawing out the similarities and distinctions between the two along the way. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic types, including functions between higher inductive types, and we show by example how relativity can be used to characterize the relational interpretation of inductive types.

Internal Parametricity for Cubical Type Theory

2020-05-22
Evan Cavallo , Robert Harper
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, … We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, observe how cubical equality regularizes parametric type theory, and examine the similarities and discrepancies between cubical and parametric type theory, which are closely related. We also abstract a formal interface to the computational interpretation and show that this also has a presheaf model.

Internalizing Representation Independence with Univalence

2020-09-11
Carlo Angiuli , Evan Cavallo , Anders Mörtberg +1 more
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our … In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.

Stable factorization from a fibred algebraic weak factorization system

2019-01-01
Evan Cavallo
We present a construction of stable diagonal factorizations, used to define categorical models of type theory with identity types, from a family of algebraic weak factorization systems on the slices … We present a construction of stable diagonal factorizations, used to define categorical models of type theory with identity types, from a family of algebraic weak factorization systems on the slices of a category. Inspired by a computational interpretation of indexed inductive types in cubical type theory due to Cavallo and Harper, it can be read as a refactoring of a construction of van den Berg and Garner, and is a new alternative among a variety of approaches to modeling identity types in the literature.

Internalizing Representation Independence with Univalence

2020-01-01
Carlo Angiuli , Evan Cavallo , Anders Mörtberg +1 more
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our … In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.
View PDF Chat

Relative elegance and cartesian cubes with one connection

2022-01-01
Evan Cavallo , Christian Sattler
We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a cubical model of homotopy type theory, on the category of cartesian cubical sets … We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a cubical model of homotopy type theory, on the category of cartesian cubical sets with one connection. We thereby identify a second model structure which both constructively models homotopy type theory and presents infinity-groupoids, the first claimed example being the equivariant cartesian model of Awodey-Cavallo-Coquand-Riehl-Sattler.
View PDF Chat

Automating Boundary Filling in Cubical Agda

2024-02-19
Maximilian Doré , Evan Cavallo , Anders Mörtberg
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy Type Theory allows the user to reason about higher … When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy Type Theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical Agda is an extension of Agda with computational support for HITs and univalence. A difficulty when working in Cubical Agda is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries. We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case - Kan solving is even undecidable - so we focus on heuristics that perform well on practical examples. We provide a solver for the contortion problem using a reformulation of contortions in terms of poset maps, while we solve Kan problems using constraint satisfaction programming. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve goals presented by Cubical Agda. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks - providing the ground for further study of proof automation in cubical type theories.
View PDF Chat

The equivariant model structure on cartesian cubical sets

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

The equivariant model structure on cartesian cubical sets

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

Automating Boundary Filling in Cubical Agda

2024-02-19
Maximilian Doré , Evan Cavallo , Anders Mörtberg
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy Type Theory allows the user to reason about higher … When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy Type Theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical Agda is an extension of Agda with computational support for HITs and univalence. A difficulty when working in Cubical Agda is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries. We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case - Kan solving is even undecidable - so we focus on heuristics that perform well on practical examples. We provide a solver for the contortion problem using a reformulation of contortions in terms of poset maps, while we solve Kan problems using constraint satisfaction programming. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve goals presented by Cubical Agda. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks - providing the ground for further study of proof automation in cubical type theories.
View PDF Chat

Modalities and Parametric Adjoints

2022-03-29
Daniel Gratzer , Evan Cavallo , G. A. Kavvos +2 more
Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and … Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and that it cannot serve as an internal language. We resolve these problems by assuming that the modal context operator is a parametric right adjoint. We show that this hitherto unrecognized structure is common. Based on these discoveries we present a new well-behaved Fitch-style multimodal type theory, which can be used as an internal language. Finally, we apply this syntax to guarded recursion and parametricity.
View PDF Chat

Relative elegance and cartesian cubes with one connection

2022-01-01
Evan Cavallo , Christian Sattler
We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a cubical model of homotopy type theory, on the category of cartesian cubical sets … We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a cubical model of homotopy type theory, on the category of cartesian cubical sets with one connection. We thereby identify a second model structure which both constructively models homotopy type theory and presents infinity-groupoids, the first claimed example being the equivariant cartesian model of Awodey-Cavallo-Coquand-Riehl-Sattler.
View PDF Chat

Internal Parametricity for Cubical Type Theory

2021-11-03
Evan Cavallo , Robert Harper
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, … We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, observe how cubical equality regularizes parametric type theory, and examine the similarities and discrepancies between cubical and parametric type theory, which are closely related. We also abstract a formal interface to the computational interpretation and show that this also has a presheaf model.
View PDF Chat

Internalizing representation independence with univalence

2021-01-04
Carlo Angiuli , Evan Cavallo , Anders Mörtberg +1 more
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our … In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.
View PDF Chat

Internalizing Representation Independence with Univalence

2020-09-11
Carlo Angiuli , Evan Cavallo , Anders Mörtberg +1 more
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our … In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.

Internal Parametricity for Cubical Type Theory

2020-05-22
Evan Cavallo , Robert Harper
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, … We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, observe how cubical equality regularizes parametric type theory, and examine the similarities and discrepancies between cubical and parametric type theory, which are closely related. We also abstract a formal interface to the computational interpretation and show that this also has a presheaf model.

Internal Parametricity for Cubical Type Theory

2020-05-01
Evan Cavallo , Robert Harper
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, … We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, and we give an account of the identity extension lemma for internal parametricity.

Unifying Cubical Models of Univalent Type Theory

2020-01-01
Evan Cavallo , Anders Mörtberg , Andrew Swan
We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is … We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.

Internalizing Representation Independence with Univalence

2020-01-01
Carlo Angiuli , Evan Cavallo , Anders Mörtberg +1 more
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our … In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.
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

Parametric Cubical Type Theory

2019-01-01
Evan Cavallo , Robert Harper
We exhibit a computational type theory which combines the higher-dimensional structure of cartesian cubical type theory with the internal parametricity primitives of parametric type theory, drawing out the similarities and … We exhibit a computational type theory which combines the higher-dimensional structure of cartesian cubical type theory with the internal parametricity primitives of parametric type theory, drawing out the similarities and distinctions between the two along the way. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic types, including functions between higher inductive types, and we show by example how relativity can be used to characterize the relational interpretation of inductive types.

Stable factorization from a fibred algebraic weak factorization system

2019-01-01
Evan Cavallo
We present a construction of stable diagonal factorizations, used to define categorical models of type theory with identity types, from a family of algebraic weak factorization systems on the slices … We present a construction of stable diagonal factorizations, used to define categorical models of type theory with identity types, from a family of algebraic weak factorization systems on the slices of a category. Inspired by a computational interpretation of indexed inductive types in cubical type theory due to Cavallo and Harper, it can be read as a refactoring of a construction of van den Berg and Garner, and is a new alternative among a variety of approaches to modeling identity types in the literature.

The RedPRL Proof Assistant (Invited Paper)

2018-07-03
Carlo Angiuli , Evan Cavallo , Kuen-Bang Hou +2 more
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, … RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory, allowing an extensional, proof-irrelevant notion of exact equality to coexist with a higher-dimensional proof-relevant notion of paths.
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.
Coauthor Papers Together
Robert Harper 7
Anders Mörtberg 5
Carlo Angiuli 4
Max Zeuner 3
Christian Sattler 2
Emily Riehl 1
G. A. Kavvos 1
Steve Awodey 1
Andrew Swan 1
Lars Birkedal 1
Daniel Gratzer 1
Kuen-Bang Hou 1
Maximilian Doré 1
Thierry Coquand 1
Adrien Guatto 1
Jonathan Sterling 1

Cubical Type Theory: a constructive interpretation of the univalence axiom

2015-05-18
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.
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

Semantics of higher inductive types

2019-06-17
Peter LeFanu Lumsdaine , Michael Shulman
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development … Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development of homotopy theory within type theory, as well as in formalizing ordinary set-level mathematics in type theory. In this article, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has *weakly stable typal initial algebras* for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specializes to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction, and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed $(\infty,1)$-category is presented by some model category to which our results apply.
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

Computational Higher Type Theory III: Univalent Universes and Exact Equality

2017-01-01
Carlo Angiuli , Kuen-Bang Hou , Robert Harper
This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher-dimensional types. We extend … This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher-dimensional types. We extend this framework to include a cumulative hierarchy of univalent Kan universes of Kan types, exact equality and other pretypes lacking Kan structure, and a cumulative hierarchy of pretype universes. As in Parts I and II, the main result is a canonicity theorem stating that closed terms of boolean type evaluate to either true or false. This establishes the computational interpretation of Cartesian cubical higher type theory based on cubical programs equipped with a deterministic operational semantics.

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.

An experimental library of formalized Mathematics based on the univalent foundations

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

A cubical model of homotopy type theory

2018-08-10
Steve Awodey
View PDF Chat

Homotopy Type Theory: Univalent Foundations of Mathematics

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

Unifying Cubical Models of Univalent Type Theory

2020-01-01
Evan Cavallo , Anders Mörtberg , Andrew Swan
We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is … We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.

Internal Parametricity for Cubical Type Theory

2020-05-01
Evan Cavallo , Robert Harper
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, … We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, and we give an account of the identity extension lemma for internal parametricity.

A dependent nominal type theory

2012-02-20
James Cheney
Nominal abstract syntax is an approach to representing names and binding pioneered by Gabbay and Pitts. So far nominal techniques have mostly been studied using classical logic or model theory, … Nominal abstract syntax is an approach to representing names and binding pioneered by Gabbay and Pitts. So far nominal techniques have mostly been studied using classical logic or model theory, not type theory. Nominal extensions to simple, dependent and ML-like polymorphic languages have been studied, but decidability and normalization results have only been established for simple nominal type theories. We present a LF-style dependent type theory extended with name-abstraction types, prove soundness and decidability of beta-eta-equivalence checking, discuss adequacy and canonical forms via an example, and discuss extensions such as dependently-typed recursion and induction principles.
View PDF Chat

Homotopy theoretic models of identity types

2008-07-14
Steve Awodey , Michael A. Warren
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing … This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
View PDF Chat

A General Framework for Relational Parametricity

2018-06-27
Kristina Sojakova , Patricia Johann
Reynolds' original theory of relational parametricity was intended to capture the observation that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his … Reynolds' original theory of relational parametricity was intended to capture the observation that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formulated in a metatheory with an impredicative universe, such as the Calculus of Inductive Constructions. A number of more abstract treatments of relational parametricity have since appeared; however, as we show, none of these seem to express Reynolds' original theory in a satisfactory way.
View PDF Chat

Abstract effects and proof-relevant logical relations

2014-01-08
Nick Benton , Martin Hofmann , Vivek Nigam
We give a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked: non-observable internal modifications, such … We give a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked: non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as 'pure' or 'read only'. This 'fictional purity' allows clients of a module to validate soundly more effect-based program equivalences than would be possible with previous semantics. Our semantics uses a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant generalisation thereof, namely setoids. The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as proofs of semantic equivalence. The transition to proof-relevance solves twoawkward problems caused by naïve use of existential quantification in Kripke logical relations, namely failure of admissibility and spurious functional dependencies.
View PDF Chat

Brouwer's fixed-point theorem in real-cohesive homotopy type theory

2017-08-17
Michael Shulman
We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental … We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental formalism of ‘crisp variables.’ This yields type theories that we call ‘spatial’ and ‘cohesive,’ in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the ‘fundamental ∞-groupoid’ or ‘shape’), disentangling the ‘identifications’ of homotopy type theory from the ‘continuous paths’ of topology. In a further refinement called ‘real-cohesion,’ the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.
View PDF Chat

Topological and Simplicial Models of Identity Types

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

The Simplicial Model of Univalent Foundations (after Voevodsky)

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

A model of type theory in cubical sets

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

Quantum Gauge Field Theory in Cohesive Homotopy Type Theory

2014-07-29
Urs Schreiber , Michael Shulman
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as … We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in quantum gauge field theory. This is a brief survey of work by the authors developed in detail elsewhere.
View PDF Chat

On the homotopy groups of spheres in homotopy type theory

2016-06-15
Guillaume Brunerie
The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the … The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the homotopy groups of spheres: the computation of the homotopy groups of the circle, the triviality of those of the form πk(Sn) with k < n, and the construction of the Hopf fibration. We then move to more advanced tools. In particular, we define the James construction which allows us to prove the Freudenthal suspension theorem and the fact that there exists a natural number n such that π4(S3) ≃ Z/nZ. Then we study the smash product of spheres, we construct the cohomology ring of a space, and we introduce the Hopf invariant, allowing us to narrow down the n to either 1 or 2. The Hopf invariant also allows us to prove that all the groups of the form π4n−1(S2n) are infinite. Finally we construct the Gysin exact sequence, allowing us to compute the cohomology of CP2 and to prove that π4(S3) ≃ Z/2Z and that more generally πn+1(Sn) ≃ Z/2Z for every n ≥ 3

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

An algebraic weak factorisation system on 01-substitution sets: a constructive proof

2016-01-01
Andrew Swan
We will construct an algebraic weak factorisation system on the category of 01 substitution sets such that the R-algebras are precisely the Kan fibrations together with a choice of Kan … We will construct an algebraic weak factorisation system on the category of 01 substitution sets such that the R-algebras are precisely the Kan fibrations together with a choice of Kan filling operation. The proof is based on Garner's small object argument for algebraic weak factorization systems. In order to ensure the proof is valid constructively, rather than applying the general small object argument, we give a direct proof based on the same ideas. We use this us to give an explanation why the J computation rule is absent from the original cubical set model and suggest a way to fix this.
View PDF Chat

Univalence for inverse diagrams and homotopy canonicity

2014-11-24
Michael Shulman
We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory … We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.
View PDF Chat

The law of excluded middle in the simplicial model of type theory

2020-09-03
Chris Kapulkin , Peter LeFanu Lumsdaine
We show that the law of excluded middle holds in Voevodsky's simplicial model of type theory. As a corollary, excluded middle is compatible with univalence. We show that the law of excluded middle holds in Voevodsky's simplicial model of type theory. As a corollary, excluded middle is compatible with univalence.

Computational Higher Type Theory II: Dependent Cubical Realizability

2016-01-01
Carlo Angiuli , Robert Harper
This is the second in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for … This is the second in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for simple types developed in Part I, and extend it to a meaning explanation of dependent higher-dimensional type theory. This extension requires generalizing the computational Kan condition given in Part I, and considering the action of type families on paths. We define identification types, which classify identifications (paths) in a type, and dependent function and pair types. The main result is a canonicity theorem, which states that a closed term of boolean type evaluates to either true or false. This result establishes the first computational interpretation of higher dependent type theory by giving a deterministic operational semantics for its programs, including operations that realize the Kan condition.

A Constructive Model of Directed Univalence in Bicubical Sets

2020-05-26
Matthew Weaver , Daniel R. Licata
Directed type theory is an analogue of homotopy type theory where types represent categories, generalizing groupoids. A bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based … Directed type theory is an analogue of homotopy type theory where types represent categories, generalizing groupoids. A bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based on equipping each type with both a notion of path and a separate notion of directed morphism. In this setting, a directed analogue of the univalence axiom asserts that there is a universe of covariant discrete fibrations whose directed morphisms correspond to functions---a higher-categorical analogue of the category of sets and functions. In this paper, we give a constructive model of a directed type theory with directed univalence in bicubical, rather than bisimplicial, sets. We formalize much of this model using Agda as the internal language of a 1-topos, following Orton and Pitts. First, building on the cubical techniques used to give computational models of homotopy type theory, we show that there is a universe of covariant discrete fibrations, with a partial directed univalence principle asserting that functions are a retract of morphisms in this universe. To complete this retraction into an equivalence, we refine the universe of covariant fibrations using the constructive sheaf models by Coquand and Ruch.
View PDF Chat

Homotopy Type Theory in Lean

2017-01-01
Floris van Doorn , Jakob von Raumer , Ulrik Buchholtz
View PDF Chat

Path Spaces of Higher Inductive Types in Homotopy Type Theory

2019-06-01
Nicolai Kraus , Jakob von Raumer
The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove … The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.
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

Varieties of Cubical Sets

2017-01-01
Ulrik Buchholtz , Edward Morehouse

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

Parametricity, automorphisms of the universe, and excluded middle

2017-06-27
Auke Bart Booij , Martı́n Hötzel Escardó , Peter LeFanu Lumsdaine +1 more
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific … It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instan ...

Axioms for Modelling Cubical Type Theory in a Topos

2018-12-11
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\&amp;quot;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.)

Multisets in type theory

2019-03-27
Håkon Robbestad Gylterud
A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a … A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative multisets, where multisets are iteratively built up from other multisets, in the context Martin-L\"of Type Theory, in the presence of Voevodsky's Univalence Axiom. Aczel 1978 introduced a model of constructive set theory in type theory, using a W-type quantifying over a universe, and an inductively defined equivalence relation on it. Our investigation takes this W-type and instead considers the identity type on it, which can be computed from the Univalence Axiom. Our thesis is that this gives a model of multisets. In order to demonstrate this, we adapt axioms of constructive set theory to multisets, and show that they hold for our model.
View PDF Chat

Identity Types in Algebraic Model Structures and Cubical Sets

2018-01-01
Andrew Swan
We give a general technique for constructing a functorial choice of very good paths objects, which can be used to implement identity types in models of type theories in direct … We give a general technique for constructing a functorial choice of very good paths objects, which can be used to implement identity types in models of type theories in direct manner with little reliance on general coherence results. We give a simple proof that applies in algebraic model structures that possess a notion of structured weak equivalence, in a sense that we define here. We then give a more direct proof that applies both to the original BCH cubical set model and more recent variants. We give an explanation how this construction relates to the one used in the CCHM cubical set model of type theory.

The HoTT library: a formalization of homotopy type theory in Coq

2016-12-22
Andrej Bauer , Jason Gross , Peter LeFanu Lumsdaine +3 more
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, … We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.
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

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

Separating Path and Identity Types in Presheaf Models of Univalent Type Theory

2018-01-01
Andrew Swan
We give a collection of results regarding path types, identity types and univalent universes in certain models of type theory based on presheaves. The main result is that path types … We give a collection of results regarding path types, identity types and univalent universes in certain models of type theory based on presheaves. The main result is that path types cannot be used directly as identity types in any Orton-Pitts style model of univalent type theory with propositional truncation in presheaf assemblies over the first and second Kleene algebras. We also give a Brouwerian counterexample showing that there is no constructive proof that there is an Orton-Pitts model of type theory in presheaves when the universe is based on a standard construction due to Hofmann and Streicher, and path types are identity types. A similar proof shows that path types are not identity types in internal presheaves in realizability toposes as long as a certain universe can be extended to a univalent one. We show that one of our key lemmas has a purely syntactic variant in intensional type theory and use it to make some minor but curious observations on the behaviour of cofibrations in syntactic categories.

The join construction

2017-01-26
Egbert Rijke
In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map … In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map from the empty type into the common codomain is a neutral element. Moreover, we show that the idempotents of the join of maps are precisely the embeddings, and we prove the `join connectivity theorem', which states that the connectivity of the join of maps equals the join of the connectivities of the individual maps. We define the image of a map $f:A\to X$ in $U$ via the join construction, as the colimit of the finite join powers of $f$. The join powers therefore provide approximations of the image inclusion, and the join connectivity theorem implies that the approximating maps into the image increase in connectivity. A modified version of the join construction can be used to show that for any map $f:A\to X$ in which $X$ is only assumed to be locally small, the image is a small type. We use the modified join construction to give an alternative construction of set-quotients, the Rezk completion of a precategory, and we define the $n$-truncation for any $n:\mathbb{N}$. Thus we see that each of these are definable operations on a univalent universe for Martin-Lof type theory with a natural numbers object, that is moreover closed under homotopy coequalizers.

Algebraic Foundations of Proof Refinement

2017-01-01
Jonathan Sterling , Robert Harper
We contribute a general apparatus for dependent tactic-based proof refinement in the LCF tradition, in which the statements of subgoals may express a dependency on the proofs of other subgoals; … We contribute a general apparatus for dependent tactic-based proof refinement in the LCF tradition, in which the statements of subgoals may express a dependency on the proofs of other subgoals; this form of dependency is extremely useful and can serve as an algorithmic alternative to extensions of LCF based on non-local instantiation of schematic variables. Additionally, we introduce a novel behavioral distinction between refinement rules and tactics based on naturality. Our framework, called Dependent LCF, is already deployed in the nascent RedPRL proof assistant for computational cubical type theory.

The Univalence Axiom in Cubical Sets

2018-06-26
Marc Bezem , Thierry Coquand , Simon Huber
In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on cubical sets as described in Bezem et al. (in: Matthes and Schubert … In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on cubical sets as described in Bezem et al. (in: Matthes and Schubert (eds.) 19th international conference on types for proofs and programs (TYPES 2013), Leibniz international proceedings in informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, vol 26, pp 107–128, 2014. https://doi.org/10.4230/LIPIcs.TYPES.2013.107 . http://drops.dagstuhl.de/opus/volltexte/2014/4628 ) and Huber (A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2015). We will also discuss Swan's construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory.
View PDF Chat

Notions of Anonymous Existence in Martin-Löf Type Theory

2016-01-01
Nicolai Kraus , Martı́n Hötzel Escardó , Thierry Coquand +1 more
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we … As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these constructions are weakly constant endofunctions on identity types. We study such endofunctions on arbitrary types and show that they always factor through a propositional type, the truncated or squashed domain. Such a factorization is impossible for weakly constant functions in general (a result by Shulman), but we present several non-trivial cases in which it can be done. Based on these results, we define a new notion of anonymous existence in type theory and compare different forms of existence carefully. In addition, we show possibly surprising consequences of the judgmental computation rule of the truncation, in particular in the context of homotopy type theory. All the results have been formalized and verified in the dependently typed programming language Agda.

HoTTSQL: proving query rewrites with univalent SQL semantics

2017-06-14
Shumo Chu , Konstantin Weitz , Alvin Cheung +1 more
Every database system contains a query optimizer that performs query rewrites. Unfortunately, developing query optimizers remains a highly challenging task. Part of the challenges comes from the intricacies and rich … Every database system contains a query optimizer that performs query rewrites. Unfortunately, developing query optimizers remains a highly challenging task. Part of the challenges comes from the intricacies and rich features of query languages, which makes reasoning about rewrite rules difficult. In this paper, we propose a machine-checkable denotational semantics for SQL, the de facto language for relational database, for rigorously validating rewrite rules. Unlike previously proposed semantics that are either non-mechanized or only cover a small amount of SQL language features, our semantics covers all major features of SQL, including bags, correlated subqueries, aggregation, and indexes. Our mechanized semantics, called HoTT SQL, is based on K-Relations and homotopy type theory, where we denote relations as mathematical functions from tuples to univalent types. We have implemented HoTTSQL in Coq, which takes only fewer than 300 lines of code and have proved a wide range of SQL rewrite rules, including those from database research literature (e.g., magic set rewrites) and real-world query optimizers (e.g., subquery elimination). Several of these rewrite rules have never been previously proven correct. In addition, while query equivalence is generally undecidable, we have implemented an automated decision procedure using HoTTSQL for conjunctive queries: a well studied decidable fragment of SQL that encompasses many real-world queries.
View PDF Chat

Canonicity for Cubical Type Theory

2016-07-14
Simon Huber
Cubical type theory is an extension of Martin-Lof type theory recently proposed by Cohen, Coquand, Mortberg and the author which allows for direct manipulation of $n$-dimensional cubes and where Voevodsky's … Cubical type theory is an extension of Martin-Lof type theory recently proposed by Cohen, Coquand, Mortberg and the author which allows for direct manipulation of $n$-dimensional cubes and where Voevodsky's Univalence Axiom is provable. In this paper we prove canonicity for cubical type theory: any natural number in a context build from only name variables is judgmentally equal to a numeral. To achieve this we formulate a typed and deterministic operational semantics and employ a computability argument adapted to a presheaf-like setting.

A cubical model of homotopy type theory

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

A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)

2014-01-01
Frédéric Chyzak , Assia Mahboubi , Thomas Sibut-Pinote +1 more
View PDF Chat

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

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