Contents

# Contents

## Definition

In dependent type theory, an identity system on a type $A$ is a correspondence on $A$, $a:A, b:A \vdash R(a, b)$, with a dependent function

$r_0: \prod_{a:A} R(a, a)$

such that for any family of types

$a:A, b:B, r:R(a, b) \vdash D(a, b, r)$
$d:\prod_{a:A} D(a, a, r(a))$

there exists a dependent function

$f:\prod_{a:A} \prod_{b:B} \prod_{r:R(a, b)} D(a, b, r)$

and a dependent function

$e:\prod_{a:A} f(a, a, r(a)) = d(a)$