{-# OPTIONS --postfix-projections --safe --without-K #-}

open import Level using (suc; _⊔_)
open import Relation.Binary
open import Data.Sum using (inj₂)
open import Relation.Binary.Construct.Union using (_∪_)
import Relation.Binary.Construct.Union as Union
open import Relation.Binary.Construct.Core.Symmetric using (SymCore)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star; ε; _◅_; _◅◅_)
import Relation.Binary.Construct.Closure.ReflexiveTransitive as Star
import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties as StarProps
open import Relation.Binary.Construct.Closure.Symmetric using (SymClosure)
import Relation.Binary.Construct.Closure.Symmetric as SymClosure
open import Relation.Binary.Construct.Closure.Equivalence using (EqClosure)
import Relation.Binary.Construct.Closure.Equivalence as EqClosure

module BV.Symmetric {a} (Atom : Set a) where

open import BV.Structure Atom

private
  variable
    A A′ : Atom
    B B′ : Atom
    P P′ : Structure
    Q Q′ : Structure
    R R′ : Structure
    S S′ : Structure

infix 5 _∼_

data _∼_ : Rel Structure a where
  `⊗-assoc     : ((P `⊗ Q) `⊗ R)  (P `⊗ (Q `⊗ R))
  `⊗-comm      : (P `⊗ Q)  (Q `⊗ P)
  `⊗-identityʳ : (P `⊗ `I)  P
  `⅋-assoc     : ((P `⅋ Q) `⅋ R)  (P `⅋ (Q `⅋ R))
  `⅋-comm      : (P `⅋ Q)  (Q `⅋ P)
  `⅋-identityʳ : (P `⅋ `I)  P
  `◁-assoc     : ((P `◁ Q) `◁ R)  (P `◁ (Q `◁ R))
  `◁-identityʳ : (P `◁ `I)  P
  `◁-identityˡ : (`I `◁ P)  P

infix 5 _∼ᶜ_

_∼ᶜ_ : Rel Structure (suc a)
_∼ᶜ_ = CongClosure _∼_

infix 5 _≃_

_≃_ : Rel Structure (suc a)
_≃_ = EqClosure _∼ᶜ_

infix 5 _⟶_

data _⟶_ : Rel Structure a where
  `axiom    :  P  P `⅋  P  `I
  `switch   : (P `⊗ Q) `⅋ R  P `⊗ (Q `⅋ R)
  `sequence : (P `◁ Q) `⅋ (R `◁ S)  (P `⅋ R) `◁ (Q `⅋ S)

  `cut        :  P  `I  P `⊗  P
  `cosequence : (P `⊗ R) `◁ (Q `⊗ S)  (P `◁ Q) `⊗ (R `◁ S)

infix 5 _⟶ᶜ_

_⟶ᶜ_ : Rel Structure (suc a)
_⟶ᶜ_ = CongClosure _⟶_

infix 5 _⟶₌_

_⟶₌_ : Rel Structure (suc a)
_⟶₌_ = _≃_  _⟶ᶜ_

infix  5 _⟶⋆_

_⟶⋆_ : Rel Structure (suc a)
_⟶⋆_ = Star _⟶₌_

step : P  Q  P ⟶₌ Q
step P⟶Q = inj₂ (emb P⟶Q)

infix 5 _⟷⋆_

_⟷⋆_ : Rel Structure (suc a)
_⟷⋆_ = SymCore _⟶⋆_