4 Search Results for "Escardó, Martín Hötzel"


Document
A Univalent Formalization of Constructive Affine Schemes

Authors: Max Zeuner and Anders Mörtberg

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)


Abstract
We present a formalization of constructive affine schemes in the Cubical Agda proof assistant. This development is not only fully constructive and predicative, it also makes crucial use of univalence. By now schemes have been formalized in various proof assistants. However, most existing formalizations follow the inherently non-constructive approach of Hartshorne’s classic "Algebraic Geometry" textbook, for which the construction of the so-called structure sheaf is rather straightforwardly formalizable and works the same with or without univalence. We follow an alternative approach that uses a point-free description of the constructive counterpart of the Zariski spectrum called the Zariski lattice and proceeds by defining the structure sheaf on formal basic opens and then lift it to the whole lattice. This general strategy is used in a plethora of textbooks, but formalizing it has proved tricky. The main result of this paper is that with the help of the univalence principle we can make this "lift from basis" strategy formal and obtain a fully formalized account of constructive affine schemes.

Cite as

Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14,
  author =	{Zeuner, Max and M\"{o}rtberg, Anders},
  title =	{{A Univalent Formalization of Constructive Affine Schemes}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{14:1--14:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.14},
  URN =		{urn:nbn:de:0030-drops-184574},
  doi =		{10.4230/LIPIcs.TYPES.2022.14},
  annote =	{Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics}
}
Document
Predicative Aspects of Order Theory in Univalent Foundations

Authors: Tom de Jong and Martín Hötzel Escardó

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)


Abstract
We investigate predicative aspects of order theory in 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. We prove our results for a general class of posets, which includes directed complete posets, bounded complete posets and sup-lattices, using a technical notion of a δ_V-complete poset. We also show that nontrivial locally small δ_V-complete posets necessarily lack decidable equality. Specifically, we derive weak excluded middle from assuming a nontrivial locally small δ_V-complete poset with decidable equality. Moreover, if we assume positivity instead of nontriviality, then we can derive full excluded middle. Secondly, we show that each of Zorn’s lemma, Tarski’s greatest fixed point theorem and Pataraia’s lemma implies propositional resizing. Hence, these principles are inherently impredicative and a predicative development of order theory must therefore do without them. Finally, 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.

Cite as

Tom de Jong and Martín Hötzel Escardó. Predicative Aspects of Order Theory in Univalent Foundations. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{dejong_et_al:LIPIcs.FSCD.2021.8,
  author =	{de Jong, Tom and Escard\'{o}, Mart{\'\i}n H\"{o}tzel},
  title =	{{Predicative Aspects of Order Theory in Univalent Foundations}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.8},
  URN =		{urn:nbn:de:0030-drops-142461},
  doi =		{10.4230/LIPIcs.FSCD.2021.8},
  annote =	{Keywords: order theory, constructivity, predicativity, univalent foundations}
}
Document
Domain Theory in Constructive and Predicative Univalent Foundations

Authors: Tom de Jong and Martín Hötzel Escardó

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)


Abstract
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_∞ model of the untyped λ-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 U₁ and suprema of directed families with indexing type in the first universe U₀. 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_∞ again gives a large, locally small, algebraic dcpo with small directed suprema.

Cite as

Tom de Jong and Martín Hötzel Escardó. Domain Theory in Constructive and Predicative Univalent Foundations. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{dejong_et_al:LIPIcs.CSL.2021.28,
  author =	{de Jong, Tom and Escard\'{o}, Mart{\'\i}n H\"{o}tzel},
  title =	{{Domain Theory in Constructive and Predicative Univalent Foundations}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.28},
  URN =		{urn:nbn:de:0030-drops-134625},
  doi =		{10.4230/LIPIcs.CSL.2021.28},
  annote =	{Keywords: domain theory, constructivity, predicativity, univalent foundations}
}
Document
The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation

Authors: Martín Hötzel Escardó and Chuangjie Xu

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)


Abstract
If all functions (N -> N) -> N are continuous then 0 = 1. We establish this in intensional (and hence also in extensional) intuitionistic dependent-type theories, with existence in the formulation of continuity expressed as a Sigma type via the Curry-Howard interpretation. But with an intuitionistic notion of anonymous existence, defined as the propositional truncation of Sigma, it is consistent that all such functions are continuous. A model is Johnstone’s topological topos. On the other hand, any of these two intuitionistic conceptions of existence give the same, consistent, notion of uniform continuity for functions (N -> 2) -> N, again valid in the topological topos. It is open whether the consistency of (uniform) continuity extends to homotopy type theory. The theorems of type theory informally proved here are also formally proved in Agda, but the development presented here is self-contained and doesn't show Agda code.

Cite as

Martín Hötzel Escardó and Chuangjie Xu. The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 153-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{hotzelescardo_et_al:LIPIcs.TLCA.2015.153,
  author =	{H\"{o}tzel Escard\'{o}, Mart{\'\i}n and Xu, Chuangjie},
  title =	{{The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{153--164},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.153},
  URN =		{urn:nbn:de:0030-drops-51618},
  doi =		{10.4230/LIPIcs.TLCA.2015.153},
  annote =	{Keywords: Dependent type, intensional Martin-L\"{o}f type theory, Curry-Howard interpretation, constructive mathematics, Brouwerian continuity axioms, anonymous exi}
}
  • Refine by Author
  • 2 Escardó, Martín Hötzel
  • 2 de Jong, Tom
  • 1 Hötzel Escardó, Martín
  • 1 Mörtberg, Anders
  • 1 Xu, Chuangjie
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Constructive mathematics
  • 3 Theory of computation → Type theory
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 2 constructivity
  • 2 predicativity
  • 2 univalent foundations
  • 1 Affine Schemes
  • 1 Brouwerian continuity axioms
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2021
  • 1 2015
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail