    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Symmetric transitive closures of binary relations
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Relation.Binary.Construct.Closure.SymmetricTransitive where

    open import Level
    open import Function.Base
    open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_)
    open import Relation.Binary.Bundles using (PartialSetoid; Setoid)
    open import Relation.Binary.Structures
      using (IsPartialEquivalence; IsEquivalence)
    open import Relation.Binary.Definitions
      using (Transitive; Symmetric; Reflexive)

    private
      variable
        a c ℓ ℓ′ : Level
        A B      : Set a

    module _ {A : Set a} (_≤_ : Rel A ℓ) where

      data Plus⇔ : Rel A (a ⊔ ℓ) where
        forth  : ∀ {x y} → x ≤ y → Plus⇔ x y
        back   : ∀ {x y} → y ≤ x → Plus⇔ x y
        forth⁺ : ∀ {x y z} → x ≤ y → Plus⇔ y z → Plus⇔ x z
        back⁺  : ∀ {x y z} → y ≤ x → Plus⇔ y z → Plus⇔ x z

      trans : Transitive Plus⇔
      trans (forth r) rel′      = forth⁺ r rel′
      trans (back r) rel′       = back⁺ r rel′
      trans (forth⁺ r rel) rel′ = forth⁺ r (trans rel rel′)
      trans (back⁺ r rel) rel′  = back⁺ r (trans rel rel′)

      sym : Symmetric Plus⇔
      sym (forth r)      = back r
      sym (back r)       = forth r
      sym (forth⁺ r rel) = trans (sym rel) (back r)
      sym (back⁺ r rel)  = trans (sym rel) (forth r)

      isPartialEquivalence : IsPartialEquivalence Plus⇔
      isPartialEquivalence = record
        { sym   = sym
        ; trans = trans
        }

      partialSetoid : PartialSetoid _ _
      partialSetoid = record
        { Carrier              = A
        ; _≈_                  = Plus⇔
        ; isPartialEquivalence = isPartialEquivalence
        }

      module _ (refl : Reflexive _≤_) where

        isEquivalence : IsEquivalence Plus⇔
        isEquivalence = record
          { refl  = forth refl
          ; sym   = sym
          ; trans = trans
          }

        setoid : Setoid _ _
        setoid = record
          { Carrier       = A
          ; _≈_           = Plus⇔
          ; isEquivalence = isEquivalence
          }

      module _ (S : Setoid c ℓ) where
        private
          module S = Setoid S

        minimal : (f : A → S.Carrier) →
                  _≤_ =[ f ]⇒ S._≈_ →
                  Plus⇔ =[ f ]⇒ S._≈_
        minimal f inj (forth r)      = inj r
        minimal f inj (back r)       = S.sym (inj r)
        minimal f inj (forth⁺ r rel) = S.trans (inj r) (minimal f inj rel)
        minimal f inj (back⁺ r rel)  = S.trans (S.sym (inj r)) (minimal f inj rel)

    module Plus⇔Reasoning (_≤_ : Rel A ℓ) where
      infix  3 forth-syntax back-syntax
      infixr 2 forth⁺-syntax back⁺-syntax

      forth-syntax : ∀ x y → x ≤ y → Plus⇔ _≤_ x y
      forth-syntax _ _ = forth

      syntax forth-syntax x y x≤y = x ⇒⟨ x≤y ⟩∎ y ∎

      back-syntax : ∀ x y → y ≤ x → Plus⇔ _≤_ x y
      back-syntax _ _ = back

      syntax back-syntax x y y≤x = x ⇐⟨ y≤x ⟩∎ y ∎

      forth⁺-syntax : ∀ x {y z} → x ≤ y → Plus⇔ _≤_ y z → Plus⇔ _≤_ x z
      forth⁺-syntax _ = forth⁺

      syntax forth⁺-syntax x x≤y y⇔z = x ⇒⟨ x≤y ⟩ y⇔z

      back⁺-syntax : ∀ x {y z} → y ≤ x → Plus⇔ _≤_ y z → Plus⇔ _≤_ x z
      back⁺-syntax _ = back⁺

      syntax back⁺-syntax x y≤x y⇔z = x ⇐⟨ y≤x ⟩ y⇔z

    module _ {_≤_ : Rel A ℓ} {_≼_ : Rel B ℓ′} where

      gmap : (f : A → B) (inj : _≤_ =[ f ]⇒ _≼_) → Plus⇔ _≤_ =[ f ]⇒ Plus⇔ _≼_
      gmap f inj (forth r)      = forth (inj r)
      gmap f inj (back r)       = back (inj r)
      gmap f inj (forth⁺ r rel) = forth⁺ (inj r) (gmap f inj rel)
      gmap f inj (back⁺ r rel)  = back⁺ (inj r) (gmap f inj rel)

    map : {_≤_ : Rel A ℓ} {_≼_ : Rel A ℓ′} (inj : _≤_ ⇒ _≼_) → Plus⇔ _≤_ ⇒ Plus⇔ _≼_
    map = gmap id