| 1. |
- Bauer, Andrej, et al.
(författare)
-
The HoTT Library : A formalization of homotopy type theory in Coq
- 2017
-
Ingår i: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. - New York, NY, USA : Association for Computing Machinery (ACM). - 9781450347051 ; , s. 164-172
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 2. |
- Birkedal, Lars, et al.
(författare)
-
Guarded Cubical Type Theory
- 2019
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 211-253
-
Tidskriftsartikel (refereegranskat)abstract
- This paper improves the treatment of equality in guarded dependent type theory ((Formula presented.)), by combining it with cubical type theory ((Formula presented.)). (Formula presented.) is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement (Formula presented.) with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. (Formula presented.) is a variation of Martin–Löf type theory in which the identity type is replaced by abstract paths between terms. (Formula presented.) provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory ((Formula presented.)), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of (Formula presented.) as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that (Formula presented.) can be given semantics in presheaves on (Formula presented.), where (Formula presented.) is the cube category, and (Formula presented.) is any small category with an initial object. We then show that the category of presheaves on (Formula presented.) provides semantics for (Formula presented.).
|
|
| 3. |
- Birkedal, Lars, et al.
(författare)
-
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
- 2016
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. - 9783959770224 ; 62, s. 23:1-23:17
-
Konferensbidrag (refereegranskat)abstract
- This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, is conjectured to have decidable type checking, and has an implemented type checker. Our new type theory, called guarded cubical type theory, provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation, and present semantics in a presheaf category.
|
|
| 4. |
|
|
| 5. |
- Coquand, Thierry, 1961, et al.
(författare)
-
Constructive Gelfand duality for C*-algebras
- 2009
-
Ingår i: Mathematical Proceedings of the Cambridge Philosophical Society. - 0305-0041 .- 1469-8064. ; 147, s. 339-344
-
Tidskriftsartikel (refereegranskat)
|
|
| 6. |
- Coquand, Thierry, 1961, et al.
(författare)
-
Integrals and Valuations
- 2009
-
Ingår i: Logic and Analysis. ; 1
-
Tidskriftsartikel (refereegranskat)
|
|
| 7. |
- Coquand, Thierry, 1961, et al.
(författare)
-
Metric complements of overt closed sets
- 2011
-
Ingår i: Mathematical logic quarterly. - : Wiley. - 0942-5616 .- 1521-3870. ; 57:4, s. 373-378
-
Tidskriftsartikel (refereegranskat)abstract
- We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its collection of points is Bishop-compact.
|
|
| 8. |
- de Boer, Menno, 1994-
(författare)
-
A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory
- 2020
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- In this licentiate thesis we present a proof of the initiality conjecture for Martin-Löf’s type theory with 0, 1, N, A+B, ∏AB, ∑AB, IdA(u,v), countable hierarchy of universes (Ui)iєN closed under these type constructors and with type of elements (ELi(a))iєN. We employ the categorical semantics of contextual categories. The proof is based on a formalization in the proof assistant Agda done by Guillaume Brunerie and the author. This work was part of a joint project with Peter LeFanu Lumsdaine and Anders Mörtberg, who are developing a separate formalization of this conjecture with respect to categories with attributes and using the proof assistant Coq over the UniMath library instead. Results from this project are planned to be published in the future.We start by carefully setting up the syntax and rules for the dependent type theory in question followed by an introduction to contextual categories. We then define the partial interpretation of raw syntax into a contextual category and we prove that this interpretation is total on well-formed input. By doing so, we define a functor from the term model, which is built out of the syntax, into any contextual category and we show that any two such functors are equal. This establishes that the term model is initial among contextual categories. At the end we discuss details of the formalization and future directions for research. In particular, we discuss a memory issue that arose in type checking the formalization and how it was resolved.
|
|
| 9. |
- Wilander, Olov, 1980-
(författare)
-
On Constructive Sets and Partial Structures
- 2011
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- The first three papers in this thesis study the formalisation of a set in type theory as a data type with an equivalence relation – an object usually known as a setoid. The corresponding formalisation of a locally small category is called an E-category. In Paper I, we show that type theory without universes is insufficient for proving that some expected properties hold of the E-category of setoids, but that a minimal universe is sufficient. In Paper II, we show that although the collection of all E-categories does not form a category, we can introduce a type-theoretic version of bicategories, and the E-categories form such an E-bicategory. In Paper III, we consider the setoids inside a type-theoretic universe. The axiom of unique substitutions is proposed and used to show that these form a small category (that is, a category witha setoid of objects and a single setoid of all arrows). We demonstrate that this construction can not be carried out without adding some new axiom to type theory. We also show that the axiom of unique substitutions is strictly weaker than the axiom of unique identity proofs. In Paper IV, we investigate partial equivalence relations, also known as partial setoids, in Heyting arithmetic in all finite types, and adapt the result that the extensional axiom of choice is equivalent to the combination of the intensional axiom of choice, classical logic, and an extensionality axiom. In Paper V, we investigate PHL, a logic of partial terms, and prove a cut elimination theorem for it and for a related calculus.
|
|
