Erasing equality

Content created by Fredrik Bakke.

Created on 2024-04-19.
Last modified on 2024-04-19.

module reflection.erasing-equality where
Imports 
open import foundation.universe-levels

open import foundation-core.identity-types

Idea

Agda's builtin primitive primEraseEquality is a special construct on identifications 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 will compute to refl, while primEraseEquality applied to the nontrivial identification in the interval will not reduce.

This primitive is useful for rewrite rules, 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

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

Recent changes