Imagen de Portada

Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Ljungström, Axel, Mörtberg, Anders
Formato:	Preprint
Publicado:	2023
Materias:	Algebraic Topology Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Computational Synthetic Cohomology Theory in Homotopy Type Theory
por: Ljungström, Axel, et al.
Publicado: (2024)

Symmetric Monoidal Smash Products in Homotopy Type Theory
por: Ljungström, Axel
Publicado: (2024)

The Steenrod squares via unordered joins
por: Ljungström, Axel, et al.
Publicado: (2025)

Formalising Inductive and Coinductive Containers
por: Damato, Stefania, et al.
Publicado: (2024)

Central H-spaces and banded types
por: Buchholtz, Ulrik, et al.
Publicado: (2023)

The equivariant model structure on cartesian cubical sets
por: Awodey, Steve, et al.
Publicado: (2024)

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
por: Brough, Jackson
Publicado: (2026)

Delooping cyclic groups with lens spaces in homotopy type theory
por: Mimram, Samuel, et al.
Publicado: (2024)

Classifying covering types in homotopy type theory
por: Mimram, Samuel, et al.
Publicado: (2025)

Hypercubical manifolds in homotopy type theory
por: Mimram, Samuel, et al.
Publicado: (2025)

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
por: Gratzer, Daniel, et al.
Publicado: (2024)

Automating Boundary Filling in Cubical Type Theories
por: Doré, Maximilian, et al.
Publicado: (2024)

The Functor of Points Approach to Schemes in Cubical Agda
por: Zeuner, Max, et al.
Publicado: (2024)

Computational techniques for sheaf cohomology of locally profinite sets
por: Schachner, Mark
Publicado: (2026)

Manifold Diagrams for Higher Categories
por: Heidemann, Lukas
Publicado: (2024)

Epimorphisms and Acyclic Types in Univalent Foundations
por: Buchholtz, Ulrik, et al.
Publicado: (2024)

Ext groups in Homotopy Type Theory
por: Christensen, J. Daniel, et al.
Publicado: (2023)

Modal Fracture of Higher Groups
por: Myers, David Jaz
Publicado: (2021)

Persistent homology of partially ordered spaces
por: Calk, Cameron, et al.
Publicado: (2023)

Formalizing the zigzag construction of path spaces of pushouts
por: Štěpančík, Vojtěch
Publicado: (2025)

On the Formalization of Network Topology Matrices in HOL
por: Aksoy, Kubra, et al.
Publicado: (2026)

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
por: de Jong, Tom, et al.
Publicado: (2026)

A type-theoretic definition of lax $(\infty,\infty)$-limits
por: Mikhail, Thomas Jan
Publicado: (2024)

Synthetic Homotopy Theory
por: Wei, Yuhang
Publicado: (2024)

On cohomology of locally profinite sets
por: Aoki, Ko
Publicado: (2024)

The Multiplicative Structures on Motivic Homotopy Groups
por: Dugger, Daniel, et al.
Publicado: (2022)

Classification of Covering Spaces and Canonical Change of Basepoint
por: Wemmenhove, Jelle, et al.
Publicado: (2024)

Non-trivial higher homotopy of first-order theories
por: Campion, Tim, et al.
Publicado: (2023)

Higher presentable categories and limits
por: Aoki, Ko
Publicado: (2025)

Choice axioms and Postnikov completeness
por: Anel, Mathieu, et al.
Publicado: (2024)

Basic Category Theory
por: Leinster, Tom
Publicado: (2016)

Interpreting type theory in a quasicategory: a Yoneda approach
por: Cherradi, El Mehdi
Publicado: (2022)

Elementary $\infty$-toposes from type theory
por: Apol, Daniël, et al.
Publicado: (2025)

Higher geometric sheaf theories
por: Stenzel, Raffael
Publicado: (2022)

$2$-dimensional Lawvere theories: commutativity and lax phenomena
por: Perutka, Tomáš
Publicado: (2026)

Internal languages of locally cartesian closed $(\infty,1)$-categories
por: Cherradi, El Mehdi
Publicado: (2025)

Path Types in Algebraic Type Theory
por: Awodey, Steve, et al.
Publicado: (2026)

Stratifying Reinforcement Learning with Signal Temporal Logic
por: Curry, Justin, et al.
Publicado: (2026)

Intrinsically Correct Sorting in Cubical Agda
por: Alexandru, Cass, et al.
Publicado: (2024)

Towards solid abelian groups: A formal proof of Nöbeling's theorem
por: Asgeirsson, Dagur
Publicado: (2023)