Stack semantics of type theory

Authors

Thierry Coquand, Bassel Mannaa, Fabian Ruch

Type: Preprint

Publication Date: 2017-06-01

Citations: 23

DOI: https://doi.org/10.1109/lics.2017.8005130

Ask PDF

Abstract

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

Locations

arXiv (Cornell University)
View PDF
IT University Of Copenhagen (IT University of Copenhagen)
View PDF

Ask a Question About This Paper

Summary

Stack semantics of type theory

2017-06-20

Thierry Coquand , Bassel Mannaa , Fabian Ruch

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an … We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

Stack Semantics of Type Theory

2017-01-01

Thierry Coquand , Bassel Mannaa , Fabian Ruch

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising the groupoid model of type theory. As an … We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

View PDF Chat

Univalent typoids

2022-01-01

Iosif Petrakis

A typoid is a type equipped with an equivalence relation, such that the terms of equivalence between the terms of the type satisfy certain conditions, with respect to a given … A typoid is a type equipped with an equivalence relation, such that the terms of equivalence between the terms of the type satisfy certain conditions, with respect to a given equivalence relation between them, that generalise the properties of the equality terms. The resulting weak 2-groupoid structure can be extended to every finite level. The introduced notions of typoid and typoid function generalise the notions of setoid and setoid function. A univalent typoid is a typoid satisfying a general version of the univalence axiom. We prove some fundamental facts on univalent typoids, their product and exponential. As a corollary, we get an interpretation of propositional truncation within the theory of typoids. The couple typoid and univalent typoid is a weak groupoid-analogue to the couple precategory and category in homotopy type theory.

Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$

2024-07-09

Tom de Jong

We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. … We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. Domain theory studies so-called directed complete posets (dcpos) and Scott continuous maps between them and has applications in a variety of fields, such as programming language semantics, higher-type computability and topology. A common approach to deal with size issues in a predicative foundation is to work with information systems, abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. In our type-theoretic approach, we instead accept that dcpos may be large and work with type universes to account for this. A priori one might expect that iterative constructions of dcpos may result in a need for ever-increasing universes and are predicatively impossible. We show, through a careful tracking of type universe parameters, that such constructions can be carried out in a predicative setting. In particular, we give a predicative reconstruction of Scott's $D_\infty$ model of the untyped $\lambda$-calculus. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.

View PDF Chat

Domain Theory in Constructive and Predicative Univalent Foundations

2023-01-01

Tom de Jong

We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. … We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. Domain theory studies so-called directed complete posets (dcpos) and Scott continuous maps between them and has applications in programming language semantics, higher-type computability and topology. A common approach to deal with size issues in a predicative foundation is to work with information systems, abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. In our type-theoretic approach, we instead accept that dcpos may be large and work with type universes to account for this. A priori one might expect that complex constructions of dcpos result in a need for ever-increasing universes and are predicatively impossible. We show that such constructions can be carried out in a predicative setting. We illustrate the development with applications in the semantics of programming languages: the soundness and computational adequacy of the Scott model of PCF and Scott's $D_\infty$ model of the untyped $\lambda$-calculus. We also give a predicative account of continuous and algebraic dcpos, and of the related notions of a small basis and its rounded ideal completion. The fact that nontrivial dcpos have large carriers is in fact unavoidable and characteristic of our predicative setting, as we explain in a complementary chapter on the constructive and predicative limitations of univalent foundations. Our account of domain theory in univalent foundations is fully formalised with only a few minor exceptions. The ability of the proof assistant Agda to infer universe levels has been invaluable for our purposes.

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 Scott model of PCF in univalent type theory

2019-04-22

Tom de Jong

We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the … We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the lifting monad (also known as the partial map classifier monad) from topos theory, which has been extended to univalent type theory by Escardo and Knapp. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or quotient inductive-inductive types. We show that one can do without these extensions.

The Scott model of PCF in univalent type theory

2019-01-01

Tom de Jong

We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the … We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the lifting monad (also known as the partial map classifier monad) from topos theory, which has been extended to univalent type theory by Escard\'o and Knapp. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or quotient inductive-inductive types. We show that one can do without these extensions.

View PDF Chat

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

The Scott model of PCF in univalent type theory

2021-07-23

Tom de Jong

Abstract We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use … Abstract We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the lifting monad (also known as the partial map classifier monad) from topos theory, which has been extended to univalent type theory by Escardó and Knapp. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or quotient inductive-inductive types. We show that one can do without these extensions.

View PDF Chat

On Small Types in Univalent Foundations

2023-05-04

Tom de Jong , Martı́n Hötzel Escardó

