------------------------------------------------------------------------
-- The Agda standard library
--
-- Apartness properties
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Core using (Rel)
module Relation.Binary.Properties.ApartnessRelation
{a ℓ₁ ℓ₂} {A : Set a}
{_≈_ : Rel A ℓ₁}
{_#_ : Rel A ℓ₂}
where
open import Function.Base using (_∘₂_)
open import Relation.Binary.Definitions using (Reflexive)
open import Relation.Binary.Consequences using (sym⇒¬-sym; cotrans⇒¬-trans)
open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)
open import Relation.Nullary.Negation using (¬_)
¬#-isEquivalence : Reflexive _≈_ → IsApartnessRelation _≈_ _#_ →
IsEquivalence (¬_ ∘₂ _#_)
¬#-isEquivalence re apart = record
{ refl = irrefl re
; sym = λ {a} {b} → sym⇒¬-sym sym {a} {b}
; trans = cotrans⇒¬-trans cotrans
} where open IsApartnessRelation apart
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