Zobrazeno 1 - 10
of 54
pro vyhledávání: '"Martín Hötzel Escardó"'
Autor:
Tom de Jong, Martín Hötzel Escardó
Publikováno v:
Logical Methods in Computer Science, Vol Volume 19, Issue 2 (2023)
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
Externí odkaz:
https://doaj.org/article/0520c76e97bc4e39962165cd3f166229
Autor:
Martín Hötzel Escardó
Publikováno v:
Journal of Homotopy and Related Structures. 16:363-366
We show that the Cantor–Schröder–Bernstein Theorem for homotopy types, or $$\infty $$ ∞ -groupoids, holds in the following form: For any two types, if each one is embedded into the other, then they are equivalent. The argument is developed in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3094f470b519f9a7c5b590ff4bf3b6ee
https://doi.org/10.1007/s40062-021-00284-6
https://doi.org/10.1007/s40062-021-00284-6
Autor:
Martín Hötzel Escardó
Publikováno v:
Mathematical Structures in Computer Science. 31:89-111
We investigate the injective types and the algebraically injective types in univalent mathematics, both in the absence and in the presence of propositional resizing. Injectivity is defined by the surjectivity of the restriction map along any embeddin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::422e751fbd36f055fce355d9bb64970f
https://doi.org/10.1017/s0960129520000225
https://doi.org/10.1017/s0960129520000225
Autor:
Paulo Oliva, Martín Hötzel Escardó
Publikováno v:
The Journal of Symbolic Logic. 82:590-607
This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J^T_R X = (X \to R) \to T X$. It is assumed throughout that $R$ is a $T$-algebra. We show that $J^T_R$ is also a strong monad, an
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::702f2c4e53921c9064503235de8094e6
https://doi.org/10.1017/jsl.2017.8
https://doi.org/10.1017/jsl.2017.8
Publikováno v:
Annals of Pure and Applied Logic. 167:794-805
A construction by Hofmann and Streicher gives an interpretation of a type-theoretic universe U in any Grothendieck topos, assuming a Grothendieck universe in set theory. Voevodsky asked what space U is interpreted as in Johnstone's topological topos.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7cdf85f5fc86bebc81c456de1a4eaf29
https://doi.org/10.1016/j.apal.2016.04.010
https://doi.org/10.1016/j.apal.2016.04.010
Autor:
Chuangjie Xu, Martín Hötzel Escardó
Publikováno v:
Scopus-Elsevier
We identify yet another category equivalent to that of Kleene–Kreisel continuous functionals. Reasoning constructively and predicatively, all functions from the Cantor space to the natural numbers are uniformly continuous in this category. We do no
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::be4099aebda8fd59bef8a30aeed525e6
https://doi.org/10.1016/j.apal.2016.04.011
https://doi.org/10.1016/j.apal.2016.04.011
Autor:
Paulo Oliva, Martín Hötzel Escardó
Publikováno v:
Turing-100
Using techniques from higher-type computability theory and proof theory we extend the well-known game-theoretic technique of backward induction to finite games of unbounded length. The main application is a closed formula for calculating strategy pro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1f08353b1d906fe0f43a2fb077b0823a
https://doi.org/10.29007/1wpl
https://doi.org/10.29007/1wpl
Autor:
Martín Hötzel Escardó
Publikováno v:
Mathematical Structures in Computer Science. 25:1578-1589
We show that the following instance of the principle of excluded middle holds: any function on the one-point compactification of the natural numbers with values on the natural numbers is either classically continuous or classically discontinuous. The
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a3b10f421b646682cc4f84fafe7bb3b3
https://doi.org/10.1017/s096012951300042x
https://doi.org/10.1017/s096012951300042x
Autor:
Martín Hötzel Escardó
Publikováno v:
MFPS
It is well-known that the Gödelʼs system T definable functions (N→N)→N are continuous, and that their restrictions from the Baire type (N→N) to the Cantor type (N→2) are uniformly continuous. We offer a new, relatively short and self-contai
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::649901d8f14bb4436c36d0ab20c3162b
https://doi.org/10.1016/j.entcs.2013.09.010
https://doi.org/10.1016/j.entcs.2013.09.010
Autor:
Martín Hötzel Escardó
Publikováno v:
J. Symbolic Logic 78, iss. 3 (2013), 764-784
We show that there are plenty of infinite sets that satisfy the omniscience principle, in a minimalistic setting for constructive mathematics that is compatible with classical mathematics. A first example of an omniscient set is the one-point compact
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6263f392fea86e8c5dd8b560ea3290ee
https://doi.org/10.2178/jsl.7803040
https://doi.org/10.2178/jsl.7803040