Finite sets in homotopy type theory

Authors

Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide

Type: Article

Publication Date: 2017-12-22

Citations: 2

DOI: https://doi.org/10.1145/3176245.3167085

Ask PDF

Abstract

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.

Locations

Radboud Repository (Radboud University)
View PDF
Data Archiving and Networked Services (DANS)
View PDF

Ask a Question About This Paper

Summary

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

Higher inductive types in Homotopy Type Theory: applications and theory

2016-04-01

Fredrik Nordvall Forsberg

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

Homotopy-Initial Algebras in Type Theory

2017-01-30

Steve Awodey , Nicola Gambino , Kristina Sojakova

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

View PDF Chat

Homotopy-initial algebras in type theory

2015-04-21

Steve Awodey , Nicola Gambino , Kristina Sojakova

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

Homotopy-initial algebras in type theory

2015-01-01

Steve Awodey , Nicola Gambino , Kristina Sojakova

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

View PDF Chat

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.

Higher Inductive Types as Homotopy-Initial Algebras

2014-02-04

Kristina Sojakova

Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs constructive type theory and abstract homotopy theory. We have a powerful interplay … Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs. A crucial ingredient in this new system are higher inductive types, which allow us to represent objects such as spheres, tori, pushouts, and quotients. We investigate a variant of higher inductive types whose computational behavior is determined up to a higher path. We show that in this setting, higher inductive types are characterized by the universal property of being a homotopy-initial algebra.

Higher Inductive Types as Homotopy-Initial Algebras

2014-01-01

Kristina Sojakova

View PDF Chat

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations

2024-02-07

Daniel Gratzer , Håkon Robbestad Gylterud , Anders Mörtberg +1 more

When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with … When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of Set hold for hSet ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that Ob(hSet) is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example when constructing internal models of type theory. In this work, we equip the type of iterative sets V0, due to Gylterud (2018) as a refinement of the pioneering work of Aczel (1978) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize V0 into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of V0 and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from V0 into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in Agda using the agda-unimath library of univalent mathematics.

View PDF Chat

Higher Inductive Types as Homotopy-Initial Algebras

2014-12-19

Kristina Sojakova

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

View PDF Chat

A Primer on Homotopy Type Theory Part 1: The Formal Type Theory

2014-11-18

James Ladyman , Stuart Presnell

This Primer is an introduction to Homotopy Type Theory (HoTT). The original source for the ideas presented here is the ``HoTT Book'' -- Homotopy Type Theory: Univalent Foundations of Mathematics … This Primer is an introduction to Homotopy Type Theory (HoTT). The original source for the ideas presented here is the ``HoTT Book'' -- Homotopy Type Theory: Univalent Foundations of Mathematics published by The Univalent Foundations Program, Institute for Advanced Study, Princeton. In what follows we freely borrow and adapt definitions, arguments and proofs from the HoTT Book throughout without always giving a specific citation. However, whereas that book provides an introduction to the subject that rapidly involves the reader in advanced technical material, the exposition in this Primer is more gently paced for the beginner. We also do more to motivate, justify, and explain some aspects of the theory in greater detail, and we address foundational and philosophical issues that the HoTT Book does not. In the course of studying HoTT we developed our own approach to interpreting it as a foundation for mathematics that is independent of the homotopy interpretation of the HoTT Book though compatible with it. In particular, we interpret types as concepts; we have a slightly different understanding of subtypes and the Curry-Howard correspondence; and we offer a novel approach to the justification of the elimination rule for identity types in section 7 below (though it builds on a known mathematical result). These ideas are developed in detail in our papers downloadable from the project website: http://www.bristol.ac.uk/arts/research/current-projects/homotopy-type-theory/. While our ideas and views about some important matters differ from those presented in the HoTT Book the theory we present is essentially the same. Part I below introduces, explains and justifies the basic ideas, language and framework of HoTT including propositional logic, simple types, functions, quantification and identity types. In the subsequent parts of this Primer we extend the theory to predicate logic, the theory of the natural numbers, topology, the real numbers, fibre bundles, calculus and manifolds, and the very important `Univalence axiom'

Non-wellfounded sets in homotopy type theory

2020-01-01

Håkon Robbestad Gylterud , Elisabeth Stenholm , Niccolò Veltri

