# Contents

## Idea

In dependent type theory with a notion of hom type (i.e. modelling $\infty$-categories as envisioned in directed homotopy type theory) and a notion of type universe, the directed univalence axiom for a type universe $U$ states that given two $U$-small types $A \colon U$ and $B \colon U$ there is an equivalence of types between the hom-type $\mathrm{hom}_U(A, B)$ and the function type $A \to B$:

$\mathrm{dua}_U(A, B) \;\colon\; \mathrm{hom}_U(A, B) \,\simeq\, (A \to B) \,.$

The definition also makes sense in analytic models of (infinity,1)-categories such as those constructed from simplicial sets.

## Definition

### In simplicial homotopy type theory

In simplicial homotopy type theory, let $A$ be a Segal type and let $x:A \vdash B(x)$ be a covariant type family. The covariant type family $x:A \vdash B(x)$ satisfies the directed univalence axiom if given two elements $x \colon A$ and $y \colon A$ there is an equivalence of types between the hom type $\mathrm{hom}_A(x, y)$ and the function type $B(x) \to B(y)$:

$\mathrm{dua}_A(x, y) \;\colon\; \mathrm{hom}_A(x, y) \,\simeq\, (B(x) \to B(y)) \,.$