{-# OPTIONS --without-K --rewriting #-}
module rewriting where
open import foundation.universe-levels using (UU)

postulate
   _↦_ : ∀ {i} {A : UU i} → A → A → UU i

{-# BUILTIN REWRITE _↦_ #-}