module Semiring.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 Semiring.Signature
open import Semiring.Syntax
open import SOAS.Metatheory.SecondOrder.Metasubstitution SR:Syn
open import SOAS.Metatheory.SecondOrder.Equality SR:Syn
private
variable
Ξ± Ξ² Ξ³ Ο : *T
Ξ Ξ Ξ : Ctx
infix 1 _βΉ_β’_ββ_
data _βΉ_β’_ββ_ : β π Ξ {Ξ±} β (π β· SR) Ξ± Ξ β (π β· SR) Ξ± Ξ β Set where
πUβα΄Έ : β
* βΜ£ βΉ β
β’ π β π ββ π
βA : β
* β β
* β β
* βΜ£ βΉ β
β’ (π β π) β π ββ π β (π β π )
βC : β
* β β
* βΜ£ βΉ β
β’ π β π ββ π β π
πUβα΄Έ : β
* βΜ£ βΉ β
β’ π β π ββ π
πUβα΄Ώ : β
* βΜ£ βΉ β
β’ π β π ββ π
βA : β
* β β
* β β
* βΜ£ βΉ β
β’ (π β π) β π ββ π β (π β π )
βDβα΄Έ : β
* β β
* β β
* βΜ£ βΉ β
β’ π β (π β π ) ββ (π β π) β (π β π )
βDβα΄Ώ : β
* β β
* β β
* βΜ£ βΉ β
β’ (π β π) β π ββ (π β π ) β (π β π )
πXβα΄Έ : β
* βΜ£ βΉ β
β’ π β π ββ π
πXβα΄Ώ : β
* βΜ£ βΉ β
β’ π β π ββ π
open EqLogic _βΉ_β’_ββ_
open β-Reasoning
πUβα΄Ώ : β
* βΜ£ βΉ β
β’ π β π β π
πUβα΄Ώ = tr (ax βC withγ π β π γ) (ax πUβα΄Έ withγ π γ)