3 citations · 5 across the 13 of their papers we have counts for
13 papers
Autoformalizing the calculation of
Daniel Carranza, Chunyi Liu, Emily Riehl +1
We report our findings and the results of our experiment of autoformalizing the homotopy type theoretic computation of in agda-unimath using Codex.
Discrete homotopy hypothesis for n-types
Daniel Carranza, Chris Kapulkin
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…
Cubical models of -presheaves and the Bousfield-Kan formula
Kensuke Arakawa, Daniel Carranza, Chris Kapulkin
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 versio…
Derived mapping spaces of -categories
Kensuke Arakawa, Daniel Carranza, Chris Kapulkin
We prove the Derived Mapping Space Lemma, which generalizes the central theorem of Cisinski's work on calculus of fractions for -categories, and allows us to provide a unif…
Categorical foundations of discrete dynamical systems
Daniel Carranza, Chris Kapulkin, Nathan Kershaw +2
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…
Nonexistence of colimits in naive discrete homotopy theory
Daniel Carranza, Chris Kapulkin, Jinho Kim
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 set…
Calculus of Fractions for Quasicategories
Daniel Carranza, Chris Kapulkin, Zachery Lindsey
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…
Diagonal Lemma for Presheaves on Eilenberg-Zilber Categories
Daniel Carranza, Chris Kapulkin, Liang Ze Wong
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…
Cofibration category of digraphs for path homology
Daniel Carranza, Brandon Doherty, Chris Kapulkin +3
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 pat…
The Hurewicz theorem for cubical homology
Daniel Carranza, Chris Kapulkin, Andrew Tonks
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…
Cubical setting for discrete homotopy theory, revisited
Daniel Carranza, Chris Kapulkin
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 wit…
Homotopy groups of cubical sets
Daniel Carranza, Chris Kapulkin
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 the…
2-adjoint equivalences in homotopy type theory
Daniel Carranza, Jonathan Chang, Chris Kapulkin +1
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.