We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements … We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. Moreover, we prove that locally small, nontrivial (directed or bounded) complete posets necessarily lack decidable equality. We prove our results for a general class of posets, which includes e.g. directed complete posets, bounded complete posets, sup-lattices and frames. Secondly, the fact that these nontrivial posets are necessarily large has the important consequence that Tarski's theorem (and similar results) cannot be applied in nontrivial instances. Furthermore, we explain that generalizations of Tarski's theorem that allow for large structures are provably false by showing that the ordinal of ordinals in a univalent universe has small suprema in the presence of set quotients. The latter also leads us to investigate the inter-definability and interaction of type universes of propositional truncations and set quotients, as well as a set replacement principle. Thirdly, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families.

View PDF Chat

On Small Types in Univalent Foundations

2021-01-01

Tom de Jong , Martı́n Hötzel Escardó

View PDF Chat

Domain Theory in Constructive and Predicative Univalent Foundations

2020-08-04

Tom de Jong , Martı́n Hötzel Escardó

We develop domain theory in constructive univalent foundations without Voevodsky's resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and proved its computational adequacy, … We develop domain theory in constructive univalent foundations without Voevodsky's resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and proved its computational adequacy, based on directed complete posets (dcpos). Here we further consider algebraic and continuous dcpos, and construct Scott's $D_\infty$ model of the untyped $\lambda$-calculus. A common approach to deal with size issues in a predicative foundation is to work with information systems or abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. Here we instead accept that dcpos may be large and work with type universes to account for this. For instance, in the Scott model of PCF, the dcpos have carriers in the second universe $\mathcal{U}_1$ and suprema of directed families with indexing type in the first universe $\mathcal{U}_0$. Seeing a poset as a category in the usual way, we can say that these dcpos are large, but locally small, and have small filtered colimits. In the case of algebraic dcpos, in order to deal with size issues, we proceed mimicking the definition of accessible category. With such a definition, our construction of Scott's $D_\infty$ again gives a large, locally small, algebraic dcpo with small directed suprema.

Domain Theory in Constructive and Predicative Univalent Foundations

2020-01-01

Tom de Jong , Martı́n Hötzel Escardó

View PDF Chat

Setoid Type Theory—A Syntactic Translation

2019-01-01

Thorsten Altenkirch , Simon Boulier , Ambrus Kaposi +1 more

View PDF Chat

Truncation levels in homotopy type theory

2015-07-15

Nicolai Kraus

Homotopy type theory (HoTT) is a branch of mathematics that combines and benefits from a variety of fields, most importantly homotopy theory, higher dimensional category theory, and, of course, type … Homotopy type theory (HoTT) is a branch of mathematics that combines and benefits from a variety of fields, most importantly homotopy theory, higher dimensional category theory, and, of course, type theory. We present several original results in homotopy type theory which are related to the truncation level of types, a concept due to Voevodsky. To begin, we give a few simple criteria for determining whether a type is 0-truncated (a set), inspired by a well-known theorem by Hedberg, and these criteria are then generalised to arbitrary n. This naturally leads to a discussion of functions that are weakly constant, i.e. map any two inputs to equal outputs. A weakly constant function does in general not factor through the propositional truncation of its domain, something that one could expect if the function really did not depend on its input. However, the factorisation is always possible for weakly constant endofunctions, which makes it possible to define a propositional notion of anonymous existence. We additionally find a few other non-trivial special cases in which the factorisation works. Further, we present a couple of constructions which are only possible with the judgmental computation rule for the truncation. Among these is an invertibility puzzle that seemingly inverts the canonical map from Nat to the truncation of Nat, which is perhaps surprising as the latter type is equivalent to the unit type. A further result is the construction of strict n-types in Martin-Lof type theory with a hierarchy of univalent universes (and without higher inductive types), and a proof that the universe U(n) is not n-truncated. This solves a hitherto open problem of the 2012/13 special year program on Univalent Foundations at the Institute for Advanced Study (Princeton). The main result of this thesis is a generalised universal property of the propositional truncation, using a construction of coherently constant functions. We show that the type of such coherently constant functions between types A and B, which can be seen as the type of natural transformations between two diagrams over the simplex category without degeneracies (i.e. finite non-empty sets and strictly increasing functions), is equivalent to the type of functions with the truncation of A as domain and B as codomain. In the general case, the definition of natural transformations between such diagrams requires an infinite tower of conditions, which exists if the type theory has Reedy limits of diagrams over the ordinal omega. If B is an n-type for some given finite n, (non-trivial) Reedy limits are unnecessary, allowing us to construct functions from the truncation of A to B in homotopy type theory without further assumptions. To obtain these results, we develop some theory on equality diagrams, especially equality semi-simplicial types. In particular, we show that the semi-simplicial equality type over any type satisfies the Kan condition, which can be seen as the simplicial version of the fundamental result by Lumsdaine, and by van den Berg and Garner, that types are weak omega-groupoids. Finally, we present some results related to formalisations of infinite structures that seem to be impossible to express internally. To give an example, we show how the simplex category can be implemented so that the categorical laws hold strictly. In the presence of very dependent types, we speculate that this makes the Reedy approach for the famous open problem of defining semi-simplicial types work.

