Zobrazeno 1 - 5
of 5
pro vyhledávání: '"Guillaume Brunerie"'
Autor:
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
Publikováno v:
Mathematical Structures in Computer Science. 31:424-468
We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5ed2b2c96ba07fa76e844ad793228f2e
https://doi.org/10.1017/s0960129521000347
https://doi.org/10.1017/s0960129521000347
Autor:
Guillaume Brunerie
Publikováno v:
Journal of Automated Reasoning. 63:255-284
In the first part of this paper we present a formalization in Agda of the James construction in homotopy type theory. We include several fragments of code to show what the Agda code looks like, and we explain several techniques that we used in the fo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::78987e30240dc02f60ccda0a9ffbcb48
https://doi.org/10.1007/s10817-018-9468-2
https://doi.org/10.1007/s10817-018-9468-2
Autor:
Daniel R. Licata, Guillaume Brunerie
Publikováno v:
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2015, Kyoto, Japan. ⟨10.1109/LICS.2015.19⟩
LICS
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2015, Kyoto, Japan. ⟨10.1109/LICS.2015.19⟩
LICS
International audience; Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe higher-dimensional paths. While so
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6c81ef2d8ef9febfe023a9441c23b5b3
https://hal.univ-cotedazur.fr/hal-01322397
https://hal.univ-cotedazur.fr/hal-01322397
Autor:
Daniel R. Licata, Guillaume Brunerie
Publikováno v:
Certified Programs and Proofs ISBN: 9783319035444
CPP
Certified Programs and Proofs
Certified Programs and Proofs, Dec 2013, Melbourne, Australia. ⟨10.1007/978-3-319-03545-1_1⟩
CPP
Certified Programs and Proofs
Certified Programs and Proofs, Dec 2013, Melbourne, Australia. ⟨10.1007/978-3-319-03545-1_1⟩
International audience; Homotopy type theory [Awodey and Warren, 2009; Voevodsky, 2011] is an extension of Martin-Löf’s intensional type theory [Martin-Löf, 1975; Nordström et al., 1990] with new principles such as Voevodsky’s univalence axiom
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9aabb0097cf60e3341f560e2fb038f4b
https://doi.org/10.1007/978-3-319-03545-1_1
https://doi.org/10.1007/978-3-319-03545-1_1
Publikováno v:
Quadrature. :41-42
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b63a924d0940245a4b44cc11d430e072
https://doi.org/10.1051/quadrature/2009007
https://doi.org/10.1051/quadrature/2009007