------------------------------------------------------------------------
-- The Agda standard library
--
-- Lifting a relation such that `nothing` is also related to `just`
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Maybe.Relation.Binary.Connected where
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Function.Bundles using (_⇔_; mk⇔)
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.Definitions using (Reflexive; Sym; Decidable)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open import Relation.Nullary.Decidable as Dec using (yes; no; map)
open import Relation.Nullary.Negation.Core using (¬_)
private
variable
a b ℓ : Level
A : Set a
B : Set b
R S T : REL A B ℓ
x y : A
------------------------------------------------------------------------
-- Definition
data Connected {A : Set a} {B : Set b} (R : REL A B ℓ)
: REL (Maybe A) (Maybe B) (a ⊔ b ⊔ ℓ) where
just : R x y → Connected R (just x) (just y)
just-nothing : Connected R (just x) nothing
nothing-just : Connected R nothing (just y)
nothing : Connected R nothing nothing
------------------------------------------------------------------------
-- Properties
drop-just : Connected R (just x) (just y) → R x y
drop-just (just p) = p
just-equivalence : R x y ⇔ Connected R (just x) (just y)
just-equivalence = mk⇔ just drop-just
------------------------------------------------------------------------
-- Relational properties
refl : Reflexive R → Reflexive (Connected R)
refl R-refl {just _} = just R-refl
refl R-refl {nothing} = nothing
reflexive : _≡_ ⇒ R → _≡_ ⇒ Connected R
reflexive reflexive ≡.refl = refl (reflexive ≡.refl)
sym : Sym R S → Sym (Connected R) (Connected S)
sym R-sym (just p) = just (R-sym p)
sym R-sym nothing-just = just-nothing
sym R-sym just-nothing = nothing-just
sym R-sym nothing = nothing
connected? : Decidable R → Decidable (Connected R)
connected? R? (just x) (just y) = Dec.map just-equivalence (R? x y)
connected? R? (just x) nothing = yes just-nothing
connected? R? nothing (just y) = yes nothing-just
connected? R? nothing nothing = yes nothing
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