Constructing a universe for the setoid model

2021-01-01

Thorsten Altenkirch , Simon Boulier , Ambrus Kaposi +2 more

Directed univalence in simplicial homotopy type theory

2024-07-12

Daniel Gratzer , Jonathan Weinberger , Ulrik Buchholtz

Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics … Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics -- where it allows for synthetic (higher) category theory -- and programming languages -- where it leads to a directed version of the structure identity principle. In this work, we construct the first types in simplicial type theory with non-trivial homomorphisms. We extend simplicial type theory with modalities and new reasoning principles to obtain triangulated type theory in order to construct the universe of discrete types $\mathcal{S}$. We prove that homomorphisms in this type correspond to ordinary functions of types i.e., that $\mathcal{S}$ is directed univalent. The construction of $\mathcal{S}$ is foundational for both of the aforementioned applications of simplicial type theory. We are able to define several crucial examples of categories and to recover important results from category theory. Using $\mathcal{S}$, we are also able to define various types whose usage is guaranteed to be functorial. These provide the first complete examples of the proposed directed structure identity principle.

View PDF Chat

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.

Categorical structures for type theory in univalent foundations

2017-01-01

Benedikt Ahrens , Peter LeFanu Lumsdaine , Vladimir Voevodsky

In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps … In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.

View PDF Chat

Cellular Cohomology in Homotopy Type Theory

2018-01-01

Ulrik Buchholtz , Kuen-Bang Hou

We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage … We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute. Cellular cohomology is a special kind of cohomology designed for cell complexes: these are built in stages by attaching spheres of progressively higher dimension, and cellular cohomology defines the groups out of the combinatorial description of how spheres are attached. Our main result is that for finite cell complexes, a wide class of cohomology theories (including the ones defined through Eilenberg-MacLane spaces) can be calculated via cellular cohomology. This result was formalized in the Agda proof assistant.

View PDF Chat

On Church’s thesis in cubical assemblies

2021-11-01

Andrew Swan , Taichi Uemura

Abstract We show that Church’s thesis, the axiom stating that all functions on the naturals are computable, does not hold in the cubical assemblies model of cubical type theory. We … Abstract We show that Church’s thesis, the axiom stating that all functions on the naturals are computable, does not hold in the cubical assemblies model of cubical type theory. We show that nevertheless Church’s thesis is consistent with univalent type theory by constructing a lex modality in cubical assemblies such that Church’s thesis holds in the corresponding reflective subuniverse.

View PDF Chat

Modalities in homotopy type theory

2017-01-01

Egbert Rijke , Michael Shulman , Bas Spitters

Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal … Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.

View PDF Chat

Cubical methods in homotopy type theory and univalent foundations

2021-11-01

Anders Mörtberg

Abstract Cubical methods have played an important role in the development of Homotopy Type Theory and Univalent Foundations (HoTT/UF) in recent years. The original motivation behind these developments was to … Abstract Cubical methods have played an important role in the development of Homotopy Type Theory and Univalent Foundations (HoTT/UF) in recent years. The original motivation behind these developments was to give constructive meaning to Voevodsky’s univalence axiom, but they have since then led to a range of new results. Among the achievements of these methods is the design of new type theories and proof assistants with native support for notions from HoTT/UF, syntactic and semantic consistency results for HoTT/UF, as well as a variety of independence results and establishing that the univalence axiom does not increase the proof theoretic strength of type theory. This paper is based on lecture notes that were written for the 2019 Homotopy Type Theory Summer School at Carnegie Mellon University. The goal of these lectures was to give an introduction to cubical methods and provide sufficient background in order to make the current research in this very active area of HoTT/UF more accessible to newcomers. The focus of these notes is hence on both the syntactic and semantic aspects of these methods, in particular on cubical type theory and the various cubical set categories that give meaning to these theories.

View PDF Chat

Constructive sheaf models of type theory

2021-10-01

Thierry Coquand , Fabian Ruch , Christian Sattler

Abstract We provide a constructive version of the notion of sheaf models of univalent type theory. We start by relativizing existing constructive models of univalent type theory to presheaves over … Abstract We provide a constructive version of the notion of sheaf models of univalent type theory. We start by relativizing existing constructive models of univalent type theory to presheaves over a base category. Any Grothendieck topology of the base category then gives rise to a family of left-exact modalities, and we recover a model of type theory by localizing the presheaf model with respect to this family of left-exact modalities. We provide then some examples.

