Publications

Papers & preprints.

2026

RedZeD: Computing persistent homology by Reduction to Zero Differentials

with N. Kershaw · preprint, 2026

2026

Towards fast computation of higher discrete homology

with J. Ender · preprint, 2026

2026

Discrete homotopy hypothesis for n-types

with D. Carranza · preprint, 2026

2026

A Toolkit for Structured Lifts

with Y. Li · Theory Appl. Categ. 45 (2026), Paper No. 19, 717-758

2025

Yet another cubical type theory, but via a semantic approach

with Y. Li · preprint, 2025

2025

(Pointed) Univalence in Universe Category Models of Type Theory

with Y. Li · preprint, 2025

2025

Fast computation of the first discrete homology group

with J. Ender · preprint, 2025

2025

Biclosed monoidal structures on the categories of digraphs and graphs

with A. Grenier · preprint, 2025

2025

Cubical models of ∞-presheaves and the Bousfield-Kan formula

with K. Arakawa and D. Carranza · preprint, 2025

2025

Derived mapping spaces of ∞-categories

with K. Arakawa and D. Carranza · Algebr. Geom. Topol. (to appear), 2025

2025

Data analysis using discrete cubical homology

with N. Kershaw · preprint, 2025

2025

Pushforwards in Homotopical Inverse Categories

with Y. Li · preprint, 2025

2025

Categorical foundations of discrete dynamical systems

with D. Carranza, N. Kershaw, R. Laubenbacher, and M. Wheeler · preprint, 2025

2025

Synthetic approach to the Quillen model structure on topological spaces

with S. Ebel · Algebr. Geom. Topol. 25 (2025), 1227-1264

2025

Extensional concepts in intensional type theory, revisited

with Y. Li · Theoret. Comput. Sci. 1029 (2025), Paper No. 115015

2025

Diagonal Lemma for Presheaves on Eilenberg-Zilber Categories

with D. Carranza and L.-Z. Wong · Theory Appl. Categ. 44 (2025), Paper No. 11, 326-343

2025

The fundamental group(oid) in discrete homotopy theory

with U. Mavinkurve · Adv. Appl. Math. 164 (2025), Paper No. 102838

2025

A cubical model for (∞,n)-categories

with T. Campion and Y. Maehara · Geom. Topol. 29 (2025), no. 3, 1115-1170

2024

Logical Structure on Inverse Functor Categories

with M. Fiore and Y. Li · preprint, 2024

2024

Efficient computations of discrete cubical homology

with N. Kershaw · submitted, 2024

2024

Homotopy n-types of cubical sets and graphs

with U. Mavinkurve · submitted, 2024

2024

Closed symmetric monoidal structures on the category of graphs

with N. Kershaw · Theory Appl. Categ. 41 (2024), Paper No. 23, 760–784

2024

Cofibration category of digraphs for path homology

with D. Carranza, B. Doherty, M. Opie, M. Sarazola, and L.-Z. Wong · Algebr. Comb. 7 (2024), no. 2, 475–514

2024

Cubical setting for discrete homotopy theory, revisited

with D. Carranza · Compos. Math. 160, no. 12 (2024), 2856–2903

2024

Cubical models of (∞,1)-categories

with B. Doherty, Z. Lindsey, and C. Sattler · Mem. Amer. Math. Soc. 297 (2024), no. 1484

2023

Nonexistence of colimits in naive discrete homotopy theory

with D. Carranza and J. Kim · Appl. Categ. Structures 31 (2023), no.5, 41

2023

Calculus of Fractions for Quasicategories

with D. Carranza and Z. Lindsey · preprint, 2023

2023

The Hurewicz theorem for cubical homology

with D. Carranza and A. Tonks · Math. Z. 305, 61 (2023)

2023

Homotopy groups of cubical sets

with D. Carranza · Expo. Math. 41 (2023) 125518, no. 4

2023

Equivalence of cubical and simplicial approaches to (∞,n)-categories

with B. Doherty and Y. Maehara · Adv. Math. 416 (2023) 108902

2021

2-adjoint equivalences in homotopy type theory

with D. Carranza, J. Chang, and R. Sandford · Log. Methods Comput. Science 17 (2021), no. 1, Paper No. 3

2021

Homotopical inverse diagrams in categories with attributes

with P. LeF. Lumsdaine · J. Pure Appl. Algebra 225 (2021), no. 4

2021

The Simplicial Model of Univalent Foundations (after Voevodsky)

with P. LeF. Lumsdaine · J. Eur. Math. Soc. (JEMS) 23 (2021), no. 6, 2071-2126

2020

The Law of Excluded Middle in the Simplicial Model of Type Theory

with P. LeF. Lumsdaine · Theory Appl. Categ. 35 (2020), Paper No. 40, 1546–1548

2020

A Cubical Approach to Straightening

with V. Voevodsky · J. Topol. 13 (4), 1682-1700, 2020

2019

A co-reflection of cubical sets into simplicial sets with applications to model structures

with Z. Lindsey and L.-Z. Wong · New York J. Math. 25 (2019), 627–641

2019

Internal Language of Finitely Complete (∞,1)-categories

with K. Szumiło · Selecta Math. (N.S.) 25 (2019), no. 2, Art. 33

2018

Threshold Properties of Prime Power Subgroups with Application to Secure Integer Comparisons

with R. Carlton and A. Essex · Topics in Cryptology – CT-RSA 2018, 137-156, LNCS 10808

2018

The Homotopy Theory of Type Theories

with P. LeF. Lumsdaine · Adv. Math. 337, 1-38, 2018

2017

Locally cartesian closed quasicategories from type theory

J. Topol. 10 (4), 1029-1049, 2017

2017

Quasicategories of frames of cofibration categories

with K. Szumiło · Appl. Categor. Struct. 25 (2017), no. 3, 323–347

2015

Homotopy limits in type theory

with J. Avigad and P. LeF. Lumsdaine · Math. Structures Comput. Science 25 (2015), no. 5, 1040–1070

2015

Univalent categories and the Rezk completion

with B. Ahrens and M. Shulman · Math. Structures Comput. Science 25 (2015), no. 5, 1010–1039

2014

Joyal's Conjecture in Homotopy Type Theory

PhD dissertation, 148 pp., 2014

2013

Homotopy Type Theory (The HoTT Book)

with as part of the Univalent Foundations Project · 2013

2012

Univalence in Simplicial Sets

with P. LeF. Lumsdaine and V. Voevodsky · not intended for publication, 2012

2012

Expressiveness of positive coalgebraic logic

with A. Kurz and J. Velebil · Advances in modal logic. Vol. 9, 368–385, Coll. Publ., London, 2012

2011

Homotopy-theoretic models of type theory

with P. Arndt · Typed lambda calculi and applications, 45–60, LNCS 6690, Springer, 2011

Google Scholar arXiv MathSciNet