### Congruences of general structures

This is the Structures.Congruences module of the Agda Universal Algebra Library.

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

module Structures.Congruences where

-- Imports from Agda and the Agda Standard Library --------------------------------------
open import Agda.Primitive using ( _⊔_ ; lsuc ) renaming ( Set  to Type )
open import Data.Product   using ( _,_ ; _×_ ; Σ-syntax ) renaming ( proj₁ to fst )
open import Function.Base  using ( _∘_ )
open import Level          using ( Level ; Lift ; lift ; lower )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

-- Imports from the Agda Universal Algebra Library --------------------------------------
open import Overture.Preliminaries using ( ∣_∣ )
open import Relations.Discrete     using ( _|:_ ; 0[_] )
open import Relations.Quotients    using ( Equivalence ; Quotient ; 0[_]Equivalence
; ⟪_⟫ ; ⌞_⌟ ; ⟪_∼_⟫-elim ; _/_ )
open import Equality.Welldefined   using ( swelldef )
open import Structures.Basic       using ( signature ; structure ; sigl
; siglʳ ; compatible )
private variable
𝓞₀ 𝓥₀ 𝓞₁ 𝓥₁ : Level
𝐹 : signature 𝓞₀ 𝓥₀
𝑅 : signature 𝓞₁ 𝓥₁
α ρ : Level

open signature
open structure

con : ∀ {α ρ} → structure 𝐹 𝑅 {α}{ρ} → Type (sigl 𝐹 ⊔ lsuc α ⊔ lsuc ρ)
con {α = α}{ρ} 𝑨 = Σ[ θ ∈ Equivalence (carrier 𝑨){α ⊔ ρ} ] (compatible 𝑨 ∣ θ ∣)
```

#### The zero congruence of a structure

```0[_]compatible : (𝑨 : structure 𝐹 𝑅 {α} {ρ}) → swelldef (siglʳ 𝐹) α
→               (𝑓 : symbol 𝐹) → (op 𝑨) 𝑓 |: (0[ carrier 𝑨 ] {ρ})

0[ 𝑨 ]compatible wd 𝑓 {i}{j} ptws0  = lift γ
where
γ : ((op 𝑨) 𝑓) i ≡ ((op 𝑨) 𝑓) j
γ = wd ((op 𝑨) 𝑓) i j (lower ∘ ptws0)

0con[_] : (𝑨 : structure 𝐹 𝑅 {α} {ρ}) → swelldef (siglʳ 𝐹) α → con 𝑨
0con[ 𝑨 ] wd = 0[ carrier 𝑨 ]Equivalence , 0[ 𝑨 ]compatible wd

```

#### Quotient structures

```_╱_  -- alias  (useful on when signature and universe parameters can be inferred)
quotient : (𝑨 : structure 𝐹 𝑅 {α}{ρ}) → con 𝑨 → structure 𝐹 𝑅
quotient 𝑨 θ = record
{ carrier = Quotient (carrier 𝑨) ∣ θ ∣     -- domain of quotient structure
; op = λ f b → ⟪ ((op 𝑨) f) (λ i → ⌞ b i ⌟) ⟫ {fst ∣ θ ∣} -- interp of operations
; rel = λ r x → ((rel 𝑨) r) (λ i → ⌞ x i ⌟)   -- interpretation of relations
}
_╱_ = quotient

/≡-elim : {𝑨 : structure 𝐹 𝑅 {α}{ρ}} ((θ , _ ) : con 𝑨){u v : carrier 𝑨}
→        ⟪ u ⟫ {∣ θ ∣} ≡ ⟪ v ⟫ {∣ θ ∣} → ∣ θ ∣ u v
/≡-elim θ {u}{v} x =  ⟪ u ∼ v ⟫-elim{R = ∣ θ ∣} x

```

#### The zero congruence of a quotient structure

```𝟎[_╱_] : (𝑨 : structure 𝐹 𝑅 {α}{ρ}) (θ : con 𝑨)
→       swelldef (siglʳ 𝐹)(lsuc (α ⊔ ρ)) → con (𝑨 ╱ θ)
𝟎[ 𝑨 ╱ θ ] wd = 0con[ 𝑨 ╱ θ ] wd

```