A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://agda.github.io/agda-stdlib/master/Relation.Nullary.Irrelevant.html below:

Relation.Nullary.Irrelevant

Relation.Nullary.Irrelevant
------------------------------------------------------------------------
-- 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