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 [[nLab:type]] $\vdash\; X_0 \colon Type$ 1. a [[nLab: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) \,; $$ 1. 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. **[[nLab:n-truncated|0-truncation]]** -- $X_0$ is [[nLab:0-truncated]]/is an [[nLab:h-set]] 1. **[[nLab:coskeleton|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 [[nLab:1-monomorphism]]; 1. **[[nLab: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 [[nLab:equivalence in homotopy type theory|equivalence]]; 1. **[[nLab:univalence|unitality]]** -- the function $$ p_1 \colon \underset{x \colon X_0}{\sum} X_1(x,x) \to X_0 $$ is an [[nLab:equivalence in homotopy type theory|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](http://nforum.mathforge.org/discussion/4537/semisegal-space/?Focus=37128#Comment_37128): A **$(1,1)$-category type** is 1. a [[nLab:type]] $\vdash\; X_0 \colon Type$ 1. a [[nLab: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) \,; $$ 1. 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 [[nLab: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. **[[nLab:n-truncated|1-truncation]]** -- $X_1$ is [[nLab:1-truncated]]/is an [[nLab:h-groupoid]] 1. **[[nLab:coskeleton|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 [[nLab:1-monomorphism]]; 1. **[[nLab: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 [[nLab:equivalence in homotopy type theory|equivalences]]; 1. **[[nLab:univalence|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 [[nLab:equivalence in homotopy type theory|equivalence]]. ## References nforum, semi segal space, [web](http://nforum.mathforge.org/discussion/4537/semisegal-space/#Item_6)