Bicategorical classifiers and truncations for partitioned groupoid assemblies
Let be the partial combinatory algebra underlying the assembly category, and let denote the category of partitioned groupoid assemblies. For a morphism , write for the bifunctor on slices induced by bipullback. Bicategorical classifier conjecture. The following should hold for : bipullback along every has both a left and a right biadjoint; there is a sub-object biclassifier classifying -truncated morphisms; for every Grothendieck universe , there is an object biclassifier classifying -fibred -truncated morphisms; and there is a biclassifier for modest -truncated morphisms, with the class of such morphisms closed under bipushforward. The paper notes that the notions of -truncated and modest morphism still need to be developed, and additionally suggests a univalence condition for the two object biclassifiers.
References
Primary source
Anthony Agwu, “A Model of Type Theory in Groupoid Assemblies”, arXiv:2507.16062 (2025).
Progress summary
Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.
Solutions 0
No solutions have been posted yet.