{-# OPTIONS --rewriting #-}

module _ where
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

postulate
  I : Set

module N (i : I) where
-- module N where
  -- variable i : I
  -- postulate i : I

  postulate
    [_] : I → Set
    rw : [ i ] ≡ Nat
  {-# REWRITE rw #-}

  f : [ i ] → Set
  f p = {! !}