prime package:Agda

Identifier ends in Integer many primes.
Get the name of the equality type.
primEraseEquality : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ y