    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Indexed unary relations over sized types
    ------------------------------------------------------------------------

    -- Sized types live in the special sort `SizeUniv` and therefore are no
    -- longer compatible with the ordinary combinators defined in
    -- `Relation.Unary`.

    {-# OPTIONS --cubical-compatible --sized-types #-}

    module Relation.Unary.Sized  where

    open import Level
    open import Size

    private
      variable
        ℓ ℓ₁ ℓ₂ : Level

    infixr 8 _⇒_
    _⇒_ : SizedSet ℓ₁ → SizedSet ℓ₂ → SizedSet (ℓ₁ ⊔ ℓ₂)
    F ⇒ G = λ i → F i → G i

    ∀[_] : SizedSet ℓ → Set ℓ
    ∀[ F ] = ∀{i} → F i