{-# OPTIONS --rewriting #-}

module HottBook.Util where

open import Agda.Primitive
open import HottBook.Chapter1

-- What the hell
-- https://agda.readthedocs.io/en/v2.6.1/language/with-abstraction.html#the-inspect-idiom
module WithAbstractionUtil {a b} {A : Set a} {B : A → Set b} where
  data Graph (f : ∀ x → B x) (x : A) (y : B x) : Set b where
    ingraph : f x ≡ y → Graph f x y
  inspect : (f : ∀ x → B x) (x : A) → Graph f x (f x)
  inspect _ _ = ingraph refl