module CommMonoid.Equality where
open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive
open import CommMonoid.Signature
open import CommMonoid.Syntax
open import SOAS.Metatheory.SecondOrder.Metasubstitution CM:Syn
open import SOAS.Metatheory.SecondOrder.Equality CM:Syn
private
variable
α β γ τ : *T
Γ Δ Π : Ctx
infix 1 _▹_⊢_≋ₐ_
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ CM) α Γ → (𝔐 ▷ CM) α Γ → Set where
εU⊕ᴸ : ⁅ * ⁆̣ ▹ ∅ ⊢ ε ⊕ 𝔞 ≋ₐ 𝔞
⊕A : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ⊕ 𝔟) ⊕ 𝔠 ≋ₐ 𝔞 ⊕ (𝔟 ⊕ 𝔠)
⊕C : ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ⊕ 𝔟 ≋ₐ 𝔟 ⊕ 𝔞
open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning
εU⊕ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ⊕ ε ≋ 𝔞
εU⊕ᴿ = tr (ax ⊕C with《 𝔞 ◃ ε 》) (ax εU⊕ᴸ with《 𝔞 》)