View PDF Chat

Cellular Cohomology in Homotopy Type Theory

2018-06-27

Ulrik Buchholtz , Kuen-Bang Hou Favonia

View PDF Chat

Semantics for two-dimensional type theory

2022-08-02

Benedikt Ahrens , Paige Randall North , Niels van der Weide

We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory … We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature.

View PDF Chat

The Independence of Markov's Principle in Type Theory

2016-02-15

Thierry Coquand , Bassel Mannaa

In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark … In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for the generic point of this model. Instead we design an extension of type theory, which intuitively extends type theory by the addition of a generic point of Cantor space. We then show the consistency of this extension by a normalization argument. Markov's principle does not hold in this extension, and it follows that it cannot be proved in type theory.

Synthetic topology in Homotopy Type Theory for probabilistic programming

2021-08-13

Martin E. Bidlingmaier , Florian Faissole , Bas Spitters

Abstract The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language … Abstract The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial σ -frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies, we define valuations and lower integrals on sets and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed.

View PDF Chat

Higher order functions and Brouwer’s thesis

2021-01-01

Jonathan Sterling

Abstract Extending Martín Escardó’s effectful forcing technique, we give a new proof of a well-known result: Brouwer’s monotone bar theorem holds for any bar that can be realized by a … Abstract Extending Martín Escardó’s effectful forcing technique, we give a new proof of a well-known result: Brouwer’s monotone bar theorem holds for any bar that can be realized by a functional of type (ℕ→ℕ)→ℕ in Gödel’s System T . Effectful forcing is an elementary alternative to standard sheaf-theoretic forcing arguments, using ideas from programming languages, including computational effects, monads, the algebra interpretation of call-by-name λ-calculus, and logical relations. Our argument proceeds by interpreting System T programs as well-founded dialogue trees whose nodes branch on a query to an oracle of type ℕ→ℕ, lifted to higher type along a call-by-name translation. To connect this interpretation to the bar theorem, we then show that Brouwer’s famous “mental constructions” of barhood constitute an invariant form of these dialogue trees in which queries to the oracle are made maximally and in order.

View PDF Chat

Partiality, Revisited

2017-01-01

Thorsten Altenkirch , Nils Anders Danielsson , Nicolai Kraus

View PDF Chat

Bicategorical type theory: semantics and syntax

2023-10-17

Benedikt Ahrens , Paige Randall North , Niels van der Weide

Abstract We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a … Abstract We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories . Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.

View PDF Chat

The Scott model of PCF in univalent type theory

2021-07-23

Tom de Jong

View PDF Chat

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type

2016-10-28

Thorsten Altenkirch , Nils Anders Danielsson , Nicolai Kraus

Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by … Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the right notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory - a higher inductive-inductive type - we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications.

View PDF Chat

Heyting-valued interpretations for Constructive Set Theory

2005-07-02

Nicola Gambino

View PDF Chat

A model of type theory in cubical sets

2014-01-01

M Bezem , Thierry Coquand , Simon Huber

The Independence of Markov's Principle in Type Theory

2016-02-15

Thierry Coquand , Bassel Mannaa

Éléments de géométrie algébrique : I. Le langage des schémas

1960-01-01

Alexander Grothendieck

The Independence of Markov's Principle in Type Theory

2016-01-01

Thierry Coquand , Bassel Mannaa

View PDF Chat

Cohomologie non abélienne

1971-01-01

Jean Giraud

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

The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010)

2014-01-01

Vladimir Voevodsky

This is the text of my talk at CMU on Feb. 4, 2010 were I gave the second public presentation of the Univalence Axiom (called "equivalence axiom" in the text). … This is the text of my talk at CMU on Feb. 4, 2010 were I gave the second public presentation of the Univalence Axiom (called "equivalence axiom" in the text). The first presentation of the axiom was in a lecture at LMU Munich in November 2009.

A Sheaf Model of the Algebraic Closure

2014-09-09

Bassel Mannaa , Thierry Coquand

In constructive algebra one cannot in general decide the irreducibility of a polynomial over a field K. This poses some problems to showing the existence of the algebraic closure of … In constructive algebra one cannot in general decide the irreducibility of a polynomial over a field K. This poses some problems to showing the existence of the algebraic closure of K. We give a possible constructive interpretation of the existence of the algebraic closure of a field in characteristic 0 by building, in a constructive metatheory, a suitable site model where there is such an algebraic closure. One can then extract computational content from this model. We give examples of computation based on this model.

View PDF Chat