public open import Primitives using
  ( I
  , intervalInv as fixl  ~  tighter ∨ ∧
  , intervalMin as infix ∧ tighter ∨
  , intervalMax as infix ∨
  )

variable A : Type
inline def ∂ (i : I) ⇒ i ∨ ~ i

example def psqueeze {a b : A} (p : I → A) (i j : I) ⇒ p (i ∧ j)