Autoformalizing the calculation of $\pi_3(S^2)$
We report our findings and the results of our experiment of autoformalizing the homotopy type theoretic computation of $\pi_3(S^2)$ in agda-unimath using Codex.
math.AT↗
arXiv subjects
Daniel Carranza
Publications and source records attributed to Daniel Carranza.
Discrete homotopy hypothesis for n-types
We show that discrete and classical homotopy theories are equivalent after localizing at n-equivalences for any non-negative integer n. By constructing an explicit homotopy inverse to the graph nerve functor associating an n-fibrant cubical set to a graph, we are also able to give explicit computations of several previously unknown discrete homotopy groups of boundaries of cubes and suspensions of cycles.
math.AT↗
Cubical models of $\infty$-presheaves and the Bousfield-Kan formula
We construct the covariant and the cocartesian model structures on the slice categories of cubical sets and marked cubical sets, respectively. As an application, we derive a version of the Bousfield-Kan formula for arbitrary cofibrantly generated monoidal model categories satisfying Muro's axiom.
math.AT↗
Derived mapping spaces of $\infty$-categories
We prove the Derived Mapping Space Lemma, which generalizes the central theorem of Cisinski's work on calculus of fractions for $\infty$-categories, and allows us to provide a unified framework for analyzing mapping spaces in localizations of ($\infty$-)categories. As an application, we give a sufficient condition for when a cubical or simplicial category is the localization of its underlying category at homotopy equivalences.
math.AT↗
Categorical foundations of discrete dynamical systems
We develop categorical foundations of discrete dynamical systems, aimed at understanding how the structure of the system affects its dynamics. We introduce the notion of cycle sets to analyze attractors of a system, and use this to generalize multiple decomposition theorems of Kadelka, Veliz-Cuba, Murrugarra, and the last two authors from Boolean networks to arbitrary discrete dynamical systems.
math.DS↗
Diagonal Lemma for Presheaves on Eilenberg-Zilber Categories
The diagonal lemma asserts that if a map of bisimplicial sets is a levelwise weak equivalence in the Kan-Quillen model structure, then it induces a weak equivalence of the diagonal simplicial sets. In this short note, we observe that the standard proof of this fact works for an arbitrary Eilenberg-Zilber category in place of the simplex category.
math.AT↗
Calculus of Fractions for Quasicategories
We describe a generalization of Gabriel and Zisman's Calculus of Fractions to quasicategories, showing that the two essentially coincide for the nerve of a category. We then prove that the marked Ex-functor can be used to compute the localization of a marked quasicategory satisfying our condition and that the appropriate (co)completeness properties of the quasicategory carry over to its localization.
math.AT↗
Nonexistence of colimits in naive discrete homotopy theory
We show that the quasicategory defined as the localization of the category of (simple) graphs at the class of A-homotopy equivalences does not admit colimits. In particular, we settle in the negative the question of whether the A-homotopy equivalences in the category of graphs are part of a model structure.
math.CO↗
Cofibration category of digraphs for path homology
We prove that the category of directed graphs and graph maps carries a cofibration category structure in which the weak equivalences are the graph maps inducing isomorphisms on path homology.
math.CO↗
The Hurewicz theorem for cubical homology
We give an elementary proof of the Hurewicz theorem relating homotopy and homology groups of a cubical Kan complex. Our approach is based on the notion of a loop space of a cubical set, developed in a companion paper ``Homotopy groups of cubical sets'' by the first two authors.
math.AT↗
Homotopy groups of cubical sets
We define and study homotopy groups of cubical sets. To this end, we give four definitions of homotopy groups of a cubical set, prove that they are equivalent, and further that they agree with their topological analogues via the geometric realization functor. We also provide purely combinatorial proofs of several classical theorems, including: product preservation, commutativity of higher homotopy groups, the long exact sequence of a fibration, and Whitehead's theorem. This is a companion paper to our "Cubical setting for discrete homotopy theory, revisited" in which we apply these results to study the homotopy theory of simple graphs.
math.AT↗
Cubical setting for discrete homotopy theory, revisited
We construct a functor associating a cubical set to a (simple) graph. We show that cubical sets arising in this way are Kan complexes, and that the A-groups of a graph coincide with the homotopy groups of the associated Kan complex. We use this to prove a conjecture of Babson, Barcelo, de Longueville, and Laubenbacher from 2006, and a strong version of the Hurewicz theorem in discrete homotopy theory.
math.CO↗
2-adjoint equivalences in homotopy type theory
We introduce the notion of (half) 2-adjoint equivalences in Homotopy Type Theory and prove their expected properties. We formalized these results in the Lean Theorem Prover.
math.LO↗