------------------------------------------------------------------------
-- 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  _⋆
 
_⋆ : R ⇒ SymClosure S → SymClosure R ⇒ SymClosure S
_⋆ f m = join (map f m)