Prove the chain mapping property

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

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 Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
-open import Chain using (Chain; Height)
+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