Tootfinder

The Groupoid-syntax of Type Theory is a Set
Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie
https://arxiv.org/abs/2509.14988 https://arxiv.org/pdf/2509.14988…

The Groupoid-syntax of Type Theory is a Set
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporate…

Replaced article(s) found for math.CT. https://arxiv.org/list/math.CT/new
[1/1]:
- Strict Rezk completions of models of HoTT and homotopy canonicity
Rafa\"el Bocquet

The latest 3blue1brown video on Burnside's lemma made me realise that the HoTT/concrete group version of the following fact:
Given a G-set X and a set Y, the set of invariant functions X − Y under the action of G is equivalent to the set of functions X/G − Y.
is just the "dependent currying" isomorphism
((s : BG) − X(s) − Y) ≃ (((s : BG) × X(s)) − Y)
since Π-types give invariants and Σ-types give orbits.

Is there an "established" name for the construction in HoTT that associates to every 1-type A the category with A as objects and paths as morphisms, i.e. turns a groupoid (type) into a groupoid (category)?