Skip to content

Commit

Permalink
Merge pull request #164 from williamdemeo/reorg
Browse files Browse the repository at this point in the history 
major reorganization
  • Loading branch information
@williamdemeo
williamdemeo authored Nov 26, 2021
2 parents 2326908 + 7a596b5 commit cde5198
Show file tree
Hide file tree
Showing 51 changed files with 1,312 additions and 1,326 deletions.
2 changes: 1 addition & 1 deletion src/Algebras/Congruences.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,6 @@ open IsCongruence
-------------------------------------------------

<span style="float:left;">[← Algebras.Products](Algebras.Products.html)</span>
<span style="float:right;">[Algebras.Func →](Algebras.Func.html)</span>
<span style="float:right;">[Algebras.Setoid →](Algebras.Setoid.html)</span>

{% include UALib.Links.md %}
12 changes: 6 additions & 6 deletions src/Algebras/Func.lagda → src/Algebras/Setoid.lagda
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
---
layout: default
title : "Algebras.Func module (Agda Universal Algebra Library)"
title : "Algebras.Setoid module (Agda Universal Algebra Library)"
date : "2021-09-17"
author: "agda-algebras development team"
---
Expand All @@ -11,17 +11,17 @@ author: "agda-algebras development team"

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

module Algebras.Func where
module Algebras.Setoid where

open import Algebras.Func.Basic
open import Algebras.Func.Products
open import Algebras.Func.Congruences
open import Algebras.Setoid.Basic
open import Algebras.Setoid.Products
open import Algebras.Setoid.Congruences

\end{code}

--------------------------------

<span style="float:left;">[← Algebras.Congruences](Algebras.Congruences.html)</span>
<span style="float:right;">[Algebras.Func.Basic →](Algebras.Func.Basic.html)</span>
<span style="float:right;">[Algebras.Setoid.Basic →](Algebras.Setoid.Basic.html)</span>

{% include UALib.Links.md %}
40 changes: 20 additions & 20 deletions src/Algebras/Func/Basic.lagda → src/Algebras/Setoid/Basic.lagda
View file
Original file line number Diff line number Diff line change
@@ -1,21 +1,21 @@
---
layout: default
title : "Algebras.Func.Basic module (Agda Universal Algebra Library)"
title : "Algebras.Setoid.Basic module (Agda Universal Algebra Library)"
date : "2021-04-23"
author: "agda-algebras development team"
---

#### <a id="basic-definitions">Basic definitions for algebras over setoids</a>

This is the [Algebras.Func.Basic][] module of the [Agda Universal Algebra Library][].
This is the [Algebras.Setoid.Basic][] module of the [Agda Universal Algebra Library][].

\begin{code}

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

open import Algebras.Basic using (𝓞 ; 𝓥 ; Signature )

module Algebras.Func.Basic {𝑆 : Signature 𝓞 𝓥} where
module Algebras.Setoid.Basic {𝑆 : Signature 𝓞 𝓥} where

-- Imports from the Agda and the Agda Standard Library --------------------
open import Agda.Primitive using ( _⊔_ ; lsuc ) renaming ( Set to Type )
Expand Down Expand Up @@ -81,7 +81,7 @@ equality.

\begin{code}

record SetoidAlgebra α ρ : Type (𝓞 ⊔ 𝓥 ⊔ lsuc (α ⊔ ρ)) where
record Algebra α ρ : Type (𝓞 ⊔ 𝓥 ⊔ lsuc (α ⊔ ρ)) where
field
Domain : Setoid α ρ
Interp : Func (⟦ 𝑆 ⟧ Domain) Domain
Expand All @@ -94,31 +94,31 @@ record SetoidAlgebra α ρ : Type (𝓞 ⊔ 𝓥 ⊔ lsuc (α ⊔ ρ)) where

\end{code}

