------------------------------------------------------------------------
-- The Agda standard library
--
-- Symmetric closures of binary relations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Construct.Closure.Symmetric where
open import Function.Base using (id; _on_)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_)
open import Relation.Binary.Definitions using (Symmetric)
import Relation.Binary.Construct.On as On
private
variable
a ℓ ℓ₁ ℓ₂ : Level
A B : Set a
R S : Rel A ℓ
------------------------------------------------------------------------
-- Definition
data SymClosure {A : Set a} (R : Rel A ℓ) (a b : A) : Set ℓ where
fwd : R a b → SymClosure R a b
bwd : R b a → SymClosure R a b
------------------------------------------------------------------------
-- Properties
-- Symmetric closures are symmetric.
symmetric : (R : Rel A ℓ) → Symmetric (SymClosure R)
symmetric _ (fwd aRb) = bwd aRb
symmetric _ (bwd bRa) = fwd bRa
------------------------------------------------------------------------
-- Operations
-- A generalised variant of `map` which allows the index type to change.
gmap : (f : A → B) → R =[ f ]⇒ S → SymClosure R =[ f ]⇒ SymClosure S
gmap _ g (fwd aRb) = fwd (g aRb)
gmap _ g (bwd bRa) = bwd (g bRa)
map : R ⇒ S → SymClosure R ⇒ SymClosure S
map = gmap id
fold : Symmetric S → R ⇒ S → SymClosure R ⇒ S
fold S-sym R⇒S (fwd aRb) = R⇒S aRb
fold S-sym R⇒S (bwd bRa) = S-sym (R⇒S bRa)
-- A generalised variant of `fold`.
gfold : Symmetric S → (f : A → B) → R =[ f ]⇒ S → SymClosure R =[ f ]⇒ S
gfold {S = S} S-sym f R⇒S = fold (On.symmetric f S S-sym) R⇒S
-- `return` could also be called `singleton`.
return : R ⇒ SymClosure R
return = fwd
-- `join` could also be called `concat`.
join : SymClosure (SymClosure R) ⇒ SymClosure R
join = fold (symmetric _) id
infix 10 _⋆
_⋆ : R ⇒ SymClosure S → SymClosure R ⇒ SymClosure S
_⋆ f m = join (map f m)
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