------------------------------------------------------------------------
-- 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₂