↑ Top


Congruences of general structures

{-# OPTIONS --without-K --exact-split --safe #-}

module Base.Structures.Sigma.Congruences where

-- Imports from the Agda Standard Library ------------------------------------------------
open import Agda.Primitive   using () renaming ( Set to Type ; lzero to ℓ₀ )
open import Data.Product     using ( _,_ ; _×_ ; Σ-syntax ) renaming ( proj₁ to fst )
open import Function         using ( _∘_ )
open import Level            using (  _⊔_ ; suc ; Level ; Lift ; lift ; lower )
open import Relation.Unary   using ( Pred ; _∈_ )
open import Relation.Binary  using ( IsEquivalence ) renaming ( Rel to BinRel )
open import Relation.Binary.PropositionalEquality using ( _≡_ )

-- Imports from the Agda Universal Algebra Library ---------------------------------------
open import Overture        using ( ∣_∣ )
open import Base.Equality   using ( swelldef )
open import Base.Relations  using ( _|:_ ; 0[_] ; Equivalence ; ⟪_⟫ ; ⌞_⌟ )
                            using ( 0[_]Equivalence ; _/_ ; ⟪_∼_⟫-elim ; Quotient )
open import Base.Structures.Sigma.Basic
                            using ( Signature ; Structure ; _ᵒ_ ; Compatible ; _ʳ_ )

private variable 𝑅 𝐹 : Signature

module _ {α ρ : Level} where

 Con : (𝑨 : Structure 𝑅 𝐹 {α}{ρ})  Type (suc (α  ρ))
 Con 𝑨 = Σ[ θ  Equivalence  𝑨 {α  ρ} ] (Compatible 𝑨  θ )

 -- The zero congruence of a structure.
 0[_]Compatible :  (𝑨 : Structure 𝑅 𝐹 {α}{ρ})  swelldef ℓ₀ α
                  (𝑓 :  𝐹 )  (𝑓  𝑨) |: (0[  𝑨  ]{ρ})

 0[ 𝑨 ]Compatible wd 𝑓 {i}{j} ptws0  = lift γ
  where
  γ : (𝑓  𝑨) i  (𝑓  𝑨) j
  γ = wd (𝑓  𝑨) i j (lower  ptws0)

 0Con[_] : (𝑨 : Structure 𝑅 𝐹 {α}{ρ})  swelldef ℓ₀ α  Con 𝑨
 0Con[ 𝑨 ] wd = 0[  𝑨  ]Equivalence , 0[ 𝑨 ]Compatible wd

Quotients of structures of sigma type

 _╱_ : (𝑨 : Structure 𝑅 𝐹 {α}{ρ})  Con 𝑨  Structure 𝑅 𝐹 {suc (α  ρ)}{ρ}

 𝑨  θ =  ( Quotient ( 𝑨 ) {α  ρ}  θ )       -- domain of quotient structure
          ,  r x  (r ʳ 𝑨) λ i   x i )       -- interpretation of relations
          , λ f b   (f  𝑨)  i   b i )    -- interp of operations

 /≡-elim :  {𝑨 : Structure 𝑅 𝐹 {α}{ρ}}( (θ , _ ) : Con 𝑨){u v :  𝑨 }
            u { θ }   v    θ  u v

 /≡-elim θ {u}{v} x =   u  v ⟫-elim {R =  θ } x

The zero congruence of an arbitrary structure

 𝟘[_╱_] :  (𝑨 : Structure 𝑅 𝐹 {α}{ρ})(θ : Con 𝑨)
          BinRel ( 𝑨  / (fst  θ )) (suc (α  ρ))

 𝟘[ 𝑨  θ ] = λ u v  u  v

𝟎[_╱_] :  {α ρ : Level}(𝑨 : Structure 𝑅 𝐹 {α}{ρ})(θ : Con 𝑨)
         swelldef ℓ₀ (suc (α  ρ))  Con (𝑨  θ)

𝟎[ 𝑨  θ ] wd = 0[  𝑨  θ  ]Equivalence , 0[ 𝑨  θ ]Compatible wd

← Base.Structures.Sigma.Products Base.Structures.Sigma.Homs →