Zobrazeno 1 - 10
of 83
pro vyhledávání: '"Lumsdaine, Peter"'
We define a general class of dependent type theories, encompassing Martin-L\"of's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing results and constructions to be give
Externí odkaz:
http://arxiv.org/abs/2009.05539
Publikováno v:
Theory and Applications of Categories, Vol. 35, 2020, No. 40, pp 1546-1548
We show that the law of excluded middle holds in Voevodsky's simplicial model of type theory. As a corollary, excluded middle is compatible with univalence.
Comment: Short note, 2 pages. v2: various revisions, no change in numbering
Comment: Short note, 2 pages. v2: various revisions, no change in numbering
Externí odkaz:
http://arxiv.org/abs/2006.13694
We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct the category with attributes $C^I
Externí odkaz:
http://arxiv.org/abs/1808.01816
Autor:
Lumsdaine, Peter LeFanu, Shulman, Mike
Publikováno v:
Math. Proc. Camb. Phil. Soc. 169 (2020) 159-208
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development of homotopy theory wit
Externí odkaz:
http://arxiv.org/abs/1705.07088
Publikováno v:
Logical Methods in Computer Science, Volume 15, Issue 1 (March 5, 2019) lmcs:4308
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,
Externí odkaz:
http://arxiv.org/abs/1705.04296
Publikováno v:
Logical Methods in Computer Science, Volume 14, Issue 3 (September 11, 2018) lmcs:4801
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
Externí odkaz:
http://arxiv.org/abs/1705.04310
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 interac
Externí odkaz:
http://arxiv.org/abs/1701.05617
Autor:
Bauer, Andrej, Gross, Jason, Lumsdaine, Peter LeFanu, Shulman, Mike, Sozeau, Matthieu, Spitters, Bas
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
Externí odkaz:
http://arxiv.org/abs/1610.04591
We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-fu
Externí odkaz:
http://arxiv.org/abs/1610.00037
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the Blakers-Massey connectivity theorem, a resul
Externí odkaz:
http://arxiv.org/abs/1605.03227