# nLab enriched type

Contents

### Context

#### Enriched category theory

enriched category theory

## Extra stuff, structure, property

### Homotopical enrichment

#### $(\infty,1)$-Category theory

(∞,1)-category theory

# Contents

## Idea

In homotopy type theory, types represent $\infty$-groupoids, so there should be something similar to enriched $\infty$-groupoids in homotopy type theory. The following definition is an experimental definition of such an object:

## Definition

Let $C$ be the subtype of types in a type universe $\mathcal{U}$ which satisfy a certain predicate $P$: for all types $T:C$, there is a term $p:P(T)$.

Then a type $T$ is $C$-enriched if for all terms $a:T$ and $b:T$, there is a dependent term $p(a,b):P(a = b)$, where $a = b$ is the identity type of $a$ and $b$ in $T$.

## Categorical semantics

Under the relation between type theory and category theory, enriched types should correspond to enriched $\infty$-groupoids in higher category theory.