Univalent Higher Categories via Complete Semi-Segal Types

Univalent Higher Categories via Complete Semi-Segal Types

[Nicolai Kraus]

[-- Attachment #1: Type: text/plain, Size: 5406 bytes --]

The following is a proposal for univalent (n,1)-categories, which we
present in
   Paolo Capriotti and Nicolai Kraus:
   Univalent Higher Categories via Complete Semi-Segal Types
   https://arxiv.org/abs/1707.03693

The goal is to define a generalisation of the univalent categories in the
HoTT book (aka AKS/Ahrens-Kapulkin-Shulman categories [1]) to capture
structures which are not "ordinary" categories.

Fix a number n.
Define a *complete semi-Segal n-type* to be:
 (0) a semisimplicial type A with n+2 levels, written (A_0, A_1, ...,
A_{n+2})
with the following properties:
 (1) "Segal": Inner horns of A have contractible types of fillers.
 (2) "complete": For every point x : A_0, the type of pairs (w, neutral
edge in A_1(w,x)) is contractible, where e : A_1(w,x) is *neutral* if outer
2-horns with e in the correct position have contractible fillers.
 (3) "n-type": The family A_1 : A_0 -> A_0 -> U is a family of (n-1)-types.

The intuition for the connection with (higher) categories is the
following.  Think of A_0 as the type of objects, and A_1 as the family of
morphisms.  The Segal condition on level 2 (i.e. contractibility of fillers
for inner 2-horns) allows us to compose morphisms.  Think of A_2(f,g,h) as
proof for g.f=h.  The Segal condition on level 3 gives associativity of
composition, level 4 gives coherence associativity (the pentagon), and so
on.
Condition (3) is not surprising: as we only have a certain number of
structure, we have a truncatedness condition to ensure that the structure
is well-behaved.  (Recall that for an AKS-category, one assumes that
morphisms are a family of sets.)

So far, we have the structure of a (higher) semicategory.  What is missing
are identities, with all their coherences, plus a univalence condition.  We
could try to add these in the direct way as it is done in the HoTT book,
but (depending on n) this would be quite a lot of additional stuff.
The alternative that we propose is inspired by Yonatan Harpaz' work [2] who
shows that, for infinity-semicategories, a very minimalistic condition
allows the construction of a degeneracy structure.  We can internalise this
idea in type theory, and it turns out that Harpaz' condition not only
allows us to derive an identity structure, but this identity structure is
automatically univalent.  This is nice as it allows the very short
definition above.  Moreover, (1,2,3) are [mere/h-] propositions.
(Completeness also allows a slick formulation of AKS-categories where one
does not have to include identities and univalence in the definition.)

We claim that complete semi-Segal n-types are a well-behaved notion of
univalent (n,1)-categories.  In our paper, Paolo and I give one reason for
this: we show that in the special case n=1, they agree with the established
notion of categories in the HoTT book (AKS), i.e. the definitions are
equivalent.  Further, it is straightforward to generalise AKS-categories to
(2,1)-categories (although that definition is already quite a mouthful); we
do this and we show that this straightforward definition is equivalent to
that of complete semi-Segal 2-types.
It also seems that we can replicate quite a couple of Lurie's results for
infinity-categories [3].  Of course, this is hopeless for Lurie's
"cell-by-cell" arguments, and other non-constructive proofs, but we were
quite surprised that there are still quite a few nontrivial things that
work, or work in other ways. (Of course, our complete semi-Segal types are
closer to complete Segal spaces than to the quasicategories that Lurie
uses.)
But this is work in progress and not written up so far.

Finally, I should say that it's not surprising that we face the usual
issues with semisimplicial types (in "book HoTT", we can only define a type
of 'complete semi-Segal n-types' for an externally fixed n, not for a
variable).  If we could find a way to define univalent n-categories in type
theory, then this would allow us to express certain coherence structures,
and I would very much expect that this would lead to a solution for the
problem of defining semisimplicial types.  Personally, I believe that
sooner or later we really won't want to restrict ourselves to a theory
without such higher structures anymore (and it's hard to justify that such
a theory should be a considered a general foundation).  If it turns out
that "book HoTT" can't to semisimplicial types, switching to an HTS-style
theory seems to be a canonical approach.  Danil Annenkov, Paolo and I have
explored some applications of such a theory with two equality types [4],
with some (very preliminary) internalisations of complete semi-Segal
types.  There, one can even consider unrestricted complete semi-Segal
types, giving a notion of "univalent infinity-categories".

References:
[0] Paolo Capriotti, Nicolai Kraus, Univalent Higher Categories via
Complete Semi-Segal Types, https://arxiv.org/abs/1707.03693
[1] Benedikt Ahrens, Chris Kapulkin, Michael Shulman, Univalent categories
and the Rezk completion, https://arxiv.org/abs/1303.0584
[2] Yonatan Harpaz,  Quasi-unital infinity-categories,
https://arxiv.org/abs/1210.0212
[3] Jacob Lurie, Higher Topos Theory, https://arxiv.org/abs/math/0608040
[4] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Two-Level Type Theory
and Applications, https://arxiv.org/abs/1705.03307

[-- Attachment #2: Type: text/html, Size: 5876 bytes --]