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