Issue447.agda

-- Abstract definitions can't be projection-like
module Issue447 where

postulate
  I : Set
  R : I → Set

module M (i : I) (r : R i) where

  abstract

    P : Set₂
    P = Set₁

    p : P
    p = Set