Generalize chains to allow equivalences

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Chain.agda

@@ -1,21 +1,37 @@
-module Chain where
+open import Equivalence
+
+module Chain {a} {A : Set a}
+             (_≈_ : A → A → Set a)
+             (≈-equiv : IsEquivalence A _≈_)
+             (_R_ : A → A → Set a)
+             (R-≈-cong : ∀ {a₁ a₁' a₂ a₂'} → a₁ ≈ a₁' → a₂ ≈ a₂' → a₁ R a₂ → a₁' R a₂') where
 
 open import Data.Nat as Nat using (ℕ; suc; _+_; _≤_)
 open import Data.Product using (_×_; Σ; _,_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 
-module _ {a} {A : Set a} (_R_ : A → A → Set a) where
+open IsEquivalence ≈-equiv
+
+module _  where
 
     data Chain : A → A → ℕ → Set a where
-        done : ∀ {a : A} → Chain a a 0
+        done : ∀ {a a' : A} → a ≈ a' → Chain a a' 0
-        step : ∀ {a₁ a₂ a₃ : A} {n : ℕ} → a₁ R a₂ → Chain a₂ a₃ n → Chain a₁ a₃ (suc n)
+        step : ∀ {a₁ a₂ a₂' a₃ : A} {n : ℕ} → a₁ R a₂ → a₂ ≈ a₂' → Chain a₂ a₃ n → Chain a₁ a₃ (suc n)
+
+    Chain-≈-cong₁ : ∀ {a₁ a₁' a₂} {n : ℕ} → a₁ ≈ a₁' → Chain a₁ a₂ n → Chain a₁' a₂ n
+    Chain-≈-cong₁ a₁≈a₁' (done a₁≈a₂) = done (≈-trans (≈-sym a₁≈a₁') a₁≈a₂)
+    Chain-≈-cong₁ a₁≈a₁' (step a₁Ra a≈a' a'a₂) = step (R-≈-cong a₁≈a₁' ≈-refl a₁Ra) a≈a' a'a₂
+
+    Chain-≈-cong₂ : ∀ {a₁ a₂ a₂'} {n : ℕ} → a₂ ≈ a₂' → Chain a₁ a₂ n → Chain a₁ a₂' n
+    Chain-≈-cong₂ a₂≈a₂' (done a₁≈a₂) = done (≈-trans a₁≈a₂ a₂≈a₂')
+    Chain-≈-cong₂ a₂≈a₂' (step a₁Ra a≈a' a'a₂) = step a₁Ra a≈a' (Chain-≈-cong₂ a₂≈a₂' a'a₂)
 
     concat : ∀ {a₁ a₂ a₃ : A} {n₁ n₂ : ℕ} → Chain a₁ a₂ n₁ → Chain a₂ a₃ n₂ → Chain a₁ a₃ (n₁ + n₂)
-    concat done a₂a₃ = a₂a₃
+    concat (done a₁≈a₂) a₂a₃ = Chain-≈-cong₁ (≈-sym a₁≈a₂) a₂a₃
-    concat (step a₁Ra aa₂) a₂a₃ = step a₁Ra (concat aa₂ a₂a₃)
+    concat (step a₁Ra a≈a' a'a₂) a₂a₃ = step a₁Ra a≈a' (concat a'a₂ a₂a₃)
 
-    empty-≡ : ∀ {a₁ a₂ : A} → Chain a₁ a₂ 0 → a₁ ≡ a₂
+    empty-≡ : ∀ {a₁ a₂ : A} → Chain a₁ a₂ 0 → a₁ ≈ a₂
-    empty-≡ done = refl
+    empty-≡ (done a₁≈a₂) = a₁≈a₂
 
     Bounded : ℕ → Set a
     Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound

Lattice.agda

@@ -1,11 +1,12 @@
 module Lattice where
 
 open import Equivalence
-open import Chain
+import Chain
 
 import Data.Nat.Properties as NatProps
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
 open import Relation.Binary.Definitions
+open import Relation.Binary.Core using (_Preserves_⟶_ )
 open import Relation.Nullary using (Dec; ¬_)
 open import Data.Nat as Nat using (ℕ; _≤_; _+_)
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
@@ -80,7 +81,7 @@ record IsFiniteHeightLattice {a} (A : Set a)
 
     field
         isLattice : IsLattice A _≈_ _⊔_ _⊓_
-        fixedHeight : Chain.Height (IsLattice._≺_ isLattice) h
+        fixedHeight : Chain.Height (_≈_) (IsLattice.≈-equiv isLattice) (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) h
 
     open IsLattice isLattice public
 
