------------------------------------------------------------------------
-- 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)