5 Search Results for "Lumsdaine, Peter LeFanu"

Document
DOI: 10.4230/LIPIcs.TYPES.2022.14
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.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
DOI: 10.4230/LIPIcs.FSCD.2023.5
Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses

Authors: Taichi Uemura

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
We show that certain diagrams of ∞-logoses are reconstructed in internal languages of their oplax limits via lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single ∞-logos but also a diagram of ∞-logoses. This also provides a higher dimensional version of Sterling’s synthetic Tait computability - a type theory for higher dimensional logical relations.
Cite as

Taichi Uemura. Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 5:1-5:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{uemura:LIPIcs.FSCD.2023.5,
  author =	{Uemura, Taichi},
  title =	{{Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.5},
  URN =		{urn:nbn:de:0030-drops-179897},
  doi =		{10.4230/LIPIcs.FSCD.2023.5},
  annote =	{Keywords: Homotopy type theory, ∞-logos, ∞-topos, oplax limit, Artin gluing, modality, synthetic Tait computability, logical relation}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2016.7
Parametricity, Automorphisms of the Universe, and Excluded Middle

Authors: Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
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 instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and for some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.
Cite as

Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman. Parametricity, Automorphisms of the Universe, and Excluded Middle. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 7:1-7:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{booij_et_al:LIPIcs.TYPES.2016.7,
  author =	{Booij, Auke B. and Escard\'{o}, Mart{\'\i}n H. and Lumsdaine, Peter LeFanu and Shulman, Michael},
  title =	{{Parametricity, Automorphisms of the Universe, and Excluded Middle}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{7:1--7:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.7},
  URN =		{urn:nbn:de:0030-drops-98554},
  doi =		{10.4230/LIPIcs.TYPES.2016.7},
  annote =	{Keywords: relational parametricity, dependent type theory, univalent foundations, homotopy type theory, excluded middle, classical mathematics, constructive mat}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.5
Displayed Categories

Authors: Benedikt Ahrens and Peter LeFanu Lumsdaine

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
We introduce and develop the notion of displayed categories. A displayed category over a category C is equivalent to "a category D and functor F : D -> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.
Cite as

Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 5:1-5:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.FSCD.2017.5,
  author =	{Ahrens, Benedikt and Lumsdaine, Peter LeFanu},
  title =	{{Displayed Categories}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.5},
  URN =		{urn:nbn:de:0030-drops-77220},
  doi =		{10.4230/LIPIcs.FSCD.2017.5},
  annote =	{Keywords: Category theory, Dependent type theory, Computer proof assistants, Coq, Univalent mathematics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.8
Categorical Structures for Type Theory in Univalent Foundations

Authors: Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
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 the setting of univalent foundations, where the relationships between them can be stated more transparently. Specifically, we construct maps between the different structures and show that these maps are equivalences under suitable assumptions. 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.
Cite as

Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical Structures for Type Theory in Univalent Foundations. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 8:1-8:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.CSL.2017.8,
  author =	{Ahrens, Benedikt and Lumsdaine, Peter LeFanu and Voevodsky, Vladimir},
  title =	{{Categorical Structures for Type Theory in Univalent Foundations}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.8},
  URN =		{urn:nbn:de:0030-drops-76960},
  doi =		{10.4230/LIPIcs.CSL.2017.8},
  annote =	{Keywords: Categorical Semantics, Type Theory, Univalence Axiom}
}
  • Refine by Author
  • 3 Lumsdaine, Peter LeFanu
  • 2 Ahrens, Benedikt
  • 1 Booij, Auke B.
  • 1 Escardó, Martín H.
  • 1 Mörtberg, Anders
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Type theory
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Affine Schemes
  • 1 Artin gluing
  • 1 Categorical Semantics
  • 1 Category theory
  • 1 Computer proof assistants
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2017
  • 2 2023
  • 1 2018

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
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact