-Algebra : (π€ : Universe)(π : Signature π π₯) β π β π₯ β π€ βΊ Μ +Algebra : (π€ : Universe)(π : Signature π π₯) β π β π₯ β π€ βΊ Μ Algebra π€ π = Ξ£ A κ π€ Μ , -- the domain Ξ f κ β£ π β£ , Op (β₯ π β₯ f) A -- the basic operations @@ -47,7 +47,7 @@ Some people prefer to represent algebraic structures in type theory using record-record algebra (π€ : Universe) (π : Signature π π₯) : (π β π₯ β π€) βΊ Μ where +record algebra (π€ : Universe) (π : Signature π π₯) : (π β π₯ β π€) βΊ Μ where constructor mkalg field univ : π€ Μ @@ -65,7 +65,7 @@ This representation of algebras as inhabitants of a record type is equivalent to open algebra algebraβAlgebra : algebra π€ π β Algebra π€ π - algebraβAlgebra π¨ = (univ π¨ , op π¨) + algebraβAlgebra π¨ = (univ π¨ , op π¨) Algebraβalgebra : Algebra π€ π β algebra π€ π Algebraβalgebra π¨ = mkalg β£ π¨ β£ β₯ π¨ β₯ @@ -97,21 +97,21 @@ Recall, in the [section on level lifting and lowering](Overture.Lifts.html#level-module _ {π : Universe} {I : π Μ}{A : π€ Μ} where +module _ {π : Universe} {I : π Μ}{A : π€ Μ} where open Lift - Lift-op : Op I A β (π¦ : Universe) β Op I (Lift{π¦} A) + Lift-op : Op I A β (π¦ : Universe) β Op I (Lift{π¦} A) Lift-op f π¦ = Ξ» x β lift (f (Ξ» i β lower (x i))) module _ {π : Signature π π₯} where - Lift-alg : Algebra π€ π β (π¦ : Universe) β Algebra (π€ β π¦) π - Lift-alg π¨ π¦ = Lift β£ π¨ β£ , (Ξ» (π : β£ π β£) β Lift-op (π Μ π¨) π¦) + Lift-alg : Algebra π€ π β (π¦ : Universe) β Algebra (π€ β π¦) π + Lift-alg π¨ π¦ = Lift β£ π¨ β£ , (Ξ» (π : β£ π β£) β Lift-op (π Μ π¨) π¦) open algebra - Lift-alg-record-type : algebra π€ π β (π¦ : Universe) β algebra (π€ β π¦) π + Lift-alg-record-type : algebra π€ π β (π¦ : Universe) β algebra (π€ β π¦) π Lift-alg-record-type π¨ π¦ = mkalg (Lift (univ π¨)) (Ξ» (f : β£ π β£) β Lift-op ((op π¨) f) π¦)@@ -136,7 +136,7 @@ The formal definition is immediate since all the work is done by the relation `|- compatible : (π¨ : Algebra π€ π) β Rel β£ π¨ β£ π¦ β π β π€ β π₯ β π¦ Μ + compatible : (π¨ : Algebra π€ π) β Rel β£ π¨ β£ π¦ β π β π€ β π₯ β π¦ Μ compatible π¨ R = β π β (π Μ π¨) |: R@@ -152,13 +152,13 @@ In the [Relations.Continuous][] module, we defined a function called `cont-compa-module _ {π€ π¦ : Universe} {I : π₯ Μ} {π : Signature π π₯} where +module _ {π€ π¦ : Universe} {I : π₯ Μ} {π : Signature π π₯} where open import Relations.Continuous using (ContRel; DepRel; cont-compatible-op; dep-compatible-op) - cont-compatible : (π¨ : Algebra π€ π) β ContRel I β£ π¨ β£ π¦ β π β π€ β π₯ β π¦ Μ + cont-compatible : (π¨ : Algebra π€ π) β ContRel I β£ π¨ β£ π¦ β π β π€ β π₯ β π¦ Μ cont-compatible π¨ R = Ξ π κ β£ π β£ , cont-compatible-op (π Μ π¨) R - dep-compatible : (π : I β Algebra π€ π) β DepRel I (Ξ» i β β£ π i β£) π¦ β π β π€ β π₯ β π¦ Μ + dep-compatible : (π : I β Algebra π€ π) β DepRel I (Ξ» i β β£ π i β£) π¦ β π β π€ β π₯ β π¦ Μ dep-compatible π R = Ξ π κ β£ π β£ , dep-compatible-op (Ξ» i β π Μ (π i)) Rdiff --git a/UALib/html/Algebras.Congruences.md b/UALib/html/Algebras.Congruences.md index e2d65c64..7e540a9a 100644 --- a/UALib/html/Algebras.Congruences.md +++ b/UALib/html/Algebras.Congruences.md @@ -26,14 +26,14 @@ Formally, we define a record type (`IsCongruence`) to represent the property of-module _ {π¦ π€ : Universe} where +module _ {π¦ π€ : Universe} where - record IsCongruence (π¨ : Algebra π€ π)(ΞΈ : Rel β£ π¨ β£ π¦) : ov π¦ β π€ Μ where + record IsCongruence (π¨ : Algebra π€ π)(ΞΈ : Rel β£ π¨ β£ π¦) : ov π¦ β π€ Μ where constructor mkcon field is-equivalence : IsEquivalence ΞΈ is-compatible : compatible π¨ ΞΈ - Con : (π¨ : Algebra π€ π) β π€ β ov π¦ Μ + Con : (π¨ : Algebra π€ π) β π€ β ov π¦ Μ Con π¨ = Ξ£ ΞΈ κ ( Rel β£ π¨ β£ π¦ ) , IsCongruence π¨ ΞΈ @@ -44,9 +44,9 @@ Each of these types captures what it means to be a congruence and they are equivIsCongruenceβCon : {π¨ : Algebra π€ π}(ΞΈ : Rel β£ π¨ β£ π¦) β IsCongruence π¨ ΞΈ β Con π¨ - IsCongruenceβCon ΞΈ p = ΞΈ , p + IsCongruenceβCon ΞΈ p = ΞΈ , p - ConβIsCongruence : {π¨ : Algebra π€ π} β ((ΞΈ , _) : Con π¨) β IsCongruence π¨ ΞΈ + ConβIsCongruence : {π¨ : Algebra π€ π} β ((ΞΈ , _) : Con π¨) β IsCongruence π¨ ΞΈ ConβIsCongruence ΞΈ = β₯ ΞΈ β₯@@ -93,11 +93,11 @@ In many areas of abstract mathematics the *quotient* of an algebra `π¨` with r-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where - _β±_ : (π¨ : Algebra π€ π) β Con{π¦} π¨ β Algebra (π€ β π¦ βΊ) π + _β±_ : (π¨ : Algebra π€ π) β Con{π¦} π¨ β Algebra (π€ β π¦ βΊ) π - π¨ β± ΞΈ = (β£ π¨ β£ / β£ ΞΈ β£) , -- the domain of the quotient algebra + π¨ β± ΞΈ = (β£ π¨ β£ / β£ ΞΈ β£) , -- the domain of the quotient algebra Ξ» π π β βͺ (π Μ π¨)(Ξ» i β fst β₯ π i β₯) β« -- the basic operations of the quotient algebra @@ -108,8 +108,8 @@ In many areas of abstract mathematics the *quotient* of an algebra `π¨` with r- π[_β±_] : (π¨ : Algebra π€ π)(ΞΈ : Con {π¦} π¨) β Rel (β£ π¨ β£ / β£ ΞΈ β£)(π€ β π¦ βΊ) - π[ π¨ β± ΞΈ ] = Ξ» u v β u β‘ v + π[_β±_] : (π¨ : Algebra π€ π)(ΞΈ : Con {π¦} π¨) β Rel (β£ π¨ β£ / β£ ΞΈ β£)(π€ β π¦ βΊ) + π[ π¨ β± ΞΈ ] = Ξ» u v β u β‘ v@@ -117,8 +117,8 @@ From this we easily obtain the zero congruence of `π¨ β± ΞΈ` by applying the- π[_β±_] : (π¨ : Algebra π€ π)(ΞΈ : Con{π¦} π¨){fe : funext π₯ (π€ β π¦ βΊ)} β Con (π¨ β± ΞΈ) - π[ π¨ β± ΞΈ ] {fe} = π[ π¨ β± ΞΈ ] , Ξ (π¨ β± ΞΈ) {fe} + π[_β±_] : (π¨ : Algebra π€ π)(ΞΈ : Con{π¦} π¨){fe : funext π₯ (π€ β π¦ βΊ)} β Con (π¨ β± ΞΈ) + π[ π¨ β± ΞΈ ] {fe} = π[ π¨ β± ΞΈ ] , Ξ (π¨ β± ΞΈ) {fe}@@ -127,10 +127,10 @@ Finally, the following elimination rule is sometimes useful.-module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where +module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where open IsCongruence - /-β‘ : (ΞΈ : Con{π¦} π¨){u v : β£ π¨ β£} β βͺ u β« {β£ ΞΈ β£} β‘ βͺ v β« β β£ ΞΈ β£ u v + /-β‘ : (ΞΈ : Con{π¦} π¨){u v : β£ π¨ β£} β βͺ u β« {β£ ΞΈ β£} β‘ βͺ v β« β β£ ΞΈ β£ u v /-β‘ ΞΈ refl = IsEquivalence.rfl (is-equivalence β₯ ΞΈ β₯)diff --git a/UALib/html/Algebras.Products.md b/UALib/html/Algebras.Products.md index 0fea2eee..24094f90 100644 --- a/UALib/html/Algebras.Products.md +++ b/UALib/html/Algebras.Products.md @@ -32,11 +32,11 @@ In the [UALib][] a *product of* π-*algebras* is represented by the following-module _ {π€ π : Universe}{I : π Μ } where +module _ {π€ π : Universe}{I : π Μ } where - β¨ : (π : I β Algebra π€ π ) β Algebra (π β π€) π + β¨ : (π : I β Algebra π€ π ) β Algebra (π β π€) π - β¨ π = (Ξ i κ I , β£ π i β£) , -- domain of the product algebra + β¨ π = (Ξ i κ I , β£ π i β£) , -- domain of the product algebra Ξ» π π i β (π Μ π i) Ξ» x β π x i -- basic operations of the product algebra@@ -49,7 +49,7 @@ The type just defined is the one that will be used throughout the [UALib][] when open algebra - β¨ ' : (π : I β algebra π€ π) β algebra (π β π€) π + β¨ ' : (π : I β algebra π€ π) β algebra (π β π€) π β¨ ' π = record { univ = β i β univ (π i) ; -- domain op = Ξ» π π i β (op (π i)) π Ξ» x β π x i } -- basic operations @@ -62,8 +62,8 @@ The type just defined is the one that will be used throughout the [UALib][] when-ov : Universe β Universe -ov π€ = π β π₯ β π€ βΊ +ov : Universe β Universe +ov π€ = π β π₯ β π€ βΊ@@ -85,7 +85,7 @@ The solution is to essentially take `π¦` itself to be the indexing type, at le-module class-products {π€ : Universe} (π¦ : Pred (Algebra π€ π)(ov π€)) where +module class-products {π€ : Universe} (π¦ : Pred (Algebra π€ π)(ov π€)) where β : ov π€ Μ β = Ξ£ π¨ κ (Algebra π€ π) , (π¨ β π¦) diff --git a/UALib/html/Algebras.Signatures.md b/UALib/html/Algebras.Signatures.md index c61cef65..2697e6d1 100644 --- a/UALib/html/Algebras.Signatures.md +++ b/UALib/html/Algebras.Signatures.md @@ -13,7 +13,7 @@ This section presents the [Algebras.Signatures][] module of the [Agda Universal {-# OPTIONS --without-K --exact-split --safe #-} -open import Universes using (π€β) +open import Universes using (π€β) module Algebras.Signatures where @@ -28,7 +28,7 @@ We define the signature of an algebraic structure in Agda like this.@@ -89,18 +89,18 @@ A *monomorphism* is an injective homomorphism and an *epimorphism* is a surjecti-Signature : (π π₯ : Universe) β (π β π₯) βΊ Μ +Signature : (π π₯ : Universe) β (π β π₯) βΊ Μ Signature π π₯ = Ξ£ F κ π Μ , (F β π₯ Μ)@@ -45,13 +45,13 @@ Here is how we could define the signature for monoids as a member of the type `S-data monoid-op {π : Universe} : π Μ where +data monoid-op {π : Universe} : π Μ where e : monoid-op; Β· : monoid-op open import MGS-MLTT using (π; π) -monoid-sig : Signature π π€β -monoid-sig = monoid-op , Ξ» { e β π; Β· β π } +monoid-sig : Signature π π€β +monoid-sig = monoid-op , Ξ» { e β π; Β· β π }diff --git a/UALib/html/Homomorphisms.Basic.md b/UALib/html/Homomorphisms.Basic.md index 5e907ef3..1b68cc6d 100644 --- a/UALib/html/Homomorphisms.Basic.md +++ b/UALib/html/Homomorphisms.Basic.md @@ -32,10 +32,10 @@ To formalize this concept, we first define a type representing the assertion tha-module _ {π€ π¦ : Universe}(π¨ : Algebra π€ π)(π© : Algebra π¦ π) where +module _ {π€ π¦ : Universe}(π¨ : Algebra π€ π)(π© : Algebra π¦ π) where - compatible-op-map : β£ π β£ β (β£ π¨ β£ β β£ π© β£) β π€ β π₯ β π¦ Μ - compatible-op-map π h = β π β h ((π Μ π¨) π) β‘ (π Μ π©) (h β π) + compatible-op-map : β£ π β£ β (β£ π¨ β£ β β£ π© β£) β π€ β π₯ β π¦ Μ + compatible-op-map π h = β π β h ((π Μ π¨) π) β‘ (π Μ π©) (h β π)@@ -45,10 +45,10 @@ We now define the type `hom π¨ π©` of homomorphisms from `π¨` to `π©` by- is-homomorphism : (β£ π¨ β£ β β£ π© β£) β π β π₯ β π€ β π¦ Μ + is-homomorphism : (β£ π¨ β£ β β£ π© β£) β π β π₯ β π€ β π¦ Μ is-homomorphism g = β π β compatible-op-map π g - hom : π β π₯ β π€ β π¦ Μ + hom : π β π₯ β π€ β π¦ Μ hom = Ξ£ g κ (β£ π¨ β£ β β£ π© β£ ) , is-homomorphism g@@ -59,10 +59,10 @@ Let's look at a few examples of homomorphisms. These examples are actually quite-module _ {π€ : Universe} where +module _ {π€ : Universe} where πΎπΉ : (A : Algebra π€ π) β hom A A - πΎπΉ _ = id , Ξ» π π β refl + πΎπΉ _ = id , Ξ» π π β refl@@ -72,11 +72,11 @@ Next, `lift` and `lower`, defined in the [Overture.Lifts][] module, are (the map open Lift - ππΎπ»π : {π¦ : Universe}{π¨ : Algebra π€ π} β hom π¨ (Lift-alg π¨ π¦) - ππΎπ»π = lift , Ξ» π π β refl + ππΎπ»π : {π¦ : Universe}{π¨ : Algebra π€ π} β hom π¨ (Lift-alg π¨ π¦) + ππΎπ»π = lift , Ξ» π π β refl - πβ΄πβ―π : {π¦ : Universe}{π¨ : Algebra π€ π} β hom (Lift-alg π¨ π¦) π¨ - πβ΄πβ―π = lower , Ξ» π π β refl + πβ΄πβ―π : {π¦ : Universe}{π¨ : Algebra π€ π} β hom (Lift-alg π¨ π¦) π¨ + πβ΄πβ―π = lower , Ξ» π π β refl-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where - is-monomorphism : (π¨ : Algebra π€ π)(π© : Algebra π¦ π) β (β£ π¨ β£ β β£ π© β£) β π β π₯ β π€ β π¦ Μ + is-monomorphism : (π¨ : Algebra π€ π)(π© : Algebra π¦ π) β (β£ π¨ β£ β β£ π© β£) β π β π₯ β π€ β π¦ Μ is-monomorphism π¨ π© g = is-homomorphism π¨ π© g Γ Monic g - mon : Algebra π€ π β Algebra π¦ π β π β π₯ β π€ β π¦ Μ + mon : Algebra π€ π β Algebra π¦ π β π β π₯ β π€ β π¦ Μ mon π¨ π© = Ξ£ g κ (β£ π¨ β£ β β£ π© β£) , is-monomorphism π¨ π© g - is-epimorphism : (π¨ : Algebra π€ π)(π© : Algebra π¦ π) β (β£ π¨ β£ β β£ π© β£) β π β π₯ β π€ β π¦ Μ + is-epimorphism : (π¨ : Algebra π€ π)(π© : Algebra π¦ π) β (β£ π¨ β£ β β£ π© β£) β π β π₯ β π€ β π¦ Μ is-epimorphism π¨ π© g = is-homomorphism π¨ π© g Γ Epic g - epi : Algebra π€ π β Algebra π¦ π β π β π₯ β π€ β π¦ Μ + epi : Algebra π€ π β Algebra π¦ π β π β π₯ β π€ β π¦ Μ epi π¨ π© = Ξ£ g κ (β£ π¨ β£ β β£ π© β£) , is-epimorphism π¨ π© g@@ -110,10 +110,10 @@ It will be convenient to have a function that takes an inhabitant of `mon` (or `mon-to-hom : (π¨ : Algebra π€ π){π© : Algebra π¦ π} β mon π¨ π© β hom π¨ π© - mon-to-hom π¨ Ο = β£ Ο β£ , fst β₯ Ο β₯ + mon-to-hom π¨ Ο = β£ Ο β£ , fst β₯ Ο β₯ epi-to-hom : {π¨ : Algebra π€ π}(π© : Algebra π¦ π) β epi π¨ π© β hom π¨ π© - epi-to-hom _ Ο = β£ Ο β£ , fst β₯ Ο β₯ + epi-to-hom _ Ο = β£ Ο β£ , fst β₯ Ο β₯@@ -128,9 +128,9 @@ The kernel of a homomorphism is a congruence relation and conversely for every c-module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where +module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where - homker-compatible : dfunext π₯ π¦ β (π© : Algebra π¦ π)(h : hom π¨ π©) β compatible π¨ (ker β£ h β£) + homker-compatible : dfunext π₯ π¦ β (π© : Algebra π¦ π)(h : hom π¨ π©) β compatible π¨ (ker β£ h β£) homker-compatible fe π© h f {u}{v} Kerhab = β£ h β£ ((f Μ π¨) u) β‘β¨ β₯ h β₯ f u β© (f Μ π©)(β£ h β£ β u) β‘β¨ ap (f Μ π©)(fe Ξ» x β Kerhab x) β© (f Μ π©)(β£ h β£ β v) β‘β¨ (β₯ h β₯ f v)β»ΒΉ β© @@ -142,8 +142,8 @@ It is convenient to define a function that takes a homomorphism and constructs a@@ -29,7 +29,7 @@ Recall, `f ~ g` means f and g are *extensionally* (or pointwise) equal; i.e., `- kercon : (π© : Algebra π¦ π){fe : dfunext π₯ π¦} β hom π¨ π© β Con{π¦} π¨ - kercon π© {fe} h = ker β£ h β£ , mkcon (ker-IsEquivalence β£ h β£)(homker-compatible fe π© h) + kercon : (π© : Algebra π¦ π){fe : dfunext π₯ π¦} β hom π¨ π© β Con{π¦} π¨ + kercon π© {fe} h = ker β£ h β£ , mkcon (ker-IsEquivalence β£ h β£)(homker-compatible fe π© h)@@ -151,11 +151,11 @@ With this congruence we construct the corresponding quotient, along with some sy- kerquo : dfunext π₯ π¦ β {π© : Algebra π¦ π} β hom π¨ π© β Algebra (π€ β π¦ βΊ) π + kerquo : dfunext π₯ π¦ β {π© : Algebra π¦ π} β hom π¨ π© β Algebra (π€ β π¦ βΊ) π kerquo fe {π©} h = π¨ β± (kercon π© {fe} h) -_[_]/ker_βΎ_ : (π¨ : Algebra π€ π)(π© : Algebra π¦ π) β hom π¨ π© β dfunext π₯ π¦ β Algebra (π€ β π¦ βΊ) π +_[_]/ker_βΎ_ : (π¨ : Algebra π€ π)(π© : Algebra π¦ π) β hom π¨ π© β dfunext π₯ π¦ β Algebra (π€ β π¦ βΊ) π π¨ [ π© ]/ker h βΎ fe = kerquo fe {π©} h infix 60 _[_]/ker_βΎ_ @@ -172,11 +172,11 @@ Given an algebra `π¨` and a congruence `ΞΈ`, the *canonical projection* is a mdiff --git a/UALib/html/Homomorphisms.Isomorphisms.md b/UALib/html/Homomorphisms.Isomorphisms.md index 6f79399c..cdfaa10d 100644 --- a/UALib/html/Homomorphisms.Isomorphisms.md +++ b/UALib/html/Homomorphisms.Isomorphisms.md @@ -19,7 +19,7 @@ Here we formalize the informal notion of isomorphism between algebraic structure module Homomorphisms.Isomorphisms {π : Signature π π₯} where open import Homomorphisms.Noether{π = π} public -open import MGS-Embeddings using (Nat; NatΞ ; NatΞ -is-embedding) public +open import MGS-Embeddings using (Nat; NatΞ ; NatΞ -is-embedding) public-module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where +module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where Οepi : (ΞΈ : Con{π¦} π¨) β epi π¨ (π¨ β± ΞΈ) - Οepi ΞΈ = (Ξ» a β βͺ a β«) , (Ξ» _ _ β refl) , cΟ-is-epic where + Οepi ΞΈ = (Ξ» a β βͺ a β«) , (Ξ» _ _ β refl) , cΟ-is-epic where cΟ-is-epic : Epic (Ξ» a β βͺ a β«) - cΟ-is-epic (C , (a , refl)) = Image_β_.im a + cΟ-is-epic (C , (a , refl)) = Image_β_.im a@@ -194,7 +194,7 @@ We combine the foregoing to define a function that takes π-algebras `π¨` an- Οker : (π© : Algebra π¦ π){fe : dfunext π₯ π¦}(h : hom π¨ π©) β epi π¨ (π¨ [ π© ]/ker h βΎ fe) + Οker : (π© : Algebra π¦ π){fe : dfunext π₯ π¦}(h : hom π¨ π©) β epi π¨ (π¨ [ π© ]/ker h βΎ fe) Οker π© {fe} h = Οepi (kercon π© {fe} h)@@ -205,7 +205,7 @@ The kernel of the canonical projection of `π¨` onto `π¨ / ΞΈ` is equal to ` open IsCongruence - ker-in-con : {fe : dfunext π₯ (π€ β π¦ βΊ)}(ΞΈ : Con{π¦} π¨) + ker-in-con : {fe : dfunext π₯ (π€ β π¦ βΊ)}(ΞΈ : Con{π¦} π¨) β β {x}{y} β β£ kercon (π¨ β± ΞΈ){fe} (Οhom ΞΈ) β£ x y β β£ ΞΈ β£ x y ker-in-con ΞΈ hyp = /-β‘ ΞΈ hyp @@ -222,10 +222,10 @@ If in addition we have a family `π½ : (i : I) β hom π¨ (β¬ i)` of homomor-module _ {π π¦ : Universe}{I : π Μ}(β¬ : I β Algebra π¦ π) where +module _ {π π¦ : Universe}{I : π Μ}(β¬ : I β Algebra π¦ π) where - β¨ -hom-co : dfunext π π¦ β {π€ : Universe}(π¨ : Algebra π€ π) β Ξ i κ I , hom π¨ (β¬ i) β hom π¨ (β¨ β¬) - β¨ -hom-co fe π¨ π½ = (Ξ» a i β β£ π½ i β£ a) , (Ξ» π πΆ β fe Ξ» i β β₯ π½ i β₯ π πΆ) + β¨ -hom-co : dfunext π π¦ β {π€ : Universe}(π¨ : Algebra π€ π) β Ξ i κ I , hom π¨ (β¬ i) β hom π¨ (β¨ β¬) + β¨ -hom-co fe π¨ π½ = (Ξ» a i β β£ π½ i β£ a) , (Ξ» π πΆ β fe Ξ» i β β₯ π½ i β₯ π πΆ)@@ -238,8 +238,8 @@ The foregoing generalizes easily to the case in which the domain is also a produ- β¨ -hom : dfunext π π¦ β {π€ : Universe}(π : I β Algebra π€ π) β Ξ i κ I , hom (π i)(β¬ i) β hom (β¨ π)(β¨ β¬) - β¨ -hom fe π π½ = (Ξ» x i β β£ π½ i β£ (x i)) , (Ξ» π πΆ β fe Ξ» i β β₯ π½ i β₯ π (Ξ» x β πΆ x i)) + β¨ -hom : dfunext π π¦ β {π€ : Universe}(π : I β Algebra π€ π) β Ξ i κ I , hom (π i)(β¬ i) β hom (β¨ π)(β¨ β¬) + β¨ -hom fe π π½ = (Ξ» x i β β£ π½ i β£ (x i)) , (Ξ» π πΆ β fe Ξ» i β β₯ π½ i β₯ π (Ξ» x β πΆ x i))@@ -252,7 +252,7 @@ Later we will need a proof of the fact that projecting out of a product algebraβ¨ -projection-hom : Ξ i κ I , hom (β¨ β¬) (β¬ i) - β¨ -projection-hom = Ξ» x β (Ξ» z β z x) , Ξ» _ _ β refl + β¨ -projection-hom = Ξ» x β (Ξ» z β z x) , Ξ» _ _ β refldiff --git a/UALib/html/Homomorphisms.HomomorphicImages.md b/UALib/html/Homomorphisms.HomomorphicImages.md index 01ab2f65..3b82b577 100644 --- a/UALib/html/Homomorphisms.HomomorphicImages.md +++ b/UALib/html/Homomorphisms.HomomorphicImages.md @@ -28,12 +28,12 @@ We begin with what seems, for our purposes, the most useful way to represent the-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where - HomImage : {π¨ : Algebra π€ π}(π© : Algebra π¦ π)(Ο : hom π¨ π©) β β£ π© β£ β π€ β π¦ Μ + HomImage : {π¨ : Algebra π€ π}(π© : Algebra π¦ π)(Ο : hom π¨ π©) β β£ π© β£ β π€ β π¦ Μ HomImage π© Ο = Ξ» b β Image β£ Ο β£ β b - HomImagesOf : Algebra π€ π β π β π₯ β π€ β π¦ βΊ Μ + HomImagesOf : Algebra π€ π β π β π₯ β π€ β π¦ βΊ Μ HomImagesOf π¨ = Ξ£ π© κ (Algebra π¦ π) , Ξ£ Ο κ (β£ π¨ β£ β β£ π© β£) , is-homomorphism π¨ π© Ο Γ Epic Ο@@ -44,7 +44,7 @@ Since we take the class of homomorphic images of an algebra to be closed under i- _is-hom-image-of_ : (π© : Algebra π¦ π)(π¨ : Algebra π€ π) β ov π¦ β π€ Μ + _is-hom-image-of_ : (π© : Algebra π¦ π)(π¨ : Algebra π€ π) β ov π¦ β π€ Μ π© is-hom-image-of π¨ = Ξ£ πͺΟ κ (HomImagesOf π¨) , β£ πͺΟ β£ β π©@@ -56,12 +56,12 @@ Given a class `π¦` of `π`-algebras, we need a type that expresses the asser-module _ {π€ : Universe} where +module _ {π€ : Universe} where - _is-hom-image-of-class_ : Algebra π€ π β Pred (Algebra π€ π)(π€ βΊ) β ov π€ Μ + _is-hom-image-of-class_ : Algebra π€ π β Pred (Algebra π€ π)(π€ βΊ) β ov π€ Μ π© is-hom-image-of-class π = Ξ£ π¨ κ (Algebra π€ π) , (π¨ β π) Γ (π© is-hom-image-of π¨) - HomImagesOfClass : Pred (Algebra π€ π) (π€ βΊ) β ov π€ Μ + HomImagesOfClass : Pred (Algebra π€ π) (π€ βΊ) β ov π€ Μ HomImagesOfClass π = Ξ£ π© κ (Algebra π€ π) , (π© is-hom-image-of-class π)@@ -78,9 +78,9 @@ The first states and proves the simple fact that the lift of an epimorphism is a open Lift -module _ {π§ π¨ : Universe} where +module _ {π§ π¨ : Universe} where - lift-of-alg-epic-is-epic : (π© : Universe){π¦ : Universe} + lift-of-alg-epic-is-epic : (π© : Universe){π¦ : Universe} {π¨ : Algebra π§ π}(π© : Algebra π¨ π)(h : hom π¨ π©) ----------------------------------------------- β Epic β£ h β£ β Epic β£ Lift-hom π© π¦ π© h β£ @@ -96,30 +96,30 @@ The first states and proves the simple fact that the lift of an epimorphism is a a : β£ π¨ β£ a = Inv β£ h β£ ΞΆ - Ξ² : lift (β£ h β£ a) β‘ (lift β β£ h β£ β lower{π¦}) (lift a) + Ξ² : lift (β£ h β£ a) β‘ (lift β β£ h β£ β lower{π¦}) (lift a) Ξ² = ap (Ξ» - β lift (β£ h β£ ( - a))) (lowerβΌlift {π¦} ) - Ξ· : y β‘ β£ lh β£ (lift a) + Ξ· : y β‘ β£ lh β£ (lift a) Ξ· = y β‘β¨ (happly liftβΌlower) y β© lift (lower y) β‘β¨ ap lift (InvIsInv β£ h β£ ΞΆ)β»ΒΉ β© lift (β£ h β£ a) β‘β¨ Ξ² β© β£ lh β£ (lift a) β - Lift-alg-hom-image : {π© π¦ : Universe} + Lift-alg-hom-image : {π© π¦ : Universe} {π¨ : Algebra π§ π}{π© : Algebra π¨ π} β π© is-hom-image-of π¨ ----------------------------------------------- β (Lift-alg π© π¦) is-hom-image-of (Lift-alg π¨ π©) - Lift-alg-hom-image {π©}{π¦}{π¨}{π©} ((πͺ , Ο , Οhom , Οepic) , Cβ B) = - (Lift-alg πͺ π¦ , β£ lΟ β£ , β₯ lΟ β₯ , lΟepic) , Lift-alg-iso Cβ B + Lift-alg-hom-image {π©}{π¦}{π¨}{π©} ((πͺ , Ο , Οhom , Οepic) , Cβ B) = + (Lift-alg πͺ π¦ , β£ lΟ β£ , β₯ lΟ β₯ , lΟepic) , Lift-alg-iso Cβ B where lΟ : hom (Lift-alg π¨ π©) (Lift-alg πͺ π¦) - lΟ = (Lift-hom π© π¦ πͺ) (Ο , Οhom) + lΟ = (Lift-hom π© π¦ πͺ) (Ο , Οhom) lΟepic : Epic β£ lΟ β£ - lΟepic = lift-of-alg-epic-is-epic π© πͺ (Ο , Οhom) Οepic + lΟepic = lift-of-alg-epic-is-epic π© πͺ (Ο , Οhom) Οepic-_β _ : {π€ π¦ : Universe}(π¨ : Algebra π€ π)(π© : Algebra π¦ π) β π β π₯ β π€ β π¦ Μ +_β _ : {π€ π¦ : Universe}(π¨ : Algebra π€ π)(π© : Algebra π¦ π) β π β π₯ β π€ β π¦ Μ π¨ β π© = Ξ£ f κ (hom π¨ π©) , Ξ£ g κ (hom π© π¨) , (β£ f β£ β β£ g β£ βΌ β£ πΎπΉ π© β£) Γ (β£ g β£ β β£ f β£ βΌ β£ πΎπΉ π¨ β£) @@ -43,19 +43,19 @@ That is, two structures are **isomorphic** provided there are homomorphisms goin-β -refl : {π€ : Universe} {π¨ : Algebra π€ π} β π¨ β π¨ -β -refl {π€}{π¨} = πΎπΉ π¨ , πΎπΉ π¨ , (Ξ» a β refl) , (Ξ» a β refl) +β -refl : {π€ : Universe} {π¨ : Algebra π€ π} β π¨ β π¨ +β -refl {π€}{π¨} = πΎπΉ π¨ , πΎπΉ π¨ , (Ξ» a β refl) , (Ξ» a β refl) -β -sym : {π€ π¦ : Universe}{π¨ : Algebra π€ π}{π© : Algebra π¦ π} +β -sym : {π€ π¦ : Universe}{π¨ : Algebra π€ π}{π© : Algebra π¦ π} β π¨ β π© β π© β π¨ -β -sym h = fst β₯ h β₯ , fst h , β₯ snd β₯ h β₯ β₯ , β£ snd β₯ h β₯ β£ +β -sym h = fst β₯ h β₯ , fst h , β₯ snd β₯ h β₯ β₯ , β£ snd β₯ h β₯ β£ -module _ {π§ π¨ π© : Universe} where +module _ {π§ π¨ π© : Universe} where β -trans : {π¨ : Algebra π§ π}{π© : Algebra π¨ π}{πͺ : Algebra π© π} β π¨ β π© β π© β πͺ β π¨ β πͺ - β -trans {π¨} {π©}{πͺ} ab bc = f , g , Ξ± , Ξ² + β -trans {π¨} {π©}{πͺ} ab bc = f , g , Ξ± , Ξ² where f1 : hom π¨ π© f1 = β£ ab β£ @@ -87,15 +87,15 @@ Fortunately, the lift operation preserves isomorphism (i.e., it's an *algebraic open Lift -module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where Lift-β : {π¨ : Algebra π€ π} β π¨ β (Lift-alg π¨ π¦) - Lift-β {π¨} = ππΎπ»π , (πβ΄πβ―π{π€}{π¦}{π¨}) , happly liftβΌlower , happly (lowerβΌlift{π¦}) + Lift-β {π¨} = ππΎπ»π , (πβ΄πβ―π{π€}{π¦}{π¨}) , happly liftβΌlower , happly (lowerβΌlift{π¦}) - Lift-hom : (π§ : Universe)(π¨ : Universe){π¨ : Algebra π€ π}(π© : Algebra π¦ π) + Lift-hom : (π§ : Universe)(π¨ : Universe){π¨ : Algebra π€ π}(π© : Algebra π¦ π) β hom π¨ π© β hom (Lift-alg π¨ π§) (Lift-alg π© π¨) - Lift-hom π§ π¨ {π¨} π© (f , fhom) = lift β f β lower , Ξ³ + Lift-hom π§ π¨ {π¨} π© (f , fhom) = lift β f β lower , Ξ³ where lABh : is-homomorphism (Lift-alg π¨ π§) π© (f β lower) lABh = β-is-hom (Lift-alg π¨ π§) π© {lower}{f} (Ξ» _ _ β refl) fhom @@ -104,10 +104,10 @@ Fortunately, the lift operation preserves isomorphism (i.e., it's an *algebraic Ξ³ = β-is-hom (Lift-alg π¨ π§) (Lift-alg π© π¨){f β lower}{lift} lABh Ξ» _ _ β refl -module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where - Lift-alg-iso : {π¨ : Algebra π€ π}{π§ : Universe} - {π© : Algebra π¦ π}{π¨ : Universe} + Lift-alg-iso : {π¨ : Algebra π€ π}{π§ : Universe} + {π© : Algebra π¦ π}{π¨ : Universe} ----------------------------------------- β π¨ β π© β (Lift-alg π¨ π§) β (Lift-alg π© π¨) @@ -124,15 +124,15 @@ The lift is also associative, up to isomorphism at least.-module _ {π π€ π¦ : Universe} where +module _ {π π€ π¦ : Universe} where - Lift-alg-assoc : {π¨ : Algebra π€ π} β Lift-alg π¨ (π¦ β π) β (Lift-alg (Lift-alg π¨ π¦) π) + Lift-alg-assoc : {π¨ : Algebra π€ π} β Lift-alg π¨ (π¦ β π) β (Lift-alg (Lift-alg π¨ π¦) π) Lift-alg-assoc {π¨} = β -trans (β -trans Ξ³ Lift-β ) Lift-β where - Ξ³ : Lift-alg π¨ (π¦ β π) β π¨ + Ξ³ : Lift-alg π¨ (π¦ β π) β π¨ Ξ³ = β -sym Lift-β - Lift-alg-associative : (π¨ : Algebra π€ π) β Lift-alg π¨ (π¦ β π) β (Lift-alg (Lift-alg π¨ π¦) π) + Lift-alg-associative : (π¨ : Algebra π€ π) β Lift-alg π¨ (π¦ β π) β (Lift-alg (Lift-alg π¨ π¦) π) Lift-alg-associative π¨ = Lift-alg-assoc {π¨}@@ -146,7 +146,7 @@ Products of isomorphic families of algebras are themselves isomorphic. The proof-module _ {π π€ π¦ : Universe}{I : π Μ}{feππ€ : dfunext π π€}{feππ¦ : dfunext π π¦} where +module _ {π π€ π¦ : Universe}{I : π Μ}{feππ€ : dfunext π π€}{feππ¦ : dfunext π π¦} where β¨ β : {π : I β Algebra π€ π}{β¬ : I β Algebra π¦ π} β Ξ i κ I , π i β β¬ i β β¨ π β β¨ β¬ @@ -171,7 +171,7 @@ Products of isomorphic families of algebras are themselves isomorphic. The proof Ο~Ο a = feππ€ Ξ» i β snd β₯ snd (AB i) β₯ (a i) Ξ³ : β¨ π β β¨ β¬ - Ξ³ = (Ο , Οhom) , ((Ο , Οhom) , Ο~Ο , Ο~Ο) + Ξ³ = (Ο , Οhom) , ((Ο , Οhom) , Ο~Ο , Ο~Ο)@@ -180,7 +180,7 @@ A nearly identical proof goes through for isomorphisms of lifted products (thoug-module _ {π π© : Universe}{I : π Μ}{fizw : dfunext (π β π©) π¦}{fiu : dfunext π π€} where +module _ {π π© : Universe}{I : π Μ}{fizw : dfunext (π β π©) π¦}{fiu : dfunext π π€} where Lift-alg-β¨ β : {π : I β Algebra π€ π}{β¬ : (Lift{π©} I) β Algebra π¦ π} β (β i β π i β β¬ (lift i)) β Lift-alg (β¨ π) π© β β¨ β¬ @@ -206,7 +206,7 @@ A nearly identical proof goes through for isomorphisms of lifted products (thoug Ο~Ο a = fiu Ξ» i β snd β₯ snd (AB i) β₯ (a i) Aβ B : β¨ π β β¨ β¬ - Aβ B = (Ο , Οhom) , ((Ο , Οhom) , Ο~Ο , Ο~Ο) + Aβ B = (Ο , Οhom) , ((Ο , Οhom) , Ο~Ο , Ο~Ο) Ξ³ : Lift-alg (β¨ π) π© β β¨ β¬ Ξ³ = β -trans (β -sym Lift-β ) Aβ B @@ -224,27 +224,27 @@ Finally, we prove some useful facts about embeddings that occasionally come in h-module _ {π π€ π¦ : Universe} where +module _ {π π€ π¦ : Universe} where - embedding-lift-nat : hfunext π π€ β hfunext π π¦ + embedding-lift-nat : hfunext π π€ β hfunext π π¦ β {I : π Μ}{A : I β π€ Μ}{B : I β π¦ Μ} - (h : Nat A B) β (β i β is-embedding (h i)) + (h : Nat A B) β (β i β is-embedding (h i)) ------------------------------------------ β is-embedding(NatΞ h) embedding-lift-nat hfiu hfiw h hem = NatΞ -is-embedding hfiu hfiw h hem - embedding-lift-nat' : hfunext π π€ β hfunext π π¦ + embedding-lift-nat' : hfunext π π€ β hfunext π π¦ β {I : π Μ}{π : I β Algebra π€ π}{β¬ : I β Algebra π¦ π} - (h : Nat(fst β π)(fst β β¬)) β (β i β is-embedding (h i)) + (h : Nat(fst β π)(fst β β¬)) β (β i β is-embedding (h i)) -------------------------------------------------------- β is-embedding(NatΞ h) embedding-lift-nat' hfiu hfiw h hem = NatΞ -is-embedding hfiu hfiw h hem - embedding-lift : hfunext π π€ β hfunext π π¦ + embedding-lift : hfunext π π€ β hfunext π π¦ β {I : π Μ} β {π : I β Algebra π€ π}{β¬ : I β Algebra π¦ π} β (h : β i β β£ π i β£ β β£ β¬ i β£) β (β i β is-embedding (h i)) ---------------------------------------------------------- @@ -253,14 +253,14 @@ Finally, we prove some useful facts about embeddings that occasionally come in h embedding-lift hfiu hfiw {I}{π}{β¬} h hem = embedding-lift-nat' hfiu hfiw {I}{π}{β¬} h hem -isoβembedding : {π€ π¦ : Universe}{π¨ : Algebra π€ π}{π© : Algebra π¦ π} +isoβembedding : {π€ π¦ : Universe}{π¨ : Algebra π€ π}{π© : Algebra π¦ π} β (Ο : π¨ β π©) β is-embedding (fst β£ Ο β£) isoβembedding Ο = equivs-are-embeddings (fst β£ Ο β£) (invertibles-are-equivs (fst β£ Ο β£) finv) where finv : invertible (fst β£ Ο β£) - finv = β£ fst β₯ Ο β₯ β£ , (snd β₯ snd Ο β₯ , fst β₯ snd Ο β₯) + finv = β£ fst β₯ Ο β₯ β£ , (snd β₯ snd Ο β₯ , fst β₯ snd Ο β₯)diff --git a/UALib/html/Homomorphisms.Noether.md b/UALib/html/Homomorphisms.Noether.md index 1d1377a1..17876ee6 100644 --- a/UALib/html/Homomorphisms.Noether.md +++ b/UALib/html/Homomorphisms.Noether.md @@ -45,20 +45,20 @@ Without further ado, we present our formalization of the first homomorphism theo-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where FirstHomTheorem|Set : (π¨ : Algebra π€ π)(π© : Algebra π¦ π)(h : hom π¨ π©) -- extensionality assumptions: β pred-ext π€ π¦ - β (fe : dfunext π₯ π¦) + β (fe : dfunext π₯ π¦) -- truncation assumptions: - β is-set β£ π© β£ + β is-set β£ π© β£ β blk-uip β£ π¨ β£ β£ kercon π© {fe} h β£ - β Ξ£ Ο κ (hom (π¨ [ π© ]/ker h βΎ fe) π©) , (β£ h β£ β‘ β£ Ο β£ β β£ Οker π© {fe} h β£) Γ Monic β£ Ο β£ Γ is-embedding β£ Ο β£ + β Ξ£ Ο κ (hom (π¨ [ π© ]/ker h βΎ fe) π©) , (β£ h β£ β‘ β£ Ο β£ β β£ Οker π© {fe} h β£) Γ Monic β£ Ο β£ Γ is-embedding β£ Ο β£ - FirstHomTheorem|Set π¨ π© h pe fe Bset buip = (Ο , Οhom) , Οcom , Οmon , Οemb + FirstHomTheorem|Set π¨ π© h pe fe Bset buip = (Ο , Οhom) , Οcom , Οmon , Οemb where ΞΈ : Con{π¦} π¨ ΞΈ = kercon π© {fe} h @@ -74,9 +74,9 @@ Without further ado, we present our formalization of the first homomorphism theo (π Μ π©) (Ξ» x β Ο (π x)) β Οmon : Monic Ο - Οmon (_ , (u , refl)) (_ , (v , refl)) Οuv = block-ext|uip pe buip ΞΎ Οuv + Οmon (_ , (u , refl)) (_ , (v , refl)) Οuv = block-ext|uip pe buip ΞΎ Οuv - Οcom : β£ h β£ β‘ Ο β β£ Οker π©{fe} h β£ + Οcom : β£ h β£ β‘ Ο β β£ Οker π©{fe} h β£ Οcom = refl Οemb : is-embedding Ο @@ -91,17 +91,17 @@ Below we will prove that the homomorphism `Ο`, whose existence we just proved, FirstIsoTheorem|Set : (π¨ : Algebra π€ π)(π© : Algebra π¦ π)(h : hom π¨ π©) -- extensionality assumptions: β pred-ext π€ π¦ - β (fe : dfunext π₯ π¦) - β dfunext π¦ π¦ + β (fe : dfunext π₯ π¦) + β dfunext π¦ π¦ -- truncation assumptions: - β is-set β£ π© β£ + β is-set β£ π© β£ β blk-uip β£ π¨ β£ β£ kercon π©{fe}h β£ β Epic β£ h β£ - β Ξ£ f κ epi (π¨ [ π© ]/ker h βΎ fe) π© , (β£ h β£ β‘ β£ f β£ β β£ Οker π©{fe}h β£) Γ Monic β£ f β£ Γ is-embedding β£ f β£ + β Ξ£ f κ epi (π¨ [ π© ]/ker h βΎ fe) π© , (β£ h β£ β‘ β£ f β£ β β£ Οker π©{fe}h β£) Γ Monic β£ f β£ Γ is-embedding β£ f β£ - FirstIsoTheorem|Set π¨ π© h pe fe feww Bset buip hE = (fmap , fhom , fepic) , refl , (snd β₯ FHT β₯) + FirstIsoTheorem|Set π¨ π© h pe fe feww Bset buip hE = (fmap , fhom , fepic) , refl , (snd β₯ FHT β₯) where FHT = FirstHomTheorem|Set π¨ π© h pe fe Bset buip -- (Ο , Οhom) , Οcom , Οmon , Οemb @@ -116,7 +116,7 @@ Below we will prove that the homomorphism `Ο`, whose existence we just proved, a : β£ π¨ β£ a = EpicInv β£ h β£ hE b - bfa : b β‘ fmap βͺ a β« + bfa : b β‘ fmap βͺ a β« bfa = (cong-app (EpicInvIsRightInv {fe = feww} β£ h β£ hE) b)β»ΒΉ Ξ³ : Image fmap β b @@ -128,15 +128,15 @@ Now we prove that the homomorphism `Ο`, whose existence is guaranteed by `First-module _ {π€ π¦ : Universe}{fe : dfunext π₯ π¦}(π¨ : Algebra π€ π)(π© : Algebra π¦ π)(h : hom π¨ π©) where +module _ {π€ π¦ : Universe}{fe : dfunext π₯ π¦}(π¨ : Algebra π€ π)(π© : Algebra π¦ π)(h : hom π¨ π©) where NoetherHomUnique : (f g : hom (π¨ [ π© ]/ker h βΎ fe) π©) - β β£ h β£ β‘ β£ f β£ β β£ Οker π© {fe} h β£ β β£ h β£ β‘ β£ g β£ β β£ Οker π©{fe} h β£ - β β a β β£ f β£ a β‘ β£ g β£ a + β β£ h β£ β‘ β£ f β£ β β£ Οker π© {fe} h β£ β β£ h β£ β‘ β£ g β£ β β£ Οker π©{fe} h β£ + β β a β β£ f β£ a β‘ β£ g β£ a - NoetherHomUnique f g hfk hgk (_ , (a , refl)) = β£ f β£ (_ , (a , refl)) β‘β¨ cong-app(hfk β»ΒΉ)a β© + NoetherHomUnique f g hfk hgk (_ , (a , refl)) = β£ f β£ (_ , (a , refl)) β‘β¨ cong-app(hfk β»ΒΉ)a β© β£ h β£ a β‘β¨ cong-app(hgk)a β© - β£ g β£ (_ , (a , refl)) β + β£ g β£ (_ , (a , refl)) β@@ -144,8 +144,8 @@ If, in addition, we postulate extensionality of functions defined on the domain- fe-NoetherHomUnique : {fuww : funext (π€ β π¦ βΊ) π¦}(f g : hom (π¨ [ π© ]/ker h βΎ fe) π©) - β β£ h β£ β‘ β£ f β£ β β£ Οker π©{fe} h β£ β β£ h β£ β‘ β£ g β£ β β£ Οker π©{fe} h β£ β β£ f β£ β‘ β£ g β£ + fe-NoetherHomUnique : {fuww : funext (π€ β π¦ βΊ) π¦}(f g : hom (π¨ [ π© ]/ker h βΎ fe) π©) + β β£ h β£ β‘ β£ f β£ β β£ Οker π©{fe} h β£ β β£ h β£ β‘ β£ g β£ β β£ Οker π©{fe} h β£ β β£ f β£ β‘ β£ g β£ fe-NoetherHomUnique {fuww} f g hfk hgk = fuww (NoetherHomUnique f g hfk hgk) @@ -156,8 +156,8 @@ The proof of `NoetherHomUnique` goes through for the special case of epimorphismNoetherIsoUnique : (f g : epi (π¨ [ π© ]/ker h βΎ fe) π©) - β β£ h β£ β‘ β£ f β£ β β£ Οker π©{fe} h β£ β β£ h β£ β‘ β£ g β£ β β£ Οker π© {fe} h β£ - β β a β β£ f β£ a β‘ β£ g β£ a + β β£ h β£ β‘ β£ f β£ β β£ Οker π©{fe} h β£ β β£ h β£ β‘ β£ g β£ β β£ Οker π© {fe} h β£ + β β a β β£ f β£ a β‘ β£ g β£ a NoetherIsoUnique f g hfk hgk = NoetherHomUnique (epi-to-hom π© f) (epi-to-hom π© g) hfk hgk @@ -173,12 +173,12 @@ The composition of homomorphisms is again a homomorphism. We formalize this in@@ -181,7 +181,7 @@ The `is-embedding` type is defined in the [Type Topology][] library in the follo-module _ {π§ π¨ π© : Universe} (π¨ : Algebra π§ π){π© : Algebra π¨ π}(πͺ : Algebra π© π) where +module _ {π§ π¨ π© : Universe} (π¨ : Algebra π§ π){π© : Algebra π¨ π}(πͺ : Algebra π© π) where β-hom : hom π¨ π© β hom π© πͺ β hom π¨ πͺ - β-hom (g , ghom) (h , hhom) = h β g , Ξ³ where + β-hom (g , ghom) (h , hhom) = h β g , Ξ³ where - Ξ³ : β π a β (h β g)((π Μ π¨) a) β‘ (π Μ πͺ)(h β g β a) + Ξ³ : β π a β (h β g)((π Μ π¨) a) β‘ (π Μ πͺ)(h β g β a) Ξ³ π a = (h β g) ((π Μ π¨) a) β‘β¨ ap h ( ghom π a ) β© h ((π Μ π©) (g β a)) β‘β¨ hhom π ( g β a ) β© @@ -189,7 +189,7 @@ The composition of homomorphisms is again a homomorphism. We formalize this in β is-homomorphism π¨ π© f β is-homomorphism π© πͺ g β is-homomorphism π¨ πͺ (g β f) - β-is-hom {f} {g} fhom ghom = β₯ β-hom (f , fhom) (g , ghom) β₯ + β-is-hom {f} {g} fhom ghom = β₯ β-hom (f , fhom) (g , ghom) β₯@@ -213,13 +213,13 @@ If `g : hom π¨ π©`, `h : hom π¨ πͺ`, `h` is surjective, and `ker h β k This, or some variation of it, is sometimes referred to as the Second Isomorphism Theorem. We formalize its statement and proof as follows. (Notice that the proof is constructive.)-module _ {π€ : Universe}{π¨ π© πͺ : Algebra π€ π} where +module _ {π€ : Universe}{π¨ π© πͺ : Algebra π€ π} where homFactor : funext π€ π€ β (g : hom π¨ π©)(h : hom π¨ πͺ) β kernel β£ h β£ β kernel β£ g β£ β Epic β£ h β£ ------------------------------------------- - β Ξ£ Ο κ (hom πͺ π©) , β£ g β£ β‘ β£ Ο β£ β β£ h β£ + β Ξ£ Ο κ (hom πͺ π©) , β£ g β£ β‘ β£ Ο β£ β β£ h β£ - homFactor fe(g , ghom)(h , hhom) KhβKg hEpi = (Ο , ΟIsHomCB) , gΟh + homFactor fe(g , ghom)(h , hhom) KhβKg hEpi = (Ο , ΟIsHomCB) , gΟh where hInv : β£ πͺ β£ β β£ π¨ β£ hInv = Ξ» c β (EpicInv h hEpi) c @@ -227,23 +227,23 @@ This, or some variation of it, is sometimes referred to as the Second Isomorphis Ο : β£ πͺ β£ β β£ π© β£ Ο = Ξ» c β g ( hInv c ) - ΞΎ : β x β kernel h (x , hInv (h x)) + ΞΎ : β x β kernel h (x , hInv (h x)) ΞΎ x = (cong-app (EpicInvIsRightInv {fe = fe} h hEpi) (h x))β»ΒΉ - gΟh : g β‘ Ο β h + gΟh : g β‘ Ο β h gΟh = fe Ξ» x β KhβKg (ΞΎ x) - ΞΆ : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£)(x : β₯ π β₯ π) β π x β‘ (h β hInv)(π x) + ΞΆ : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£)(x : β₯ π β₯ π) β π x β‘ (h β hInv)(π x) ΞΆ π π x = (cong-app (EpicInvIsRightInv {fe = fe} h hEpi) (π x))β»ΒΉ - ΞΉ : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£) β π β‘ h β (hInv β π) + ΞΉ : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£) β π β‘ h β (hInv β π) ΞΉ π π = ap (Ξ» - β - β π)(EpicInvIsRightInv {fe = fe} h hEpi)β»ΒΉ - useker : β π π β g(hInv (h((π Μ π¨)(hInv β π)))) β‘ g((π Μ π¨)(hInv β π)) + useker : β π π β g(hInv (h((π Μ π¨)(hInv β π)))) β‘ g((π Μ π¨)(hInv β π)) useker π c = KhβKg (cong-app (EpicInvIsRightInv{fe = fe} h hEpi) (h ((π Μ π¨)(hInv β c))) ) - ΟIsHomCB : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£) β Ο((π Μ πͺ) π) β‘ (π Μ π©)(Ο β π) + ΟIsHomCB : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£) β Ο((π Μ πͺ) π) β‘ (π Μ π©)(Ο β π) ΟIsHomCB π π = g (hInv ((π Μ πͺ) π)) β‘β¨ i β© g (hInv ((π Μ πͺ)(h β (hInv β π)))) β‘β¨ ii β© @@ -273,14 +273,14 @@ Here's a more general version.@@ -73,7 +73,7 @@ Before moving on to the next subsection, let us pause to make a public import of-module _ {π§ π¨ π© : Universe}{π¨ : Algebra π§ π}{πͺ : Algebra π© π} where +module _ {π§ π¨ π© : Universe}{π¨ : Algebra π§ π}{πͺ : Algebra π© π} where HomFactor : funext π§ π¨ β funext π© π© β (π© : Algebra π¨ π)(Ξ± : hom π¨ π©)(Ξ² : hom π¨ πͺ) β kernel β£ Ξ² β£ β kernel β£ Ξ± β£ β Epic β£ Ξ² β£ ------------------------------------------- - β Ξ£ Ο κ (hom πͺ π©) , β£ Ξ± β£ β‘ β£ Ο β£ β β£ Ξ² β£ + β Ξ£ Ο κ (hom πͺ π©) , β£ Ξ± β£ β‘ β£ Ο β£ β β£ Ξ² β£ - HomFactor fxy fzz π© Ξ± Ξ² KΞ²Ξ± Ξ²E = (Ο , ΟIsHomCB) , Ξ±ΟΞ² + HomFactor fxy fzz π© Ξ± Ξ² KΞ²Ξ± Ξ²E = (Ο , ΟIsHomCB) , Ξ±ΟΞ² where Ξ²Inv : β£ πͺ β£ β β£ π¨ β£ Ξ²Inv = Ξ» y β (EpicInv β£ Ξ² β£ Ξ²E) y @@ -288,20 +288,20 @@ Here's a more general version. Ο : β£ πͺ β£ β β£ π© β£ Ο = Ξ» y β β£ Ξ± β£ ( Ξ²Inv y ) - ΞΎ : (x : β£ π¨ β£) β kernel β£ Ξ² β£ (x , Ξ²Inv (β£ Ξ² β£ x)) + ΞΎ : (x : β£ π¨ β£) β kernel β£ Ξ² β£ (x , Ξ²Inv (β£ Ξ² β£ x)) ΞΎ x = ( cong-app (EpicInvIsRightInv {fe = fzz} β£ Ξ² β£ Ξ²E) ( β£ Ξ² β£ x ) )β»ΒΉ - Ξ±ΟΞ² : β£ Ξ± β£ β‘ Ο β β£ Ξ² β£ + Ξ±ΟΞ² : β£ Ξ± β£ β‘ Ο β β£ Ξ² β£ Ξ±ΟΞ² = fxy Ξ» x β KΞ²Ξ± (ΞΎ x) - ΞΉ : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£) β π β‘ β£ Ξ² β£ β (Ξ²Inv β π) + ΞΉ : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£) β π β‘ β£ Ξ² β£ β (Ξ²Inv β π) ΞΉ π π = ap (Ξ» - β - β π) (EpicInvIsRightInv{fe = fzz} β£ Ξ² β£ Ξ²E)β»ΒΉ - useker : β π π β β£ Ξ± β£ (Ξ²Inv (β£ Ξ² β£((π Μ π¨)(Ξ²Inv β π)))) β‘ β£ Ξ± β£((π Μ π¨)(Ξ²Inv β π)) + useker : β π π β β£ Ξ± β£ (Ξ²Inv (β£ Ξ² β£((π Μ π¨)(Ξ²Inv β π)))) β‘ β£ Ξ± β£((π Μ π¨)(Ξ²Inv β π)) useker π π = KΞ²Ξ± (cong-app (EpicInvIsRightInv {fe = fzz} β£ Ξ² β£ Ξ²E) (β£ Ξ² β£ ((π Μ π¨)(Ξ²Inv β π)))) - ΟIsHomCB : β π π β Ο ((π Μ πͺ) π) β‘ ((π Μ π©)(Ο β π)) + ΟIsHomCB : β π π β Ο ((π Μ πͺ) π) β‘ ((π Μ π©)(Ο β π)) ΟIsHomCB π π = β£ Ξ± β£ (Ξ²Inv ((π Μ πͺ) π)) β‘β¨ i β© β£ Ξ± β£ (Ξ²Inv ((π Μ πͺ)(β£ Ξ² β£ β (Ξ²Inv β π)))) β‘β¨ ii β© @@ -324,11 +324,11 @@ If, in addition to the hypotheses of the last theorem, we assume Ξ± is epic, the β (π© : Algebra π¨ π)(Ξ± : hom π¨ π©)(Ξ² : hom π¨ πͺ) β kernel β£ Ξ² β£ β kernel β£ Ξ± β£ β Epic β£ Ξ² β£ β Epic β£ Ξ± β£ ---------------------------------------------------------- - β Ξ£ Ο κ (epi πͺ π©) , β£ Ξ± β£ β‘ β£ Ο β£ β β£ Ξ² β£ + β Ξ£ Ο κ (epi πͺ π©) , β£ Ξ± β£ β‘ β£ Ο β£ β β£ Ξ² β£ - HomFactorEpi fxy fzz fyy π© Ξ± Ξ² kerincl Ξ²e Ξ±e = (fst β£ ΟF β£ , (snd β£ ΟF β£ , ΟE)) , β₯ ΟF β₯ + HomFactorEpi fxy fzz fyy π© Ξ± Ξ² kerincl Ξ²e Ξ±e = (fst β£ ΟF β£ , (snd β£ ΟF β£ , ΟE)) , β₯ ΟF β₯ where - ΟF : Ξ£ Ο κ (hom πͺ π©) , β£ Ξ± β£ β‘ β£ Ο β£ β β£ Ξ² β£ + ΟF : Ξ£ Ο κ (hom πͺ π©) , β£ Ξ± β£ β‘ β£ Ο β£ β β£ Ξ² β£ ΟF = HomFactor fxy fzz π© Ξ± Ξ² kerincl Ξ²e Ξ²inv : β£ πͺ β£ β β£ π¨ β£ diff --git a/UALib/html/Level.html b/UALib/html/Level.html index 00c1f7d9..fdf2067c 100644 --- a/UALib/html/Level.html +++ b/UALib/html/Level.html @@ -11,12 +11,12 @@ -- Levels. open import Agda.Primitive as Prim public - using (Level; _β_; SetΟ) - renaming (lzero to zero; lsuc to suc) + using (Level; _β_; SetΟ) + renaming (lzero to zero; lsuc to suc) -- Lifting. -record Lift {a} β (A : Set a) : Set (a β β) where +record Lift {a} β (A : Set a) : Set (a β β) where constructor lift field lower : A @@ -24,5 +24,11 @@ -- Synonyms -0β : Level +0β : Level 0β = zero + +levelOfType : β {a} β Set a β Level +levelOfType {a} _ = a + +levelOfTerm : β {a} {A : Set a} β A β Level +levelOfTerm {a} _ = a diff --git a/UALib/html/Overture.Equality.md b/UALib/html/Overture.Equality.md index 3c021e91..f00b7ec2 100644 --- a/UALib/html/Overture.Equality.md +++ b/UALib/html/Overture.Equality.md @@ -48,7 +48,7 @@ The datatype we use to represent definitional equality is imported from the Iden data _β‘_ {A : π€ Μ} : A β A β π€ Μ where refl : {x : A} β x β‘ x -open import Identity-Type renaming (_β‘_ to infix 0 _β‘_) public +open import Identity-Type renaming (_β‘_ to infix 0 _β‘_) publicdiff --git a/UALib/html/Overture.FunExtensionality.md b/UALib/html/Overture.FunExtensionality.md index 023ae79a..f4bcc95b 100644 --- a/UALib/html/Overture.FunExtensionality.md +++ b/UALib/html/Overture.FunExtensionality.md @@ -44,7 +44,7 @@ As explained above, a natural notion of function equality is defined as follows: module hide-βΌ {A : π€ Μ } where - _βΌ_ : {B : A β π¦ Μ } β Ξ B β Ξ B β π€ β π¦ Μ + _βΌ_ : {B : A β π¦ Μ } β Ξ B β Ξ B β π€ β π¦ Μ f βΌ g = Ξ x κ A , f x β‘ g x infix 0 _βΌ_ @@ -59,7 +59,7 @@ As explained above, a natural notion of function equality is defined as follows: module hide-funext where - dfunext : β π€ π¦ β π€ βΊ β π¦ βΊ Μ + dfunext : β π€ π¦ β π€ βΊ β π¦ βΊ Μ dfunext π€ π¦ = {A : π€ Μ }{B : A β π¦ Μ }{f g : Ξ x κ A , B x} β f βΌ g β f β‘ g-open import MGS-FunExt-from-Univalence using (funext; dfunext) public +open import MGS-FunExt-from-Univalence using (funext; dfunext) public@@ -103,7 +103,7 @@ First, a type is a *singleton* if it has exactly one inhabitant and a *subsingle-module hide-tt-defs {π€ : Universe} where +module hide-tt-defs {π€ : Universe} where is-center : (A : π€ Μ ) β A β π€ Μ is-center A c = (x : A) β c β‘ x @@ -123,9 +123,9 @@ Next, we consider the type `is-equiv` which is used to assert that a function isdiff --git a/UALib/html/Overture.Inverses.md b/UALib/html/Overture.Inverses.md index ccaba06c..0a55d0c7 100644 --- a/UALib/html/Overture.Inverses.md +++ b/UALib/html/Overture.Inverses.md @@ -28,7 +28,7 @@ We begin by defining an inductive type that represents the semantic concept of * module _ {A : π€ Μ }{B : π¦ Μ } where - data Image_β_ (f : A β B) : B β π€ β π¦ Μ + data Image_β_ (f : A β B) : B β π€ β π¦ Μ where im : (x : A) β Image f β f x eq : (b : B) β (a : A) β b β‘ f a β Image f β b @@ -74,7 +74,7 @@ An epic (or surjective) function from `A` to `B` is as an inhabitant of the `Epi-module hide-tt-defs' {π€ π¦ : Universe} where +module hide-tt-defs' {π€ π¦ : Universe} where - fiber : {A : π€ Μ } {B : π¦ Μ } (f : A β B) β B β π€ β π¦ Μ + fiber : {A : π€ Μ } {B : π¦ Μ } (f : A β B) β B β π€ β π¦ Μ fiber {A} f y = Ξ£ x κ A , f x β‘ y@@ -134,7 +134,7 @@ A function is called an *equivalence* if all of its fibers are singletons.- is-equiv : {A : π€ Μ } {B : π¦ Μ } β (A β B) β π€ β π¦ Μ + is-equiv : {A : π€ Μ } {B : π¦ Μ } β (A β B) β π€ β π¦ Μ is-equiv f = β y β is-singleton (fiber f y)@@ -147,10 +147,10 @@ We are finally ready to fulfill our promise of a type that provides an alternati module hide-hfunext where - hfunext : β π€ π¦ β (π€ β π¦)βΊ Μ + hfunext : β π€ π¦ β (π€ β π¦)βΊ Μ hfunext π€ π¦ = {A : π€ Μ}{B : A β π¦ Μ} (f g : Ξ B) β is-equiv (happly{f = f}{g}) -open import MGS-FunExt-from-Univalence using (hfunext) public +open import MGS-FunExt-from-Univalence using (hfunext) public- Epic : (A β B) β π€ β π¦ Μ + Epic : (A β B) β π€ β π¦ Μ Epic f = β y β Image f β y@@ -147,7 +147,7 @@ We say that a function `f : A β B` is *monic* (or *injective*) if it does not module _ {A : π€ Μ}{B : π¦ Μ} where - Monic : (f : A β B) β π€ β π¦ Μ + Monic : (f : A β B) β π€ β π¦ Μ Monic f = β x y β f x β‘ f y β x β‘ ymodule hide-is-embedding{A : π€ Μ}{B : π¦ Μ} where - is-embedding : (A β B) β π€ β π¦ Μ + is-embedding : (A β B) β π€ β π¦ Μ is-embedding f = β b β is-subsingleton (fiber f b) open import MGS-Embeddings using (is-embedding) public @@ -209,8 +209,8 @@ Finally, embeddings are monic; from a proof `p : is-embedding f` that `f` is an embedding-is-monic f femb x y fxfy = ap prβ ((femb (f x)) fx fy) where fx fy : fiber f (f x) - fx = x , refl - fy = y , (fxfy β»ΒΉ) + fx = x , refl + fy = y , (fxfy β»ΒΉ)diff --git a/UALib/html/Overture.Lifts.md b/UALib/html/Overture.Lifts.md index 59694d16..fe5ed555 100644 --- a/UALib/html/Overture.Lifts.md +++ b/UALib/html/Overture.Lifts.md @@ -46,7 +46,7 @@ The general `Lift` record type that we now describe makes these situations easie-record Lift {π¦ π€ : Universe} (A : π€ Μ) : π€ β π¦ Μ where +record Lift {π¦ π€ : Universe} (A : π€ Μ) : π€ β π¦ Μ where constructor lift field lower : A open Lift @@ -57,10 +57,10 @@ The point of having a ramified hierarchy of universes is to avoid Russell's para-liftβΌlower : {π¦ π€ : Universe}{A : π€ Μ} β lift β lower β‘ ππ (Lift{π¦} A) +liftβΌlower : {π¦ π€ : Universe}{A : π€ Μ} β lift β lower β‘ ππ (Lift{π¦} A) liftβΌlower = refl -lowerβΌlift : {π¦ π€ : Universe}{A : π€ Μ} β lower{π¦}{π€} β lift β‘ ππ A +lowerβΌlift : {π¦ π€ : Universe}{A : π€ Μ} β lower{π¦}{π€} β lift β‘ ππ A lowerβΌlift = refldiff --git a/UALib/html/Overture.Preliminaries.md b/UALib/html/Overture.Preliminaries.md index a50beb04..dcc95c32 100644 --- a/UALib/html/Overture.Preliminaries.md +++ b/UALib/html/Overture.Preliminaries.md @@ -87,7 +87,7 @@ Since we use the `public` directive, the `Universes` module will be available to-variable π π§ π¨ π© : Universe +variable π π§ π¨ π© : Universe@@ -125,7 +125,7 @@ The dependent product type is defined in the [Type Topology][] library. For peda module hide-sigma where - record Ξ£ {π€ π₯} {A : π€ Μ } (B : A β π₯ Μ ) : π€ β π₯ Μ where + record Ξ£ {π€ π₯} {A : π€ Μ } (B : A β π₯ Μ ) : π€ β π₯ Μ where constructor _,_ field prβ : A @@ -139,7 +139,7 @@ Agda's default syntax for this type is `Ξ£ A (Ξ» x β B)`, but we prefer the no- -Ξ£ : {π€ π₯ : Universe} (A : π€ Μ ) (B : A β π₯ Μ ) β π€ β π₯ Μ + -Ξ£ : {π€ π₯ : Universe} (A : π€ Μ ) (B : A β π₯ Μ ) β π€ β π₯ Μ -Ξ£ A B = Ξ£ B syntax -Ξ£ A (Ξ» x β B) = Ξ£ x κ A , B @@ -152,7 +152,7 @@ A special case of the Sigma type is the one in which the type `B` doesn't depend@@ -207,7 +207,7 @@ We define the following types representing *implication* for binary relations. ( _on_ : {A : π€ Μ}{B : π¦ Μ}{C : π© Μ} β (B β B β C) β (A β B) β (A β A β C) R on g = Ξ» x y β R (g x) (g y) -_β_ : {A : π€ Μ}{B : π¦ Μ} β REL A B π§ β REL A B π¨ β π€ β π¦ β π§ β π¨ Μ +_β_ : {A : π€ Μ}{B : π¦ Μ} β REL A B π§ β REL A B π¨ β π€ β π¦ β π§ β π¨ Μ P β Q = β {i j} β P i j β Q i j infixr 4 _β_ @@ -218,7 +218,7 @@ The `_on_` and `_β_` types combine to give a nice, general implication operati- _Γ_ : π€ Μ β π₯ Μ β π€ β π₯ Μ + _Γ_ : π€ Μ β π₯ Μ β π€ β π₯ Μ A Γ B = Ξ£ x κ A , B@@ -163,12 +163,12 @@ Given universes `π€` and `π₯`, a type `X : π€ Μ`, and a type family `Y :-module hide-pi {π€ π¦ : Universe} where +module hide-pi {π€ π¦ : Universe} where - Ξ : {A : π€ Μ } (B : A β π¦ Μ ) β π€ β π¦ Μ + Ξ : {A : π€ Μ } (B : A β π¦ Μ ) β π€ β π¦ Μ Ξ {A} B = (x : A) β B x - -Ξ : (A : π€ Μ )(B : A β π¦ Μ ) β π€ β π¦ Μ + -Ξ : (A : π€ Μ )(B : A β π¦ Μ ) β π€ β π¦ Μ -Ξ A B = Ξ B infixr -1 -Ξ @@ -185,7 +185,7 @@ Now that we have studied these important types, defined in the [Type Topology][]diff --git a/UALib/html/Relations.Discrete.md b/UALib/html/Relations.Discrete.md index 0e86baf5..23685824 100644 --- a/UALib/html/Relations.Discrete.md +++ b/UALib/html/Relations.Discrete.md @@ -27,7 +27,7 @@ Given two universes `π€ π¦` and a type `A : π€ Μ`, the type `Pred A π¦`-open import Sigma-Type renaming (_,_ to infixr 50 _,_) public +open import Sigma-Type renaming (_,_ to infixr 50 _,_) public open import MGS-MLTT using (prβ; prβ; _Γ_; -Ξ£; Ξ ; -Ξ ) public@@ -197,7 +197,7 @@ The definition of `Ξ£` (and thus, of `Γ`) includes the fields `prβ` and `pr-module _ {π€ : Universe}{A : π€ Μ }{B : A β π₯ Μ} where +module _ {π€ : Universe}{A : π€ Μ }{B : A β π₯ Μ} where β£_β£ fst : Ξ£ B β A β£ x , y β£ = x diff --git a/UALib/html/Relation.Binary.Core.html b/UALib/html/Relation.Binary.Core.html index 85c80401..41ad374f 100644 --- a/UALib/html/Relation.Binary.Core.html +++ b/UALib/html/Relation.Binary.Core.html @@ -4,272 +4,82 @@ -- Properties of binary relations ------------------------------------------------------------------------ --- Note that all the definitions in this file are re-exported by --- `Relation.Binary`. +-- The contents of this module should be accessed via `Relation.Binary`. -{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --without-K --safe #-} -module Relation.Binary.Core where +module Relation.Binary.Core where -open import Agda.Builtin.Equality using (_β‘_) renaming (refl to β‘-refl) +open import Data.Product using (_Γ_) +open import Function.Base using (_on_) +open import Level using (Level; _β_; suc) -open import Data.Maybe.Base using (Maybe) -open import Data.Product using (_Γ_) -open import Data.Sum.Base using (_β_) -open import Function using (_on_; flip) -open import Level -open import Relation.Nullary using (Dec; Β¬_) +private + variable + a b c β ββ ββ ββ : Level + A : Set a + B : Set b + C : Set c -private - variable - a b c β ββ ββ ββ : Level - A : Set a - B : Set b - C : Set c +------------------------------------------------------------------------ +-- Definitions +------------------------------------------------------------------------ ------------------------------------------------------------------------- --- Definition. ------------------------------------------------------------------------- +-- Heterogeneous binary relations --- Heterogeneous binary relations +REL : Set a β Set b β (β : Level) β Set (a β b β suc β) +REL A B β = A β B β Set β -REL : Set a β Set b β (β : Level) β Set (a β b β suc β) -REL A B β = A β B β Set β +-- Homogeneous binary relations --- Homogeneous binary relations +Rel : Set a β (β : Level) β Set (a β suc β) +Rel A β = REL A A β -Rel : Set a β (β : Level) β Set (a β suc β) -Rel A β = REL A A β +------------------------------------------------------------------------ +-- Relationships between relations +------------------------------------------------------------------------ ------------------------------------------------------------------------- --- Simple properties ------------------------------------------------------------------------- +infix 4 _β_ _β_ _=[_]β_ -infixr 4 _β_ _=[_]β_ +-- Implication/containment - could also be written _β_. +-- and corresponding notion of equivalence --- Implication/containment - could also be written _β_. +_β_ : REL A B ββ β REL A B ββ β Set _ +P β Q = β {x y} β P x y β Q x y -_β_ : REL A B ββ β REL A B ββ β Set _ -P β Q = β {i j} β P i j β Q i j +_β_ : REL A B ββ β REL A B ββ β Set _ +P β Q = P β Q Γ Q β P --- Generalised implication - if P β‘ Q it can be read as "f preserves P". +-- Generalised implication - if P β‘ Q it can be read as "f preserves P". -_=[_]β_ : Rel A ββ β (A β B) β Rel B ββ β Set _ -P =[ f ]β Q = P β (Q on f) +_=[_]β_ : Rel A ββ β (A β B) β Rel B ββ β Set _ +P =[ f ]β Q = P β (Q on f) --- A synonym for _=[_]β_. +-- A synonym for _=[_]β_. -_Preserves_βΆ_ : (A β B) β Rel A ββ β Rel B ββ β Set _ -f Preserves P βΆ Q = P =[ f ]β Q +_Preserves_βΆ_ : (A β B) β Rel A ββ β Rel B ββ β Set _ +f Preserves P βΆ Q = P =[ f ]β Q --- A binary variant of _Preserves_βΆ_. +-- A binary variant of _Preserves_βΆ_. -_Preservesβ_βΆ_βΆ_ : (A β B β C) β Rel A ββ β Rel B ββ β Rel C ββ β Set _ -_+_ Preservesβ P βΆ Q βΆ R = - β {x y u v} β P x y β Q u v β R (x + u) (y + v) +_Preservesβ_βΆ_βΆ_ : (A β B β C) β Rel A ββ β Rel B ββ β Rel C ββ β Set _ +_β_ Preservesβ P βΆ Q βΆ R = β {x y u v} β P x y β Q u v β R (x β u) (y β v) --- Reflexivity - defined without an underlying equality. It could --- alternatively be defined as `_β_ β _βΌ_` for some equality `_β_`. --- Confusingly the convention in the library is to use the name "refl" --- for proofs of Reflexive and `reflexive` for proofs of type `_β_ β _βΌ_`, --- e.g. in the definition of `IsEquivalence` later in this file. This --- convention is a legacy from the early days of the library. +------------------------------------------------------------------------ +-- Relationships between a binary relation and a unary operation +------------------------------------------------------------------------ -Reflexive : Rel A β β Set _ -Reflexive _βΌ_ = β {x} β x βΌ x +Contractive : Rel A β β (A β A) β Set _ +Contractive _β€_ f = β {x} β f x β€ x --- Generalised symmetry. +Extensive : Rel A β β (A β A) β Set _ +Extensive _β€_ f = β {x} β x β€ f x -Sym : REL A B ββ β REL B A ββ β Set _ -Sym P Q = P β flip Q +Idempotentβ : Rel A β β (A β A) β Set _ +Idempotentβ _β_ f = β {x} β f (f x) β f x --- Symmetry. - -Symmetric : Rel A β β Set _ -Symmetric _βΌ_ = Sym _βΌ_ _βΌ_ - --- Generalised transitivity. - -Trans : REL A B ββ β REL B C ββ β REL A C ββ β Set _ -Trans P Q R = β {i j k} β P i j β Q j k β R i k - --- A flipped variant of generalised transitivity. - -TransFlip : REL A B ββ β REL B C ββ β REL A C ββ β Set _ -TransFlip P Q R = β {i j k} β Q j k β P i j β R i k - --- Transitivity. - -Transitive : Rel A β β Set _ -Transitive _βΌ_ = Trans _βΌ_ _βΌ_ _βΌ_ - --- Generalised antisymmetry - -Antisym : REL A B ββ β REL B A ββ β REL A B ββ β Set _ -Antisym R S E = β {i j} β R i j β S j i β E i j - --- Antisymmetry. - -Antisymmetric : Rel A ββ β Rel A ββ β Set _ -Antisymmetric _β_ _β€_ = Antisym _β€_ _β€_ _β_ - --- Irreflexivity - this is defined terms of the underlying equality. - -Irreflexive : REL A B ββ β REL A B ββ β Set _ -Irreflexive _β_ _<_ = β {x y} β x β y β Β¬ (x < y) - --- Asymmetry. - -Asymmetric : Rel A β β Set _ -Asymmetric _<_ = β {x y} β x < y β Β¬ (y < x) - --- Generalised connex - exactly one of the two relations holds. - -Connex : REL A B ββ β REL B A ββ β Set _ -Connex P Q = β x y β P x y β Q y x - --- Totality. - -Total : Rel A β β Set _ -Total _βΌ_ = Connex _βΌ_ _βΌ_ - --- Generalised trichotomy - exactly one of three types has a witness. - -data Tri (A : Set a) (B : Set b) (C : Set c) : Set (a β b β c) where - tri< : ( a : A) (Β¬b : Β¬ B) (Β¬c : Β¬ C) β Tri A B C - triβ : (Β¬a : Β¬ A) ( b : B) (Β¬c : Β¬ C) β Tri A B C - tri> : (Β¬a : Β¬ A) (Β¬b : Β¬ B) ( c : C) β Tri A B C - --- Trichotomy. - -Trichotomous : Rel A ββ β Rel A ββ β Set _ -Trichotomous _β_ _<_ = β x y β Tri (x < y) (x β y) (x > y) - where _>_ = flip _<_ - --- Generalised maximum element. - -Max : REL A B β β B β Set _ -Max _β€_ T = β x β x β€ T - --- Maximum element. - -Maximum : Rel A β β A β Set _ -Maximum = Max - --- Generalised minimum element. - -Min : REL A B β β A β Set _ -Min R = Max (flip R) - --- Minimum element. - -Minimum : Rel A β β A β Set _ -Minimum = Min - --- Unary relations respecting a binary relation. - -_βΆ_Respects_ : (A β Set ββ) β (B β Set ββ) β REL A B ββ β Set _ -P βΆ Q Respects _βΌ_ = β {x y} β x βΌ y β P x β Q y - --- Unary relation respects a binary relation. - -_Respects_ : (A β Set ββ) β Rel A ββ β Set _ -P Respects _βΌ_ = P βΆ P Respects _βΌ_ - --- Right respecting - relatedness is preserved on the right by equality. - -_RespectsΚ³_ : REL A B ββ β Rel B ββ β Set _ -_βΌ_ RespectsΚ³ _β_ = β {x} β (x βΌ_) Respects _β_ - --- Left respecting - relatedness is preserved on the left by equality. - -_RespectsΛ‘_ : REL A B ββ β Rel A ββ β Set _ -P RespectsΛ‘ _βΌ_ = β {y} β (flip P y) Respects _βΌ_ - --- Respecting - relatedness is preserved on both sides by equality - -_Respectsβ_ : Rel A ββ β Rel A ββ β Set _ -P Respectsβ _βΌ_ = (P RespectsΚ³ _βΌ_) Γ (P RespectsΛ‘ _βΌ_) - --- Substitutivity - any two related elements satisfy exactly the same --- set of unary relations. Note that only the various derivatives --- of propositional equality can satisfy this property. - -Substitutive : Rel A ββ β (ββ : Level) β Set _ -Substitutive {A = A} _βΌ_ p = (P : A β Set p) β P Respects _βΌ_ - --- Decidability - it is possible to determine whether a given pair of --- elements are related. - -Decidable : REL A B β β Set _ -Decidable _βΌ_ = β x y β Dec (x βΌ y) - --- Weak decidability - it is sometimes possible to determine if a given --- pair of elements are related. - -WeaklyDecidable : REL A B β β Set _ -WeaklyDecidable _βΌ_ = β x y β Maybe (x βΌ y) - --- Irrelevancy - all proofs that a given pair of elements are related --- are indistinguishable. - -Irrelevant : REL A B β β Set _ -Irrelevant _βΌ_ = β {x y} (a b : x βΌ y) β a β‘ b - --- Recomputability - we can rebuild a relevant proof given an --- irrelevant one. - -Recomputable : REL A B β β Set _ -Recomputable _βΌ_ = β {x y} β .(x βΌ y) β x βΌ y - --- Universal - all pairs of elements are related - -Universal : REL A B β β Set _ -Universal _βΌ_ = β x y β x βΌ y - --- Non-emptiness - at least one pair of elements are related. - -record NonEmpty {A : Set a} {B : Set b} - (T : REL A B β) : Set (a β b β β) where - constructor nonEmpty - field - {x} : A - {y} : B - proof : T x y - ------------------------------------------------------------------------- --- Equivalence relations - --- The preorders of this library are defined in terms of an underlying --- equivalence relation, and hence equivalence relations are not --- defined in terms of preorders. - --- This record is defined here instead of with the rest of the --- structures in `Relation.Binary` due to dependency cyles with --- `Relation.Binary.PropositionalEquality`. - -record IsEquivalence {A : Set a} (_β_ : Rel A β) : Set (a β β) where - field - refl : Reflexive _β_ - sym : Symmetric _β_ - trans : Transitive _β_ - - reflexive : _β‘_ β _β_ - reflexive β‘-refl = refl - - - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.1 - -Conn = Connex -{-# WARNING_ON_USAGE Conn -"Warning: Conn was deprecated in v1.1. -Please use Connex instead." -#-} +-- cf. Algebra.Definitions.{_IdempotentOn_,Idempotent,IdempotentFun} +-- Idempotentβ is essentially the same as IdempotentFun except that +-- here we can specify the relation `_β_` "in place" instead of having +-- to do `open import Algebra.Definitions (_β_)` ahead of time. diff --git a/UALib/html/Relation.Binary.PropositionalEquality.Core.html b/UALib/html/Relation.Binary.PropositionalEquality.Core.html index 1cf00128..140ace6c 100644 --- a/UALib/html/Relation.Binary.PropositionalEquality.Core.html +++ b/UALib/html/Relation.Binary.PropositionalEquality.Core.html @@ -12,104 +12,114 @@ module Relation.Binary.PropositionalEquality.Core where open import Data.Product using (_,_) -open import Function using (_β_) -open import Level -open import Relation.Binary.Core -open import Relation.Nullary using (Β¬_) +open import Function.Base using (_β_) +open import Level +open import Relation.Binary.Core +open import Relation.Binary.Definitions +open import Relation.Nullary using (Β¬_) -private - variable - a b β : Level - A : Set a - B : Set b +private + variable + a b β : Level + A B C : Set a ------------------------------------------------------------------------- --- Propositional equality +------------------------------------------------------------------------ +-- Propositional equality -open import Agda.Builtin.Equality public +open import Agda.Builtin.Equality public -infix 4 _β’_ -_β’_ : {A : Set a} β Rel A a -x β’ y = Β¬ x β‘ y +infix 4 _β’_ +_β’_ : {A : Set a} β Rel A a +x β’ y = Β¬ x β‘ y ------------------------------------------------------------------------- --- Properties of _β‘_ +------------------------------------------------------------------------ +-- A variant of `refl` where the argument is explicit -sym : Symmetric {A = A} _β‘_ -sym refl = refl +pattern erefl x = refl {x = x} -trans : Transitive {A = A} _β‘_ -trans refl eq = eq +------------------------------------------------------------------------ +-- Congruence lemmas -subst : Substitutive {A = A} _β‘_ β -subst P refl p = p +cong : β (f : A β B) {x y} β x β‘ y β f x β‘ f y +cong f refl = refl -cong : β (f : A β B) {x y} β x β‘ y β f x β‘ f y -cong f refl = refl +congβ² : β {f : A β B} x β f x β‘ f x +congβ² _ = refl -respΛ‘ : β (βΌ : Rel A β) β βΌ RespectsΛ‘ _β‘_ -respΛ‘ _βΌ_ refl xβΌy = xβΌy +icong : β {f : A β B} {x y} β x β‘ y β f x β‘ f y +icong = cong _ -respΚ³ : β (βΌ : Rel A β) β βΌ RespectsΚ³ _β‘_ -respΚ³ _βΌ_ refl xβΌy = xβΌy +icongβ² : β {f : A β B} x β f x β‘ f x +icongβ² _ = refl -respβ : β (βΌ : Rel A β) β βΌ Respectsβ _β‘_ -respβ _βΌ_ = respΚ³ _βΌ_ , respΛ‘ _βΌ_ +congβ : β (f : A β B β C) {x y u v} β x β‘ y β u β‘ v β f x u β‘ f y v +congβ f refl refl = refl -isEquivalence : IsEquivalence {A = A} _β‘_ -isEquivalence = record - { refl = refl - ; sym = sym - ; trans = trans - } +cong-app : β {A : Set a} {B : A β Set b} {f g : (x : A) β B x} β + f β‘ g β (x : A) β f x β‘ g x +cong-app refl x = refl ------------------------------------------------------------------------- --- Various equality rearrangement lemmas +------------------------------------------------------------------------ +-- Properties of _β‘_ -trans-reflΚ³ : β {x y : A} (p : x β‘ y) β trans p refl β‘ p -trans-reflΚ³ refl = refl +sym : Symmetric {A = A} _β‘_ +sym refl = refl -trans-assoc : β {x y z u : A} (p : x β‘ y) {q : y β‘ z} {r : z β‘ u} β - trans (trans p q) r β‘ trans p (trans q r) -trans-assoc refl = refl +trans : Transitive {A = A} _β‘_ +trans refl eq = eq -trans-symΛ‘ : β {x y : A} (p : x β‘ y) β trans (sym p) p β‘ refl -trans-symΛ‘ refl = refl +subst : Substitutive {A = A} _β‘_ β +subst P refl p = p -trans-symΚ³ : β {x y : A} (p : x β‘ y) β trans p (sym p) β‘ refl -trans-symΚ³ refl = refl +substβ : β (_βΌ_ : REL A B β) {x y u v} β x β‘ y β u β‘ v β x βΌ u β y βΌ v +substβ _ refl refl p = p ------------------------------------------------------------------------- --- Properties of _β’_ +resp : β (P : A β Set β) β P Respects _β‘_ +resp P refl p = p -β’-sym : Symmetric {A = A} _β’_ -β’-sym xβ’y = xβ’y β sym +respΛ‘ : β (βΌ : Rel A β) β βΌ RespectsΛ‘ _β‘_ +respΛ‘ _βΌ_ refl xβΌy = xβΌy ------------------------------------------------------------------------- --- Convenient syntax for equational reasoning +respΚ³ : β (βΌ : Rel A β) β βΌ RespectsΚ³ _β‘_ +respΚ³ _βΌ_ refl xβΌy = xβΌy --- This is a special instance of `Relation.Binary.Reasoning.Setoid`. --- Rather than instantiating the latter with (setoid A), we reimplement --- equation chains from scratch since then goals are printed much more --- readably. +respβ : β (βΌ : Rel A β) β βΌ Respectsβ _β‘_ +respβ _βΌ_ = respΚ³ _βΌ_ , respΛ‘ _βΌ_ -module β‘-Reasoning {A : Set a} where +------------------------------------------------------------------------ +-- Properties of _β’_ - infix 3 _β - infixr 2 _β‘β¨β©_ _β‘β¨_β©_ _β‘Λβ¨_β©_ - infix 1 begin_ +β’-sym : Symmetric {A = A} _β’_ +β’-sym xβ’y = xβ’y β sym - begin_ : β{x y : A} β x β‘ y β x β‘ y - begin_ xβ‘y = xβ‘y +------------------------------------------------------------------------ +-- Convenient syntax for equational reasoning - _β‘β¨β©_ : β (x {y} : A) β x β‘ y β x β‘ y - _ β‘β¨β© xβ‘y = xβ‘y +-- This is a special instance of `Relation.Binary.Reasoning.Setoid`. +-- Rather than instantiating the latter with (setoid A), we reimplement +-- equation chains from scratch since then goals are printed much more +-- readably. - _β‘β¨_β©_ : β (x {y z} : A) β x β‘ y β y β‘ z β x β‘ z - _ β‘β¨ xβ‘y β© yβ‘z = trans xβ‘y yβ‘z +module β‘-Reasoning {A : Set a} where - _β‘Λβ¨_β©_ : β (x {y z} : A) β y β‘ x β y β‘ z β x β‘ z - _ β‘Λβ¨ yβ‘x β© yβ‘z = trans (sym yβ‘x) yβ‘z + infix 3 _β + infixr 2 _β‘β¨β©_ step-β‘ step-β‘Λ + infix 1 begin_ - _β : β (x : A) β x β‘ x - _β _ = refl + begin_ : β{x y : A} β x β‘ y β x β‘ y + begin_ xβ‘y = xβ‘y + + _β‘β¨β©_ : β (x {y} : A) β x β‘ y β x β‘ y + _ β‘β¨β© xβ‘y = xβ‘y + + step-β‘ : β (x {y z} : A) β y β‘ z β x β‘ y β x β‘ z + step-β‘ _ yβ‘z xβ‘y = trans xβ‘y yβ‘z + + step-β‘Λ : β (x {y z} : A) β y β‘ z β y β‘ x β x β‘ z + step-β‘Λ _ yβ‘z yβ‘x = trans (sym yβ‘x) yβ‘z + + _β : β (x : A) β x β‘ x + _β _ = refl + + syntax step-β‘ x yβ‘z xβ‘y = x β‘β¨ xβ‘y β© yβ‘z + syntax step-β‘Λ x yβ‘z yβ‘x = x β‘Λβ¨ yβ‘x β© yβ‘z diff --git a/UALib/html/Relation.Nullary.html b/UALib/html/Relation.Nullary.html index 5d0de5eb..afc27284 100644 --- a/UALib/html/Relation.Nullary.html +++ b/UALib/html/Relation.Nullary.html @@ -11,29 +11,60 @@ module Relation.Nullary where open import Agda.Builtin.Equality +open import Agda.Builtin.Bool -open import Data.Empty hiding (β₯-elim) -open import Data.Empty.Irrelevant -open import Level +open import Data.Empty hiding (β₯-elim) +open import Data.Empty.Irrelevant +open import Level --- Negation. +------------------------------------------------------------------------ +-- Negation. -infix 3 Β¬_ +infix 3 Β¬_ +infix 2 _because_ -Β¬_ : β {β} β Set β β Set β -Β¬ P = P β β₯ +Β¬_ : β {β} β Set β β Set β +Β¬ P = P β β₯ --- Decidable relations. +------------------------------------------------------------------------ +-- `Reflects` idiom. -data Dec {p} (P : Set p) : Set p where - yes : ( p : P) β Dec P - no : (Β¬p : Β¬ P) β Dec P +-- The truth value of P is reflected by a boolean value. --- Given an irrelevant proof of a decidable type, a proof can --- be recomputed and subsequently used in relevant contexts. -recompute : β {a} {A : Set a} β Dec A β .A β A -recompute (yes x) _ = x -recompute (no Β¬p) x = β₯-elim (Β¬p x) +data Reflects {p} (P : Set p) : Bool β Set p where + ofΚΈ : ( p : P) β Reflects P true + ofβΏ : (Β¬p : Β¬ P) β Reflects P false -Irrelevant : β {p} β Set p β Set p -Irrelevant P = β (pβ pβ : P) β pβ β‘ pβ +------------------------------------------------------------------------ +-- Decidability. + +-- Decidability proofs have two parts: the `does` term which contains +-- the boolean result and the `proof` term which contains a proof that +-- reflects the boolean result. This definition allows the boolean +-- part of the decision procedure to compute independently from the +-- proof. This leads to better computational behaviour when we only care +-- about the result and not the proof. See README.Decidability for +-- further details. + +record Dec {p} (P : Set p) : Set p where + constructor _because_ + field + does : Bool + proof : Reflects P does + +open Dec public + +pattern yes p = true because ofΚΈ p +pattern no Β¬p = false because ofβΏ Β¬p + +-- Given an irrelevant proof of a decidable type, a proof can +-- be recomputed and subsequently used in relevant contexts. +recompute : β {a} {A : Set a} β Dec A β .A β A +recompute (yes x) _ = x +recompute (no Β¬p) x = β₯-elim (Β¬p x) + +------------------------------------------------------------------------ +-- Irrelevant types + +Irrelevant : β {p} β Set p β Set p +Irrelevant P = β (pβ pβ : P) β pβ β‘ pβ diff --git a/UALib/html/Relation.Unary.html b/UALib/html/Relation.Unary.html index 934eb9fc..a5045355 100644 --- a/UALib/html/Relation.Unary.html +++ b/UALib/html/Relation.Unary.html @@ -11,280 +11,287 @@ open import Data.Empty open import Data.Unit.Base using (β€) open import Data.Product -open import Data.Sum using (_β_; [_,_]) -open import Function -open import Level -open import Relation.Nullary hiding (Irrelevant) -open import Relation.Binary.PropositionalEquality.Core using (_β‘_) +open import Data.Sum.Base using (_β_; [_,_]) +open import Function.Base +open import Level +open import Relation.Nullary hiding (Irrelevant) +open import Relation.Nullary.Decidable.Core using (True) +open import Relation.Binary.PropositionalEquality.Core using (_β‘_) -private - variable - a b c β ββ ββ : Level - A : Set a - B : Set b - C : Set c +private + variable + a b c β ββ ββ : Level + A : Set a + B : Set b + C : Set c ------------------------------------------------------------------------- --- Unary relations +------------------------------------------------------------------------ +-- Definition --- Unary relations are known as predicates and `Pred A β` can be viewed --- as some property that elements of type A might satisfy. +-- Unary relations are known as predicates and `Pred A β` can be viewed +-- as some property that elements of type A might satisfy. --- Consequently `P : Pred A β` can also be seen as a subset of A --- containing all the elements of A that satisfy property P. This view --- informs much of the notation used below. +-- Consequently `P : Pred A β` can also be seen as a subset of A +-- containing all the elements of A that satisfy property P. This view +-- informs much of the notation used below. -Pred : β {a} β Set a β (β : Level) β Set (a β suc β) -Pred A β = A β Set β +Pred : β {a} β Set a β (β : Level) β Set (a β suc β) +Pred A β = A β Set β ------------------------------------------------------------------------- --- Special sets +------------------------------------------------------------------------ +-- Special sets --- The empty set. +-- The empty set. -β : Pred A 0β -β = Ξ» _ β β₯ +β : Pred A 0β +β = Ξ» _ β β₯ --- The singleton set. +-- The singleton set. -ο½_ο½ : A β Pred A _ -ο½ x ο½ = x β‘_ +ο½_ο½ : A β Pred A _ +ο½ x ο½ = x β‘_ --- The universal set. +-- The universal set. -U : Pred A 0β -U = Ξ» _ β β€ +U : Pred A 0β +U = Ξ» _ β β€ ------------------------------------------------------------------------- --- Membership +------------------------------------------------------------------------ +-- Membership -infix 4 _β_ _β_ +infix 4 _β_ _β_ -_β_ : A β Pred A β β Set _ -x β P = P x +_β_ : A β Pred A β β Set _ +x β P = P x -_β_ : A β Pred A β β Set _ -x β P = Β¬ x β P +_β_ : A β Pred A β β Set _ +x β P = Β¬ x β P ------------------------------------------------------------------------- --- Subset relations +------------------------------------------------------------------------ +-- Subset relations -infix 4 _β_ _β_ _β_ _β_ _β_ _β_ _β_ _β _ +infix 4 _β_ _β_ _β_ _β_ _β_ _β_ _β_ _β _ -_β_ : Pred A ββ β Pred A ββ β Set _ -P β Q = β {x} β x β P β x β Q +_β_ : Pred A ββ β Pred A ββ β Set _ +P β Q = β {x} β x β P β x β Q -_β_ : Pred A ββ β Pred A ββ β Set _ -P β Q = Q β P +_β_ : Pred A ββ β Pred A ββ β Set _ +P β Q = Q β P -_β_ : Pred A ββ β Pred A ββ β Set _ -P β Q = Β¬ (P β Q) +_β_ : Pred A ββ β Pred A ββ β Set _ +P β Q = Β¬ (P β Q) -_β_ : Pred A ββ β Pred A ββ β Set _ -P β Q = Β¬ (P β Q) +_β_ : Pred A ββ β Pred A ββ β Set _ +P β Q = Β¬ (P β Q) -_β_ : Pred A ββ β Pred A ββ β Set _ -P β Q = P β Q Γ Q β P +_β_ : Pred A ββ β Pred A ββ β Set _ +P β Q = P β Q Γ Q β P -_β_ : Pred A ββ β Pred A ββ β Set _ -P β Q = Q β P +_β_ : Pred A ββ β Pred A ββ β Set _ +P β Q = Q β P -_β_ : Pred A ββ β Pred A ββ β Set _ -P β Q = Β¬ (P β Q) +_β_ : Pred A ββ β Pred A ββ β Set _ +P β Q = Β¬ (P β Q) -_β _ : Pred A ββ β Pred A ββ β Set _ -P β Q = Β¬ (P β Q) +_β _ : Pred A ββ β Pred A ββ β Set _ +P β Q = Β¬ (P β Q) --- The following primed variants of _β_ can be used when 'x' can't --- be inferred from 'x β P'. +-- The following primed variants of _β_ can be used when 'x' can't +-- be inferred from 'x β P'. -infix 4 _ββ²_ _ββ²_ _ββ²_ _ββ²_ _ββ²_ _ββ²_ _ββ²_ _β β²_ +infix 4 _ββ²_ _ββ²_ _ββ²_ _ββ²_ _ββ²_ _ββ²_ _ββ²_ _β β²_ -_ββ²_ : Pred A ββ β Pred A ββ β Set _ -P ββ² Q = β x β x β P β x β Q +_ββ²_ : Pred A ββ β Pred A ββ β Set _ +P ββ² Q = β x β x β P β x β Q -_ββ²_ : Pred A ββ β Pred A ββ β Set _ -Q ββ² P = P ββ² Q +_ββ²_ : Pred A ββ β Pred A ββ β Set _ +Q ββ² P = P ββ² Q -_ββ²_ : Pred A ββ β Pred A ββ β Set _ -P ββ² Q = Β¬ (P ββ² Q) +_ββ²_ : Pred A ββ β Pred A ββ β Set _ +P ββ² Q = Β¬ (P ββ² Q) -_ββ²_ : Pred A ββ β Pred A ββ β Set _ -P ββ² Q = Β¬ (P ββ² Q) +_ββ²_ : Pred A ββ β Pred A ββ β Set _ +P ββ² Q = Β¬ (P ββ² Q) -_ββ²_ : Pred A ββ β Pred A ββ β Set _ -P ββ² Q = P ββ² Q Γ Q ββ² P +_ββ²_ : Pred A ββ β Pred A ββ β Set _ +P ββ² Q = P ββ² Q Γ Q ββ² P -_ββ²_ : Pred A ββ β Pred A ββ β Set _ -P ββ² Q = Q ββ² P +_ββ²_ : Pred A ββ β Pred A ββ β Set _ +P ββ² Q = Q ββ² P -_ββ²_ : Pred A ββ β Pred A ββ β Set _ -P ββ² Q = Β¬ (P ββ² Q) +_ββ²_ : Pred A ββ β Pred A ββ β Set _ +P ββ² Q = Β¬ (P ββ² Q) -_β β²_ : Pred A ββ β Pred A ββ β Set _ -P β β² Q = Β¬ (P ββ² Q) +_β β²_ : Pred A ββ β Pred A ββ β Set _ +P β β² Q = Β¬ (P ββ² Q) ------------------------------------------------------------------------- --- Properties of sets +------------------------------------------------------------------------ +-- Properties of sets -infix 10 Satisfiable Universal IUniversal +infix 10 Satisfiable Universal IUniversal --- Emptiness - no element satisfies P. +-- Emptiness - no element satisfies P. -Empty : Pred A β β Set _ -Empty P = β x β x β P +Empty : Pred A β β Set _ +Empty P = β x β x β P --- Satisfiable - at least one element satisfies P. +-- Satisfiable - at least one element satisfies P. -Satisfiable : Pred A β β Set _ -Satisfiable P = β Ξ» x β x β P +Satisfiable : Pred A β β Set _ +Satisfiable P = β Ξ» x β x β P -syntax Satisfiable P = ββ¨ P β© +syntax Satisfiable P = ββ¨ P β© --- Universality - all elements satisfy P. +-- Universality - all elements satisfy P. -Universal : Pred A β β Set _ -Universal P = β x β x β P +Universal : Pred A β β Set _ +Universal P = β x β x β P -syntax Universal P = Ξ [ P ] +syntax Universal P = Ξ [ P ] --- Implicit universality - all elements satisfy P. +-- Implicit universality - all elements satisfy P. -IUniversal : Pred A β β Set _ -IUniversal P = β {x} β x β P +IUniversal : Pred A β β Set _ +IUniversal P = β {x} β x β P -syntax IUniversal P = β[ P ] +syntax IUniversal P = β[ P ] --- Decidability - it is possible to determine if an arbitrary element --- satisfies P. +-- Decidability - it is possible to determine if an arbitrary element +-- satisfies P. -Decidable : Pred A β β Set _ -Decidable P = β x β Dec (P x) +Decidable : Pred A β β Set _ +Decidable P = β x β Dec (P x) --- Irrelevance - any two proofs that an element satifies P are --- indistinguishable. +-- Erasure: A decidable predicate gives rise to another one, more +-- amenable to Ξ·-expansion -Irrelevant : Pred A β β Set _ -Irrelevant P = β {x} (a : P x) (b : P x) β a β‘ b +β_β : {P : Pred A β} β Decidable P β Pred A β +β P? β a = Lift _ (True (P? a)) --- Recomputability - we can rebuild a relevant proof given an --- irrelevant one. +-- Irrelevance - any two proofs that an element satifies P are +-- indistinguishable. -Recomputable : Pred A β β Set _ -Recomputable P = β {x} β .(P x) β P x +Irrelevant : Pred A β β Set _ +Irrelevant P = β {x} (a : P x) (b : P x) β a β‘ b ------------------------------------------------------------------------- --- Operations on sets +-- Recomputability - we can rebuild a relevant proof given an +-- irrelevant one. -infix 10 β β -infixr 9 _β’_ -infixr 8 _β_ -infixr 7 _β©_ -infixr 6 _βͺ_ -infix 4 _β¬_ +Recomputable : Pred A β β Set _ +Recomputable P = β {x} β .(P x) β P x --- Complement. +------------------------------------------------------------------------ +-- Operations on sets -β : Pred A β β Pred A β -β P = Ξ» x β x β P +infix 10 β β +infixr 9 _β’_ +infixr 8 _β_ +infixr 7 _β©_ +infixr 6 _βͺ_ +infix 4 _β¬_ --- Implication. +-- Complement. -_β_ : Pred A ββ β Pred A ββ β Pred A _ -P β Q = Ξ» x β x β P β x β Q +β : Pred A β β Pred A β +β P = Ξ» x β x β P --- Union. +-- Implication. -_βͺ_ : Pred A ββ β Pred A ββ β Pred A _ -P βͺ Q = Ξ» x β x β P β x β Q +_β_ : Pred A ββ β Pred A ββ β Pred A _ +P β Q = Ξ» x β x β P β x β Q --- Intersection. +-- Union. -_β©_ : Pred A ββ β Pred A ββ β Pred A _ -P β© Q = Ξ» x β x β P Γ x β Q +_βͺ_ : Pred A ββ β Pred A ββ β Pred A _ +P βͺ Q = Ξ» x β x β P β x β Q --- Infinitary union. +-- Intersection. -β : β {i} (I : Set i) β (I β Pred A β) β Pred A _ -β I P = Ξ» x β Ξ£[ i β I ] P i x +_β©_ : Pred A ββ β Pred A ββ β Pred A _ +P β© Q = Ξ» x β x β P Γ x β Q -syntax β I (Ξ» i β P) = β[ i βΆ I ] P +-- Infinitary union. --- Infinitary intersection. +β : β {i} (I : Set i) β (I β Pred A β) β Pred A _ +β I P = Ξ» x β Ξ£[ i β I ] P i x -β : β {i} (I : Set i) β (I β Pred A β) β Pred A _ -β I P = Ξ» x β (i : I) β P i x +syntax β I (Ξ» i β P) = β[ i βΆ I ] P -syntax β I (Ξ» i β P) = β[ i βΆ I ] P +-- Infinitary intersection. --- Positive version of non-disjointness, dual to inclusion. +β : β {i} (I : Set i) β (I β Pred A β) β Pred A _ +β I P = Ξ» x β (i : I) β P i x -_β¬_ : Pred A ββ β Pred A ββ β Set _ -P β¬ Q = β Ξ» x β x β P Γ x β Q +syntax β I (Ξ» i β P) = β[ i βΆ I ] P --- Update. +-- Positive version of non-disjointness, dual to inclusion. -_β’_ : (A β B) β Pred B β β Pred A β -f β’ P = Ξ» x β P (f x) +_β¬_ : Pred A ββ β Pred A ββ β Set _ +P β¬ Q = β Ξ» x β x β P Γ x β Q ------------------------------------------------------------------------- --- Predicate combinators +-- Update. --- These differ from the set operations above, as the carrier set of the --- resulting predicates are not the same as the carrier set of the --- component predicates. +_β’_ : (A β B) β Pred B β β Pred A β +f β’ P = Ξ» x β P (f x) -infixr 2 _β¨Γβ©_ -infixr 2 _β¨ββ©_ -infixr 1 _β¨ββ©_ -infixr 0 _β¨ββ©_ -infixl 9 _β¨Β·β©_ -infix 10 _~ -infixr 9 _β¨ββ©_ -infixr 2 _//_ _\\_ +------------------------------------------------------------------------ +-- Predicate combinators --- Product. +-- These differ from the set operations above, as the carrier set of the +-- resulting predicates are not the same as the carrier set of the +-- component predicates. -_β¨Γβ©_ : Pred A ββ β Pred B ββ β Pred (A Γ B) _ -(P β¨Γβ© Q) (x , y) = x β P Γ y β Q +infixr 2 _β¨Γβ©_ +infixr 2 _β¨ββ©_ +infixr 1 _β¨ββ©_ +infixr 0 _β¨ββ©_ +infixl 9 _β¨Β·β©_ +infix 10 _~ +infixr 9 _β¨ββ©_ +infixr 2 _//_ _\\_ --- Sum over one element. +-- Product. -_β¨ββ©_ : Pred A β β Pred B β β Pred (A β B) _ -P β¨ββ© Q = [ P , Q ] +_β¨Γβ©_ : Pred A ββ β Pred B ββ β Pred (A Γ B) _ +(P β¨Γβ© Q) (x , y) = x β P Γ y β Q --- Sum over two elements. +-- Sum over one element. -_β¨ββ©_ : Pred A ββ β Pred B ββ β Pred (A Γ B) _ -(P β¨ββ© Q) (x , y) = x β P β y β Q +_β¨ββ©_ : Pred A β β Pred B β β Pred (A β B) _ +P β¨ββ© Q = [ P , Q ] --- Implication. +-- Sum over two elements. -_β¨ββ©_ : Pred A ββ β Pred B ββ β Pred (A β B) _ -(P β¨ββ© Q) f = P β Q β f +_β¨ββ©_ : Pred A ββ β Pred B ββ β Pred (A Γ B) _ +(P β¨ββ© Q) (x , y) = x β P β y β Q --- Product. +-- Implication. -_β¨Β·β©_ : (P : Pred A ββ) (Q : Pred B ββ) β - (P β¨Γβ© (P β¨ββ© Q)) β Q β uncurry (flip _$_) -(P β¨Β·β© Q) (p , f) = f p +_β¨ββ©_ : Pred A ββ β Pred B ββ β Pred (A β B) _ +(P β¨ββ© Q) f = P β Q β f --- Converse. +-- Product. -_~ : Pred (A Γ B) β β Pred (B Γ A) β -P ~ = P β swap +_β¨Β·β©_ : (P : Pred A ββ) (Q : Pred B ββ) β + (P β¨Γβ© (P β¨ββ© Q)) β Q β uncurry (flip _$_) +(P β¨Β·β© Q) (p , f) = f p --- Composition. +-- Converse. -_β¨ββ©_ : Pred (A Γ B) ββ β Pred (B Γ C) ββ β Pred (A Γ C) _ -(P β¨ββ© Q) (x , z) = β Ξ» y β (x , y) β P Γ (y , z) β Q +_~ : Pred (A Γ B) β β Pred (B Γ A) β +P ~ = P β swap --- Post-division. +-- Composition. -_//_ : Pred (A Γ C) ββ β Pred (B Γ C) ββ β Pred (A Γ B) _ -(P // Q) (x , y) = Q β (y ,_) β P β (x ,_) +_β¨ββ©_ : Pred (A Γ B) ββ β Pred (B Γ C) ββ β Pred (A Γ C) _ +(P β¨ββ© Q) (x , z) = β Ξ» y β (x , y) β P Γ (y , z) β Q --- Pre-division. +-- Post-division. -_\\_ : Pred (A Γ C) ββ β Pred (A Γ B) ββ β Pred (B Γ C) _ -P \\ Q = (P ~ // Q ~) ~ +_//_ : Pred (A Γ C) ββ β Pred (B Γ C) ββ β Pred (A Γ B) _ +(P // Q) (x , y) = Q β (y ,_) β P β (x ,_) + +-- Pre-division. + +_\\_ : Pred (A Γ C) ββ β Pred (A Γ B) ββ β Pred (B Γ C) _ +P \\ Q = (P ~ // Q ~) ~ diff --git a/UALib/html/Relations.Continuous.md b/UALib/html/Relations.Continuous.md index 9fbe7e76..9645c1ff 100644 --- a/UALib/html/Relations.Continuous.md +++ b/UALib/html/Relations.Continuous.md @@ -39,10 +39,10 @@ To define `DepRel`, the type of *dependent relations*, we exploit the full power@@ -92,14 +92,14 @@ Above we saw lifts of continuous relations and what it means for such relations module _ {I J : π₯ Μ} {π : I β π€ Μ} where - eval-dep-rel : DepRel I π π¦ β (β i β (J β π i)) β π₯ β π¦ Μ + eval-dep-rel : DepRel I π π¦ β (β i β (J β π i)) β π₯ β π¦ Μ eval-dep-rel R πΆ = β j β R (Ξ» i β (πΆ i) j) - dep-compatible-op : (β i β Op J (π i)) β DepRel I π π¦ β π₯ β π€ β π¦ Μ + dep-compatible-op : (β i β Op J (π i)) β DepRel I π π¦ β π₯ β π€ β π¦ Μ dep-compatible-op π R = β πΆ β (eval-dep-rel R) πΆ β R Ξ» i β (π i)(πΆ i) -- equivalent definition using Ξ notation - dep-compatible'-op : (Ξ i κ I , Op J (π i)) β DepRel I π π¦ β π₯ β π€ β π¦ Μ + dep-compatible'-op : (Ξ i κ I , Op J (π i)) β DepRel I π π¦ β π₯ β π€ β π¦ Μ dep-compatible'-op π R = Ξ πΆ κ (Ξ i κ I , (J β π i)) , ((eval-dep-rel R) πΆ β R Ξ» i β (π i)(πΆ i))-ContRel : π₯ Μ β π€ Μ β (π¦ : Universe) β π₯ β π€ β π¦ βΊ Μ +ContRel : π₯ Μ β π€ Μ β (π¦ : Universe) β π₯ β π€ β π¦ βΊ Μ ContRel I A π¦ = (I β A) β π¦ Μ -DepRel : (I : π₯ Μ) β (I β π€ Μ) β (π¦ : Universe) β π₯ β π€ β π¦ βΊ Μ +DepRel : (I : π₯ Μ) β (I β π€ Μ) β (π¦ : Universe) β π₯ β π€ β π¦ βΊ Μ DepRel I π π¦ = Ξ π β π¦ Μ@@ -61,10 +61,10 @@ It will be helpful to have some functions that make it easy to assert that a giv module _ {I J : π₯ Μ} {A : π€ Μ} where - eval-cont-rel : ContRel I A π¦ β (I β J β A) β π₯ β π¦ Μ + eval-cont-rel : ContRel I A π¦ β (I β J β A) β π₯ β π¦ Μ eval-cont-rel R πΆ = Ξ j κ J , R Ξ» i β πΆ i j - cont-compatible-op : Op J A β ContRel I A π¦ β π₯ β π€ β π¦ Μ + cont-compatible-op : Op J A β ContRel I A π¦ β π₯ β π€ β π¦ Μ cont-compatible-op π R = Ξ πΆ κ (I β J β A) , (eval-cont-rel R πΆ β R Ξ» i β (π (πΆ i)))-Pred : π€ Μ β (π¦ : Universe) β π€ β π¦ βΊ Μ +Pred : π€ Μ β (π¦ : Universe) β π€ β π¦ βΊ Μ Pred A π¦ = A β π¦ Μ@@ -50,7 +50,7 @@ The "subset" relation is denoted, as usual, with the `β` symbol.[1](Relat-_β_ : {A : π€ Μ } β Pred A π¦ β Pred A π© β π€ β π¦ β π© Μ +_β_ : {A : π€ Μ } β Pred A π¦ β Pred A π© β π€ β π¦ β π© Μ P β Q = β {x} β x β P β x β Q infix 4 _β_ @@ -68,7 +68,7 @@ Here is a small collection of tools that will come in handy later. The first is@@ -192,7 +192,7 @@ The *total relation* over `A`, which in set theory is the full Cartesian product open import Unit-Type using (π) - π : Rel A π€β + π : Rel A π€β π a b = πinfixr 1 _β_ _βͺ_ -data _β_ (A : π€ Μ) (B : π¦ Μ) : π€ β π¦ Μ where +data _β_ (A : π€ Μ) (B : π¦ Μ) : π€ β π¦ Μ where injβ : (x : A) β A β B injβ : (y : B) β A β B @@ -78,7 +78,7 @@ And this can be used to represent *union*, as follows.@@ -173,16 +173,16 @@ Similarly, the *identity relation* (which is equivalent to the kernel of an inje module _ {A : π€ Μ } where π : Rel A π€ - π x y = x β‘ y + π x y = x β‘ y π-pred : Pred (A Γ A) π€ - π-pred (x , y) = x β‘ y + π-pred (x , y) = x β‘ y π-sigma : π€ Μ - π-sigma = Ξ£ x κ A , Ξ£ y κ A , x β‘ y + π-sigma = Ξ£ x κ A , Ξ£ y κ A , x β‘ y π-sigma' : π€ Μ - π-sigma' = Ξ£ (x , y) κ (A Γ A) , x β‘ y + π-sigma' = Ξ£ (x , y) κ (A Γ A) , x β‘ y-_βͺ_ : {A : π€ Μ} β Pred A π¦ β Pred A π© β Pred A (π¦ β π©) +_βͺ_ : {A : π€ Μ} β Pred A π¦ β Pred A π© β Pred A (π¦ β π©) P βͺ Q = Ξ» x β x β P β x β Q @@ -88,7 +88,7 @@ Next we define convenient notation for asserting that the image of a function (t@@ -111,7 +111,7 @@ Before closing our little predicates toolbox, let's insert a type that provides-Im_β_ : {A : π€ Μ}{B : π¦ Μ} β (A β B) β Pred B π© β π€ β π© Μ +Im_β_ : {A : π€ Μ}{B : π¦ Μ} β (A β B) β Pred B π© β π€ β π© Μ Im f β S = β x β f x β S@@ -100,7 +100,7 @@ The *empty set* is naturally represented by the *empty type*, `π`.[2](Re open import Empty-Type using (π) -β : {A : π€ Μ} β Pred A π€β +β : {A : π€ Μ} β Pred A π€β β _ = πο½_ο½ : {A : π€ Μ} β A β Pred A _ -ο½ x ο½ = x β‘_ +ο½ x ο½ = x β‘_@@ -127,7 +127,7 @@ A generalization of the notion of binary relation is a *relation from* `A` *to*-REL : π€ Μ β π¦ Μ β (π© : Universe) β π€ β π¦ β π© βΊ Μ +REL : π€ Μ β π¦ Μ β (π© : Universe) β π€ β π¦ β π© βΊ Μ REL A B π© = A β B β π© Μ@@ -136,7 +136,7 @@ In the special case, where `π¦ β‘ π€` and `B β‘ A`, we have-Rel : π€ Μ β (π© : Universe) β π€ β π© βΊ Μ +Rel : π€ Μ β (π© : Universe) β π€ β π© βΊ Μ Rel A π© = REL A A π©@@ -152,16 +152,16 @@ The *kernel* of `f : A β B` is defined informally by `{(x , y) β A Γ A : f module _ {A : π€ Μ}{B : π¦ Μ} where ker : (A β B) β Rel A π¦ - ker g x y = g x β‘ g y + ker g x y = g x β‘ g y kernel : (A β B) β Pred (A Γ A) π¦ - kernel g (x , y) = g x β‘ g y + kernel g (x , y) = g x β‘ g y - ker-sigma : (A β B) β π€ β π¦ Μ - ker-sigma g = Ξ£ x κ A , Ξ£ y κ A , g x β‘ g y + ker-sigma : (A β B) β π€ β π¦ Μ + ker-sigma g = Ξ£ x κ A , Ξ£ y κ A , g x β‘ g y - ker-sigma' : (A β B) β π€ β π¦ Μ - ker-sigma' g = Ξ£ (x , y) κ (A Γ A) , g x β‘ g y + ker-sigma' : (A β B) β π€ β π¦ Μ + ker-sigma' g = Ξ£ (x , y) κ (A Γ A) , g x β‘ g y-_=[_]β_ : {A : π€ Μ}{B : π¦ Μ} β Rel A π§ β (A β B) β Rel B π¨ β π€ β π§ β π¨ Μ +_=[_]β_ : {A : π€ Μ}{B : π¦ Μ} β Rel A π§ β (A β B) β Rel B π¨ β π€ β π§ β π¨ Μ P =[ g ]β Q = P β (Q on g) infixr 4 _=[_]β_ @@ -235,7 +235,7 @@ In the next subsection, we will define types that are useful for asserting and p--The type of operations -Op : π₯ Μ β π€ Μ β π€ β π₯ Μ +Op : π₯ Μ β π€ Μ β π€ β π₯ Μ Op I A = (I β A) β A@@ -257,10 +257,10 @@ Here is how we implement this in the [UALib][].-eval-rel : {A : π€ Μ}{I : π₯ Μ} β Rel A π¦ β Rel (I β A)(π₯ β π¦) +eval-rel : {A : π€ Μ}{I : π₯ Μ} β Rel A π¦ β Rel (I β A)(π₯ β π¦) eval-rel R u v = Ξ i κ _ , R (u i) (v i) -_|:_ : {A : π€ Μ}{I : π₯ Μ} β Op I A β Rel A π¦ β π€ β π₯ β π¦ Μ +_|:_ : {A : π€ Μ}{I : π₯ Μ} β Op I A β Rel A π¦ β π€ β π₯ β π¦ Μ f |: R = (eval-rel R) =[ f ]β R@@ -271,7 +271,7 @@ In case it helps the reader, we note that instead of using the slick implication-compatible-fun : {A : π€ Μ}{I : π₯ Μ} β (f : Op I A)(R : Rel A π¦) β π€ β π₯ β π¦ Μ +compatible-fun : {A : π€ Μ}{I : π₯ Μ} β (f : Op I A)(R : Rel A π¦) β π€ β π₯ β π¦ Μ compatible-fun f R = β u v β (eval-rel R) u v β R (f u) (f v)diff --git a/UALib/html/Relations.Extensionality.md b/UALib/html/Relations.Extensionality.md index 7b0ba076..2a551d45 100644 --- a/UALib/html/Relations.Extensionality.md +++ b/UALib/html/Relations.Extensionality.md @@ -24,8 +24,8 @@ The principle of *proposition extensionality* asserts that logically equivalent-pred-ext : (π€ π¦ : Universe) β (π€ β π¦) βΊ Μ -pred-ext π€ π¦ = β {A : π€ Μ}{P Q : Pred A π¦ } β P β Q β Q β P β P β‘ Q +pred-ext : (π€ π¦ : Universe) β (π€ β π¦) βΊ Μ +pred-ext π€ π¦ = β {A : π€ Μ}{P Q : Pred A π¦ } β P β Q β Q β P β P β‘ Q@@ -39,20 +39,20 @@ We need an identity type for congruence classes (blocks) over sets so that two d-module _ {π€ π¦ : Universe}{A : π€ Μ}{R : Rel A π¦} where +module _ {π€ π¦ : Universe}{A : π€ Μ}{R : Rel A π¦} where - block-ext : pred-ext π€ π¦ β IsEquivalence R β {u v : A} β R u v β [ u ]{R} β‘ [ v ]{R} + block-ext : pred-ext π€ π¦ β IsEquivalence R β {u v : A} β R u v β [ u ]{R} β‘ [ v ]{R} block-ext pe Req {u}{v} Ruv = pe (/-subset Req Ruv) (/-supset Req Ruv) to-subtype|uip : blk-uip A R β {C D : Pred A π¦}{c : IsBlock C {R}}{d : IsBlock D {R}} - β C β‘ D β (C , c) β‘ (D , d) + β C β‘ D β (C , c) β‘ (D , d) - to-subtype|uip buip {C}{D}{c}{d}CD = to-Ξ£-β‘(CD , buip D(transport(Ξ» B β IsBlock B)CD c)d) + to-subtype|uip buip {C}{D}{c}{d}CD = to-Ξ£-β‘(CD , buip D(transport(Ξ» B β IsBlock B)CD c)d) block-ext|uip : pred-ext π€ π¦ β blk-uip A R β IsEquivalence R - β β {u v : A} β R u v β βͺ u β« β‘ βͺ v β« + β β {u v : A} β R u v β βͺ u β« β‘ βͺ v β« block-ext|uip pe buip Req Ruv = to-subtype|uip buip (block-ext pe Req Ruv) @@ -72,11 +72,11 @@ We could also define *relation extensionality* principles which generalize the p-cont-rel-ext : (π€ π₯ π¦ : Universe) β (π€ β π₯ β π¦) βΊ Μ -cont-rel-ext π€ π₯ π¦ = β {I : π₯ Μ}{A : π€ Μ}{P Q : ContRel I A π¦ } β P β Q β Q β P β P β‘ Q +cont-rel-ext : (π€ π₯ π¦ : Universe) β (π€ β π₯ β π¦) βΊ Μ +cont-rel-ext π€ π₯ π¦ = β {I : π₯ Μ}{A : π€ Μ}{P Q : ContRel I A π¦ } β P β Q β Q β P β P β‘ Q -dep-rel-ext : (π€ π₯ π¦ : Universe) β (π€ β π₯ β π¦) βΊ Μ -dep-rel-ext π€ π₯ π¦ = β {I : π₯ Μ}{π : I β π€ Μ}{P Q : DepRel I π π¦ } β P β Q β Q β P β P β‘ Q +dep-rel-ext : (π€ π₯ π¦ : Universe) β (π€ β π₯ β π¦) βΊ Μ +dep-rel-ext π€ π₯ π¦ = β {I : π₯ Μ}{π : I β π€ Μ}{P Q : DepRel I π π¦ } β P β Q β Q β P β P β‘ Qdiff --git a/UALib/html/Relations.Quotients.md b/UALib/html/Relations.Quotients.md index 6cbdf272..c965aa9b 100644 --- a/UALib/html/Relations.Quotients.md +++ b/UALib/html/Relations.Quotients.md @@ -28,18 +28,18 @@ Let `π€ : Universe` be a universe and `A : π€ Μ` a type. In [Relations.Dis-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where - Refl : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ + Refl : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ Refl _β_ = β{x} β x β x - Symm : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ + Symm : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ Symm _β_ = β{x}{y} β x β y β y β x - Antisymm : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ - Antisymm _β_ = β{x}{y} β x β y β y β x β x β‘ y + Antisymm : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ + Antisymm _β_ = β{x}{y} β x β y β y β x β x β‘ y - Trans : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ + Trans : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ Trans _β_ = β{x}{y}{z} β x β y β y β z β x β z@@ -50,7 +50,7 @@ The [Type Topology][] library defines the following *uniqueness-of-proofs* princ module hide-is-subsingleton-valued where - is-subsingleton-valued : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ + is-subsingleton-valued : {A : π€ Μ} β Rel A π¦ β π€ β π¦ Μ is-subsingleton-valued _β_ = β x y β is-subsingleton (x β y) open import MGS-Quotient using (is-subsingleton-valued) public @@ -66,9 +66,9 @@ A binary relation is called a *preorder* if it is reflexive and transitive. An *-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where - record IsEquivalence {A : π€ Μ}(R : Rel A π¦) : π€ β π¦ Μ where + record IsEquivalence {A : π€ Μ}(R : Rel A π¦) : π€ β π¦ Μ where field rfl : Refl R ; sym : Symm R ; trans : Trans R@@ -77,7 +77,7 @@ And we define the type of equivalence relations over a given type `A` as follows- Equivalence : π€ Μ β π€ β π¦ βΊ Μ + Equivalence : π€ Μ β π€ β π¦ βΊ Μ Equivalence A = Ξ£ R κ Rel A π¦ , IsEquivalence R@@ -113,10 +113,10 @@ A predicate `C` over `A` is an `R`-block if and only if `C β‘ [ u ]` for some `-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where - IsBlock : {A : π€ Μ}(C : Pred A π¦){R : Rel A π¦} β π€ β π¦ βΊ Μ - IsBlock {A} C {R} = Ξ£ u κ A , C β‘ [ u ] {R} + IsBlock : {A : π€ Μ}(C : Pred A π¦){R : Rel A π¦} β π€ β π¦ βΊ Μ + IsBlock {A} C {R} = Ξ£ u κ A , C β‘ [ u ] {R}@@ -126,7 +126,7 @@ If `R` is an equivalence relation on `A`, then the *quotient* of `A` modulo `R`- _/_ : (A : π€ Μ ) β Rel A π¦ β π€ β (π¦ βΊ) Μ + _/_ : (A : π€ Μ ) β Rel A π¦ β π€ β (π¦ βΊ) Μ A / R = Ξ£ C κ Pred A π¦ , IsBlock C {R} infix -1 _/_ @@ -138,7 +138,7 @@ We use the following type to represent an \ab R-block with a designated represenβͺ_β« : {A : π€ Μ} β A β {R : Rel A π¦} β A / R - βͺ a β«{R} = [ a ]{R} , (a , refl) + βͺ a β«{R} = [ a ]{R} , (a , refl)@@ -147,7 +147,7 @@ Dually, the next type provides an *elimination rule*.[2](Relations.Quotientβ_β : {A : π€ Μ}{R : Rel A π¦} β A / R β A - β C , a , p β = a + β C , a , p β = a@@ -157,7 +157,7 @@ It will be convenient to have the following subset inclusion lemmas on hand when-module _ {π€ π¦ : Universe}{A : π€ Μ}{x y : A}{R : Rel A π¦} where +module _ {π€ π¦ : Universe}{A : π€ Μ}{x y : A}{R : Rel A π¦} where open IsEquivalence /-subset : IsEquivalence R β R x y β [ x ]{R} β [ y ]{R} diff --git a/UALib/html/Relations.Truncation.md b/UALib/html/Relations.Truncation.md index 4881d20f..0c4b0752 100644 --- a/UALib/html/Relations.Truncation.md +++ b/UALib/html/Relations.Truncation.md @@ -22,7 +22,7 @@ Readers who want to learn more about "proof-relevant mathematics" and other conc open import Relations.Quotients public -open import MGS-MLTT using (_β_) public +open import MGS-MLTT using (_β_) public@@ -47,12 +47,12 @@ This notion is formalized in the [Type Topology][] library, using the `is-subsin-module hide-is-set {π€ : Universe} where +module hide-is-set {π€ : Universe} where is-set : π€ Μ β π€ Μ - is-set A = (x y : A) β is-subsingleton (x β‘ y) + is-set A = (x y : A) β is-subsingleton (x β‘ y) -open import MGS-Embeddings using (is-set) public +open import MGS-Embeddings using (is-set) public@@ -62,12 +62,12 @@ We will also need the function [to-Ξ£-β‘](https://www.cs.bham.ac.uk/~mhe/HoTT-U-module hide-to-Ξ£-β‘ {π€ π¦ : Universe}{A : π€ Μ}{B : A β π¦ Μ} where +module hide-to-Ξ£-β‘ {π€ π¦ : Universe}{A : π€ Μ}{B : A β π¦ Μ} where - to-Ξ£-β‘ : {Ο Ο : Ξ£ B} β Ξ£ p κ β£ Ο β£ β‘ β£ Ο β£ , (transport B p β₯ Ο β₯) β‘ β₯ Ο β₯ β Ο β‘ Ο - to-Ξ£-β‘ (refl {x = x} , refl {x = a}) = refl {x = (x , a)} + to-Ξ£-β‘ : {Ο Ο : Ξ£ B} β Ξ£ p κ β£ Ο β£ β‘ β£ Ο β£ , (transport B p β₯ Ο β₯) β‘ β₯ Ο β₯ β Ο β‘ Ο + to-Ξ£-β‘ (refl {x = x} , refl {x = a}) = refl {x = (x , a)} -open import MGS-Embeddings using (to-Ξ£-β‘) public +open import MGS-Embeddings using (to-Ξ£-β‘) public@@ -80,23 +80,23 @@ Before moving on to define [propositions](Overture.Truncation.html#propositions)-module _ {π€ π¦ : Universe}{A : π€ Μ}{B : π¦ Μ} where +module _ {π€ π¦ : Universe}{A : π€ Μ}{B : π¦ Μ} where - monic-is-embedding|Set : (f : A β B) β is-set B β Monic f β is-embedding f + monic-is-embedding|Set : (f : A β B) β is-set B β Monic f β is-embedding f - monic-is-embedding|Set f Bset fmon b (u , fuβ‘b) (v , fvβ‘b) = Ξ³ + monic-is-embedding|Set f Bset fmon b (u , fuβ‘b) (v , fvβ‘b) = Ξ³ where - fuv : f u β‘ f v + fuv : f u β‘ f v fuv = β‘-trans fuβ‘b (fvβ‘b β»ΒΉ) - uv : u β‘ v + uv : u β‘ v uv = fmon u v fuv - arg1 : Ξ£ p κ (u β‘ v) , (transport (Ξ» a β f a β‘ b) p fuβ‘b) β‘ fvβ‘b - arg1 = uv , Bset (f v) b (transport (Ξ» a β f a β‘ b) uv fuβ‘b) fvβ‘b + arg1 : Ξ£ p κ (u β‘ v) , (transport (Ξ» a β f a β‘ b) p fuβ‘b) β‘ fvβ‘b + arg1 = uv , Bset (f v) b (transport (Ξ» a β f a β‘ b) uv fuβ‘b) fvβ‘b - Ξ³ : u , fuβ‘b β‘ v , fvβ‘b - Ξ³ = to-Ξ£-β‘ arg1 + Ξ³ : u , fuβ‘b β‘ v , fvβ‘b + Ξ³ = to-Ξ£-β‘ arg1@@ -106,8 +106,8 @@ Embeddings are always monic, so we conclude that when a function's codomain is a- embedding-iff-monic|Set : (f : A β B) β is-set B β is-embedding f β Monic f - embedding-iff-monic|Set f Bset = (embedding-is-monic f), (monic-is-embedding|Set f Bset) + embedding-iff-monic|Set : (f : A β B) β is-set B β is-embedding f β Monic f + embedding-iff-monic|Set f Bset = (embedding-is-monic f), (monic-is-embedding|Set f Bset)@@ -125,7 +125,7 @@ In the next module ([Relations.Extensionality][]) we will define a *quotient ext-blk-uip : {π¦ π€ : Universe}(A : π€ Μ)(R : Rel A π¦ ) β π€ β π¦ βΊ Μ +blk-uip : {π¦ π€ : Universe}(A : π€ Μ)(R : Rel A π¦ ) β π€ β π¦ βΊ Μ blk-uip {π¦} A R = β (C : Pred A π¦) β is-subsingleton (IsBlock C {R})@@ -142,27 +142,27 @@ Naturally, we define the corresponding *truncated continuous relation type* and-module _ {π€ : Universe}{I : π₯ Μ} where +module _ {π€ : Universe}{I : π₯ Μ} where open import Relations.Continuous using (ContRel; DepRel) - IsContProp : {A : π€ Μ}{π¦ : Universe} β ContRel I A π¦ β π₯ β π€ β π¦ Μ + IsContProp : {A : π€ Μ}{π¦ : Universe} β ContRel I A π¦ β π₯ β π€ β π¦ Μ IsContProp {A = A} P = Ξ π κ (I β A) , is-subsingleton (P π) - ContProp : π€ Μ β (π¦ : Universe) β π€ β π₯ β π¦ βΊ Μ + ContProp : π€ Μ β (π¦ : Universe) β π€ β π₯ β π¦ βΊ Μ ContProp A π¦ = Ξ£ P κ (ContRel I A π¦) , IsContProp P - cont-prop-ext : π€ Μ β (π¦ : Universe) β π€ β π₯ β π¦ βΊ Μ - cont-prop-ext A π¦ = {P Q : ContProp A π¦ } β β£ P β£ β β£ Q β£ β β£ Q β£ β β£ P β£ β P β‘ Q + cont-prop-ext : π€ Μ β (π¦ : Universe) β π€ β π₯ β π¦ βΊ Μ + cont-prop-ext A π¦ = {P Q : ContProp A π¦ } β β£ P β£ β β£ Q β£ β β£ Q β£ β β£ P β£ β P β‘ Q - IsDepProp : {I : π₯ Μ}{π : I β π€ Μ}{π¦ : Universe} β DepRel I π π¦ β π₯ β π€ β π¦ Μ + IsDepProp : {I : π₯ Μ}{π : I β π€ Μ}{π¦ : Universe} β DepRel I π π¦ β π₯ β π€ β π¦ Μ IsDepProp {I = I} {π} P = Ξ π κ Ξ π , is-subsingleton (P π) - DepProp : (I β π€ Μ) β (π¦ : Universe) β π€ β π₯ β π¦ βΊ Μ + DepProp : (I β π€ Μ) β (π¦ : Universe) β π€ β π₯ β π¦ βΊ Μ DepProp π π¦ = Ξ£ P κ (DepRel I π π¦) , IsDepProp P - dep-prop-ext : (I β π€ Μ) β (π¦ : Universe) β π€ β π₯ β π¦ βΊ Μ - dep-prop-ext π π¦ = {P Q : DepProp π π¦} β β£ P β£ β β£ Q β£ β β£ Q β£ β β£ P β£ β P β‘ Q + dep-prop-ext : (I β π€ Μ) β (π¦ : Universe) β π€ β π₯ β π¦ βΊ Μ + dep-prop-ext π π¦ = {P Q : DepProp π π¦} β β£ P β£ β β£ Q β£ β β£ Q β£ β β£ P β£ β P β‘ Qdiff --git a/UALib/html/Strict.html b/UALib/html/Strict.html index c2bda9fe..677eeeeb 100644 --- a/UALib/html/Strict.html +++ b/UALib/html/Strict.html @@ -12,11 +12,11 @@ open import Agda.Builtin.Equality open import Agda.Builtin.Strict - renaming ( primForce to force - ; primForceLemma to force-β‘) public + renaming ( primForce to force + ; primForceLemma to force-β‘) public -- Derived combinators -module _ {β ββ² : Level} {A : Set β} {B : Set ββ²} where +module _ {β ββ² : Level} {A : Set β} {B : Set ββ²} where forceβ² : A β (A β B) β B forceβ² = force diff --git a/UALib/html/Subalgebras.Subalgebras.md b/UALib/html/Subalgebras.Subalgebras.md index 14ac778a..cd74fef0 100644 --- a/UALib/html/Subalgebras.Subalgebras.md +++ b/UALib/html/Subalgebras.Subalgebras.md @@ -29,10 +29,10 @@ Given algebras `π¨ : Algebra π€ π` and `π© : Algebra π¦ π`, we say-_IsSubalgebraOf_ : {π¦ π€ : Universe}(π© : Algebra π¦ π)(π¨ : Algebra π€ π) β π β π₯ β π€ β π¦ Μ +_IsSubalgebraOf_ : {π¦ π€ : Universe}(π© : Algebra π¦ π)(π¨ : Algebra π€ π) β π β π₯ β π€ β π¦ Μ π© IsSubalgebraOf π¨ = Ξ£ h κ hom π© π¨ , is-embedding β£ h β£ -Subalgebra : {π¦ π€ : Universe} β Algebra π€ π β ov π¦ β π€ Μ +Subalgebra : {π¦ π€ : Universe} β Algebra π€ π β ov π¦ β π€ Μ Subalgebra {π¦} π¨ = Ξ£ π© κ (Algebra π¦ π) , π© IsSubalgebraOf π¨@@ -50,17 +50,17 @@ We take this opportunity to prove an important lemma that makes use of the `IsSu -- open Congruence -module _ {π€ π¦ : Universe}(π¨ : Algebra π€ π)(π© : Algebra π¦ π)(h : hom π¨ π©) +module _ {π€ π¦ : Universe}(π¨ : Algebra π€ π)(π© : Algebra π¦ π)(h : hom π¨ π©) -- extensionality assumptions: - (pe : pred-ext π€ π¦)(fe : dfunext π₯ π¦) + (pe : pred-ext π€ π¦)(fe : dfunext π₯ π¦) -- truncation assumptions: - (Bset : is-set β£ π© β£) + (Bset : is-set β£ π© β£) (buip : blk-uip β£ π¨ β£ β£ kercon π© {fe} h β£) where FirstHomCorollary|Set : (π¨ [ π© ]/ker h βΎ fe) IsSubalgebraOf π© - FirstHomCorollary|Set = Οhom , Οemb + FirstHomCorollary|Set = Οhom , Οemb where hh = FirstHomTheorem|Set π¨ π© h pe fe Bset buip Οhom : hom (π¨ [ π© ]/ker h βΎ fe) π© @@ -75,12 +75,12 @@ If we apply the foregoing theorem to the special case in which the `π¨` is ter-module _ {π€ π¦ π§ : Universe}(X : π§ Μ)(π© : Algebra π¦ π)(h : hom (π» X) π©) +module _ {π€ π¦ π§ : Universe}(X : π§ Μ)(π© : Algebra π¦ π)(h : hom (π» X) π©) -- extensionality assumptions: - (pe : pred-ext (ov π§) π¦)(fe : dfunext π₯ π¦) + (pe : pred-ext (ov π§) π¦)(fe : dfunext π₯ π¦) -- truncation assumptions: - (Bset : is-set β£ π© β£) + (Bset : is-set β£ π© β£) (buip : blk-uip (Term X) β£ kercon π© {fe} h β£) where @@ -93,7 +93,7 @@ If we apply the foregoing theorem to the special case in which the `π¨` is ter@@ -28,9 +28,9 @@ We first show how to represent in [Agda][] the collection of subuniverses of an-_β€_ : {π¦ π€ : Universe} β Algebra π¦ π β Algebra π€ π β π β π₯ β π€ β π¦ Μ +_β€_ : {π¦ π€ : Universe} β Algebra π¦ π β Algebra π€ π β π β π₯ β π€ β π¦ Μ π© β€ π¨ = π© IsSubalgebraOf π¨@@ -109,9 +109,9 @@ Suppose `π¦ : Pred (Algebra π€ π) π©` denotes a class of `π`-algebra-module _ {π¦ π€ π© : Universe} where +module _ {π¦ π€ π© : Universe} where - _IsSubalgebraOfClass_ : Algebra π¦ π β Pred (Algebra π€ π) π© β ov (π€ β π¦) β π© Μ + _IsSubalgebraOfClass_ : Algebra π¦ π β Pred (Algebra π€ π) π© β ov (π€ β π¦) β π© Μ π© IsSubalgebraOfClass π¦ = Ξ£ π¨ κ Algebra π€ π , Ξ£ sa κ Subalgebra{π¦} π¨ , (π¨ β π¦) Γ (π© β β£ sa β£)@@ -120,7 +120,7 @@ Using this type, we express the collection of all subalgebras of algebras in a c-SubalgebraOfClass : {π¦ π€ : Universe} β Pred (Algebra π€ π)(ov π€) β ov (π€ β π¦) Μ +SubalgebraOfClass : {π¦ π€ : Universe} β Pred (Algebra π€ π)(ov π€) β ov (π€ β π¦) Μ SubalgebraOfClass {π¦} π¦ = Ξ£ π© κ Algebra π¦ π , π© IsSubalgebraOfClass π¦@@ -137,7 +137,7 @@ First we show that the subalgebra relation is a *preorder*; i.e., it is a reflexβ€-reflexive : (π¨ : Algebra π€ π) β π¨ β€ π¨ -β€-reflexive π¨ = (ππ β£ π¨ β£ , Ξ» π π β refl) , id-is-embedding +β€-reflexive π¨ = (ππ β£ π¨ β£ , Ξ» π π β refl) , id-is-embedding β€-refl : {π¨ : Algebra π€ π} β π¨ β€ π¨ β€-refl {π¨ = π¨} = β€-reflexive π¨ @@ -146,7 +146,7 @@ First we show that the subalgebra relation is a *preorder*; i.e., it is a reflex β€-transitivity : (π¨ : Algebra π§ π)(π© : Algebra π¨ π)(πͺ : Algebra π© π) β πͺ β€ π© β π© β€ π¨ β πͺ β€ π¨ -β€-transitivity π¨ π© πͺ CB BA = (β-hom πͺ π¨ β£ CB β£ β£ BA β£) , β-embedding β₯ BA β₯ β₯ CB β₯ +β€-transitivity π¨ π© πͺ CB BA = (β-hom πͺ π¨ β£ CB β£ β£ BA β£) , β-embedding β₯ BA β₯ β₯ CB β₯ β€-trans : (π¨ : Algebra π§ π){π© : Algebra π¨ π}{πͺ : Algebra π© π} β πͺ β€ π© β π© β€ π¨ β πͺ β€ π¨ β€-trans π¨ {π©}{πͺ} = β€-transitivity π¨ π© πͺ @@ -160,7 +160,7 @@ Next we prove that if two algebras are isomorphic and one of them is a subalgebr β€-iso : (π¨ : Algebra π§ π){π© : Algebra π¨ π}{πͺ : Algebra π© π} β πͺ β π© β π© β€ π¨ β πͺ β€ π¨ -β€-iso π¨ {π©} {πͺ} CB BA = (g β f , gfhom) , gfemb +β€-iso π¨ {π©} {πͺ} CB BA = (g β f , gfhom) , gfemb where f : β£ πͺ β£ β β£ π© β£ f = fst β£ CB β£ @@ -183,13 +183,13 @@ Next we prove that if two algebras are isomorphic and one of them is a subalgebr β€-TRANS-β : (π¨ : Algebra π§ π){π© : Algebra π¨ π}(πͺ : Algebra π© π) β π¨ β€ π© β π© β πͺ β π¨ β€ πͺ -β€-TRANS-β π¨ πͺ Aβ€B Bβ C = (β-hom π¨ πͺ β£ Aβ€B β£ β£ Bβ C β£) , β-embedding (isoβembedding Bβ C)(β₯ Aβ€B β₯) +β€-TRANS-β π¨ πͺ Aβ€B Bβ C = (β-hom π¨ πͺ β£ Aβ€B β£ β£ Bβ C β£) , β-embedding (isoβembedding Bβ C)(β₯ Aβ€B β₯) β€-mono : (π© : Algebra π¦ π){π¦ π¦' : Pred (Algebra π€ π) π©} β π¦ β π¦' β π© IsSubalgebraOfClass π¦ β π© IsSubalgebraOfClass π¦' -β€-mono π© KK' KB = β£ KB β£ , fst β₯ KB β₯ , KK' (β£ snd β₯ KB β₯ β£) , β₯ (snd β₯ KB β₯) β₯ +β€-mono π© KK' KB = β£ KB β£ , fst β₯ KB β₯ , KK' (β£ snd β₯ KB β₯ β£) , β₯ (snd β₯ KB β₯) β₯@@ -202,17 +202,17 @@ Next we prove that if two algebras are isomorphic and one of them is a subalgebr module _ {π¦ : Pred (Algebra π€ π)(ov π€)}{π© : Algebra π€ π} where Lift-is-sub : π© IsSubalgebraOfClass π¦ β (Lift-alg π© π€) IsSubalgebraOfClass π¦ - Lift-is-sub (π¨ , (sa , (KA , Bβ sa))) = π¨ , sa , KA , β -trans (β -sym Lift-β ) Bβ sa + Lift-is-sub (π¨ , (sa , (KA , Bβ sa))) = π¨ , sa , KA , β -trans (β -sym Lift-β ) Bβ sa -Lift-β€ : (π¨ : Algebra π§ π){π© : Algebra π¨ π}{π© : Universe} β π© β€ π¨ β Lift-alg π© π© β€ π¨ +Lift-β€ : (π¨ : Algebra π§ π){π© : Algebra π¨ π}{π© : Universe} β π© β€ π¨ β Lift-alg π© π© β€ π¨ Lift-β€ π¨ Bβ€A = β€-iso π¨ (β -sym Lift-β ) Bβ€A -β€-Lift : (π¨ : Algebra π§ π){π© : Universe}{π© : Algebra π¨ π} β π© β€ π¨ β π© β€ Lift-alg π¨ π© +β€-Lift : (π¨ : Algebra π§ π){π© : Universe}{π© : Algebra π¨ π} β π© β€ π¨ β π© β€ Lift-alg π¨ π© β€-Lift π¨ {π©} {π©} Bβ€A = β€-TRANS-β π© {π¨} (Lift-alg π¨ π©) Bβ€A Lift-β -module _ {π§ π¨ π© π¦ : Universe} where +module _ {π§ π¨ π© π¦ : Universe} where Lift-β€-Lift : {π¨ : Algebra π§ π}(π© : Algebra π¨ π) β π¨ β€ π© β Lift-alg π¨ π© β€ Lift-alg π© π¦ Lift-β€-Lift {π¨} π© Aβ€B = β€-trans (Lift-alg π© π¦) (β€-trans π© lAA Aβ€B) Bβ€lB diff --git a/UALib/html/Subalgebras.Subuniverses.md b/UALib/html/Subalgebras.Subuniverses.md index 9c2ec694..7635710e 100644 --- a/UALib/html/Subalgebras.Subuniverses.md +++ b/UALib/html/Subalgebras.Subuniverses.md @@ -20,7 +20,7 @@ We start by defining a type that represents the important concept of **subuniver module Subalgebras.Subuniverses {π : Signature π π₯} where open import Terms.Operations{π = π} public -open import Relation.Unary using (β) public +open import Relation.Unary using (β) public-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where - Subuniverses : (π¨ : Algebra π€ π) β Pred (Pred β£ π¨ β£ π¦)(π β π₯ β π€ β π¦) + Subuniverses : (π¨ : Algebra π€ π) β Pred (Pred β£ π¨ β£ π¦)(π β π₯ β π€ β π¦) Subuniverses π¨ B = (π : β£ π β£)(π : β₯ π β₯ π β β£ π¨ β£) β Im π β B β (π Μ π¨) π β B@@ -39,8 +39,8 @@ Here's one way to construct an algebra out of a subuniverse.- SubunivAlg : (π¨ : Algebra π€ π)(B : Pred β£ π¨ β£ π¦) β B β Subuniverses π¨ β Algebra (π€ β π¦) π - SubunivAlg π¨ B BβSubA = Ξ£ B , Ξ» π π β (π Μ π¨)(fst β π) , BβSubA π (fst β π)(snd β π) + SubunivAlg : (π¨ : Algebra π€ π)(B : Pred β£ π¨ β£ π¦) β B β Subuniverses π¨ β Algebra (π€ β π¦) π + SubunivAlg π¨ B BβSubA = Ξ£ B , Ξ» π π β (π Μ π¨)(fst β π) , BβSubA π (fst β π)(snd β π)@@ -52,7 +52,7 @@ Next we define a type to represent a single subuniverse of an algebra. If `π¨`- record Subuniverse {π¨ : Algebra π€ π} : ov (π€ β π¦) Μ where + record Subuniverse {π¨ : Algebra π€ π} : ov (π€ β π¦) Μ where constructor mksub field sset : Pred β£ π¨ β£ π¦ @@ -71,7 +71,7 @@ We define an inductive type, denoted by `Sg`, that represents the subuniverse ge- data Sg (π¨ : Algebra π€ π)(X : Pred β£ π¨ β£ π¦) : Pred β£ π¨ β£ (π β π₯ β π¦ β π€) where + data Sg (π¨ : Algebra π€ π)(X : Pred β£ π¨ β£ π¦) : Pred β£ π¨ β£ (π β π₯ β π¦ β π€) where var : β {v} β v β X β v β Sg π¨ X app : (π : β£ π β£)(π : β₯ π β₯ π β β£ π¨ β£) β Im π β Sg π¨ X β (π Μ π¨) π β Sg π¨ X @@ -81,7 +81,7 @@ Given an arbitrary subset `X` of the domain `β£ π¨ β£` of an `π`-algebra-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where sgIsSub : {π¨ : Algebra π€ π}{X : Pred β£ π¨ β£ π¦} β Sg π¨ X β Subuniverses π¨ sgIsSub = app @@ -92,7 +92,7 @@ Next we prove by structural induction that `Sg X` is the smallest subuniverse of- sgIsSmallest : {π‘ : Universe}(π¨ : Algebra π€ π){X : Pred β£ π¨ β£ π¦}(Y : Pred β£ π¨ β£ π‘) + sgIsSmallest : {π‘ : Universe}(π¨ : Algebra π€ π){X : Pred β£ π¨ β£ π¦}(Y : Pred β£ π¨ β£ π‘) β Y β Subuniverses π¨ β X β Y β Sg π¨ X β Y sgIsSmallest _ _ _ XinY (var Xv) = XinY Xv @@ -117,12 +117,12 @@ Here we formalize a few basic properties of subuniverses. First, the intersectio-module _ {π π€ π¦ : Universe} where +module _ {π π€ π¦ : Universe} where sub-intersection : {π¨ : Algebra π€ π}{I : π Μ}{π : I β Pred β£ π¨ β£ π¦} β Ξ i κ I , π i β Subuniverses π¨ ---------------------------------- - β β I π β Subuniverses π¨ + β β I π β Subuniverses π¨ sub-intersection Ξ± π π Ξ² = Ξ» i β Ξ± i π π (Ξ» x β Ξ² x i) @@ -142,9 +142,9 @@ Next, subuniverses are closed under the action of term operations.-module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where - sub-term-closed : {π§ : Universe}{X : π§ Μ}(π¨ : Algebra π€ π){B : Pred β£ π¨ β£ π¦} + sub-term-closed : {π§ : Universe}{X : π§ Μ}(π¨ : Algebra π€ π){B : Pred β£ π¨ β£ π¦} β (B β Subuniverses π¨) β (t : Term X)(b : X β β£ π¨ β£) β Ξ x κ X , (b x β B) β (t Μ π¨) b β B @@ -170,7 +170,7 @@ Alternatively, we could express the preceeding fact using an inductive type repr- data TermImage (π¨ : Algebra π€ π)(Y : Pred β£ π¨ β£ π¦) : Pred β£ π¨ β£ (π β π₯ β π€ β π¦) + data TermImage (π¨ : Algebra π€ π)(Y : Pred β£ π¨ β£ π¦) : Pred β£ π¨ β£ (π β π₯ β π€ β π¦) where var : β {y : β£ π¨ β£} β y β Y β y β TermImage π¨ Y app : β π π‘ β Ξ x κ β₯ π β₯ π , π‘ x β TermImage π¨ Y β (π Μ π¨) π‘ β TermImage π¨ Y @@ -206,7 +206,7 @@ Now that we have developed the machinery of subuniverse generation, we can prove- hom-image-is-sub : dfunext π₯ π¦ β {π¨ : Algebra π€ π}{π© : Algebra π¦ π} + hom-image-is-sub : dfunext π₯ π¦ β {π¨ : Algebra π€ π}{π© : Algebra π¦ π} (Ο : hom π¨ π©) β (HomImage π© Ο) β Subuniverses π© hom-image-is-sub fe {π¨}{π©} Ο π b Imfb = eq ((π Μ π©) b) ((π Μ π¨) ar) Ξ³ @@ -214,10 +214,10 @@ Now that we have developed the machinery of subuniverse generation, we can prove ar : β₯ π β₯ π β β£ π¨ β£ ar = Ξ» x β Inv β£ Ο β£ (Imfb x) - ΞΆ : β£ Ο β£ β ar β‘ b + ΞΆ : β£ Ο β£ β ar β‘ b ΞΆ = fe (Ξ» x β InvIsInv β£ Ο β£ (Imfb x)) - Ξ³ : (π Μ π©) b β‘ β£ Ο β£ ((π Μ π¨) ar) + Ξ³ : (π Μ π©) b β‘ β£ Ο β£ ((π Μ π¨) ar) Ξ³ = (π Μ π©) b β‘β¨ ap (π Μ π©)(ΞΆ β»ΒΉ) β© (π Μ π©) (β£ Ο β£ β ar) β‘β¨(β₯ Ο β₯ π ar)β»ΒΉ β© β£ Ο β£ ((π Μ π¨) ar) β @@ -231,9 +231,9 @@ Next we prove the important fact that homomorphisms are uniquely determined by t hom-unique : funext π₯ π¦ β {π¨ : Algebra π€ π}{π© : Algebra π¦ π} (X : Pred β£ π¨ β£ π€) (g h : hom π¨ π©) - β Ξ x κ β£ π¨ β£ , (x β X β β£ g β£ x β‘ β£ h β£ x) + β Ξ x κ β£ π¨ β£ , (x β X β β£ g β£ x β‘ β£ h β£ x) ------------------------------------------------- - β Ξ a κ β£ π¨ β£ , (a β Sg π¨ X β β£ g β£ a β‘ β£ h β£ a) + β Ξ a κ β£ π¨ β£ , (a β Sg π¨ X β β£ g β£ a β‘ β£ h β£ a) hom-unique _ _ _ _ Ξ± a (var x) = Ξ± a x diff --git a/UALib/html/Subalgebras.Univalent.md b/UALib/html/Subalgebras.Univalent.md index 2a45f5e7..c4832e60 100644 --- a/UALib/html/Subalgebras.Univalent.md +++ b/UALib/html/Subalgebras.Univalent.md @@ -36,21 +36,21 @@ This module can be safely skipped, or even left out of the Agda Universal Algebr open import MGS-Subsingleton-Theorems using (Ξ -is-subsingleton) open import MGS-Embeddings using (embedding-gives-ap-is-equiv; prβ-embedding; - lr-implication; rl-implication; inverse; Γ-is-subsingleton; _β_; _β_; + lr-implication; rl-implication; inverse; Γ-is-subsingleton; _β_; _β_; logically-equivalent-subsingletons-are-equivalent) -module mhe_subgroup_generalization {π¦ : Universe} {π¨ : Algebra π¦ π} (ua : Univalence) where +module mhe_subgroup_generalization {π¦ : Universe} {π¨ : Algebra π¦ π} (ua : Univalence) where - open import MGS-Powerset renaming (_β_ to _ββ_; _β_ to _ββ_; β-is-subsingleton to ββ-is-subsingleton) + open import MGS-Powerset renaming (_β_ to _ββ_; _β_ to _ββ_; β-is-subsingleton to ββ-is-subsingleton) using (π; equiv-to-subsingleton; powersets-are-sets'; subset-extensionality'; propext; _holds; Ξ©) - op-closed : (β£ π¨ β£ β π¦ Μ) β π β π₯ β π¦ Μ + op-closed : (β£ π¨ β£ β π¦ Μ) β π β π₯ β π¦ Μ op-closed B = (f : β£ π β£)(a : β₯ π β₯ f β β£ π¨ β£) β ((i : β₯ π β₯ f) β B (a i)) β B ((f Μ π¨) a) - subuniverse : π β π₯ β π¦ βΊ Μ + subuniverse : π β π₯ β π¦ βΊ Μ subuniverse = Ξ£ B κ (π β£ π¨ β£) , op-closed ( _ββ B) @@ -67,51 +67,51 @@ This module can be safely skipped, or even left out of the Agda Universal Algebr --so equality of subalgebras is equality of their underlying subsets in the powerset: - ap-prβ : (B C : subuniverse) β B β‘ C β β£ B β£ β‘ β£ C β£ + ap-prβ : (B C : subuniverse) β B β‘ C β β£ B β£ β‘ β£ C β£ ap-prβ B C = ap β£_β£ ap-prβ-is-equiv : (B C : subuniverse) β is-equiv (ap-prβ B C) ap-prβ-is-equiv = embedding-gives-ap-is-equiv β£_β£ prβ-is-embedding - subuniverse-is-a-set : is-set subuniverse + subuniverse-is-a-set : is-set subuniverse subuniverse-is-a-set B C = equiv-to-subsingleton - (ap-prβ B C , ap-prβ-is-equiv B C) + (ap-prβ B C , ap-prβ-is-equiv B C) (powersets-are-sets' ua β£ B β£ β£ C β£) subuniverse-equal-gives-membership-equiv : (B C : subuniverse) - β B β‘ C + β B β‘ C --------------------- - β (β x β x ββ β£ B β£ β x ββ β£ C β£) + β (β x β x ββ β£ B β£ β x ββ β£ C β£) subuniverse-equal-gives-membership-equiv B C Bβ‘C x = - transport (Ξ» - β x ββ β£ - β£) Bβ‘C , transport (Ξ» - β x ββ β£ - β£ ) ( Bβ‘C β»ΒΉ ) + transport (Ξ» - β x ββ β£ - β£) Bβ‘C , transport (Ξ» - β x ββ β£ - β£ ) ( Bβ‘C β»ΒΉ ) membership-equiv-gives-carrier-equal : (B C : subuniverse) - β (β x β x ββ β£ B β£ β x ββ β£ C β£) + β (β x β x ββ β£ B β£ β x ββ β£ C β£) -------------------------------- - β β£ B β£ β‘ β£ C β£ + β β£ B β£ β‘ β£ C β£ membership-equiv-gives-carrier-equal B C Ο = subset-extensionality' ua Ξ± Ξ² where Ξ± : β£ B β£ ββ β£ C β£ - Ξ± x = lr-implication (Ο x) + Ξ± x = lr-implication (Ο x) Ξ² : β£ C β£ ββ β£ B β£ - Ξ² x = rl-implication (Ο x) + Ξ² x = rl-implication (Ο x) membership-equiv-gives-subuniverse-equality : (B C : subuniverse) - β (β x β x ββ β£ B β£ β x ββ β£ C β£) + β (β x β x ββ β£ B β£ β x ββ β£ C β£) ----------------------------- - β B β‘ C + β B β‘ C membership-equiv-gives-subuniverse-equality B C = inverse (ap-prβ B C) (ap-prβ-is-equiv B C) β (membership-equiv-gives-carrier-equal B C) - membership-equiv-is-subsingleton : (B C : subuniverse) β is-subsingleton (β x β x ββ β£ B β£ β x ββ β£ C β£) + membership-equiv-is-subsingleton : (B C : subuniverse) β is-subsingleton (β x β x ββ β£ B β£ β x ββ β£ C β£) membership-equiv-is-subsingleton B C = Ξ -is-subsingleton gfe (Ξ» x β Γ-is-subsingleton @@ -119,32 +119,32 @@ This module can be safely skipped, or even left out of the Agda Universal Algebr (Ξ -is-subsingleton gfe (Ξ» _ β ββ-is-subsingleton β£ B β£ x ))) - subuniverse-equality : (B C : subuniverse) β (B β‘ C) β (β x β (x ββ β£ B β£) β (x ββ β£ C β£)) + subuniverse-equality : (B C : subuniverse) β (B β‘ C) β (β x β (x ββ β£ B β£) β (x ββ β£ C β£)) subuniverse-equality B C = logically-equivalent-subsingletons-are-equivalent _ _ (subuniverse-is-a-set B C) (membership-equiv-is-subsingleton B C) - (subuniverse-equal-gives-membership-equiv B C , membership-equiv-gives-subuniverse-equality B C) + (subuniverse-equal-gives-membership-equiv B C , membership-equiv-gives-subuniverse-equality B C) carrier-equality-gives-membership-equiv : (B C : subuniverse) - β β£ B β£ β‘ β£ C β£ + β β£ B β£ β‘ β£ C β£ ------------------------------- - β (β x β x ββ β£ B β£ β x ββ β£ C β£) + β (β x β x ββ β£ B β£ β x ββ β£ C β£) - carrier-equality-gives-membership-equiv B C refl x = id , id + carrier-equality-gives-membership-equiv B C refl x = id , id --so we have... - carrier-equiv : (B C : subuniverse) β (β x β x ββ β£ B β£ β x ββ β£ C β£) β (β£ B β£ β‘ β£ C β£) + carrier-equiv : (B C : subuniverse) β (β x β x ββ β£ B β£ β x ββ β£ C β£) β (β£ B β£ β‘ β£ C β£) carrier-equiv B C = logically-equivalent-subsingletons-are-equivalent _ _ (membership-equiv-is-subsingleton B C)(powersets-are-sets' ua β£ B β£ β£ C β£) - (membership-equiv-gives-carrier-equal B C , carrier-equality-gives-membership-equiv B C) + (membership-equiv-gives-carrier-equal B C , carrier-equality-gives-membership-equiv B C) -- ...which yields an alternative subuniverse equality lemma. - subuniverse-equality' : (B C : subuniverse) β (B β‘ C) β (β£ B β£ β‘ β£ C β£) + subuniverse-equality' : (B C : subuniverse) β (B β‘ C) β (β£ B β£ β‘ β£ C β£) - subuniverse-equality' B C = (subuniverse-equality B C) β (carrier-equiv B C) + subuniverse-equality' B C = (subuniverse-equality B C) β (carrier-equiv B C)diff --git a/UALib/html/Terms.Basic.md b/UALib/html/Terms.Basic.md index 4c814c79..bd7112ec 100644 --- a/UALib/html/Terms.Basic.md +++ b/UALib/html/Terms.Basic.md @@ -41,7 +41,7 @@ The definition of `Term X` is recursive, indicating that an inductive type could-data Term {π§ : Universe}(X : π§ Μ ) : ov π§ Μ where +data Term {π§ : Universe}(X : π§ Μ ) : ov π§ Μ where generator : X β Term X node : (f : β£ π β£)(π‘ : β₯ π β₯ f β Term X) β Term X @@ -68,8 +68,8 @@ In [Agda][] the term algebra can be defined as simply as one could hope.@@ -35,7 +35,7 @@ Thus the interpretation of a term is defined by induction on the structure of th-π» : {π§ : Universe}(X : π§ Μ ) β Algebra (ov π§) π -π» X = Term X , node +π» : {π§ : Universe}(X : π§ Μ ) β Algebra (ov π§) π +π» X = Term X , node@@ -86,7 +86,7 @@ We now prove this in [Agda][], starting with the fact that every map from `X` to-module _ {π€ π§ : Universe}{X : π§ Μ } where +module _ {π€ π§ : Universe}{X : π§ Μ } where free-lift : (π¨ : Algebra π€ π)(h : X β β£ π¨ β£) β β£ π» X β£ β β£ π¨ β£ @@ -109,7 +109,7 @@ The free lift so defined is a homomorphism by construction. Indeed, here is the lift-hom : (π¨ : Algebra π€ π) β (X β β£ π¨ β£) β hom (π» X) π¨ - lift-hom π¨ h = free-lift π¨ h , Ξ» f a β ap (f Μ π¨) refl + lift-hom π¨ h = free-lift π¨ h , Ξ» f a β ap (f Μ π¨) refl@@ -118,9 +118,9 @@ Finally, we prove that the homomorphism is unique. This requires `funext π₯free-unique : funext π₯ π€ β (π¨ : Algebra π€ π)(g h : hom (π» X) π¨) - β (β x β β£ g β£ (generator x) β‘ β£ h β£ (generator x)) + β (β x β β£ g β£ (generator x) β‘ β£ h β£ (generator x)) ---------------------------------------------------- - β β (t : Term X) β β£ g β£ t β‘ β£ h β£ t + β β (t : Term X) β β£ g β£ t β‘ β£ h β£ t free-unique _ _ _ _ p (generator x) = p x @@ -129,7 +129,7 @@ Finally, we prove that the homomorphism is unique. This requires `funext π₯ (π Μ π¨)(β£ h β£ β π‘) β‘β¨ (β₯ h β₯ π π‘)β»ΒΉ β© β£ h β£ (node π π‘) β where - Ξ± : (π Μ π¨) (β£ g β£ β π‘) β‘ (π Μ π¨) (β£ h β£ β π‘) + Ξ± : (π Μ π¨) (β£ g β£ β π‘) β‘ (π Μ π¨) (β£ h β£ β π‘) Ξ± = ap (π Μ π¨) (fe Ξ» i β free-unique fe π¨ g h p (π‘ i))@@ -148,7 +148,7 @@ If we further assume that each of the mappings from `X` to `β£ π¨ β£` is *su where hββ»ΒΉy = Inv hβ (hE y) - Ξ· : y β‘ β£ lift-hom π¨ hβ β£ (generator hββ»ΒΉy) + Ξ· : y β‘ β£ lift-hom π¨ hβ β£ (generator hββ»ΒΉy) Ξ· = (InvIsInv hβ (hE y))β»ΒΉ Ξ³ : Image β£ lift-hom π¨ hβ β£ β y diff --git a/UALib/html/Terms.Operations.md b/UALib/html/Terms.Operations.md index 68908f47..f3050878 100644 --- a/UALib/html/Terms.Operations.md +++ b/UALib/html/Terms.Operations.md @@ -19,7 +19,7 @@ Here we define *term operations* which are simply terms interpreted in a particu module Terms.Operations {π : Signature π π₯} where -open import Terms.Basic{π = π} renaming (generator to β) public +open import Terms.Basic{π = π} renaming (generator to β) public-module _ {π€ π§ : Universe}{X : π§ Μ } where +module _ {π€ π§ : Universe}{X : π§ Μ } where -- new notation @@ -61,15 +61,15 @@ It turns out that the intepretation of a term is the same as the `free-lift` (mo- free-lift-interp : dfunext π₯ π€ β (π¨ : Algebra π€ π)(Ξ· : X β β£ π¨ β£)(p : Term X) - β (π¨ β¦ p β§) Ξ· β‘ (free-lift π¨ Ξ·) p + free-lift-interp : dfunext π₯ π€ β (π¨ : Algebra π€ π)(Ξ· : X β β£ π¨ β£)(p : Term X) + β (π¨ β¦ p β§) Ξ· β‘ (free-lift π¨ Ξ·) p free-lift-interp _ π¨ Ξ· (β x) = refl free-lift-interp fe π¨ Ξ· (node π π‘) = ap (π Μ π¨) (fe Ξ» i β free-lift-interp fe π¨ Ξ· (π‘ i)) -- old version - free-lift-interp' : dfunext π₯ π€ β (π¨ : Algebra π€ π)(h : X β β£ π¨ β£)(p : Term X) - β (p Μ π¨) h β‘ (free-lift π¨ h) p + free-lift-interp' : dfunext π₯ π€ β (π¨ : Algebra π€ π)(h : X β β£ π¨ β£)(p : Term X) + β (p Μ π¨) h β‘ (free-lift π¨ h) p free-lift-interp' _ π¨ h (β x) = refl free-lift-interp' fe π¨ h (node π π‘) = ap (π Μ π¨) (fe Ξ» i β free-lift-interp' fe π¨ h (π‘ i)) @@ -96,36 +96,36 @@ We claim that for all `p : Term X` there exists `q : Term X` and `π± : X β-term-interp : {π§ : Universe}{X : π§ Μ} (π : β£ π β£){π π‘ : β₯ π β₯ π β Term X} - β π β‘ π‘ β node π π β‘ (π Μ π» X) π‘ +term-interp : {π§ : Universe}{X : π§ Μ} (π : β£ π β£){π π‘ : β₯ π β₯ π β Term X} + β π β‘ π‘ β node π π β‘ (π Μ π» X) π‘ term-interp π {π }{π‘} st = ap (node π) st -module _ {π§ : Universe}{X : π§ Μ}{fe : dfunext π₯ (ov π§)} where +module _ {π§ : Universe}{X : π§ Μ}{fe : dfunext π₯ (ov π§)} where - term-gen : (p : β£ π» X β£) β Ξ£ q κ β£ π» X β£ , p β‘ (π» X β¦ q β§) β - term-gen (β x) = (β x) , refl - term-gen (node π π‘) = node π (Ξ» i β β£ term-gen (π‘ i) β£) , term-interp π (fe Ξ» i β β₯ term-gen (π‘ i) β₯) + term-gen : (p : β£ π» X β£) β Ξ£ q κ β£ π» X β£ , p β‘ (π» X β¦ q β§) β + term-gen (β x) = (β x) , refl + term-gen (node π π‘) = node π (Ξ» i β β£ term-gen (π‘ i) β£) , term-interp π (fe Ξ» i β β₯ term-gen (π‘ i) β₯) - term-gen-agreement : (p : β£ π» X β£) β (π» X β¦ p β§) β β‘ (π» X β¦ β£ term-gen p β£ β§) β + term-gen-agreement : (p : β£ π» X β£) β (π» X β¦ p β§) β β‘ (π» X β¦ β£ term-gen p β£ β§) β term-gen-agreement (β x) = refl term-gen-agreement (node f π‘) = ap (f Μ π» X) (fe Ξ» x β term-gen-agreement (π‘ x)) - term-agreement : (p : β£ π» X β£) β p β‘ (π» X β¦ p β§) β + term-agreement : (p : β£ π» X β£) β p β‘ (π» X β¦ p β§) β term-agreement p = snd (term-gen p) β (term-gen-agreement p)β»ΒΉ -- old version: - term-gen' : (p : β£ π» X β£) β Ξ£ q κ β£ π» X β£ , p β‘ (q Μ π» X) β - term-gen' (β x) = (β x) , refl - term-gen' (node π π‘) = node π (Ξ» i β β£ term-gen' (π‘ i) β£) , term-interp π (fe Ξ» i β β₯ term-gen' (π‘ i) β₯) + term-gen' : (p : β£ π» X β£) β Ξ£ q κ β£ π» X β£ , p β‘ (q Μ π» X) β + term-gen' (β x) = (β x) , refl + term-gen' (node π π‘) = node π (Ξ» i β β£ term-gen' (π‘ i) β£) , term-interp π (fe Ξ» i β β₯ term-gen' (π‘ i) β₯) - term-gen-agreement' : (p : β£ π» X β£) β (p Μ π» X) β β‘ (β£ term-gen' p β£ Μ π» X) β + term-gen-agreement' : (p : β£ π» X β£) β (p Μ π» X) β β‘ (β£ term-gen' p β£ Μ π» X) β term-gen-agreement' (β x) = refl term-gen-agreement' (node f π‘) = ap (f Μ π» X) (fe Ξ» x β term-gen-agreement' (π‘ x)) - term-agreement' : (p : β£ π» X β£) β p β‘ (p Μ π» X) β + term-agreement' : (p : β£ π» X β£) β p β‘ (p Μ π» X) β term-agreement' p = snd (term-gen' p) β (term-gen-agreement' p)β»ΒΉ @@ -137,10 +137,10 @@ We claim that for all `p : Term X` there exists `q : Term X` and `π± : X β-module _ {π€ π¦ π§ : Universe}{X : π§ Μ }{I : π¦ Μ} where +module _ {π€ π¦ π§ : Universe}{X : π§ Μ }{I : π¦ Μ} where - interp-prod : dfunext π₯ (π€ β π¦) β (p : Term X)(π : I β Algebra π€ π)(π : X β β i β β£ π i β£) - β (β¨ π β¦ p β§) π β‘ Ξ» i β (π i β¦ p β§) (Ξ» j β π j i) + interp-prod : dfunext π₯ (π€ β π¦) β (p : Term X)(π : I β Algebra π€ π)(π : X β β i β β£ π i β£) + β (β¨ π β¦ p β§) π β‘ Ξ» i β (π i β¦ p β§) (Ξ» j β π j i) interp-prod _ (β xβ) π π = refl @@ -151,8 +151,8 @@ We claim that for all `p : Term X` there exists `q : Term X` and `π± : X β (Ξ» i β (π Μ π i) (Ξ» x β (π i β¦ π‘ x β§) Ξ» j β π j i)) β -- inferred type: π‘ : X β β£ β¨ π β£ - interp-prod2 : dfunext (π€ β π¦ β π§) (π€ β π¦) β dfunext π₯ (π€ β π¦) β (p : Term X)(π : I β Algebra π€ π) - β β¨ π β¦ p β§ β‘ (Ξ» π‘ β (Ξ» i β (π i β¦ p β§) Ξ» x β π‘ x i)) + interp-prod2 : dfunext (π€ β π¦ β π§) (π€ β π¦) β dfunext π₯ (π€ β π¦) β (p : Term X)(π : I β Algebra π€ π) + β β¨ π β¦ p β§ β‘ (Ξ» π‘ β (Ξ» i β (π i β¦ p β§) Ξ» x β π‘ x i)) interp-prod2 _ _ (β xβ) π = refl @@ -163,13 +163,13 @@ We claim that for all `p : Term X` there exists `q : Term X` and `π± : X β (f Μ β¨ π)(Ξ» s β Ξ» j β (π j β¦ t s β§) (Ξ» β β tup β j)) β‘β¨ refl β© (Ξ» i β (f Μ π i)(Ξ» s β (π i β¦ t s β§) (Ξ» β β tup β i))) β -module _ {π€ π§ : Universe}{X : π§ Μ } where +module _ {π€ π§ : Universe}{X : π§ Μ } where - interp-prod' : {π¦ : Universe} β dfunext π₯ (π€ β π¦) + interp-prod' : {π¦ : Universe} β dfunext π₯ (π€ β π¦) β (p : Term X){I : π¦ Μ} (π : I β Algebra π€ π)(π : X β β i β β£ π i β£) --------------------------------------------------- - β (p Μ (β¨ π)) π β‘ (Ξ» i β (p Μ π i) (Ξ» j β π j i)) + β (p Μ (β¨ π)) π β‘ (Ξ» i β (p Μ π i) (Ξ» j β π j i)) interp-prod' _ (β xβ) π π = refl @@ -180,10 +180,10 @@ We claim that for all `p : Term X` there exists `q : Term X` and `π± : X β (Ξ» i β (π Μ π i) (Ξ» x β (π‘ x Μ π i)(Ξ» j β π j i))) β - interp-prod2' : dfunext (π€ β π§) π€ β dfunext π₯ π€ + interp-prod2' : dfunext (π€ β π§) π€ β dfunext π₯ π€ β (p : Term X){I : π€ Μ }(π : I β Algebra π€ π) ------------------------------------------------------------------ - β (p Μ β¨ π) β‘ Ξ»(π‘ : X β β£ β¨ π β£) β (Ξ» i β (p Μ π i)(Ξ» x β π‘ x i)) + β (p Μ β¨ π) β‘ Ξ»(π‘ : X β β£ β¨ π β£) β (Ξ» i β (p Μ π i)(Ξ» x β π‘ x i)) interp-prod2' _ _ (β xβ) π = refl @@ -205,12 +205,12 @@ We now prove two important facts about term operations. The first of these, whi-module _ {π€ π¦ π§ : Universe}{X : π§ Μ} where +module _ {π€ π¦ π§ : Universe}{X : π§ Μ} where - comm-hom-term : dfunext π₯ π¦ β {π¨ : Algebra π€ π} (π© : Algebra π¦ π) + comm-hom-term : dfunext π₯ π¦ β {π¨ : Algebra π€ π} (π© : Algebra π¦ π) (h : hom π¨ π©) (t : Term X) (a : X β β£ π¨ β£) ----------------------------------------- - β β£ h β£ ((π¨ β¦ t β§) a) β‘ (π© β¦ t β§) (β£ h β£ β a) + β β£ h β£ ((π¨ β¦ t β§) a) β‘ (π© β¦ t β§) (β£ h β£ β a) comm-hom-term _ π© h (β x) a = refl @@ -221,10 +221,10 @@ We now prove two important facts about term operations. The first of these, whi i = β₯ h β₯ π Ξ» r β (π¨ β¦ π‘ r β§) a ii = ap (π Μ π©)(fe (Ξ» i β comm-hom-term fe π© h (π‘ i) a)) - comm-hom-term' : dfunext π₯ π¦ β {π¨ : Algebra π€ π} (π© : Algebra π¦ π) + comm-hom-term' : dfunext π₯ π¦ β {π¨ : Algebra π€ π} (π© : Algebra π¦ π) (h : hom π¨ π©) (t : Term X) (a : X β β£ π¨ β£) ----------------------------------------- - β β£ h β£ ((π¨ β¦ t β§) a) β‘ (π© β¦ t β§) (β£ h β£ β a) + β β£ h β£ ((π¨ β¦ t β§) a) β‘ (π© β¦ t β§) (β£ h β£ β a) comm-hom-term' _ π© h (β x) a = refl @@ -242,7 +242,7 @@ To conclude this module, we prove that every term is compatible with every congr-module _ {π¦ π€ : Universe}{X : π€ Μ} where +module _ {π¦ π€ : Universe}{X : π€ Μ} where open IsCongruence diff --git a/UALib/html/UALib.md b/UALib/html/UALib.md index 0759eb79..f2ca1018 100644 --- a/UALib/html/UALib.md +++ b/UALib/html/UALib.md @@ -43,6 +43,15 @@ of citation. **Author**. [William DeMeo][] **Affiliation**. [Department of Algebra][], [Charles University in Prague][] + ++ +**DEPRECATED** This is the documentation for the old version of the Agda Universal Algebra Library. For the lastest version, please go to: + +[https://ualib.github.io/agda-algebras](https://ualib.github.io/agda-algebras) + +
+ **Abstract**. The [Agda Universal Algebra Library][] ([UALib][]) is a library of types and programs (theorems and proofs) that formalizes the foundations of universal algebra in dependent type theory using the [Agda][] proof assistant language. In the latest version of the library we have defined many new types for representing the important constructs and theorems that comprise part of the foundations of general (universal) algebra and equational logic. These types are implemented in so called "literate" Agda files, with the `.lagda` extension, and they are grouped into modules so that they may be easily imported into other Agda programs. @@ -65,18 +74,18 @@ We hope the library will be useful to mathematicians and computer scientists who-{-# OPTIONS --without-K --exact-split --safe #-} +{-# OPTIONS --without-K --exact-split --safe #-} -module UALib where +module UALib where -open import Preface -open import Overture -open import Relations -open import Algebras -open import Homomorphisms -open import Terms -open import Subalgebras -open import Varieties +open import Preface +open import Overture +open import Relations +open import Algebras +open import Homomorphisms +open import Terms +open import Subalgebras +open import Varietiesdiff --git a/UALib/html/Varieties.EquationalLogic.md b/UALib/html/Varieties.EquationalLogic.md index d9fd33ea..55203d73 100644 --- a/UALib/html/Varieties.EquationalLogic.md +++ b/UALib/html/Varieties.EquationalLogic.md @@ -30,11 +30,11 @@ We also prove some closure and invariance properties of β§. In particular, we {-# OPTIONS --without-K --exact-split --safe #-} open import Algebras.Signatures using (Signature; π; π₯) -open import Universes using (Universe; _Μ) +open import Universes using (Universe; _Μ) -module Varieties.EquationalLogic {π : Signature π π₯}{π§ : Universe}{X : π§ Μ} where +module Varieties.EquationalLogic {π : Signature π π₯}{π§ : Universe}{X : π§ Μ} where -open import Subalgebras.Subalgebras{π = π} hiding (Universe; _Μ) public +open import Subalgebras.Subalgebras{π = π} hiding (Universe; _Μ) public open import MGS-Embeddings using (embeddings-are-lc) public @@ -47,11 +47,11 @@ We define the binary "models" relation β§ using infix syntax so that we may wri-module _ {π€ : Universe} where - _β§_β_ : Algebra π€ π β Term X β Term X β π€ β π§ Μ - π¨ β§ p β q = π¨ β¦ p β§ β‘ π¨ β¦ q β§ +module _ {π€ : Universe} where + _β§_β_ : Algebra π€ π β Term X β Term X β π€ β π§ Μ + π¨ β§ p β q = π¨ β¦ p β§ β‘ π¨ β¦ q β§ - _β§_β_ : Pred(Algebra π€ π)(ov π€) β Term X β Term X β π§ β ov π€ Μ + _β§_β_ : Pred(Algebra π€ π)(ov π€) β Term X β Term X β π§ β ov π€ Μ π¦ β§ p β q = {π¨ : Algebra _ π} β π¦ π¨ β π¨ β§ p β q@@ -68,8 +68,8 @@ Here we define a type `Th` so that, if π¦ denotes a class of algebras, then `T- Th : Pred (Algebra π€ π)(ov π€) β Pred(Term X Γ Term X)(π§ β ov π€) - Th π¦ = Ξ» (p , q) β π¦ β§ p β q + Th : Pred (Algebra π€ π)(ov π€) β Pred(Term X Γ Term X)(π§ β ov π€) + Th π¦ = Ξ» (p , q) β π¦ β§ p β q@@ -77,8 +77,8 @@ If β° denotes a set of identities, then the class of algebras satisfying all id- Mod : Pred(Term X Γ Term X)(π§ β ov π€) β Pred(Algebra π€ π)(ov (π§ β π€)) - Mod β° = Ξ» π¨ β β p q β (p , q) β β° β π¨ β§ p β q + Mod : Pred(Term X Γ Term X)(π§ β ov π€) β Pred(Algebra π€ π)(ov (π§ β π€)) + Mod β° = Ξ» π¨ β β p q β (p , q) β β° β π¨ β§ p β q@@ -92,15 +92,15 @@ The binary relation β§ would be practically useless if it were not an *algebrai-DFunExt : π€Ο -DFunExt = (π€ π₯ : Universe) β dfunext π€ π₯ +DFunExt : π€Ο +DFunExt = (π€ π₯ : Universe) β dfunext π€ π₯ -module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where +module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where β§-I-invar : DFunExt β (π© : Algebra π¦ π)(p q : Term X) β π¨ β§ p β q β π¨ β π© β π© β§ p β q - β§-I-invar fe π© p q Apq (f , g , fβΌg , gβΌf) = (fe (π§ β π¦) π¦) Ξ» x β + β§-I-invar fe π© p q Apq (f , g , fβΌg , gβΌf) = (fe (π§ β π¦) π¦) Ξ» x β (π© β¦ p β§) x β‘β¨ refl β© (π© β¦ p β§) (β£ πΎπΉ π© β£ β x) β‘β¨ ap (π© β¦ p β§) ((fe π§ π¦) Ξ» i β ((fβΌg)(x i))β»ΒΉ)β© (π© β¦ p β§) ((β£ f β£ β β£ g β£) β x) β‘β¨ (comm-hom-term (fe π₯ π¦) π© f p (β£ g β£ β x))β»ΒΉ β© @@ -118,7 +118,7 @@ The β§ relation is also invariant under the algebraic lift and lower operations-module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where +module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where β§-Lift-invar : DFunExt β (p q : Term X) β π¨ β§ p β q β Lift-alg π¨ π¦ β§ p β q β§-Lift-invar fe p q Apq = β§-I-invar fe (Lift-alg π¨ _) p q Apq Lift-β @@ -138,18 +138,18 @@ Identities modeled by an algebra π¨ are also modeled by every subalgebra of-module _ {π€ π¦ : Universe} +module _ {π€ π¦ : Universe} -- (fwxw : dfunext (π¦ β π§) π¦)(fvu : dfunext π₯ π€) where β§-S-invar : DFunExt β {π¨ : Algebra π€ π}(π© : Algebra π¦ π){p q : Term X} β π¨ β§ p β q β π© β€ π¨ β π© β§ p β q - β§-S-invar fe {π¨} π© {p}{q} Apq Bβ€A = (fe (π§ β π¦) π¦) Ξ» b β (embeddings-are-lc β£ h β£ β₯ Bβ€A β₯) (ΞΎ b) + β§-S-invar fe {π¨} π© {p}{q} Apq Bβ€A = (fe (π§ β π¦) π¦) Ξ» b β (embeddings-are-lc β£ h β£ β₯ Bβ€A β₯) (ΞΎ b) where h : hom π© π¨ h = β£ Bβ€A β£ - ΞΎ : β b β β£ h β£ ((π© β¦ p β§) b) β‘ β£ h β£ ((π© β¦ q β§) b) + ΞΎ : β b β β£ h β£ ((π© β¦ p β§) b) β‘ β£ h β£ ((π© β¦ q β§) b) ΞΎ b = β£ h β£((π© β¦ p β§) b) β‘β¨ comm-hom-term (fe π₯ π€) π¨ h p b β© (π¨ β¦ p β§)(β£ h β£ β b) β‘β¨ happly Apq (β£ h β£ β b) β© (π¨ β¦ q β§)(β£ h β£ β b) β‘β¨ (comm-hom-term (fe π₯ π€) π¨ h q b)β»ΒΉ β© @@ -163,7 +163,7 @@ Next, identities modeled by a class of algebras is also modeled by all subalgebr β§-S-class-invar : DFunExt β {π¦ : Pred (Algebra π€ π)(ov π€)}(p q : Term X) β π¦ β§ p β q β (π© : SubalgebraOfClass{π¦} π¦) β β£ π© β£ β§ p β q - β§-S-class-invar fe p q Kpq (π© , π¨ , SA , (ka , BisSA)) = β§-S-invar fe π© {p}{q}((Kpq ka)) (h , hem) + β§-S-class-invar fe p q Kpq (π© , π¨ , SA , (ka , BisSA)) = β§-S-invar fe π© {p}{q}((Kpq ka)) (h , hem) where h : hom π© π¨ h = β-hom π© π¨ (β£ BisSA β£) β£ snd SA β£ @@ -181,15 +181,15 @@ An identity satisfied by all algebras in an indexed collection is also satisfied-module _ {π€ π¦ : Universe}(I : π¦ Μ)(π : I β Algebra π€ π) where +module _ {π€ π¦ : Universe}(I : π¦ Μ)(π : I β Algebra π€ π) where β§-P-invar : DFunExt β {p q : Term X} β (β i β π i β§ p β q) β β¨ π β§ p β q β§-P-invar fe {p}{q} πpq = Ξ³ where - Ξ³ : β¨ π β¦ p β§ β‘ β¨ π β¦ q β§ - Ξ³ = (fe (π§ β π€ β π¦) (π€ β π¦)) Ξ» a β (β¨ π β¦ p β§) a β‘β¨ interp-prod (fe π₯ (π€ β π¦)) p π a β© + Ξ³ : β¨ π β¦ p β§ β‘ β¨ π β¦ q β§ + Ξ³ = (fe (π§ β π€ β π¦) (π€ β π¦)) Ξ» a β (β¨ π β¦ p β§) a β‘β¨ interp-prod (fe π₯ (π€ β π¦)) p π a β© (Ξ» i β (π i β¦ p β§)(Ξ» x β (a x)i)) β‘β¨ (fe π¦ π€) (Ξ» i β cong-app (πpq i) (Ξ» x β (a x) i)) β© - (Ξ» i β (π i β¦ q β§)(Ξ» x β (a x)i)) β‘β¨ (interp-prod (fe π₯ (π€ β π¦)) q π a)β»ΒΉ β© + (Ξ» i β (π i β¦ q β§)(Ξ» x β (a x)i)) β‘β¨ (interp-prod (fe π₯ (π€ β π¦)) q π a)β»ΒΉ β© (β¨ π β¦ q β§) a β@@ -226,9 +226,9 @@ If an algebra π¨ models an identity p β q, then the pair (p , q) belongs to-module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where +module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where - β§-H-invar : DFunExt β {p q : Term X}(Ο : hom (π» X) π¨) β π¨ β§ p β q β β£ Ο β£ p β‘ β£ Ο β£ q + β§-H-invar : DFunExt β {p q : Term X}(Ο : hom (π» X) π¨) β π¨ β§ p β q β β£ Ο β£ p β‘ β£ Ο β£ q β§-H-invar fe {p}{q} Ο Ξ² = β£ Ο β£ p β‘β¨ ap β£ Ο β£ (term-agreement {fe = (fe π₯ (ov π§))} p) β© β£ Ο β£((π» X β¦ p β§) β) β‘β¨ (comm-hom-term (fe π₯ π€) π¨ Ο p β ) β© @@ -249,10 +249,10 @@ More generally, an identity is satisfied by all algebras in a class if and only -- β (the "only if" direction) β§-H-class-invar : DFunExt β {p q : Term X} - β π¦ β§ p β q β β π¨ Ο β π¨ β π¦ β β£ Ο β£ β (π» X β¦ p β§) β‘ β£ Ο β£ β (π» X β¦ q β§) + β π¦ β§ p β q β β π¨ Ο β π¨ β π¦ β β£ Ο β£ β (π» X β¦ p β§) β‘ β£ Ο β£ β (π» X β¦ q β§) β§-H-class-invar fe {p}{q} Ξ± π¨ Ο ka = (fe (ov π§) π€) ΞΎ where - ΞΎ : β(π : X β β£ π» X β£ ) β β£ Ο β£ ((π» X β¦ p β§) π) β‘ β£ Ο β£ ((π» X β¦ q β§) π) + ΞΎ : β(π : X β β£ π» X β£ ) β β£ Ο β£ ((π» X β¦ p β§) π) β‘ β£ Ο β£ ((π» X β¦ q β§) π) ΞΎ π = β£ Ο β£ ((π» X β¦ p β§) π) β‘β¨ comm-hom-term (fe π₯ π€) π¨ Ο p π β© (π¨ β¦ p β§)(β£ Ο β£ β π) β‘β¨ happly (Ξ± ka) (β£ Ο β£ β π) β© (π¨ β¦ q β§)(β£ Ο β£ β π) β‘β¨ (comm-hom-term (fe π₯ π€) π¨ Ο q π)β»ΒΉ β© @@ -261,7 +261,7 @@ More generally, an identity is satisfied by all algebras in a class if and only -- β (the "if" direction) β§-H-class-coinvar : DFunExt β {p q : Term X} - β (β π¨ Ο β π¨ β π¦ β β£ Ο β£ β (π» X β¦ p β§) β‘ β£ Ο β£ β (π» X β¦ q β§)) β π¦ β§ p β q + β (β π¨ Ο β π¨ β π¦ β β£ Ο β£ β (π» X β¦ p β§) β‘ β£ Ο β£ β (π» X β¦ q β§)) β π¦ β§ p β q β§-H-class-coinvar fe {p}{q} Ξ² {π¨} ka = Ξ³ where @@ -269,14 +269,14 @@ More generally, an identity is satisfied by all algebras in a class if and only Ο π = lift-hom π¨ π Ξ³ : π¨ β§ p β q - Ξ³ = (fe (π§ β π€) π€) Ξ» π β (π¨ β¦ p β§)(β£ Ο π β£ β β) β‘β¨(comm-hom-term (fe π₯ π€) π¨ (Ο π) p β)β»ΒΉ β© + Ξ³ = (fe (π§ β π€) π€) Ξ» π β (π¨ β¦ p β§)(β£ Ο π β£ β β) β‘β¨(comm-hom-term (fe π₯ π€) π¨ (Ο π) p β)β»ΒΉ β© (β£ Ο π β£ β (π» X β¦ p β§)) β β‘β¨ cong-app (Ξ² π¨ (Ο π) ka) β β© (β£ Ο π β£ β (π» X β¦ q β§)) β β‘β¨ (comm-hom-term (fe π₯ π€) π¨ (Ο π) q β) β© (π¨ β¦ q β§)(β£ Ο π β£ β β) β - β§-H : DFunExt β {p q : Term X} β π¦ β§ p β q β (β π¨ Ο β π¨ β π¦ β β£ Ο β£ β (π» X β¦ p β§) β‘ β£ Ο β£ β(π» X β¦ q β§)) - β§-H fe {p}{q} = β§-H-class-invar fe {p}{q} , β§-H-class-coinvar fe {p}{q} + β§-H : DFunExt β {p q : Term X} β π¦ β§ p β q β (β π¨ Ο β π¨ β π¦ β β£ Ο β£ β (π» X β¦ p β§) β‘ β£ Ο β£ β(π» X β¦ q β§)) + β§-H fe {p}{q} = β§-H-class-invar fe {p}{q} , β§-H-class-coinvar fe {p}{q}diff --git a/UALib/html/Varieties.FreeAlgebras.md b/UALib/html/Varieties.FreeAlgebras.md index 1200622b..7ed97877 100644 --- a/UALib/html/Varieties.FreeAlgebras.md +++ b/UALib/html/Varieties.FreeAlgebras.md @@ -16,9 +16,9 @@ First we will define the relatively free algebra in a variety, which is the "fre {-# OPTIONS --without-K --exact-split --safe #-} open import Algebras.Signatures using (Signature; π; π₯) -open import MGS-Subsingleton-Theorems using (Universe; _Μ) +open import MGS-Subsingleton-Theorems using (Universe; _Μ) -module Varieties.FreeAlgebras {π : Signature π π₯} {π€ : Universe}{X : π€ Μ} where +module Varieties.FreeAlgebras {π : Signature π π₯} {π€ : Universe}{X : π€ Μ} where open import Varieties.Preservation {π = π}{π€}{π€}{X} public @@ -49,8 +49,8 @@ First, we represent the congruence relation `ΟCon`, modulo which `π» X` yieldΟ : (π¦ : Pred (Algebra π€ π) π) β Pred (β£ π» X β£ Γ β£ π» X β£) π -Ο π¦ (p , q) = β(π¨ : Algebra π€ π)(sA : π¨ β S{π€}{π€} π¦)(h : X β β£ π¨ β£ ) - β (free-lift π¨ h) p β‘ (free-lift π¨ h) q +Ο π¦ (p , q) = β(π¨ : Algebra π€ π)(sA : π¨ β S{π€}{π€} π¦)(h : X β β£ π¨ β£ ) + β (free-lift π¨ h) p β‘ (free-lift π¨ h) q@@ -59,7 +59,7 @@ We convert the predicate Ο into a relation by [currying](https://en.wikipedia.oΟRel : (π¦ : Pred (Algebra π€ π) π) β Rel β£ π» X β£ π -ΟRel π¦ p q = Ο π¦ (p , q) +ΟRel π¦ p q = Ο π¦ (p , q)@@ -70,13 +70,13 @@ To express `ΟRel` as a congruence of the term algebra `π» X`, we must prove t-Οcompatible : (π¦ : Pred (Algebra π€ π) π){fe : dfunext π₯ π€} β compatible (π» X)(ΟRel π¦) +Οcompatible : (π¦ : Pred (Algebra π€ π) π){fe : dfunext π₯ π€} β compatible (π» X)(ΟRel π¦) Οcompatible π¦{fe} π {p} {q} Οpq π¨ sA h = Ξ³ where Ο : hom (π» X) π¨ Ο = lift-hom π¨ h - Ξ³ : β£ Ο β£ ((π Μ π» X) p) β‘ β£ Ο β£ ((π Μ π» X) q) + Ξ³ : β£ Ο β£ ((π Μ π» X) p) β‘ β£ Ο β£ ((π Μ π» X) q) Ξ³ = β£ Ο β£ ((π Μ π» X) p) β‘β¨ β₯ Ο β₯ π p β© (π Μ π¨) (β£ Ο β£ β p) β‘β¨ ap(π Μ π¨)(fe Ξ» x β (Οpq x) π¨ sA h) β© @@ -94,8 +94,8 @@ We have collected all the pieces necessary to express the collection of identiti-ΟCon : (π¦ : Pred (Algebra π€ π) π){fe : dfunext π₯ π€} β Con (π» X) -ΟCon π¦ {fe} = (ΟRel π¦) , mkcon ΟIsEquivalence (Οcompatible π¦ {fe}) +ΟCon : (π¦ : Pred (Algebra π€ π) π){fe : dfunext π₯ π€} β Con (π» X) +ΟCon π¦ {fe} = (ΟRel π¦) , mkcon ΟIsEquivalence (Οcompatible π¦ {fe})@@ -187,18 +187,18 @@ We will need the following facts relating `homβ`, `homπ½`, `and Ο`.- Οlemma0 : β p q β β£ homβ β£ p β‘ β£ homβ β£ q β (p , q) β Ο π¦ - Οlemma0 p q phomβq π¨ sA h = cong-app phomβq (π¨ , sA , h) + Οlemma0 : β p q β β£ homβ β£ p β‘ β£ homβ β£ q β (p , q) β Ο π¦ + Οlemma0 p q phomβq π¨ sA h = cong-app phomβq (π¨ , sA , h) Οlemma0-ap : {π¨ : Algebra π€ π}{h : X β β£ π¨ β£} β π¨ β S{π€}{π€} π¦ β kernel β£ homπ½ β£ β kernel (free-lift π¨ h) - Οlemma0-ap {π¨}{h} skA {p , q} x = Ξ³ where + Οlemma0-ap {π¨}{h} skA {p , q} x = Ξ³ where - Ξ½ : β£ homβ β£ p β‘ β£ homβ β£ q + Ξ½ : β£ homβ β£ p β‘ β£ homβ β£ q Ξ½ = ker-in-con {ov π€}{ov π€}{π» X}{fe π₯ πβΊ}(kercon β {fe π₯ π} homβ) {p}{q} x - Ξ³ : (free-lift π¨ h) p β‘ (free-lift π¨ h) q + Ξ³ : (free-lift π¨ h) p β‘ (free-lift π¨ h) q Ξ³ = ((Οlemma0 p q) Ξ½) π¨ skA h @@ -236,7 +236,7 @@ It turns out that the homomorphism so defined is equivalent to `homπ½`.- homπ½-is-lift-hom : β p β β£ π β£ p β‘ β£ homπ½ β£ p + homπ½-is-lift-hom : β p β β£ π β£ p β‘ β£ homπ½ β£ p homπ½-is-lift-hom (β x) = refl homπ½-is-lift-hom (node π π) = β£ π β£ (node π π) β‘β¨ β₯ π β₯ π π β© @@ -251,7 +251,7 @@ We need a three more lemmas before we are ready to tackle our main goal.Οlemma1 : kernel β£ π β£ β Ο π¦ - Οlemma1 {p , q} πpq π¨ sA h = Ξ³ + Οlemma1 {p , q} πpq π¨ sA h = Ξ³ where f : hom π½ π¨ f = π½-lift-hom π¨ sA h @@ -260,10 +260,10 @@ We need a three more lemmas before we are ready to tackle our main goal. h' = β-hom (π» X) π¨ π f Ο = lift-hom π¨ h - hβ‘Ο : β t β (β£ f β£ β β£ π β£) t β‘ β£ Ο β£ t + hβ‘Ο : β t β (β£ f β£ β β£ π β£) t β‘ β£ Ο β£ t hβ‘Ο t = free-unique (fe π₯ π€) π¨ h' Ο (Ξ» x β refl) t - Ξ³ : β£ Ο β£ p β‘ β£ Ο β£ q + Ξ³ : β£ Ο β£ p β‘ β£ Ο β£ q Ξ³ = β£ Ο β£ p β‘β¨ (hβ‘Ο p)β»ΒΉ β© β£ f β£ ( β£ π β£ p ) β‘β¨ ap β£ f β£ πpq β© β£ f β£ ( β£ π β£ q ) β‘β¨ hβ‘Ο q β© @@ -271,16 +271,16 @@ We need a three more lemmas before we are ready to tackle our main goal. Οlemma2 : kernel β£ homπ½ β£ β Ο π¦ - Οlemma2 {p , q} hyp = Οlemma1 {p , q} Ξ³ + Οlemma2 {p , q} hyp = Οlemma1 {p , q} Ξ³ where - Ξ³ : (free-lift π½ Xβͺπ½) p β‘ (free-lift π½ Xβͺπ½) q + Ξ³ : (free-lift π½ Xβͺπ½) p β‘ (free-lift π½ Xβͺπ½) q Ξ³ = (homπ½-is-lift-hom p) β hyp β (homπ½-is-lift-hom q)β»ΒΉ - Οlemma3 : β p q β (p , q) β Ο π¦ β π¦ β§ p β q + Οlemma3 : β p q β (p , q) β Ο π¦ β π¦ β§ p β q Οlemma3 p q pΟq {π¨} kA = Ξ³ where - Ξ³ : π¨ β¦ p β§ β‘ π¨ β¦ q β§ + Ξ³ : π¨ β¦ p β§ β‘ π¨ β¦ q β§ Ξ³ = fe π€ π€ Ξ» h β (π¨ β¦ p β§) h β‘β¨ free-lift-interp (fe π₯ π€) π¨ h p β© (free-lift π¨ h) p β‘β¨ pΟq π¨ (siso (sbase kA) (β -sym Lift-β )) h β© (free-lift π¨ h) q β‘β¨ (free-lift-interp (fe π₯ π€) π¨ h q)β»ΒΉ β© @@ -292,24 +292,24 @@ With these results in hand, it is now trivial to prove the main theorem of this@@ -42,7 +42,7 @@ First we prove that the closure operator H is compatible with identities that ho H-id1 p q Ξ± (hbase x) = β§-Lift-invar fe p q (Ξ± x) H-id1 p q Ξ± (hlift{π¨} x) = β§-Lift-invar fe p q (H-id1 p q Ξ± x) - H-id1 p q Ξ± (hhimg{π¨}{πͺ} HA((π© , Ο , (Οhom , Οsur)), Bβ C)) = β§-I-invar fe πͺ p q Ξ³ Bβ C + H-id1 p q Ξ± (hhimg{π¨}{πͺ} HA((π© , Ο , (Οhom , Οsur)), Bβ C)) = β§-I-invar fe πͺ p q Ξ³ Bβ C where Ξ² : π¨ β§ p β q Ξ² = (H-id1 p q Ξ±) HA @@ -50,14 +50,14 @@ First we prove that the closure operator H is compatible with identities that ho preim : β π x β β£ π¨ β£ preim π x = Inv Ο (Οsur (π x)) - ΞΆ : β π β Ο β (preim π) β‘ π + ΞΆ : β π β Ο β (preim π) β‘ π ΞΆ π = (fe π§ π€) Ξ» x β InvIsInv Ο (Οsur (π x)) - Ξ³ : π© β¦ p β§ β‘ π© β¦ q β§ + Ξ³ : π© β¦ p β§ β‘ π© β¦ q β§ Ξ³ = (fe πΎπ π€) Ξ» π β (π© β¦ p β§) π β‘β¨ (ap (π© β¦ p β§) (ΞΆ π))β»ΒΉ β© - (π© β¦ p β§)(Ο β(preim π)) β‘β¨(comm-hom-term (fe π₯ π€) π©(Ο , Οhom) p(preim π))β»ΒΉ β© + (π© β¦ p β§)(Ο β(preim π)) β‘β¨(comm-hom-term (fe π₯ π€) π©(Ο , Οhom) p(preim π))β»ΒΉ β© Ο((π¨ β¦ p β§)(preim π)) β‘β¨ ap Ο (happly Ξ² (preim π)) β© - Ο((π¨ β¦ q β§)(preim π)) β‘β¨ comm-hom-term (fe π₯ π€) π© (Ο , Οhom) q (preim π) β© + Ο((π¨ β¦ q β§)(preim π)) β‘β¨ comm-hom-term (fe π₯ π€) π© (Ο , Οhom) q (preim π) β© (π© β¦ q β§)(Ο β(preim π)) β‘β¨ ap (π© β¦ q β§) (ΞΆ π) β© (π© β¦ q β§) π β @@ -86,7 +86,7 @@ The converse of the foregoing result is almost too obvious to bother with. Nonet S-id1 p q Ξ± (slift x) = β§-Lift-invar fe p q ((S-id1 p q Ξ±) x) S-id1 p q Ξ± (ssub{π¨}{π©} sA Bβ€A) = - β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β -refl) + β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β -refl) where --Apply S-β§ to the class π¦ βͺ ο½ π¨ ο½ Ξ² : π¨ β§ p β q Ξ² = S-id1 p q Ξ± sA @@ -99,7 +99,7 @@ The converse of the foregoing result is almost too obvious to bother with. Nonet Ξ³ {π©} (injβ y) = Apq y S-id1 p q Ξ± (ssubw{π¨}{π©} sA Bβ€A) = - β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β -refl) + β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β -refl) where --Apply S-β§ to the class π¦ βͺ ο½ π¨ ο½ Ξ² : π¨ β§ p β q Ξ² = S-id1 p q Ξ± sA @@ -138,12 +138,12 @@ Again, the obvious converse is barely worth the bits needed to formalize it. P-id1 p q Ξ± (produ{I}{π} x) = β§-P-lift-invar I π fe {p}{q} IH where - IH : β i β (Lift-alg (π i) π€) β¦ p β§ β‘ (Lift-alg (π i) π€) β¦ q β§ + IH : β i β (Lift-alg (π i) π€) β¦ p β§ β‘ (Lift-alg (π i) π€) β¦ q β§ IH i = β§-Lift-invar fe p q ((P-id1 p q Ξ±) (x i)) P-id1 p q Ξ± (prodw{I}{π} x) = β§-P-lift-invar I π fe {p}{q}IH where - IH : β i β Lift-alg (π i) π€ β¦ p β§ β‘ Lift-alg (π i) π€ β¦ q β§ + IH : β i β Lift-alg (π i) π€ β¦ p β§ β‘ Lift-alg (π i) π€ β¦ q β§ IH i = β§-Lift-invar fe p q ((P-id1 p q Ξ±) (x i)) P-id1 p q Ξ± (pisou{π¨}{π©} x xβ) = β§-I-invar fe π© p q (P-id1 p q Ξ± x) xβ @@ -172,7 +172,7 @@ Finally, we prove the analogous preservation lemmas for the closure operator `V` V-id1 p q Ξ± (vlift{π¨} x) = β§-Lift-invar fe p q ((V-id1 p q Ξ±) x) V-id1 p q Ξ± (vliftw{π¨} x) = β§-Lift-invar fe p q ((V-id1 p q Ξ±) x) - V-id1 p q Ξ± (vhimg{π¨}{πͺ}VA((π© , Ο , (Οh , ΟE)) , Bβ C)) = β§-I-invar fe πͺ p q Ξ³ Bβ C + V-id1 p q Ξ± (vhimg{π¨}{πͺ}VA((π© , Ο , (Οh , ΟE)) , Bβ C)) = β§-I-invar fe πͺ p q Ξ³ Bβ C where IH : π¨ β§ p β q IH = V-id1 p q Ξ± VA @@ -180,18 +180,18 @@ Finally, we prove the analogous preservation lemmas for the closure operator `V` preim : β π (x : X) β β£ π¨ β£ preim π x = (Inv Ο (ΟE (π x))) - ΞΆ : β π β Ο β (preim π) β‘ π + ΞΆ : β π β Ο β (preim π) β‘ π ΞΆ π = (fe π§ π€) Ξ» x β InvIsInv Ο (ΟE (π x)) - Ξ³ : (π© β¦ p β§) β‘ (π© β¦ q β§) + Ξ³ : (π© β¦ p β§) β‘ (π© β¦ q β§) Ξ³ = (fe πΎπ π€) Ξ» π β (π© β¦ p β§) π β‘β¨ (ap (π© β¦ p β§) (ΞΆ π))β»ΒΉ β© - (π© β¦ p β§)(Ο β(preim π)) β‘β¨(comm-hom-term (fe π₯ π€) π©(Ο , Οh) p(preim π))β»ΒΉ β© + (π© β¦ p β§)(Ο β(preim π)) β‘β¨(comm-hom-term (fe π₯ π€) π©(Ο , Οh) p(preim π))β»ΒΉ β© Ο ((π¨ β¦ p β§)(preim π)) β‘β¨ ap Ο (happly IH (preim π)) β© - Ο ((π¨ β¦ q β§)(preim π)) β‘β¨ comm-hom-term (fe π₯ π€) π© (Ο , Οh) q (preim π) β© + Ο ((π¨ β¦ q β§)(preim π)) β‘β¨ comm-hom-term (fe π₯ π€) π© (Ο , Οh) q (preim π) β© (π© β¦ q β§)(Ο β(preim π)) β‘β¨ ap (π© β¦ q β§) (ΞΆ π) β© (π© β¦ q β§) π β - V-id1 p q Ξ± (vssub {π¨}{π©} VA Bβ€A) = β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β -refl) + V-id1 p q Ξ± (vssub {π¨}{π©} VA Bβ€A) = β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β -refl) where IH : π¨ β§ p β q IH = V-id1 p q Ξ± VA @@ -204,7 +204,7 @@ Finally, we prove the analogous preservation lemmas for the closure operator `V` Ξ³ {π©} (injβ y) = Asinglepq y V-id1 p q Ξ± ( vssubw {π¨}{π©} VA Bβ€A ) = - β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β -refl) + β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β -refl) where IH : π¨ β§ p β q IH = V-id1 p q Ξ± VA @@ -227,13 +227,13 @@ Finally, we prove the analogous preservation lemmas for the closure operator `V` -- open id1 {π€}{X}{(fe π€ π€) = fe π€ π€}{(fe π₯ π€) = fe π₯ π€} - V-id1' : (p q : Term X) β π¦ β§ p β q β V{π€}{ov π€ βΊ} π¦ β§ p β q + V-id1' : (p q : Term X) β π¦ β§ p β q β V{π€}{ov π€ βΊ} π¦ β§ p β q V-id1' p q Ξ± (vbase x) = β§-Lift-invar fe p q (Ξ± x) V-id1' p q Ξ± (vlift{π¨} x) = β§-Lift-invar fe p q ((V-id1 p q Ξ±) x) V-id1' p q Ξ± (vliftw{π¨} x) = β§-Lift-invar fe p q ((V-id1' p q Ξ±) x) - V-id1' p q Ξ± (vhimg{π¨}{πͺ} VA ((π© , Ο , (Οh , ΟE)) , Bβ C)) = + V-id1' p q Ξ± (vhimg{π¨}{πͺ} VA ((π© , Ο , (Οh , ΟE)) , Bβ C)) = β§-I-invar fe πͺ p q Ξ³ Bβ C where IH : π¨ β§ p β q @@ -242,14 +242,14 @@ Finally, we prove the analogous preservation lemmas for the closure operator `V` preim : β π x β β£ π¨ β£ preim π x = (Inv Ο (ΟE (π x))) - ΞΆ : β π β Ο β (preim π) β‘ π + ΞΆ : β π β Ο β (preim π) β‘ π ΞΆ π = (fe π§ πβΊ) Ξ» x β InvIsInv Ο (ΟE (π x)) - Ξ³ : π© β¦ p β§ β‘ π© β¦ q β§ - Ξ³ = (fe (π§ β πβΊ) πβΊ) Ξ» π β (π© β¦ p β§) π β‘β¨ (ap (π© β¦ p β§) (ΞΆ π))β»ΒΉ β© - (π© β¦ p β§) (Ο β (preim π)) β‘β¨(comm-hom-term (fe π₯ πβΊ) π© (Ο , Οh) p (preim π))β»ΒΉ β© + Ξ³ : π© β¦ p β§ β‘ π© β¦ q β§ + Ξ³ = (fe (π§ β πβΊ) πβΊ) Ξ» π β (π© β¦ p β§) π β‘β¨ (ap (π© β¦ p β§) (ΞΆ π))β»ΒΉ β© + (π© β¦ p β§) (Ο β (preim π)) β‘β¨(comm-hom-term (fe π₯ πβΊ) π© (Ο , Οh) p (preim π))β»ΒΉ β© Ο((π¨ β¦ p β§)(preim π)) β‘β¨ ap Ο (happly IH (preim π))β© - Ο((π¨ β¦ q β§)(preim π)) β‘β¨ comm-hom-term (fe π₯ πβΊ) π© (Ο , Οh) q (preim π)β© + Ο((π¨ β¦ q β§)(preim π)) β‘β¨ comm-hom-term (fe π₯ πβΊ) π© (Ο , Οh) q (preim π)β© (π© β¦ q β§)(Ο β (preim π)) β‘β¨ ap (π© β¦ q β§) (ΞΆ π)β© (π© β¦ q β§) π β @@ -269,19 +269,19 @@ From `V-id1` it follows that if π¦ is a class of structures, then the set of i- class-models-kernel : β p q β (p , q) β kernel β£ homπ½ β£ β π¦ β§ p β q + class-models-kernel : β p q β (p , q) β kernel β£ homπ½ β£ β π¦ β§ p β q class-models-kernel p q hyp = Οlemma3 p q (Οlemma2 hyp)- ππ¦ : Pred (Algebra πβΊ π) (πβΊ βΊ) + ππ¦ : Pred (Algebra πβΊ π) (πβΊ βΊ) ππ¦ = V{π€}{πβΊ} π¦ kernel-in-theory : kernel β£ homπ½ β£ β Th (V π¦) - kernel-in-theory {p , q} pKq = (class-ids-β {fe = fe} p q (class-models-kernel p q pKq)) + kernel-in-theory {p , q} pKq = (class-ids-β {fe = fe} p q (class-models-kernel p q pKq)) _β _ : π€ Μ β Algebra πβΊ π β πβΊ Μ X β π¨ = Ξ£ h κ (X β β£ π¨ β£) , Epic h π½-ModTh-epi : (π¨ : Algebra πβΊ π) β (X β π¨) β π¨ β Mod (Th ππ¦) β epi π½ π¨ - π½-ModTh-epi π¨ (Ξ· , Ξ·E) AinMTV = Ξ³ + π½-ModTh-epi π¨ (Ξ· , Ξ·E) AinMTV = Ξ³ where Ο : hom (π» X) π¨ Ο = lift-hom π¨ Ξ· @@ -317,11 +317,11 @@ With these results in hand, it is now trivial to prove the main theorem of this ΟE : Epic β£ Ο β£ ΟE = lift-of-epi-is-epi Ξ·E - pqlem2 : β p q β (p , q) β kernel β£ homπ½ β£ β π¨ β§ p β q + pqlem2 : β p q β (p , q) β kernel β£ homπ½ β£ β π¨ β§ p β q pqlem2 p q hyp = AinMTV p q (kernel-in-theory hyp) kerincl : kernel β£ homπ½ β£ β kernel β£ Ο β£ - kerincl {p , q} x = β£ Ο β£ p β‘β¨ (free-lift-interp (fe π₯ πβΊ) π¨ Ξ· p)β»ΒΉ β© + kerincl {p , q} x = β£ Ο β£ p β‘β¨ (free-lift-interp (fe π₯ πβΊ) π¨ Ξ· p)β»ΒΉ β© (π¨ β¦ p β§) Ξ· β‘β¨ happly (pqlem2 p q x) Ξ· β© (π¨ β¦ q β§) Ξ· β‘β¨ free-lift-interp (fe π₯ πβΊ) π¨ Ξ· q β© β£ Ο β£ q β @@ -345,7 +345,7 @@ Finally we come to one of the main theorems of this module; it asserts that ever (pe : pred-ext (ov π€)(ov π€)) -- truncation assumptions: - (Cset : is-set β£ β β£) + (Cset : is-set β£ β β£) (Keruip : blk-uip (Term X) β£ kercon β {fe π₯ π} homβ β£) where @@ -372,10 +372,10 @@ With this result in hand, along with what we proved earlier---namely, `PS(π¦) open Vlift {π€}{fe π π€}{fe πβΊ πβΊ}{fe π π}{π¦} - π½βSP : hfunext (ov π€)(ov π€) β π½ β (S{π}{πβΊ} (P{π€}{π} π¦)) + π½βSP : hfunext (ov π€)(ov π€) β π½ β (S{π}{πβΊ} (P{π€}{π} π¦)) π½βSP hfe = ssub (class-prod-s-β-sp hfe) π½β€β - π½βπ : hfunext (ov π€)(ov π€) β π½ β V π¦ + π½βπ : hfunext (ov π€)(ov π€) β π½ β V π¦ π½βπ hfe = SPβV' (π½βSP hfe)@@ -386,12 +386,12 @@ Now that we have all of the necessary ingredients, it is all but trivial to comb- Birkhoff : hfunext (ov π€)(ov π€) β (β π¨ β X β π¨) β Mod (Th (V π¦)) β V π¦ + Birkhoff : hfunext (ov π€)(ov π€) β (β π¨ β X β π¨) β Mod (Th (V π¦)) β V π¦ Birkhoff hfe π {π¨} Ξ± = Ξ³ where Ξ³ : π¨ β (V π¦) - Ξ³ = vhimg (π½βπ hfe) ((π¨ , π½-ModTh-epi π¨ (π π¨) Ξ± ) , β -refl) + Ξ³ = vhimg (π½βπ hfe) ((π¨ , π½-ModTh-epi π¨ (π π¨) Ξ± ) , β -refl)diff --git a/UALib/html/Varieties.Preservation.md b/UALib/html/Varieties.Preservation.md index 4b033918..958980fc 100644 --- a/UALib/html/Varieties.Preservation.md +++ b/UALib/html/Varieties.Preservation.md @@ -15,16 +15,16 @@ This section presents the [Varieties.Preservation][] module of the [Agda Univers {-# OPTIONS --without-K --exact-split --safe #-} open import Algebras.Signatures using (Signature; π; π₯) -open import Universes using (Universe; _Μ) +open import Universes using (Universe; _Μ) -module Varieties.Preservation {π : Signature π π₯} {π€ π§ : Universe}{X : π§ Μ} where +module Varieties.Preservation {π : Signature π π₯} {π€ π§ : Universe}{X : π§ Μ} where open import Varieties.Varieties {π = π}{π§}{X} public -π πβΊ πΎπ : Universe +π πβΊ πΎπ : Universe π = ov π€ -πβΊ = (ov π€) βΊ -- (this will be the level of the relatively free algebra) -πΎπ = π€ β π§ +πβΊ = (ov π€) βΊ -- (this will be the level of the relatively free algebra) +πΎπ = π€ β π§- π± : Pred (Algebra (ov π€ βΊ) π) (ov π€ βΊ βΊ) - π± = V{π€}{ov π€ βΊ} π¦ + π± : Pred (Algebra (ov π€ βΊ) π) (ov π€ βΊ βΊ) + π± = V{π€}{ov π€ βΊ} π¦ - class-ids-β : (p q : β£ π» X β£) β π¦ β§ p β q β (p , q) β Th π± + class-ids-β : (p q : β£ π» X β£) β π¦ β§ p β q β (p , q) β Th π± class-ids-β p q pKq VCloA = V-id1' p q pKq VCloA - class-ids-β : (p q : β£ π» X β£) β (p , q) β Th π± β π¦ β§ p β q + class-ids-β : (p q : β£ π» X β£) β (p , q) β Th π± β π¦ β§ p β q class-ids-β p q Thpq {π¨} KA = β§-lower-invar fe p q (Thpq (vbase KA)) - class-identities : (p q : β£ π» X β£) β π¦ β§ p β q β ((p , q) β Th π±) - class-identities p q = class-ids-β p q , class-ids-β p q + class-identities : (p q : β£ π» X β£) β π¦ β§ p β q β ((p , q) β Th π±) + class-identities p q = class-ids-β p q , class-ids-β p q@@ -290,7 +290,7 @@ Once again, and for the last time, completeness dictates that we formalize the c-module _ {π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where +module _ {π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where V-id2 : DFunExt β (p q : Term X) β (V{π€}{π¦} π¦ β§ p β q) β (π¦ β§ p β q) V-id2 fe p q Vpq {π¨} KA = β§-lower-invar fe p q (Vpq (vbase KA)) diff --git a/UALib/html/Varieties.Varieties.md b/UALib/html/Varieties.Varieties.md index fbb85cda..caf641a8 100644 --- a/UALib/html/Varieties.Varieties.md +++ b/UALib/html/Varieties.Varieties.md @@ -14,9 +14,9 @@ This section presents the [Varieties.Varieties][] module of the [Agda Universal {-# OPTIONS --without-K --exact-split --safe #-} open import Algebras.Signatures using (Signature; π; π₯) -open import Universes using (Universe; _Μ) +open import Universes using (Universe; _Μ) -module Varieties.Varieties {π : Signature π π₯}{π§ : Universe}{X : π§ Μ} where +module Varieties.Varieties {π : Signature π π₯}{π§ : Universe}{X : π§ Μ} where open import Varieties.EquationalLogic {π = π}{π§}{X} public @@ -44,7 +44,7 @@ We define the inductive type `H` to represent classes of algebras that include a-data H {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred (Algebra (π€ β π¦) π)(ov(π€ β π¦)) +data H {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred (Algebra (π€ β π¦) π)(ov(π€ β π¦)) where hbase : {π¨ : Algebra π€ π} β π¨ β π¦ β Lift-alg π¨ π¦ β H π¦ hlift : {π¨ : Algebra π€ π} β π¨ β H{π€}{π€} π¦ β Lift-alg π¨ π¦ β H π¦ @@ -61,7 +61,7 @@ The most useful inductive type that we have found for representing the semantic-data S {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred(Algebra(π€ β π¦)π)(ov(π€ β π¦)) +data S {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred(Algebra(π€ β π¦)π)(ov(π€ β π¦)) where sbase : {π¨ : Algebra π€ π} β π¨ β π¦ β Lift-alg π¨ π¦ β S π¦ slift : {π¨ : Algebra π€ π} β π¨ β S{π€}{π€} π¦ β Lift-alg π¨ π¦ β S π¦ @@ -79,11 +79,11 @@ The most useful inductive type that we have found for representing the semantic-data P {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred(Algebra(π€ β π¦)π)(ov(π€ β π¦)) +data P {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred(Algebra(π€ β π¦)π)(ov(π€ β π¦)) where pbase : {π¨ : Algebra π€ π} β π¨ β π¦ β Lift-alg π¨ π¦ β P π¦ pliftu : {π¨ : Algebra π€ π} β π¨ β P{π€}{π€} π¦ β Lift-alg π¨ π¦ β P π¦ - pliftw : {π¨ : Algebra (π€ β π¦) π} β π¨ β P{π€}{π¦} π¦ β Lift-alg π¨ (π€ β π¦) β P π¦ + pliftw : {π¨ : Algebra (π€ β π¦) π} β π¨ β P{π€}{π¦} π¦ β Lift-alg π¨ (π€ β π¦) β P π¦ produ : {I : π¦ Μ }{π : I β Algebra π€ π} β (β i β (π i) β P{π€}{π€} π¦) β β¨ π β P π¦ prodw : {I : π¦ Μ }{π : I β Algebra _ π} β (β i β (π i) β P{π€}{π¦} π¦) β β¨ π β P π¦ pisou : {π¨ : Algebra π€ π}{π© : Algebra _ π} β π¨ β P{π€}{π€} π¦ β π¨ β π© β π© β P π¦ @@ -101,11 +101,11 @@ We now define `V` as an inductive type.-data V {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred(Algebra(π€ β π¦)π)(ov(π€ β π¦)) +data V {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred(Algebra(π€ β π¦)π)(ov(π€ β π¦)) where vbase : {π¨ : Algebra π€ π} β π¨ β π¦ β Lift-alg π¨ π¦ β V π¦ vlift : {π¨ : Algebra π€ π} β π¨ β V{π€}{π€} π¦ β Lift-alg π¨ π¦ β V π¦ - vliftw : {π¨ : Algebra _ π} β π¨ β V{π€}{π¦} π¦ β Lift-alg π¨ (π€ β π¦) β V π¦ + vliftw : {π¨ : Algebra _ π} β π¨ β V{π€}{π¦} π¦ β Lift-alg π¨ (π€ β π¦) β V π¦ vhimg : {π¨ π© : Algebra _ π} β π¨ β V{π€}{π¦} π¦ β π© is-hom-image-of π¨ β π© β V π¦ vssub : {π¨ : Algebra π€ π}{π© : Algebra _ π} β π¨ β V{π€}{π€} π¦ β π© β€ π¨ β π© β V π¦ vssubw : {π¨ π© : Algebra _ π} β π¨ β V{π€}{π¦} π¦ β π© β€ π¨ β π© β V π¦ @@ -122,10 +122,10 @@ With the closure operator V representing closure under HSP, we represent formall-is-variety : {π€ : Universe}(π± : Pred (Algebra π€ π)(ov π€)) β ov π€ Μ +is-variety : {π€ : Universe}(π± : Pred (Algebra π€ π)(ov π€)) β ov π€ Μ is-variety{π€} π± = V{π€}{π€} π± β π± -variety : (π€ : Universe) β (ov π€)βΊ Μ +variety : (π€ : Universe) β (ov π€)βΊ Μ variety π€ = Ξ£ π± κ (Pred (Algebra π€ π)(ov π€)) , is-variety π±@@ -140,7 +140,7 @@ First, `P` is a closure operator. This is proved by checking that `P` is *monot-P-mono : {π€ π¦ : Universe}{π¦ π¦' : Pred(Algebra π€ π)(ov π€)} +P-mono : {π€ π¦ : Universe}{π¦ π¦' : Pred(Algebra π€ π)(ov π€)} β π¦ β π¦' β P{π€}{π¦} π¦ β P{π€}{π¦} π¦' P-mono kk' (pbase x) = pbase (kk' x) @@ -152,14 +152,14 @@ First, `P` is a closure operator. This is proved by checking that `P` is *monot P-mono kk' (pisow x xβ) = pisow (P-mono kk' x) xβ -P-expa : {π€ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} β π¦ β P{π€}{π€} π¦ +P-expa : {π€ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} β π¦ β P{π€}{π€} π¦ P-expa{π€}{π¦} {π¨} KA = pisou{π¨ = (Lift-alg π¨ π€)}{π© = π¨} (pbase KA) (β -sym Lift-β ) -module _ {π€ π¦ : Universe} where +module _ {π€ π¦ : Universe} where P-idemp : {π¦ : Pred (Algebra π€ π)(ov π€)} - β P{π€ β π¦}{π€ β π¦} (P{π€}{π€ β π¦} π¦) β P{π€}{π€ β π¦} π¦ + β P{π€ β π¦}{π€ β π¦} (P{π€}{π€ β π¦} π¦) β P{π€}{π€ β π¦} π¦ P-idemp (pbase x) = pliftw x P-idemp (pliftu x) = pliftw (P-idemp x) @@ -175,7 +175,7 @@ Similarly, S is a closure operator. The facts that S is idempotent and expansiv-S-mono : {π€ π¦ : Universe}{π¦ π¦' : Pred (Algebra π€ π)(ov π€)} +S-mono : {π€ π¦ : Universe}{π¦ π¦' : Pred (Algebra π€ π)(ov π€)} β π¦ β π¦' β S{π€}{π¦} π¦ β S{π€}{π¦} π¦' S-mono kk' (sbase x) = sbase (kk' x) @@ -190,11 +190,11 @@ We sometimes want to go back and forth between our two representations of subalg-module _ {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where +module _ {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where - subalgebraβS : {π© : Algebra (π€ β π¦) π} β π© IsSubalgebraOfClass π¦ β π© β S{π€}{π¦} π¦ + subalgebraβS : {π© : Algebra (π€ β π¦) π} β π© IsSubalgebraOfClass π¦ β π© β S{π€}{π¦} π¦ - subalgebraβS {π©} (π¨ , ((πͺ , Cβ€A) , KA , Bβ C)) = ssub sA Bβ€A + subalgebraβS {π©} (π¨ , ((πͺ , Cβ€A) , KA , Bβ C)) = ssub sA Bβ€A where Bβ€A : π© β€ π¨ Bβ€A = β€-iso π¨ Bβ C Cβ€A @@ -206,12 +206,12 @@ We sometimes want to go back and forth between our two representations of subalg sA = siso slAu (β -sym Lift-β ) -module _ {π€ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where +module _ {π€ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where Sβsubalgebra : {π© : Algebra π€ π} β π© β S{π€}{π€} π¦ β π© IsSubalgebraOfClass π¦ - Sβsubalgebra (sbase{π©} x) = π© , (π© , β€-refl) , x , (β -sym Lift-β ) - Sβsubalgebra (slift{π©} x) = β£ BS β£ , SA , β£ snd β₯ BS β₯ β£ , β -trans (β -sym Lift-β ) Bβ SA + Sβsubalgebra (sbase{π©} x) = π© , (π© , β€-refl) , x , (β -sym Lift-β ) + Sβsubalgebra (slift{π©} x) = β£ BS β£ , SA , β£ snd β₯ BS β₯ β£ , β -trans (β -sym Lift-β ) Bβ SA where BS : π© IsSubalgebraOfClass π¦ BS = Sβsubalgebra x @@ -220,7 +220,7 @@ We sometimes want to go back and forth between our two representations of subalg Bβ SA : π© β β£ SA β£ Bβ SA = β₯ snd β₯ BS β₯ β₯ - Sβsubalgebra {π©} (ssub{π¨} sA Bβ€A) = β£ AS β£ , (π© , Bβ€AS) , β£ snd β₯ AS β₯ β£ , β -refl + Sβsubalgebra {π©} (ssub{π¨} sA Bβ€A) = β£ AS β£ , (π© , Bβ€AS) , β£ snd β₯ AS β₯ β£ , β -refl where AS : π¨ IsSubalgebraOfClass π¦ AS = Sβsubalgebra sA @@ -231,7 +231,7 @@ We sometimes want to go back and forth between our two representations of subalg Bβ€AS : π© β€ β£ AS β£ Bβ€AS = β€-trans β£ AS β£ Bβ€SA β₯ SA β₯ - Sβsubalgebra {π©} (ssubw{π¨} sA Bβ€A) = β£ AS β£ , (π© , Bβ€AS) , β£ snd β₯ AS β₯ β£ , β -refl + Sβsubalgebra {π©} (ssubw{π¨} sA Bβ€A) = β£ AS β£ , (π© , Bβ€AS) , β£ snd β₯ AS β₯ β£ , β -refl where AS : π¨ IsSubalgebraOfClass π¦ AS = Sβsubalgebra sA @@ -242,7 +242,7 @@ We sometimes want to go back and forth between our two representations of subalg Bβ€AS : π© β€ β£ AS β£ Bβ€AS = β€-trans β£ AS β£ Bβ€SA β₯ SA β₯ - Sβsubalgebra {π©} (siso{π¨} sA Aβ B) = β£ AS β£ , SA , β£ snd β₯ AS β₯ β£ , (β -trans (β -sym Aβ B) Aβ SA) + Sβsubalgebra {π©} (siso{π¨} sA Aβ B) = β£ AS β£ , SA , β£ snd β₯ AS β₯ β£ , (β -trans (β -sym Aβ B) Aβ SA) where AS : π¨ IsSubalgebraOfClass π¦ AS = Sβsubalgebra sA @@ -256,17 +256,17 @@ We sometimes want to go back and forth between our two representations of subalg Next we observe that lifting to a higher universe does not break the property of being a subalgebra of an algebra of a class. In other words, if we lift a subalgebra of an algebra in a class, the result is still a subalgebra of an algebra in the class.-module _ {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where +module _ {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where Lift-alg-subP : {π© : Algebra π€ π} β π© IsSubalgebraOfClass (P{π€}{π€} π¦) ------------------------------------------------- β (Lift-alg π© π¦) IsSubalgebraOfClass (P{π€}{π¦} π¦) - Lift-alg-subP {π©}(π¨ , (πͺ , Cβ€A) , pA , Bβ C ) = - lA , (lC , lCβ€lA) , plA , (Lift-alg-iso Bβ C) + Lift-alg-subP {π©}(π¨ , (πͺ , Cβ€A) , pA , Bβ C ) = + lA , (lC , lCβ€lA) , plA , (Lift-alg-iso Bβ C) where - lA lC : Algebra (π€ β π¦) π + lA lC : Algebra (π€ β π¦) π lA = Lift-alg π¨ π¦ lC = Lift-alg πͺ π¦ @@ -281,16 +281,16 @@ The next lemma would be too obvious to care about were it not for the fact that-SβSP : {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} - β S{π€}{π¦} π¦ β S{π€ β π¦}{π€ β π¦} (P{π€}{π¦} π¦) +SβSP : {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} + β S{π€}{π¦} π¦ β S{π€ β π¦}{π€ β π¦} (P{π€}{π¦} π¦) SβSP {π€}{π¦}{π¦}{.(Lift-alg π¨ π¦)}(sbase{π¨} x) = siso spllA(β -sym Lift-β ) where - llA : Algebra (π€ β π¦) π - llA = Lift-alg (Lift-alg π¨ π¦) (π€ β π¦) + llA : Algebra (π€ β π¦) π + llA = Lift-alg (Lift-alg π¨ π¦) (π€ β π¦) spllA : llA β S (P π¦) - spllA = sbase{π€ β π¦}{π€ β π¦} (pbase x) + spllA = sbase{π€ β π¦}{π€ β π¦} (pbase x) SβSP {π€}{π¦}{π¦} {.(Lift-alg π¨ π¦)} (slift{π¨} x) = subalgebraβS lAsc where @@ -306,7 +306,7 @@ The next lemma would be too obvious to care about were it not for the fact that SβSP {π€}{π¦}{π¦}{π©}(ssub{π¨} sA Bβ€A) = ssub (subalgebraβS lAsc)( β€-Lift π¨ Bβ€A ) where - lA : Algebra (π€ β π¦) π + lA : Algebra (π€ β π¦) π lA = Lift-alg π¨ π¦ splAu : π¨ β S (P π¦) @@ -320,16 +320,16 @@ The next lemma would be too obvious to care about were it not for the fact that SβSP (ssubw{π¨} sA Bβ€A) = ssubw (SβSP sA) Bβ€A -SβSP {π€}{π¦}{π¦}{π©}(siso{π¨} sA Aβ B) = siso{π€ β π¦}{π€ β π¦} lAsp lAβ B +SβSP {π€}{π¦}{π¦}{π©}(siso{π¨} sA Aβ B) = siso{π€ β π¦}{π€ β π¦} lAsp lAβ B where - lA : Algebra (π€ β π¦) π + lA : Algebra (π€ β π¦) π lA = Lift-alg π¨ π¦ lAsc : lA IsSubalgebraOfClass (P π¦) lAsc = Lift-alg-subP (Sβsubalgebra{π€}{P{π€}{π€} π¦}{π¨} (SβSP sA)) lAsp : lA β S(P π¦) - lAsp = subalgebraβS{π€ β π¦}{π€ β π¦}{P{π€}{π¦} π¦}{lA} lAsc + lAsp = subalgebraβS{π€ β π¦}{π€ β π¦}{P{π€}{π¦} π¦}{lA} lAsc lAβ B : lA β π© lAβ B = β -trans (β -sym Lift-β ) Aβ B @@ -344,12 +344,12 @@ We need to formalize one more lemma before arriving the main objective of this s module _ {π¦ : Pred(Algebra π€ π)(ov π€)} where - lemPSβSP : hfunext π¦ π€ β dfunext π¦ π€ β {I : π¦ Μ}{β¬ : I β Algebra π€ π} + lemPSβSP : hfunext π¦ π€ β dfunext π¦ π€ β {I : π¦ Μ}{β¬ : I β Algebra π€ π} β (β i β (β¬ i) IsSubalgebraOfClass π¦) ------------------------------------- β β¨ β¬ IsSubalgebraOfClass (P{π€}{π¦} π¦) - lemPSβSP hfeπ¦π€ feπ¦π€ {I}{β¬} Bβ€K = β¨ π , (β¨ SA , β¨ SAβ€β¨ π) , ΞΎ , (β¨ β {feππ€ = feπ¦π€}{feππ¦ = feπ¦π€} Bβ SA) + lemPSβSP hfeπ¦π€ feπ¦π€ {I}{β¬} Bβ€K = β¨ π , (β¨ SA , β¨ SAβ€β¨ π) , ΞΎ , (β¨ β {feππ€ = feπ¦π€}{feππ¦ = feπ¦π€} Bβ SA) where π : I β Algebra π€ π π = Ξ» i β β£ Bβ€K i β£ @@ -374,7 +374,7 @@ We need to formalize one more lemma before arriving the main objective of this s Ξ³ = embedding-lift hfeπ¦π€ hfeπ¦π€ {I}{SA}{π}h(Ξ» i β β₯ SAβ€π i β₯) β¨ SAβ€β¨ π : β¨ SA β€ β¨ π - β¨ SAβ€β¨ π = (Ξ± , Ξ²) , Ξ³ + β¨ SAβ€β¨ π = (Ξ± , Ξ²) , Ξ³ ΞΎ : β¨ π β P π¦ ΞΎ = produ (Ξ» i β P-expa (β£ snd β₯ Bβ€K i β₯ β£)) @@ -390,10 +390,10 @@ Finally, we are in a position to prove that a product of subalgebras of algebras-module _ {fovu : dfunext (ov π€) (ov π€)}{π¦ : Pred (Algebra π€ π)(ov π€)} where +module _ {fovu : dfunext (ov π€) (ov π€)}{π¦ : Pred (Algebra π€ π)(ov π€)} where PSβSP : -- extensionality assumptions: - hfunext (ov π€)(ov π€) + hfunext (ov π€)(ov π€) β P{ov π€}{ov π€} (S{π€}{ov π€} π¦) β S{ov π€}{ov π€} (P{π€}{ov π€} π¦) @@ -434,7 +434,7 @@ We conclude this subsection with three more inclusion relations that will have b-PβV : {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} β P{π€}{π¦} π¦ β V{π€}{π¦} π¦ +PβV : {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} β P{π€}{π¦} π¦ β V{π€}{π¦} π¦ PβV (pbase x) = vbase x PβV{π€} (pliftu x) = vlift (PβV{π€}{π€} x) @@ -445,8 +445,8 @@ We conclude this subsection with three more inclusion relations that will have b PβV (pisow x xβ) = visow (PβV x) xβ -SPβV : {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} - β S{π€ β π¦}{π€ β π¦} (P{π€}{π¦} π¦) β V π¦ +SPβV : {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} + β S{π€ β π¦}{π€ β π¦} (P{π€}{π¦} π¦) β V π¦ SPβV (sbase{π¨} PCloA) = PβV (pisow PCloA Lift-β ) SPβV (slift{π¨} x) = vliftw (SPβV x) @@ -463,53 +463,53 @@ As mentioned earlier, a technical hurdle that must be overcome when formalizing open Lift -module Vlift {feβ : dfunext (ov π€) π€} - {feβ : dfunext ((ov π€) β ((ov π€)βΊ)) ((ov π€) βΊ)} - {feβ : dfunext (ov π€) (ov π€)} +module Vlift {feβ : dfunext (ov π€) π€} + {feβ : dfunext ((ov π€) β ((ov π€)βΊ)) ((ov π€) βΊ)} + {feβ : dfunext (ov π€) (ov π€)} {π¦ : Pred (Algebra π€ π)(ov π€)} where VlA : {π¨ : Algebra (ov π€) π} β π¨ β V{π€}{ov π€} π¦ - β Lift-alg π¨ (ov π€ βΊ) β V{π€}{ov π€ βΊ} π¦ + β Lift-alg π¨ (ov π€ βΊ) β V{π€}{ov π€ βΊ} π¦ VlA (vbase{π¨} x) = visow (vbase x) (Lift-alg-associative π¨) VlA (vlift{π¨} x) = visow (vlift x) (Lift-alg-associative π¨) VlA (vliftw{π¨} x) = visow (VlA x) (Lift-alg-associative π¨) VlA (vhimg{π¨}{π©} x hB) = vhimg (VlA x) (Lift-alg-hom-image hB) - VlA (vssub{π¨}{π©} x Bβ€A) = vssubw (vlift{π¦ = (ov π€ βΊ)} x) (Lift-β€-Lift π¨ Bβ€A) + VlA (vssub{π¨}{π©} x Bβ€A) = vssubw (vlift{π¦ = (ov π€ βΊ)} x) (Lift-β€-Lift π¨ Bβ€A) VlA (vssubw{π¨}{π©} x Bβ€A) = vssubw (VlA x) (Lift-β€-Lift π¨ Bβ€A) VlA (vprodu{I}{π} x) = visow (vprodw vlA) (β -sym Bβ A) where - π° : (ov π€ βΊ) Μ + π° : (ov π€ βΊ) Μ π° = Lift I - lA : π° β Algebra (ov π€ βΊ) π - lA i = Lift-alg (π (lower i)) (ov π€ βΊ) + lA : π° β Algebra (ov π€ βΊ) π + lA i = Lift-alg (π (lower i)) (ov π€ βΊ) - vlA : β i β (lA i) β V{π€}{ov π€ βΊ} π¦ + vlA : β i β (lA i) β V{π€}{ov π€ βΊ} π¦ vlA i = vlift (x (lower i)) iso-components : β i β π i β lA (lift i) iso-components i = Lift-β - Bβ A : Lift-alg (β¨ π) (ov π€ βΊ) β β¨ lA + Bβ A : Lift-alg (β¨ π) (ov π€ βΊ) β β¨ lA Bβ A = Lift-alg-β¨ β {fizw = feβ}{fiu = feβ} iso-components VlA (vprodw{I}{π} x) = visow (vprodw vlA) (β -sym Bβ A) where - π° : (ov π€ βΊ) Μ + π° : (ov π€ βΊ) Μ π° = Lift I - lA : π° β Algebra (ov π€ βΊ) π - lA i = Lift-alg (π (lower i)) (ov π€ βΊ) + lA : π° β Algebra (ov π€ βΊ) π + lA i = Lift-alg (π (lower i)) (ov π€ βΊ) - vlA : β i β (lA i) β V{π€}{ov π€ βΊ} π¦ + vlA : β i β (lA i) β V{π€}{ov π€ βΊ} π¦ vlA i = VlA (x (lower i)) iso-components : β i β π i β lA (lift i) iso-components i = Lift-β - Bβ A : Lift-alg (β¨ π) (ov π€ βΊ) β β¨ lA + Bβ A : Lift-alg (β¨ π) (ov π€ βΊ) β β¨ lA Bβ A = Lift-alg-β¨ β {fizw = feβ}{fiu = feβ} iso-components VlA (visou{π¨}{π©} x Aβ B) = visow (vlift x) (Lift-alg-iso Aβ B) @@ -525,21 +525,21 @@ Above we proved that `SP(π¦) β V(π¦)`, and we did so under fairly general -- module _ {π¦ : Pred (Algebra π€ π) (ov π€)} where - SPβV' : S{ov π€}{ov π€ βΊ} (P{π€}{ov π€} π¦) β V π¦ + SPβV' : S{ov π€}{ov π€ βΊ} (P{π€}{ov π€} π¦) β V π¦ SPβV' (sbase{π¨} x) = visow (VlA (SPβV (sbase x))) (β -sym (Lift-alg-associative π¨)) SPβV' (slift x) = VlA (SPβV x) SPβV' (ssub{π¨}{π©} spA Bβ€A) = vssubw (VlA (SPβV spA)) Bβ€lA where - Bβ€lA : π© β€ Lift-alg π¨ (ov π€ βΊ) + Bβ€lA : π© β€ Lift-alg π¨ (ov π€ βΊ) Bβ€lA = β€-Lift π¨ Bβ€A SPβV' (ssubw spA Bβ€A) = vssubw (SPβV' spA) Bβ€A SPβV' (siso{π¨}{π©} x Aβ B) = visow (VlA (SPβV x)) Ξ³ where - Ξ³ : Lift-alg π¨ (ov π€ βΊ) β π© + Ξ³ : Lift-alg π¨ (ov π€ βΊ) β π© Ξ³ = β -trans (β -sym Lift-β ) Aβ B@@ -555,9 +555,9 @@ Before doing so, we need to redefine the class product so that each factor comes module class-products-with-maps {X : π€ Μ} - {feππ€ : dfunext (ov π€) π€} - {feβ : dfunext ((ov π€) β ((ov π€)βΊ)) ((ov π€) βΊ)} - {feβ : dfunext (ov π€) (ov π€)} + {feππ€ : dfunext (ov π€) π€} + {feβ : dfunext ((ov π€) β ((ov π€)βΊ)) ((ov π€) βΊ)} + {feβ : dfunext (ov π€) (ov π€)} (π¦ : Pred (Algebra π€ π)(ov π€)) where @@ -616,7 +616,7 @@ So, since `PSβSP`, we see that that the product of all subalgebras of a class- class-prod-s-β-sp : hfunext (ov π€) (ov π€) β class-product β S(P π¦) + class-prod-s-β-sp : hfunext (ov π€) (ov π€) β class-product β S(P π¦) class-prod-s-β-sp hfe = PSβSP {fovu = feβ} hfe class-prod-s-β-ps