Non-wellfounded material sets have previously been modeled in Martin-L\"of type theory by Lindstr\"om using setoids. In this paper we construct models of non-wellfounded material sets in Homotopy Type Theory (HoTT) … Non-wellfounded material sets have previously been modeled in Martin-L\"of type theory by Lindstr\"om using setoids. In this paper we construct models of non-wellfounded material sets in Homotopy Type Theory (HoTT) where equality is interpreted as the identity type. The first model satisfies Scott's Anti-Foundation Axiom (SAFA) and dualises the construction of iterative sets. The second model satisfies Aczel's Anti-Foundation Axiom (AFA), and is constructed by adaption of Aczel--Mendler's terminal coalgebra theorem to type theory, which requires propositional resizing. In an bid to extend coalgebraic theory and anti-foundation axioms to higher type levels, we formulate generalisations of AFA and SAFA, and construct a hierarchy of models which satisfies the SAFA generalisations. These generalisations build on the framework of Univalent Material Set Theory, previously developed by two of the authors. Since the model constructions are based on M-types, the paper also includes a characterisation of the identity type of M-types as indexed M-types. Our results are formalised in the proof-assistant Agda.

View PDF Chat

Semantics for Homotopy Type Theory

2019-01-01

Roberta Bonacina

Sets in homotopy type theory

2015-01-30

Egbert Rijke , Bas Spitters

Homotopy Type Theory may be seen as an internal language for the $\infty$-category of weak $\infty$-groupoids which in particular models the univalence axiom. Voevodsky proposes this language for weak $\infty$-groupoids … Homotopy Type Theory may be seen as an internal language for the $\infty$-category of weak $\infty$-groupoids which in particular models the univalence axiom. Voevodsky proposes this language for weak $\infty$-groupoids as a new foundation for mathematics called the Univalent Foundations of Mathematics. It includes the sets as weak $\infty$-groupoids with contractible connected components, and thereby it includes (much of) the traditional set theoretical foundations as a special case. We thus wonder whether those `discrete' groupoids do in fact form a (predicative) topos. More generally, homotopy type theory is conjectured to be the internal language of `elementary' $\infty$-toposes. We prove that sets in homotopy type theory form a $\Pi W$-pretopos. This is similar to the fact that the $0$-truncation of an $\infty$-topos is a topos. We show that both a subobject classifier and a $0$-object classifier are available for the type theoretical universe of sets. However, both of these are large and moreover, the $0$-object classifier for sets is a function between $1$-types (i.e. groupoids) rather than between sets. Assuming an impredicative propositional resizing rule we may render the subobject classifier small and then we actually obtain a topos of sets.

View PDF Chat

The category of iterative sets in homotopy type theory and univalent foundations

2024-11-19

Daniel Gratzer , Håkon Robbestad Gylterud , Anders Mörtberg +1 more

Abstract When working in homotopy type theory and univalent foundations, the traditional role of the category of sets, $\mathcal{Set}$ , is replaced by the category $\mathcal{hSet}$ of homotopy sets (h-sets); … Abstract When working in homotopy type theory and univalent foundations, the traditional role of the category of sets, $\mathcal{Set}$ , is replaced by the category $\mathcal{hSet}$ of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of $\mathcal{Set}$ hold for $\mathcal{hSet}$ ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that $\mathsf{Ob}\,\mathcal{hSet}$ is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example, when constructing internal models of type theory. In this work, we equip the type of iterative sets $\mathsf{V}^0$ , due to Gylterud ((2018). The Journal of Symbolic Logic 83 (3) 1132–1146) as a refinement of the pioneering work of Aczel ((1978). Logic Colloquium’77 , Studies in Logic and the Foundations of Mathematics, vol. 96, Elsevier, 55–66.) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize $\mathsf{V}^0$ into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of $\mathsf{V}^0$ and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from $\mathsf{V}^0$ into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in $\texttt{Agda}$ using the $\texttt{agda}$ - $\texttt{unimath}$ library of univalent mathematics.

View PDF Chat

Constructive Set Theory from a Weak Tarski Universe

2014-01-01

Cesare Gallozzi

The aim of this thesis is to give a concise introduction to homotopy type theory, to Aczel's constructive set theory and to simplicial sets and their homotopy theory in particular … The aim of this thesis is to give a concise introduction to homotopy type theory, to Aczel's constructive set theory and to simplicial sets and their homotopy theory in particular referring to their standard model structure, showing some of their interactions. The original part of this thesis consists in the final chapter where we introduce in the type theoretic context a definition of weak Tarski universe motivated by categorical models like the one given by simplicial sets. The weakening of this notion, although present in some imprecise form in mathematical folklore was not published before, at the best of our knowledge. Moreover, we show using the axiom of function extensionality that the type theoretic interpretation of constructive set theory generalises to homotopy type theory with a weak Tarski universe.

Classifying Types

2019-01-01

Egbert Rijke

