Setoid.Varieties.Preservation

Equation preservation for setoid algebras

This is the Setoid.Varieties.Preservation module of the Agda Universal Algebra Library.

This module proves that the classes H𝒦, S𝒦, P𝒦, and V𝒦 all satisfy the same identities.

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

module Setoid.Varieties.Preservation where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library -------------------------------
open import Data.Product           using ( _,_ ; proj₁ ; proj₂ )
open import Data.Unit.Polymorphic  using ( ⊤ )
open import Function               using ()  renaming ( Func to _⟶_ )
open import Level                  using ( Level ; _⊔_ )
open import Relation.Binary        using ( Setoid )
open import Relation.Unary         using ( Pred ; _⊆_ ; _∈_ )

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Overture                           using  ( 𝑆 )
open import Overture.Terms                     using  ( Term )
open import Setoid.Algebras                    using  ( Algebra ; ov ; ⨅ )
open import Setoid.Homomorphisms               using  ( ≅⨅⁺-refl ; ≅-refl
                                                      ; IdHomImage ; ≅-sym )
open import Setoid.Subalgebras                 using  ( _≤_ ; ⨅-≤ ; ≅-trans-≤
                                                      ; ≤-reflexive )
open import Setoid.Terms                       using  ( module Environment)
open import Setoid.Varieties.Closure           using  ( H ; S ; P ; V ; S-expa ; H-expa
                                                      ; P-expa ; V-expa ; Level-closure )
open import Setoid.Varieties.Properties        using  ( ⊧-H-invar ; ⊧-S-invar
                                                      ; ⊧-P-invar ; ⊧-I-invar )
open import Setoid.Varieties.SoundAndComplete  using  ( _⊧_ ; _⊫_ ; ⊫-proof
                                                      ; _≈̇_ ; _⊢_▹_≈_ ; Th)
open _⟶_      using () renaming ( to to _⟨$⟩_ )
open Algebra  using ( Domain )

Closure properties

The types defined above represent operators with useful closure properties. We now prove a handful of such properties that we need later.

module _  {α ρᵃ ℓ : Level}{𝒦 : Pred(Algebra {𝑆 = 𝑆} α ρᵃ) (α ⊔ ρᵃ ⊔ ov {𝑆 = 𝑆} ℓ)} where
  private
    a = α ⊔ ρᵃ
    oaℓ = ov {𝑆 = 𝑆} (a ⊔ ℓ)

  S⊆SP : ∀{ι} → S ℓ 𝒦 ⊆ S {β = α}{ρᵃ} (a ⊔ ℓ ⊔ ι) (P {β = α}{ρᵃ} ℓ ι 𝒦)
  S⊆SP {ι} (𝑨 , (kA , B≤A )) = 𝑨 , (pA , B≤A)
    where
    pA : 𝑨 ∈ P ℓ ι 𝒦
    pA = ⊤ , (λ _ → 𝑨) , (λ _ → kA) , ≅⨅⁺-refl

  P⊆SP : ∀{ι} → P ℓ ι 𝒦 ⊆ S (a ⊔ ℓ ⊔ ι) (P {β = α}{ρᵃ}ℓ ι 𝒦)
  P⊆SP {ι} x = S-expa{ℓ = a ⊔ ℓ ⊔ ι} x


  P⊆HSP : ∀{ι} →  P {β = α}{ρᵃ} ℓ ι 𝒦 ⊆ H (a ⊔ ℓ ⊔ ι) (S (a ⊔ ℓ ⊔ ι) (P ℓ ι 𝒦))
  P⊆HSP {ι} x = H-expa{ℓ = a ⊔ ℓ ⊔ ι}  (S-expa{ℓ = a ⊔ ℓ ⊔ ι} x)

  P⊆V : ∀{ι} → P ℓ ι 𝒦 ⊆ V ℓ ι 𝒦
  P⊆V = P⊆HSP

  SP⊆V : ∀{ι} → S{β = α}{ρᵇ = ρᵃ} (a ⊔ ℓ ⊔ ι) (P {β = α}{ρᵃ} ℓ ι 𝒦) ⊆ V ℓ ι 𝒦
  SP⊆V {ι} x = H-expa{ℓ = a ⊔ ℓ ⊔ ι} x

