Spahn (n,1)-category in Ho TT

References

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

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

  1. a type X 0:Type\vdash\; X_0 \colon Type

  2. a dependent type x 0,x 1:X 0X 1(x 0,x 1):Typex_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type;

    we write

    X Δ 2x 0,x 1,x 2:X 0X 1(x 1,x 2)×X 1(x 0,x 2)×X 1(x 0,x 1); 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)):X Δ 2X 2(f 0,f 1,f 2):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-truncationX 0X_0 is 0-truncated/is an h-set

  2. 1-coskeletalness – the function

    p 1:(x 0,x 1):X 0×X 0X 1(x 0,x 1)X 0×X 0 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)(f 12,f 01)):((x 0,x 1,x 2),(f 12,f 02,f 01)):X Δ 2X 2(x 0,x 1,x 2):X 0X 1(x 0,x 1)×X 1(x 1,x 2) ( (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:x:X 0X 1(x,x)X 0 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)(1,1)-category type is

  1. a type X 0:Type\vdash\; X_0 \colon Type

  2. a dependent type x 0,x 1:X 0X 1(x 0,x 1):Typex_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type;

    we write

    X Δ 2x 0,x 1,x 2:X 0X 1(x 1,x 2)×X 1(x 0,x 2)×X 1(x 0,x 1); 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)):X Δ 2X 2(f 12,f 02,f 01):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 Δ 3(x 0,x 1,x 2,x 3,x 4:X 1)f ij:X 1(x i,x j)X 2(f 12,f 02,f 01)×X 2(f 23,f 13,f 12)×, 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

    (σ 123,σ 023,σ 013,σ 012):X Δ 3X 3(σ 123,σ 023,σ 013,σ 012):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-truncationX 1X_1 is 1-truncated/is an h-groupoid

  2. 2-coskeletalness – the function

    p 1:(f 12,f 02,f 01):X Δ 2X 2(f 12,f 02,f 01)X Δ 2 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)(f 12,f 01)):((x 0,x 1,x 2),(f 0,f 1,f 2)):X Δ 2X 2(x 0,x 1,x 2):X 0X 1(x 0,x 1)×X 1(x 1,x 2) ( (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 ij,σ ijk)(f 01,f 12,f 23)):f ij:X 1(x i,x j)σ i 0i 1i 2:X 2(f i 1i 2,f i 0i 2,f i 0i 1)X 3(σ ,)(x 0,x 1,x 2,x 3):X 0X 1(x 0,x 1)×X 1(x 1,x 2)×X 1(x 2,x 3) ( (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)x 0):x 0,x 1:X 0X 1(x 0,x 1) X 0 (((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

Created on December 1, 2012 at 05:12:56. See the history of this page for a list of all contributions to it.