[Agda] Inspect.

[flicky frans]

Hello. I am probably missing something obvious, but why `inspect' is
not defined like this?

record Reveal_·_is_ {α β} {A : Set α} {B : A -> Set β}
  (f : (x : A) -> B x) (x : A) (y : B x) : Set (α ⊔ β) where
    constructor [_]
    field eq : f x ≡ y

inspect : ∀ {α β} {A : Set α} {B : A -> Set β}
        -> (f : (x : A) -> B x) -> (x : A) -> Reveal f · x is f x
inspect f x = [ refl ]

This looks simpler and still allows you to pattern-match on (f x) and
to remember, that (f x ≡ y).