Finally, we are in a position to prove that a product of subalgebras of algebras in a class 𝒦 is a subalgebra of a product of algebras in 𝒦.

  PS⊆SP : P (a ⊔ ℓ) oaℓ (S{β = α}{ρᵃ} ℓ 𝒦) ⊆ S oaℓ (P ℓ oaℓ 𝒦)
  PS⊆SP {𝑩} (I , ( 𝒜 , sA , B≅⨅A )) = Goal
    where
    ℬ : I → Algebra {𝑆 = 𝑆} α ρᵃ
    ℬ i = sA i .proj₁

    kB : (i : I) → ℬ i ∈ 𝒦
    kB i =  sA i .proj₂ .proj₁

    ⨅A≤⨅B : ⨅ 𝒜 ≤ ⨅ ℬ
    ⨅A≤⨅B = ⨅-≤ λ i → proj₂ (proj₂ (sA i))
    Goal : 𝑩 ∈ S{β = oaℓ}{oaℓ}oaℓ (P {β = oaℓ}{oaℓ} ℓ oaℓ 𝒦)
    Goal = ⨅ ℬ , (I , (ℬ , (kB , ≅-refl))) , (≅-trans-≤ B≅⨅A ⨅A≤⨅B)

H preserves identities

First we prove that the closure operator H is compatible with identities that hold in the given class.

module _   {α ρᵃ ℓ χ : Level}
            {𝒦 : Pred(Algebra {𝑆 = 𝑆} α ρᵃ) (α ⊔ ρᵃ ⊔ ov {𝑆 = 𝑆} ℓ)}
            {X : Type χ}
            {p q : Term {𝑆 = 𝑆} X}
            where

  H-id1 : 𝒦 ⊫ (p ≈̇ q) → H {β = α}{ρᵃ}ℓ 𝒦 ⊫ (p ≈̇ q)
  H-id1 σ .⊫-proof 𝑩 (𝑨 , kA , BimgA) = ⊧-H-invar{p = p}{q} (σ .⊫-proof 𝑨 kA) BimgA

The converse of the foregoing result is almost too obvious to bother with. Nonetheless, we formalize it for completeness.

  H-id2 : H ℓ 𝒦 ⊫ (p ≈̇ q) → 𝒦 ⊫ (p ≈̇ q)
  H-id2 Hpq .⊫-proof 𝑨 kA = Hpq .⊫-proof 𝑨 (𝑨 , (kA , IdHomImage))

S preserves identities

Identities are inherited by subalgebras, so a class and its subalgebra closure satisfy the same equations. S-id1 is the substantive direction and is immediate from ⊧-S-invar of Setoid.Varieties.Properties: an identity true in 𝑨 is true in anything embedded in 𝑨. S-id2 is the converse, and holds for the same reason H-id2 above does, namely that S is expansive: 𝒦 ⊆ S ℓ 𝒦 by ≤-reflexive, so an identity holding throughout the closure holds in particular on 𝒦.

  S-id1 : 𝒦 ⊫ (p ≈̇ q) → (S {β = α}{ρᵃ} ℓ 𝒦) ⊫ (p ≈̇ q)
  S-id1 σ .⊫-proof 𝑩 (𝑨 , kA , B≤A) = ⊧-S-invar{p = p}{q} (σ .⊫-proof 𝑨 kA) B≤A

  S-id2 : S ℓ 𝒦 ⊫ (p ≈̇ q) → 𝒦 ⊫ (p ≈̇ q)
  S-id2 Spq .⊫-proof 𝑨 kA = Spq .⊫-proof 𝑨 (𝑨 , (kA , ≤-reflexive))

P preserves identities

