    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- A type `A` is irrelevant if all of its elements are equal.
    -- This is also refered to as "A is an h-proposition".
    ------------------------------------------------------------------------

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

    module Relation.Nullary.Irrelevant where

    open import Agda.Builtin.Equality using (_≡_)
    open import Level using (Level)

    private
      variable
        p : Level

    Irrelevant : Set p → Set p
    Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