It should be clear that the two types `Algebroid` and `SetoidAlgebra` are equivalent. (We tend to use the latter throughout most of the [agda-algebras][] library.)
It should be clear that the two types `Algebroid` and `Algebra` are equivalent. (We tend to use the latter throughout most of the [agda-algebras][] library.)

\begin{code}

open SetoidAlgebra
open Algebra

-- Forgetful Functor
𝕌[_] : SetoidAlgebra α ρ → Type α
𝕌[_] : Algebra α ρ → Type α
𝕌[ 𝑨 ] = Carrier (Domain 𝑨)

𝔻[_] : SetoidAlgebra α ρ → Setoid α ρ
𝔻[_] : Algebra α ρ → Setoid α ρ
𝔻[ 𝑨 ] = Domain 𝑨

-- The universe level of a SetoidAlgebra
-- The universe level of a Algebra

Level-of-Alg : {α ρ 𝓞 𝓥 : Level}{𝑆 : Signature 𝓞 𝓥} → SetoidAlgebra α ρ → Level
Level-of-Alg : {α ρ 𝓞 𝓥 : Level}{𝑆 : Signature 𝓞 𝓥} → Algebra α ρ → Level
Level-of-Alg {α = α}{ρ}{𝓞}{𝓥} _ = 𝓞 ⊔ 𝓥 ⊔ lsuc (α ⊔ ρ)

Level-of-Carrier : {α ρ 𝓞 𝓥 : Level}{𝑆 : Signature 𝓞 𝓥} → SetoidAlgebra α ρ → Level
Level-of-Carrier : {α ρ 𝓞 𝓥 : Level}{𝑆 : Signature 𝓞 𝓥} → Algebra α ρ → Level
Level-of-Carrier {α = α} _ = α


open SetoidAlgebra
open Algebra

_̂_ : (f : ∣ 𝑆 ∣)(𝑨 : SetoidAlgebra α ρ) → (∥ 𝑆 ∥ f → 𝕌[ 𝑨 ]) → 𝕌[ 𝑨 ]
_̂_ : (f : ∣ 𝑆 ∣)(𝑨 : Algebra α ρ) → (∥ 𝑆 ∥ f → 𝕌[ 𝑨 ]) → 𝕌[ 𝑨 ]

f ̂ 𝑨 = λ a → (Interp 𝑨) ⟨$⟩ (f , a)

Expand All @@ -129,15 +129,15 @@ f ̂ 𝑨 = λ a → (Interp 𝑨) ⟨$⟩ (f , a)

\begin{code}

module _ (𝑨 : SetoidAlgebra α ρ) where
module _ (𝑨 : Algebra α ρ) where

open SetoidAlgebra 𝑨 using ( Interp ) renaming ( Domain to A )
open Algebra 𝑨 using ( Interp ) renaming ( Domain to A )
open Setoid A using (sym ; trans ) renaming ( Carrier to ∣A∣ ; _≈_ to _≈₁_ ; refl to refl₁ )

open Level


Lift-Algˡ : (ℓ : Level) → SetoidAlgebra (α ⊔ ℓ) ρ
Lift-Algˡ : (ℓ : Level) → Algebra (α ⊔ ℓ) ρ

