    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Polymorphic versions of standard definitions in Relation.Unary
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Relation.Unary.Polymorphic where

    open import Data.Empty.Polymorphic using (⊥)
    open import Data.Unit.Polymorphic using (⊤)
    open import Level using (Level)
    open import Relation.Unary using (Pred)

    private
      variable
        a ℓ : Level
        A : Set a

    ------------------------------------------------------------------------
    -- Special sets

    -- The empty set.

    ∅ : Pred A ℓ
    ∅ = λ _ → ⊥

    -- The universal set.

    U : Pred A ℓ
    U = λ _ → ⊤