---
tag: M9QE6HKDAC
kind: statement
role: proposition
name: Complexity of Identity Type
sources:
  - wikipedia: en:44638758@r1350881027
    locator: Identity type, section Complexity of Identity Type
    note: adopted
    mention: wikipedia://en/44638758#N1EM
    sections: [Statement]
inventory: [C2R9KYNYRD]
---

## Statement

Martin Hofmann and Thomas Streicher refuted the idea that type theory required all terms of the identity type to be the same.

A popular branches of research into the identity type are homotopy type theory and its cubical type theory.