Cover Image

homotopy.io: a proof assistant for finitely-presented globular $n$-categories

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Corbyn, Nathan, Heidemann, Lukas, Hu, Nick, Sarti, Chiara, Tataru, Calin, Vicary, Jamie
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science Category Theory
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A layout algorithm for higher-dimensional string diagrams
by: Tataru, Calin, et al.
Published: (2023)

The theory and applications of anticolimits
by: Tataru, Calin, et al.
Published: (2024)

Naturality for higher-dimensional path types
by: Benjamin, Thibaut, et al.
Published: (2025)

A Syntax for Strictly Associative and Unital $\infty$-Categories
by: Finster, Eric, et al.
Published: (2023)

Manifold Diagrams for Higher Categories
by: Heidemann, Lukas
Published: (2024)

Partial orders are the free conservative cocompletion of total orders
by: Tataru, Calin
Published: (2024)

Delooping presented groups in homotopy type theory
by: Champin, Camil, et al.
Published: (2024)

Higher presentable categories and limits
by: Aoki, Ko
Published: (2025)

Beyond Eckmann-Hilton: Commutativity in Higher Categories
by: Benjamin, Thibaut, et al.
Published: (2025)

Universal categories
by: Schoutens, Hans
Published: (2025)

Traced monoidal categories as algebraic structures in $\mathbf{Prof}$
by: Hu, Nick, et al.
Published: (2021)

The category of propositional deductive systems
by: Russo, Ciro
Published: (2025)

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

Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
by: Spadetto, Matteo
Published: (2023)

A monoidal category of dependently sorted algebraic theories I: syntax
by: Almeida, Daniel
Published: (2025)

Presentation of finite Reedy categories as localizations of finite direct categories
by: Sato, Genki
Published: (2025)

Etale algebras over finite Heyting algebras
by: Evgeny, Kuznetsov
Published: (2024)

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

Strict Rezk completions of models of HoTT and homotopy canonicity
by: Bocquet, Rafaël
Published: (2023)

The $\infty$-category of $\infty$-categories in simplicial type theory
by: Gratzer, Daniel, et al.
Published: (2026)

Computads for weak $ω$-categories as an inductive type
by: Dean, Christopher J., et al.
Published: (2022)

Invertible cells in $ω$-categories
by: Benjamin, Thibaut, et al.
Published: (2024)

The internal languages of univalent categories
by: van der Weide, Niels
Published: (2024)

E-Graphs With Bindings
by: Tiurin, Aleksei, et al.
Published: (2025)

Hofmann-Streicher lifting of fibred categories
by: Slattery, Andrew, et al.
Published: (2025)

Unbiasing symmetric monoidal categories in Lean
by: Carlier, Robin
Published: (2026)

Monoidal categories graded by partial commutative monoids
by: Earnshaw, Matthew, et al.
Published: (2026)

Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
by: Tiurin, Aleksei, et al.
Published: (2024)

A type theory for invertibility in weak $ω$-categories
by: Benjamin, Thibaut, et al.
Published: (2026)

A type-theoretic approach to semistrict higher categories
by: Rice, Alex
Published: (2025)

Monoidal weak omega-categories as models of a type theory
by: Benjamin, Thibaut
Published: (2021)

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

Between Markov and restriction: Two more monads on categories for relations
by: Cioffo, Cipriano Junior, et al.
Published: (2025)

Globular weak $ω$-categories as models of a type theory
by: Benjamin, Thibaut, et al.
Published: (2021)

Logical relations for call-by-push-value models, via internal fibrations in a 2-category
by: de Amorim, Pedro H. Azevedo, et al.
Published: (2025)

A bialgebraic characterization of symmetric powers in $\mathbb{Q}_{\ge 0}$-linear symmetric monoidal categories
by: Vienney, Jean-Baptiste
Published: (2023)

When Lawvere meets Peirce: an equational presentation of boolean hyperdoctrines
by: Bonchi, Filippo, et al.
Published: (2024)

Various topos of types constructions
by: Kanalas, Kristóf
Published: (2025)

Existence Theorem for Cumulative Universe Towers and Its Applications
by: Reizi, Higuchi Joaquim
Published: (2025)

Term Assignment and Categorical Models for Intuitionistic Linear Logic with Subexponentials
by: Rogozin, Daniel
Published: (2025)