arXiv subjects

Camil Champin

Publications and source records attributed to Camil Champin.

3 recordsLinked to original sources

arXiv2026

Computads with invertible generators for weak {\omega}-categories

We extend the notion of computads for weak $\omega$-categories to allow marking certain generators as invertible, and describe inductively the free $\omega$-categories they generate. This gives a simple, finite description of the walking equivalences, the $\omega$-categories classifying invertible cells. We then construct a coreflection from generalised to ordinary computads, preserving the generated $\omega$-categories, and conclude that $\omega$-categories generated by generalised computads are cofibrant. Finally, we study the subcategory of generalised computads and generator-preserving morphisms, and show that it is a presheaf topos, similarly to the case of ordinary computads.

math.CT↗

arXiv2026

A type theory for invertibility in weak $\omega$-categories

We present a conservative extension ICaTT of the dependent type theory CaTT for weak $\omega$-categories with a type witnessing coinductive invertibility of cells. This extension allows for a concise description of the "walking equivalence" as a context, and of a set of maps characterising $\omega$-equifibrations as substitutions. We provide an implementation of our theory, which we use to formalise basic properties of invertible cells. These properties allow us to give semantics of ICaTT in marked weak $\omega$-categories, building a fibrant marked $\omega$-category out of every model of ICaTT.

math.CT↗

arXiv2024

Delooping presented groups in homotopy type theory

Homotopy type theory is a logical setting based on Martin-L\"of type theory in which geometric constructions and proofs can be carried out synthetically. Here, types can be interpreted as spaces up to homotopy, and proofs as homotopy-invariant constructions. In this context, the loop spaces of pointed connected groupoids provide a natural representation of groups, and every group can be realized as the loop space of such a type, which is then called a delooping of the group. There are two main methods for constructing a delooping of an arbitrary group G. The first describes it as a pointed higher inductive type, while the second takes the connected component of the principal G-torsor in the type of sets equipped with a G-action. We show that, when a presentation, or even just a generating set, is known for the group, simpler variants of these constructions can be used to build deloopings. The resulting types are more amenable to computation and lead to simpler metatheoretic reasoning. Finally, we develop a type-theoretic notion of 2-polygraph for manipulating higher inductive types such as those arising in the description of deloopings. This allows us to investigate a construction of the Cayley graph of a generated group and to show that it encodes the relations of the group, as well as a Cayley complex encoding relations between relations. Many of the developments in this article have been formalized in the cubical version of the Agda proof assistant.

cs.LO↗