This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Erasing equality

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