Where is the operator ≣ defined?

Question

I am trying to write Agda program and struggle with package lookup for reference in the module import section.

As far as I know ≣ is produced from \===.

Grepping agda-library and agda-stdlib projects don't show anything:

grep -r -E  "===[^=]"  ./agda-stdlib/ ./agda-stdlib/src

module Hell3 where

open import Prelude
open import Reflection
--open import Equality
open import Builtin.Reflection
open import Container.List


example : (3 ^ 4) ≣ 81
example = refl 82

Not in scope:
  ≣ at /home/Hell3.agda:11,19-20
when scope checking ≣

Answer 1

Following snippet is correct.

module Hell3 where
open import Relation.Binary.PropositionalEquality  
open import Data.Nat  
example : 3 ^ 4 ≡ 81
example = refl

Thanks to Agda discord channel. So my conclusion is that HoTTEST using custom definitions for standard API - refl doesn't take arguments and erefl should be used, and as noted in the comment here quadbar operator is actually triplebar one.