The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Similar Items
Formalizing Computational Paths and Fundamental Groups in Lean
by: Ramos, Arthur F., et al.
Published: (2025)
by: Ramos, Arthur F., et al.
Published: (2025)
A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
by: Ramos, Arthur, et al.
Published: (2025)
by: Ramos, Arthur, et al.
Published: (2025)
Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model
by: Martinez-Rivillas, Daniel O., et al.
Published: (2026)
by: Martinez-Rivillas, Daniel O., et al.
Published: (2026)
Meaning as Use, Application, Employment, Purpose, Usefulness
by: de Queiroz, Ruy J. G. B.
Published: (2025)
by: de Queiroz, Ruy J. G. B.
Published: (2025)
From the Notebooks to the Investigations and Beyond
by: de Queiroz, Ruy J. G. B.
Published: (2025)
by: de Queiroz, Ruy J. G. B.
Published: (2025)
Continuous and algebraic domains in univalent foundations
by: de Jong, Tom, et al.
Published: (2024)
by: de Jong, Tom, et al.
Published: (2024)
The Directed Van Kampen Theorem in Lean
by: Basold, Henning, et al.
Published: (2023)
by: Basold, Henning, et al.
Published: (2023)
2-Coherent Internal Models of Homotopical Type Theory
by: Chen, Joshua
Published: (2025)
by: Chen, Joshua
Published: (2025)
Projective Presentations of Lex Modalities
by: Williams, Mark Damuni
Published: (2025)
by: Williams, Mark Damuni
Published: (2025)
Type Theory with Explicit Universe Polymorphism (revised and extended version)
by: Bezem, Marc, et al.
Published: (2022)
by: Bezem, Marc, et al.
Published: (2022)
On some computational properties of open sets
by: Normann, Dag, et al.
Published: (2024)
by: Normann, Dag, et al.
Published: (2024)
On symmetries of spheres in univalent foundations
by: Cagne, Pierre, et al.
Published: (2024)
by: Cagne, Pierre, et al.
Published: (2024)
Symmetries in Sorting
by: Choudhury, Vikraman, et al.
Published: (2025)
by: Choudhury, Vikraman, et al.
Published: (2025)
A vector logic for extensional formal semantics
by: Quigley, Daniel
Published: (2024)
by: Quigley, Daniel
Published: (2024)
Logic in Mathematics and Computer Science
by: Zach, Richard
Published: (2024)
by: Zach, Richard
Published: (2024)
On the Realizability of Prime Conjectures in Heyting Arithmetic
by: Rosko, Milan
Published: (2025)
by: Rosko, Milan
Published: (2025)
Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
by: Gylterud, Håkon Robbestad, et al.
Published: (2020)
by: Gylterud, Håkon Robbestad, et al.
Published: (2020)
Universal Gluing and Contextual Choice: Categorical Logic and the Foundations of Analytic Approximation
by: Santacana, Andreu Ballus
Published: (2025)
by: Santacana, Andreu Ballus
Published: (2025)
Computability of Initial Value Problems
by: Brattka, Vasco, et al.
Published: (2024)
by: Brattka, Vasco, et al.
Published: (2024)
A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
by: Ramos, Arthur F., et al.
Published: (2026)
by: Ramos, Arthur F., et al.
Published: (2026)
Univalent Material Set Theory
by: Gylterud, Håkon Robbestad, et al.
Published: (2023)
by: Gylterud, Håkon Robbestad, et al.
Published: (2023)
A Logspace Constructive Proof of L=SL
by: Buss, Sam, et al.
Published: (2025)
by: Buss, Sam, et al.
Published: (2025)
Reordered Computable Numbers
by: Janicki, Philip
Published: (2023)
by: Janicki, Philip
Published: (2023)
Computability of the Hahn-Banach Theorem Revisited
by: Brattka, Vasco, et al.
Published: (2026)
by: Brattka, Vasco, et al.
Published: (2026)
The Solver's Paradox in Formal Problem Spaces
by: Rosko, Milan
Published: (2025)
by: Rosko, Milan
Published: (2025)
Formal P-Category Theory and Normalization by Evaluation in Rocq
by: Berry, David G., et al.
Published: (2025)
by: Berry, David G., et al.
Published: (2025)
Computing Distinguishing Formulae for Threshold-Based Behavioural Distances
by: Forster, Jonas, et al.
Published: (2026)
by: Forster, Jonas, et al.
Published: (2026)
Internal Effectful Forcing in System T
by: Escardo, Martin H., et al.
Published: (2025)
by: Escardo, Martin H., et al.
Published: (2025)
The equational theory of the Weihrauch lattice with (iterated) composition
by: Pradic, Cécilia
Published: (2024)
by: Pradic, Cécilia
Published: (2024)
Arithmetics within the Linear Time Hierarchy
by: Pollett, Chris
Published: (2025)
by: Pollett, Chris
Published: (2025)
A Coherence Construction for the Propositional Universe
by: Huang, Xu
Published: (2024)
by: Huang, Xu
Published: (2024)
Uniform Computability of PAC Learning
by: Brattka, Vasco, et al.
Published: (2026)
by: Brattka, Vasco, et al.
Published: (2026)
A declarative approach to specifying distributed algorithms using three-valued modal logic
by: Gabbay, Murdoch J., et al.
Published: (2025)
by: Gabbay, Murdoch J., et al.
Published: (2025)
A proof complexity conjecture and the Incompleteness theorem
by: Krajicek, Jan
Published: (2023)
by: Krajicek, Jan
Published: (2023)
The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification
by: Rahnama, Moses
Published: (2025)
by: Rahnama, Moses
Published: (2025)
Matching logic -- a new axiomatization
by: Leuştean, Laurenţiu, et al.
Published: (2025)
by: Leuştean, Laurenţiu, et al.
Published: (2025)
Notes on applicative matching logic
by: Leuştean, Laurenţiu
Published: (2025)
by: Leuştean, Laurenţiu
Published: (2025)
Computational Paths Form a Weak ω-Groupoid
by: Ramos, Arthur F., et al.
Published: (2025)
by: Ramos, Arthur F., et al.
Published: (2025)
The Tactician's Web of Large-Scale Formal Knowledge
by: Blaauwbroek, Lasse
Published: (2024)
by: Blaauwbroek, Lasse
Published: (2024)
On the existence of strong proof complexity generators
by: Krajicek, Jan
Published: (2022)
by: Krajicek, Jan
Published: (2022)