# Erasing equality

```agda
module reflection.erasing-equality where
```

<details><summary>Imports</summary>

```agda
open import foundation.universe-levels

open import foundation-core.identity-types
```

</details>

## Idea

Agda's builtin primitive `primEraseEquality` is a special construct on
[identifications](foundation-core.identity-types.md) that for every
identification `x ＝ y` gives an identification `x ＝ y` with the following
reduction behaviour:

- If the two end points `x ＝ y` normalize to the same term, `primEraseEquality`
  reduces to `refl`.

For example, `primEraseEquality` applied to the loop of the
[circle](synthetic-homotopy-theory.circle.md) will compute to `refl`, while
`primEraseEquality` applied to the nontrivial identification in the
[interval](synthetic-homotopy-theory.interval-type.md) will not reduce.

This primitive is useful for [rewrite rules](reflection.rewriting.md), as it
ensures that the identification used in defining the rewrite rule also computes
to `refl`. Concretely, if the identification `β` defines a rewrite rule, and `β`
is defined via `primEraseEqaulity`, then we have the strict equality `β ≐ refl`.

## Primitives

```agda
primitive
  primEraseEquality : {l : Level} {A : UU l} {x y : A} → x ＝ y → x ＝ y
```

## External links

- [Built-ins#Equality](https://agda.readthedocs.io/en/latest/language/built-ins.html#equality)
  at Agda's documentation pages