------------------------------------------------------------------------ -- 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₂
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4