{-# OPTIONS --cubical --safe #-}

module DepthComonads.Inspect where

open import DepthComonads.Level
open import DepthComonads.Path

record Reveal_·_is_ {A : Type a} {B : A → Type b} (f : (x : A) → B x) (x : A) (y : B x) : Type b where
  constructor 〖_〗
  field eq : f x ≡ y

inspect : {A : Type a} {B : A → Type b} (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = 〖 refl 〗