------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of polymorphic versions of standard definitions in
-- Relation.Unary
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Unary.Polymorphic.Properties where
open import Data.Unit.Polymorphic.Base using (tt)
open import Level using (Level)
open import Relation.Binary.Definitions hiding (Decidable; Universal; Empty)
open import Relation.Nullary.Decidable.Core using (yes; no)
open import Relation.Unary hiding (∅; U)
open import Relation.Unary.Polymorphic using (∅; U)
private
variable
a ℓ ℓ₁ ℓ₂ : Level
A : Set a
------------------------------------------------------------------------
-- The empty set
∅? : Decidable {A = A} {ℓ} ∅
∅? _ = no λ()
∅-Empty : Empty {A = A} {ℓ} ∅
∅-Empty _ ()
∁∅-Universal : Universal {A = A} {ℓ} (∁ ∅)
∁∅-Universal _ ()
------------------------------------------------------------------------
-- The universe
U? : Decidable {A = A} {ℓ} U
U? _ = yes tt
U-Universal : Universal {A = A} {ℓ} U
U-Universal _ = _
∁U-Empty : Empty {A = A} {ℓ} (∁ U)
∁U-Empty _ x∈∁U = x∈∁U _
------------------------------------------------------------------------
-- Subset properties
∅-⊆ : (P : Pred A ℓ₁) → ∅ {ℓ = ℓ₂} ⊆ P
∅-⊆ _ ()
⊆-U : (P : Pred A ℓ₁) → P ⊆ U {ℓ = ℓ₂}
⊆-U _ _ = _
⊆-min : Min {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊆_ ∅
⊆-min = ∅-⊆
⊆-max : Max {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊆_ U
⊆-max = ⊆-U
∅-⊆′ : (P : Pred A ℓ₁) → ∅ {ℓ = ℓ₂} ⊆′ P
∅-⊆′ _ _ = λ ()
⊆′-U : (P : Pred A ℓ₁) → P ⊆′ U {ℓ = ℓ₂}
⊆′-U _ _ _ = _
⊆′-min : Min {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊆′_ ∅
⊆′-min = ∅-⊆′
⊆′-max : Max {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊆′_ U
⊆′-max = ⊆′-U
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