@@ -96,15 +97,23 @@ module ChainMapping {a b} {A : Set a} {B : Set b}
     {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
     (slA : IsSemilattice A _≈₁_ _⊔₁_) (slB : IsSemilattice B _≈₂_ _⊔₂_) where
 
-    open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_; ≈-equiv to ≈₁-equiv)
+    open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_; ≈-equiv to ≈₁-equiv; ≺-cong to ≺₁-cong)
-    open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_; ≈-equiv to ≈₂-equiv)
+    open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_; ≈-equiv to ≈₂-equiv; ≺-cong to ≺₂-cong)
 
-    Chain-map : ∀ (f : A → B) → Monotonic _≼₁_ _≼₂_ f → Injective _≈₁_ _≈₂_ f →
+    open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; step to step₁; done to done₁)
-                ∀ {a₁ a₂ : A} {n : ℕ} → Chain _≺₁_ a₁ a₂ n → Chain _≺₂_ (f a₁) (f a₂) n
+    open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; step to step₂; done to done₂)
-    Chain-map f Monotonicᶠ Injectiveᶠ done = done
+
-    Chain-map f Monotonicᶠ Injectiveᶠ (step (a₁≼₁a , a₁̷≈₁a) aa₂) =
+    Chain-map : ∀ (f : A → B) →
+                Monotonic _≼₁_ _≼₂_ f →
+                Injective _≈₁_ _≈₂_ f →
+                f Preserves _≈₁_ ⟶  _≈₂_ →
+                ∀ {a₁ a₂ : A} {n : ℕ} → Chain₁ a₁ a₂ n → Chain₂ (f a₁) (f a₂) n
+    Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (done₁ a₁≈a₂) =
+        done₂ (Preservesᶠ a₁≈a₂)
+    Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (step₁ (a₁≼₁a , a₁̷≈₁a) a≈₁a' a'a₂) =
         let fa₁≺₂fa = (Monotonicᶠ a₁≼₁a , λ fa₁≈₂fa → a₁̷≈₁a (Injectiveᶠ fa₁≈₂fa))
-        in step fa₁≺₂fa (Chain-map f Monotonicᶠ Injectiveᶠ aa₂)
+            fa≈fa' = Preservesᶠ a≈₁a'
+        in step₂ fa₁≺₂fa fa≈fa' (Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ a'a₂)
 
 record Semilattice {a} (A : Set a) : Set (lsuc a) where
     field
@@ -354,9 +363,9 @@ module IsFiniteHeightLatticeInstances where
 
         module ProdLattice = IsLatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊓₁_ _⊔₂_ _⊓₂_ (IsFiniteHeightLattice.isLattice lA) (IsFiniteHeightLattice.isLattice lB)
         open ProdLattice using (_⊔_; _⊓_; _≈_) public
-        open IsLattice ProdLattice.ProdIsLattice using (_≼_; _≺_)
+        open IsLattice ProdLattice.ProdIsLattice using (_≼_; _≺_; ≺-cong; ≈-equiv)
-        open IsFiniteHeightLattice lA using () renaming (⊔-idemp to ⊔₁-idemp; _≼_ to _≼₁_)
+        open IsFiniteHeightLattice lA using () renaming (⊔-idemp to ⊔₁-idemp; _≼_ to _≼₁_; ≈-refl to ≈₁-refl)
-        open IsFiniteHeightLattice lB using () renaming (⊔-idemp to ⊔₂-idemp; _≼_ to _≼₂_)
+        open IsFiniteHeightLattice lB using () renaming (⊔-idemp to ⊔₂-idemp; _≼_ to _≼₂_; ≈-refl to ≈₂-refl)
 
         module ChainMapping₁ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lA) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice)
         module ChainMapping₂ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lB) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice)
@@ -365,9 +374,15 @@ module IsFiniteHeightLatticeInstances where
             a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
             a,∙-Monotonic a {b₁} {b₂} (b , b₁⊔b≈b₂) = ((a , b) , (⊔₁-idemp a , b₁⊔b≈b₂))
 
+            a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶  _≈_
+            a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)
+
             ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
             ∙,b-Monotonic b {a₁} {a₂} (a , a₁⊔a≈a₂) = ((a , b) , (a₁⊔a≈a₂ , ⊔₂-idemp b))
 
+            ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
+            ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
+
             amin : A
             amin = proj₁ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lA)))
 
@@ -385,9 +400,9 @@ module IsFiniteHeightLatticeInstances where
             { isLattice = ProdLattice.ProdIsLattice
             ; fixedHeight =
                 ( ( ((amin , bmin) , (amax , bmax))
-                  , concat _≺_
+                  , Chain.concat _≈_ ≈-equiv _≺_ ≺-cong
-                      (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lA))))
+                      (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lA))))
-                      (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lB))))
+                      (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lB))))
                   )
                 , _
                 )