Contents

# Contents

## Idea

In dependent type theory, and particularly homotopy type theory, an identification is a word sometimes used for an inhabitant of an identity type.

Thus an identification $p:a=b$ provides a “reason”, a “witness”, or a “proof” that $a$ and $b$ “are equal”, or more precisely a way in which to identify them. The distinguishing feature of homotopy type theory is that in general, there may be more than one way to identify two things, i.e. more than one identification between two given elements.