The study of homotopy theoretic phenomena in the language of type theory is sometimes loosely called `synthetic homotopy theory'. Homotopy theory in type theory is only one of the many … The study of homotopy theoretic phenomena in the language of type theory is sometimes loosely called `synthetic homotopy theory'. Homotopy theory in type theory is only one of the many aspects of homotopy type theory, which also includes the study of the set theoretic semantics (models of homotopy type theory and univalence in a meta-theory of sets or categories), type theoretic semantics (internal models of homotopy type theory), and computational semantics, as well as the study of various questions in the internal language of homotopy type theory which are not necessarily motivated by homotopy theory, or questions related to the development of formalized libraries of mathematics based on homotopy type theory. This thesis concerns the development of synthetic homotopy theory.

Homotopy Type Theory: A Synthetic Approach to Higher Equalities

2018-01-18

Michael Shulman

Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which … Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which two objects can be equal, ways in which those ways-to-be-equal can be equal, ad infinitum. Though apparently complicated, such structures are increasingly important in mathematics. Philosophically, they are an inevitable result of the notion that whenever we form a collection of things, we must simultaneously consider when two of those things are the same. The “synthetic” nature of HoTT/UF enables a much simpler description of infinity groupoids than is available in set theory, thereby aligning with modern mathematics while placing “equality” back in the foundations of logic. This chapter will introduce the basic ideas of HoTT/UF for a philosophical audience, including Voevodsky’s univalence axiom and higher inductive types.

View PDF Chat

The category of iterative sets in homotopy type theory and univalent foundations

2024-11-19

Daniel Gratzer , Håkon Robbestad Gylterud , Anders Mörtberg +1 more

View PDF Chat

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

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">></ETX>

Higher Inductive Types as Homotopy-Initial Algebras

2014-12-19

Kristina Sojakova

View PDF Chat

An induction principle and pigeonhole principles for K-finite sets

1995-12-01

Andreas Blass

Abstract We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Bénabou and Loiseau. We also comment … Abstract We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Bénabou and Loiseau. We also comment on some variants of this pigeonhole principle.

View PDF Chat

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-06-01

Daniel R. Licata , Michael Shulman

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

View PDF Chat

Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics

1993-04-01

Wim Veldman , Marc Bezem

At first sight, the argument which F. P. Ramsey gave for (the infinite case of) his famous theorem from 1927, is hopelessly unconstructive. If suitably reformulated, the theorem is true … At first sight, the argument which F. P. Ramsey gave for (the infinite case of) his famous theorem from 1927, is hopelessly unconstructive. If suitably reformulated, the theorem is true intuitionistically as well as classically: we offer a proof which should convince both the classical and the intuitionistic reader.

View PDF Chat

Constructing the propositional truncation using non-recursive HITs

2016-01-12

Floris van Doorn

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

View PDF Chat

Constructions with Non-Recursive Higher Inductive Types

2016-07-05

Nicolai Kraus

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

View PDF Chat

Finiteness and rational sequences, constructively

2017-01-01

Tarmo Uustalu , Niccolò Veltri

Abstract Rational sequences are possibly infinite sequences with a finite number of distinct suffixes. In this paper, we present different implementations of rational sequences in Martin–Löf type theory. First, we … Abstract Rational sequences are possibly infinite sequences with a finite number of distinct suffixes. In this paper, we present different implementations of rational sequences in Martin–Löf type theory. First, we literally translate the above definition of rational sequence into the language of type theory, i.e., we construct predicates on possibly infinite sequences expressing the finiteness of the set of suffixes. In type theory, there exist several inequivalent notions of finiteness. We consider two of them, listability and Noetherianness, and show that in the implementation of rational sequences the two notions are interchangeable. Then we introduce the type of lists with backpointers, which is an inductive implementation of rational sequences. Lists with backpointers can be unwound into rational sequences, and rational sequences can be truncated into lists with backpointers. As an example, we see how to convert the fractional representation of a rational number into its decimal representation and vice versa.

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

Sur la notion d'ensemble fini

1920-01-01

Casimir Kuratowski

Le but de cette note est d'introduire une définition d'un ensemble fini et de démontrer son équivalence avec la définition donnée par Wacław Sierpiński. Le but de cette note est d'introduire une définition d'un ensemble fini et de démontrer son équivalence avec la définition donnée par Wacław Sierpiński.

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

Variations on Noetherianness

2016-04-01

Denis Firsov , Tarmo Uustalu , Niccolò Veltri

In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda programming language. We … In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda programming language. We want to say that a set is Noetherian, if, when we are shown elements from it one after another, we will sooner or later have seen some element twice. This idea can be made precise in a number of ways. We explore the properties and connections of some of the possible encodings. In particular, we show that certain implementations imply decidable equality while others do not, and we construct counterexamples in the latter case. Additionally, we explore the relation between Noetherianness and other notions of finiteness.

View PDF Chat

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