Zobrazeno 1 - 10
of 41
pro vyhledávání: '"Mörtberg, Anders"'
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy Type Theory allows the user to reason about higher structures, such as topological spaces, using higher
Externí odkaz:
http://arxiv.org/abs/2402.12169
When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of Set ho
Externí odkaz:
http://arxiv.org/abs/2402.04893
Autor:
Ljungström, Axel, Mörtberg, Anders
This paper discusses the development of synthetic cohomology in Homotopy Type Theory (HoTT), as well as its computer formalisation. The objectives of this paper are (1) to generalise previous work on integral cohomology in HoTT by the current authors
Externí odkaz:
http://arxiv.org/abs/2401.16336
Autor:
Ljungström, Axel, Mörtberg, Anders
Brunerie's 2016 PhD thesis contains the first synthetic proof in Homotopy Type Theory (HoTT) of the classical result that the fourth homotopy group of the 3-sphere is $\mathbb{Z}/2\mathbb{Z}$. The proof is one of the most impressive pieces of synthet
Externí odkaz:
http://arxiv.org/abs/2302.00151
In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. These rings may be de
Externí odkaz:
http://arxiv.org/abs/2212.04182
Autor:
Zeuner, Max, Mörtberg, Anders
Publikováno v:
28th International Conference on Types for Proofs and Programs (TYPES 2022), LIPIcs, volume 269
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 pr
Externí odkaz:
http://arxiv.org/abs/2212.02902
Publikováno v:
In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '22), 2022, ACM, New York, NY, USA
In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant. In the present work, we describe what w
Externí odkaz:
http://arxiv.org/abs/2112.06984
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming lang
Externí odkaz:
http://arxiv.org/abs/2009.05547
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in
Externí odkaz:
http://arxiv.org/abs/1802.01170
Publikováno v:
J Autom Reasoning (2019) Vol 63, 285-318
The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept
Externí odkaz:
http://arxiv.org/abs/1612.00693