1
{-# OPTIONS --universe-polymorphism #-}
3
module TrustMe-with-doubly-indexed-equality where
5
open import Common.Level
9
data _≡_ {a} {A : Set a} : A → A → Set a where
12
{-# BUILTIN EQUALITY _≡_ #-}
13
{-# BUILTIN REFL refl #-}
16
primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
25
sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
28
evaluates-to-refl : sym (sym eq) ≡ eq
29
evaluates-to-refl = refl