Domain (Lift-Algˡ ℓ) = record { Carrier = Lift ℓ ∣A∣
; _≈_ = λ x y → lower x ≈₁ lower y
Expand All @@ -151,7 +151,7 @@ module _ (𝑨 : SetoidAlgebra α ρ) where
≈cong (Interp (Lift-Algˡ ℓ)) (refl , la=lb) = ≈cong (Interp 𝑨) ((refl , la=lb))


Lift-Algʳ : (ℓ : Level) → SetoidAlgebra α (ρ ⊔ ℓ)
Lift-Algʳ : (ℓ : Level) → Algebra α (ρ ⊔ ℓ)

Domain (Lift-Algʳ ℓ) =
record { Carrier = ∣A∣
Expand All @@ -164,15 +164,15 @@ module _ (𝑨 : SetoidAlgebra α ρ) where
Interp (Lift-Algʳ ℓ ) ⟨$⟩ (f , la) = (f ̂ 𝑨) la
≈cong (Interp (Lift-Algʳ ℓ)) (refl , la≡lb) = lift (≈cong (Interp 𝑨) (≡.refl , λ i → lower (la≡lb i)))

Lift-Alg : (𝑨 : SetoidAlgebra α ρ)(ℓ₀ ℓ₁ : Level) → SetoidAlgebra (α ⊔ ℓ₀) (ρ ⊔ ℓ₁)
Lift-Alg : (𝑨 : Algebra α ρ)(ℓ₀ ℓ₁ : Level) → Algebra (α ⊔ ℓ₀) (ρ ⊔ ℓ₁)
Lift-Alg 𝑨 ℓ₀ ℓ₁ = Lift-Algʳ (Lift-Algˡ 𝑨 ℓ₀) ℓ₁

\end{code}


--------------------------------

<span style="float:left;">[↑ Algebras.Func](Algebras.Func.html)</span>
<span style="float:right;">[Algebras.Func.Products →](Algebras.Func.Products.html)</span>
<span style="float:left;">[↑ Algebras.Setoid](Algebras.Setoid.html)</span>
<span style="float:right;">[Algebras.Setoid.Products →](Algebras.Setoid.Products.html)</span>

{% include UALib.Links.md %}
51 changes: 25 additions & 26 deletions src/Algebras/Func/Congruences.lagda → src/Algebras/Setoid/Congruences.lagda
View file
Original file line number Diff line number Diff line change
@@ -1,37 +1,36 @@
---
layout: default
title : "Algebras.Func.Congruences module (The Agda Universal Algebra Library)"
title : "Algebras.Setoid.Congruences module (The Agda Universal Algebra Library)"
date : "2021-09-15"
author: "agda-algebras development team"
---

#### <a id="congruences-of-setoidalgebras">Congruences of Setoid Algebras</a>

This is the [Algebras.Func.Congruences][] module of the [Agda Universal Algebra Library][].
This is the [Algebras.Setoid.Congruences][] module of the [Agda Universal Algebra Library][].

\begin{code}

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

open import Algebras.Basic using (𝓞 ; 𝓥 ; Signature)

module Algebras.Func.Congruences {𝑆 : Signature 𝓞 𝓥} where
module Algebras.Setoid.Congruences {𝑆 : Signature 𝓞 𝓥} where

-- Imports from the Agda Standard Library ---------------------------------------
open import Function using ( id )
open import Function.Bundles using ( Func )
open import Agda.Primitive using ( _⊔_ ; Level ) renaming ( Set to Type )
open import Data.Product using ( _,_ ; Σ-syntax )
open import Relation.Binary using ( Setoid ; IsEquivalence ) renaming ( Rel to BinRel )
open import Relation.Binary.PropositionalEquality
using ( refl )
open import Function using ( id )
open import Function.Bundles using ( Func )
open import Agda.Primitive using ( _⊔_ ; Level ) renaming ( Set to Type )
open import Data.Product using ( _,_ ; Σ-syntax )
open import Relation.Binary using ( Setoid ; IsEquivalence ) renaming ( Rel to BinRel )
open import Relation.Binary.PropositionalEquality using ( refl )

-- Imports from the Agda Universal Algebras Library ------------------------------
open import Overture.Preliminaries using ( ∣_∣ ; ∥_∥ )
open import Relations.Discrete using ( 0[_] ; _|:_ )
open import Algebras.Func.Basic {𝑆 = 𝑆} using ( ov ; SetoidAlgebra ; 𝕌[_] ; _̂_ )
open import Relations.Quotients using ( Equivalence )
open import Relations.Func.Quotients using ( ⟪_⟫ ; _/_ ; ⟪_∼_⟫-elim )
open import Overture.Preliminaries using ( ∣_∣ ; ∥_∥ )
open import Relations.Discrete using ( 0[_] ; _|:_ )
open import Algebras.Setoid.Basic {𝑆 = 𝑆} using ( ov ; Algebra ; 𝕌[_] ; _̂_ )
open import Relations.Quotients using ( Equivalence )
open import Relations.Setoid.Quotients using ( ⟪_⟫ ; _/_ ; ⟪_∼_⟫-elim )

private variable α ρ ℓ : Level

Expand All @@ -41,8 +40,8 @@ We now define the function `compatible` so that, if `𝑨` denotes an algebra an

\begin{code}

-- SetoidAlgebra compatibility with binary relation
_∣≈_ : (𝑨 : SetoidAlgebra α ρ) → BinRel 𝕌[ 𝑨 ] ℓ → Type _
-- Algebra compatibility with binary relation
_∣≈_ : (𝑨 : Algebra α ρ) → BinRel 𝕌[ 𝑨 ] ℓ → Type _
𝑨 ∣≈ R = ∀ 𝑓 → (𝑓 ̂ 𝑨) |: R

\end{code}
Expand All @@ -54,9 +53,9 @@ Congruences should obviously contain the equality relation on the underlying set

\begin{code}

module _ (𝑨 : SetoidAlgebra α ρ) where
module _ (𝑨 : Algebra α ρ) where

open SetoidAlgebra 𝑨 using () renaming (Domain to A )
open Algebra 𝑨 using () renaming (Domain to A )
open Setoid A using ( _≈_ )

record IsCongruence (θ : BinRel 𝕌[ 𝑨 ] ℓ) : Type (𝓞 ⊔ 𝓥 ⊔ ρ ⊔ ℓ ⊔ α) where
Expand All @@ -79,10 +78,10 @@ Each of these types captures what it means to be a congruence and they are equiv

\begin{code}

IsCongruence→Con : {𝑨 : SetoidAlgebra α ρ}(θ : BinRel 𝕌[ 𝑨 ] ℓ) → IsCongruence 𝑨 θ → Con 𝑨
IsCongruence→Con : {𝑨 : Algebra α ρ}(θ : BinRel 𝕌[ 𝑨 ] ℓ) → IsCongruence 𝑨 θ → Con 𝑨
IsCongruence→Con θ p = θ , p

Con→IsCongruence : {𝑨 : SetoidAlgebra α ρ}((θ , _) : Con 𝑨 {ℓ}) → IsCongruence 𝑨 θ
Con→IsCongruence : {𝑨 : Algebra α ρ}((θ , _) : Con 𝑨 {ℓ}) → IsCongruence 𝑨 θ
Con→IsCongruence θ = ∥ θ ∥

\end{code}
Expand All @@ -95,17 +94,17 @@ In many areas of abstract mathematics the *quotient* of an algebra `𝑨` with r

\begin{code}

open SetoidAlgebra using ( Domain ; Interp )
open Algebra using ( Domain ; Interp )
open Setoid using ( Carrier )
open Func using ( cong ) renaming ( f to _⟨$⟩_ )

_╱_ : (𝑨 : SetoidAlgebra α ρ) → Con 𝑨 {ℓ} → SetoidAlgebra α ℓ
_╱_ : (𝑨 : Algebra α ρ) → Con 𝑨 {ℓ} → Algebra α ℓ
Domain (𝑨 ╱ θ) = 𝕌[ 𝑨 ] / (Eqv ∥ θ ∥)
(Interp (𝑨 ╱ θ)) ⟨$⟩ (f , a) = (f ̂ 𝑨) a
cong (Interp (𝑨 ╱ θ)) {f , u} {.f , v} (refl , a) = is-compatible ∥ θ ∥ f a

module _ (𝑨 : SetoidAlgebra α ρ) where
open SetoidAlgebra 𝑨 using ( ) renaming (Domain to A )
module _ (𝑨 : Algebra α ρ) where
open Algebra 𝑨 using ( ) renaming (Domain to A )
open Setoid A using ( _≈_ ) renaming (refl to refl₁)

_/∙_ : 𝕌[ 𝑨 ] → (θ : Con 𝑨{ℓ}) → Carrier (Domain (𝑨 ╱ θ))
Expand All @@ -118,7 +117,7 @@ module _ (𝑨 : SetoidAlgebra α ρ) where

--------------------------------------

<span style="float:left;">[← Algebras.Func.Products](Algebras.Func.Products.html)</span>
<span style="float:left;">[← Algebras.Setoid.Products](Algebras.Setoid.Products.html)</span>
<span style="float:right;">[Homomorphisms →](Homomorphisms.html)</span>

{% include UALib.Links.md %}
55 changes: 27 additions & 28 deletions src/Algebras/Func/Products.lagda → src/Algebras/Setoid/Products.lagda
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
---
layout: default
title : "Algebras.Func.Products module (Agda Universal Algebra Library)"
title : "Algebras.Setoid.Products module (Agda Universal Algebra Library)"
date : "2021-07-03"
author: "agda-algebras development team"
---

#### <a id="products-of-setoidalgebras">Products of Setoid Algebras</a>

This is the [Algebras.Func.Products][] module of the [Agda Universal Algebra Library][].
This is the [Algebras.Setoid.Products][] module of the [Agda Universal Algebra Library][].

\begin{code}

Expand All @@ -16,33 +16,32 @@ This is the [Algebras.Func.Products][] module of the [Agda Universal Algebra Lib

open import Algebras.Basic using (𝓞 ; 𝓥 ; Signature)

module Algebras.Func.Products {𝑆 : Signature 𝓞 𝓥} where
module Algebras.Setoid.Products {𝑆 : Signature 𝓞 𝓥} where

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Agda.Primitive using ( lsuc ; _⊔_ ; Level ) renaming ( Set to Type )
open import Data.Product using ( _,_ ; Σ-syntax ; _×_ )
open import Function.Base using ( flip )
open import Function.Bundles using ( Func )
open import Relation.Binary using ( Setoid ; IsEquivalence ; Decidable )
open import Relation.Binary.PropositionalEquality
using ( refl ; _≡_ )
open import Relation.Unary using ( Pred ; _⊆_ ; _∈_ )
open import Agda.Primitive using ( lsuc ; _⊔_ ; Level ) renaming ( Set to Type )
open import Data.Product using ( _,_ ; Σ-syntax ; _×_ )
open import Function.Base using ( flip )
open import Function.Bundles using ( Func )
open import Relation.Binary using ( Setoid ; IsEquivalence ; Decidable )
open import Relation.Binary.PropositionalEquality using ( refl ; _≡_ )
open import Relation.Unary using ( Pred ; _⊆_ ; _∈_ )

open Func using ( cong ) renaming ( f to _<$>_ )
open Setoid using ( Carrier ; _≈_ ) renaming ( isEquivalence to isEqv )
open IsEquivalence using () renaming ( refl to reflE ; sym to symE ; trans to transE )
open Func using ( cong ) renaming ( f to _<$>_ )
open Setoid using ( Carrier ; _≈_ ) renaming ( isEquivalence to isEqv )
open IsEquivalence using () renaming ( refl to reflE ; sym to symE ; trans to transE )


-- Imports from agda-algebras -----------------------------------------------------
open import Overture.Preliminaries using ( ∣_∣; ∥_∥)
open import Overture.Surjective using ( proj ; projIsOnto ) renaming ( IsSurjective to onto )
open import Algebras.Func.Basic {𝑆 = 𝑆} using ( ⟦_⟧ ; SetoidAlgebra ; _̂_ ; ov ; 𝕌[_])
open import Overture.Preliminaries using ( ∣_∣; ∥_∥)
open import Overture.Surjective using ( proj ; projIsOnto ) renaming ( IsSurjective to onto )
open import Algebras.Setoid.Basic {𝑆 = 𝑆} using ( ⟦_⟧ ; Algebra ; _̂_ ; ov ; 𝕌[_])

private variable α ρ ι : Level

open SetoidAlgebra
open Algebra

⨅ : {I : Type ι }(𝒜 : I → SetoidAlgebra α ρ) → SetoidAlgebra (α ⊔ ι) (ρ ⊔ ι)
⨅ : {I : Type ι }(𝒜 : I → Algebra α ρ) → Algebra (α ⊔ ι) (ρ ⊔ ι)

Domain (⨅ {I} 𝒜) =

Expand All @@ -62,20 +61,20 @@ cong (Interp (⨅ {I} 𝒜)) (refl , f=g ) = λ i → cong (Interp (𝒜 i)) (r

\end{code}

#### <a id="products-of-classes-of-setoidalgebras">Products of classes of SetoidAlgebras</a>
#### <a id="products-of-classes-of-setoidalgebras">Products of classes of Algebras</a>

\begin{code}

module _ {𝒦 : Pred (SetoidAlgebra α ρ) (ov α)} where
module _ {𝒦 : Pred (Algebra α ρ) (ov α)} where

ℑ : Type (ov(α ⊔ ρ))
ℑ = Σ[ 𝑨 ∈ (SetoidAlgebra α ρ) ] 𝑨 ∈ 𝒦
ℑ = Σ[ 𝑨 ∈ (Algebra α ρ) ] 𝑨 ∈ 𝒦


𝔄 : ℑ → SetoidAlgebra α ρ
𝔄 : ℑ → Algebra α ρ
𝔄 i = ∣ i ∣

class-product : SetoidAlgebra (ov (α ⊔ ρ)) _
class-product : Algebra (ov (α ⊔ ρ)) _
class-product = ⨅ 𝔄

\end{code}
Expand All @@ -87,7 +86,7 @@ product `⨅ 𝔄` onto the `(𝑨 , p)`-th component.

#### Proving the coordinate projections are surjective

Suppose `I` is an index type and `𝒜 : I → SetoidAlgebra α ρ` is an indexed collection of algebras.
Suppose `I` is an index type and `𝒜 : I → Algebra α ρ` is an indexed collection of algebras.
Let `⨅ 𝒜` be the product algebra defined above. Given `i : I`, consider the projection of `⨅ 𝒜`
onto the `i-th` coordinate. Of course this projection ought to be a surjective map from `⨅ 𝒜` onto
`𝒜 i`. However, this is impossible if `I` is just an arbitrary type. Indeed, we must have an
Expand All @@ -101,7 +100,7 @@ projection of a product of algebras over such an index type is surjective.
module _ {I : Type ι} -- index type
{_≟_ : Decidable{A = I} _≡_} -- with decidable equality

{𝒜 : I → SetoidAlgebra α ρ} -- indexed collection of algebras
{𝒜 : I → Algebra α ρ} -- indexed collection of algebras
{𝒜I : ∀ i → 𝕌[ 𝒜 i ] } -- each of which is nonempty
where

Expand All @@ -112,7 +111,7 @@ module _ {I : Type ι} -- index type

--------------------------------

<span style="float:left;">[← Algebras.Func.Basic](Algebras.Func.Basic.html)</span>
<span style="float:right;">[Algebras.Func.Congruences →](Algebras.Func.Congruences.html)</span>
<span style="float:left;">[← Algebras.Setoid.Basic](Algebras.Setoid.Basic.html)</span>
<span style="float:right;">[Algebras.Setoid.Congruences →](Algebras.Setoid.Congruences.html)</span>

{% include UALib.Links.md %}
Loading

0 comments on commit cde5198

Please sign in to comment.