The same for products, with one extra step. P-id1 combines ⊧-P-invar, that a product of models is a model, with ⊧-I-invar, that satisfaction transports across an isomorphism. The second is needed because membership in P ℓ ι 𝒦 holds only up to isomorphism: an inhabitant supplies a family 𝒜 together with a proof 𝑨 ≅ ⨅ 𝒜, not an equality. P-id2 is once more the expansiveness converse, this time by way of P-expa.

  P-id1 : ∀{ι} → 𝒦 ⊫ (p ≈̇ q) → P {β = α}{ρᵃ}ℓ ι 𝒦 ⊫ (p ≈̇ q)
  P-id1 σ .⊫-proof 𝑨 (I , 𝒜 , kA , A≅⨅A) = ⊧-I-invar 𝑨 p q IH (≅-sym A≅⨅A)
    where
    ih : ∀ i → 𝒜 i ⊧ (p ≈̇ q)
    ih i = σ .⊫-proof (𝒜 i) (kA i)
    IH : ⨅ 𝒜 ⊧ (p ≈̇ q)
    IH = ⊧-P-invar {p = p}{q} 𝒜 ih

  P-id2 : ∀{ι} → P ℓ ι 𝒦 ⊫ (p ≈̇ q) → 𝒦 ⊫ (p ≈̇ q)
  P-id2{ι} PKpq .⊫-proof 𝑨 kA = PKpq .⊫-proof 𝑨 (P-expa {ℓ = ℓ}{ι} kA)

V preserves identities

Finally, we prove the analogous preservation lemmas for the closure operator V.

module _
  {α ρᵃ ℓ ι χ : Level}
  {𝒦 : Pred(Algebra {𝑆 = 𝑆} α ρᵃ) (α ⊔ ρᵃ ⊔ ov {𝑆 = 𝑆} ℓ)}
  {X : Type χ}
  {p q : Term {𝑆 = 𝑆} X}
  where

  private aℓι = α ⊔ ρᵃ ⊔ ℓ ⊔ ι

  V-id1 : 𝒦 ⊫ (p ≈̇ q) → V ℓ ι 𝒦 ⊫ (p ≈̇ q)
  V-id1 σ .⊫-proof 𝑩 (𝑨 , (⨅A , p⨅A , A≤⨅A) , BimgA) =
    H-id1{ℓ = aℓι}{𝒦 = S aℓι (P {β = α}{ρᵃ}ℓ ι 𝒦)} spK⊧pq .⊫-proof 𝑩 (𝑨 , (spA , BimgA))
      where
      spA : 𝑨 ∈ S aℓι (P {β = α}{ρᵃ}ℓ ι 𝒦)
      spA = ⨅A , (p⨅A , A≤⨅A)
      spK⊧pq : S aℓι (P ℓ ι 𝒦) ⊫ (p ≈̇ q)
      spK⊧pq = S-id1{ℓ = aℓι} (P-id1{ℓ = ℓ} {𝒦 = 𝒦} σ)

  V-id2 : V ℓ ι 𝒦 ⊫ (p ≈̇ q) → 𝒦 ⊫ (p ≈̇ q)
  V-id2 Vpq .⊫-proof 𝑨 kA = Vpq .⊫-proof 𝑨 (V-expa ℓ ι kA)

  Lift-id1 : ∀{β ρᵇ} → 𝒦 ⊫ (p ≈̇ q) → Level-closure{α}{ρᵃ}{β}{ρᵇ} ℓ 𝒦 ⊫ (p ≈̇ q)
  Lift-id1 pKq .⊫-proof 𝑨 (𝑩 , kB , B≅A) ρ = Goal
    where
    open Environment 𝑨
    open Setoid (Domain 𝑨) using (_≈_)
    Goal : ⟦ p ⟧ ⟨$⟩ ρ ≈ ⟦ q ⟧ ⟨$⟩ ρ
    Goal = ⊧-I-invar 𝑨 p q (pKq .⊫-proof 𝑩 kB) B≅A ρ

Class identities

From V-id1 it follows that if 𝒦 is a class of structures, then the set of identities modeled by all structures in 𝒦 is equivalent to the set of identities modeled by all structures in V 𝒦. In other terms, Th (V 𝒦) is precisely the set of identities modeled by 𝒦. We formalize this observation as follows.

  classIds-⊆-VIds : 𝒦 ⊫ (p ≈̇ q)  → (p , q) ∈ Th (V ℓ ι 𝒦)
  classIds-⊆-VIds pKq = V-id1 pKq

  VIds-⊆-classIds : (p , q) ∈ Th (V ℓ ι 𝒦) → 𝒦 ⊫ (p ≈̇ q)
  VIds-⊆-classIds Thpq = V-id2 Thpq