From acf4a048142e71f0bdd9ac9581e97b4f07d7c07c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 20 Aug 2023 20:49:08 -0700 Subject: [PATCH] Prove the chain mapping property Signed-off-by: Danila Fedorin --- Lattice.agda | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index af572aa..bf3eb90 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -7,8 +7,9 @@ open import Relation.Nullary using (Dec; ¬_) open import Data.Nat as Nat using (ℕ; _≤_) open import Data.Product using (_×_; Σ; _,_) open import Data.Sum using (_⊎_; inj₁; inj₂) -open import Agda.Primitive using (lsuc; Level) -open import Chain using (Chain; Height) +open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_) +open import Chain using (Chain; Height; done; step) +open import Function.Definitions using (Injective) record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where field @@ -70,6 +71,24 @@ record IsFiniteHeightLattice {a} (A : Set a) open IsLattice isLattice public +module _ {a b} {A : Set a} {B : Set b} + (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b) + (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) + (slA : IsSemilattice A _≈₁_ _⊔₁_) (slB : IsSemilattice B _≈₂_ _⊔₂_) where + + open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_) + open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_) + + Monotonic : (A → B) → Set (a ⊔ℓ b) + Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂ + + Chain-map : ∀ (f : A → B) → Monotonic f → Injective _≈₁_ _≈₂_ f → + ∀ {a₁ a₂ : A} {n : ℕ} → Chain _≺₁_ a₁ a₂ n → Chain _≺₂_ (f a₁) (f a₂) n + Chain-map f Monotonicᶠ Injectiveᶠ done = done + Chain-map f Monotonicᶠ Injectiveᶠ (step (a₁≼₁a , a₁̷≈₁a) aa₂) = + let fa₁≺₂fa = (Monotonicᶠ a₁≼₁a , λ fa₁≈₂fa → a₁̷≈₁a (Injectiveᶠ fa₁≈₂fa)) + in step fa₁≺₂fa (Chain-map f Monotonicᶠ Injectiveᶠ aa₂) + record Semilattice {a} (A : Set a) : Set (lsuc a) where field _≈_ : A → A → Set a