Spahn (n,1)-category in Ho TT

To explore the above suggestion, let’s start with the lowest-degree case: with $(0,1)$-category types. How about the following definition?:

A $(0,1)$-category type is

1. a type $\vdash\; X_0 \colon Type$

2. a dependent type $x_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type$;

   we write

   $$X^{\partial \Delta^2} \coloneqq \underset{x_0,x_1,x_2 \colon X_0}{\sum} X_1(x_1,x_2) \times X_1(x_0,x_2) \times X_1(x_0,x_1) \,;$$

3. a dependent type

   $$((x_0,x_1,x_2), (f_0, f_1, f_2)) \colon X^{\partial \Delta^2} \;\vdash \; X_2(f_0,f_1,f_2) \colon Type \,;$$

such that

1. 0-truncation – $X_0$ is 0-truncated/is an h-set

2. 1-coskeletalness – the function

   $$p_1 \colon \underset{(x_0,x_1) \colon X_0 \times X_0 }{\sum} X_1(x_0,x_1) \to X_0 \times X_0$$

   is a 1-monomorphism;

3. Segal condition – the function

   $$( (f_{12},f_{02},f_{01}) \mapsto (f_{12},f_{01}) ) \colon \underset{((x_0,x_1,x_2),(f_{12},f_{02},f_{01})) \colon X^{\partial \Delta^2}}{\sum} X_2 \to \underset{ (x_0,x_1,x_2) \colon X_0 }{\sum} X_1(x_0,x_1) \times X_1(x_1, x_2)$$

   is an equivalence;

4. unitality – the function

   $$p_1 \colon \underset{x \colon X_0}{\sum} X_1(x,x) \to X_0$$

   is an equivalence. To explore the above suggestion, let’s start with the lowest-degree case: with (0,1)-category types. How about the following definition?:

And then the next step in exploring #4:

A $(1,1)$-category type is

1. a type $\vdash\; X_0 \colon Type$

2. a dependent type $x_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type$;

   we write

   $$X^{\partial \Delta^2} \coloneqq \underset{x_0,x_1,x_2 \colon X_0}{\sum} X_1(x_1,x_2) \times X_1(x_0,x_2) \times X_1(x_0,x_1) \,;$$

3. a dependent type

   $$((x_0,x_1,x_2), (f_{12}, f_{02}, f_{01})) \colon X^{\partial \Delta^2} \;\vdash \; X_2(f_{12}, f_{02}, f_{01}) \colon Type \,;$$

   we write

   $$X^{\partial \Delta^3} \coloneqq \underset{(x_0,x_1,x_2,x_3,x_4 \colon X_1) }{\sum} \underset{ f_{i j} \colon X_1(x_i, x_j)}{\sum} X_2(f_{12},f_{02},f_{01}) \times X_2(f_{23}, f_{13}, f_{12}) \times \cdots \,,$$

• a dependent type

  $$(\sigma_{123}, \sigma_{023}, \sigma_{013}, \sigma_{012}) \colon X^{\partial \Delta^3} \;\vdash\; X_3(\sigma_{123}, \sigma_{023}, \sigma_{013}, \sigma_{012}) \colon Type$$

such that

1. 1-truncation – $X_1$ is 1-truncated/is an h-groupoid

2. 2-coskeletalness – the function

   $$p_1 \colon \underset{(f_{12},f_{02}, f_{01}) \colon X^{\partial \Delta^2}}{\sum} X_2(f_{12},f_{02}, f_{01}) \to X^{\partial \Delta^2}$$

   is a 1-monomorphism;

3. Segal condition – the functions

   $$( (f_{12},f_{02},f_{01}) \mapsto (f_{12},f_{01}) ) \colon \underset{((x_0,x_1,x_2),(f_0,f_1,f_2)) \colon X^{\partial \Delta^2}}{\sum} X_2 \to \underset{ (x_0,x_1,x_2) \colon X_0 }{\sum} X_1(x_0,x_1) \times X_1(x_1, x_2)$$

   and

   $$( (f_{i j}, \sigma_{i j k}) \mapsto (f_{01}, f_{12}, f_{23}) ) \colon \underset{f_{i j} \colon X_1(x_i,x_j)}{\sum} \underset{\sigma_{i_0 i_1 i_2} \colon X_2(f_{i_1 i_2}, f_{i_0 i_2}, f_{i_0 i_1})}{\sum} X_3( \sigma_{\cdots}, \cdots ) \to \underset{(x_0,x_1,x_2,x_3) \colon X_0}{\sum} X_1(x_0,x_1) \times X_1(x_1,x_2) \times X_1(x_2,x_3)$$

   are equivalences;

4. unitality – the function

   $$(((x_0,x_1),f) \mapsto x_0) \colon \underset{x_0,x_1 \colon X_0}{\sum} X_1(x_0,x_1)_{\simeq} \to X_0$$

   is an equivalence.

References

nforum, semi segal space, web