From bf74b35c1438768b707048f732a26421926b66af Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 29 Sep 2023 21:19:48 -0700
Subject: [PATCH] Add proof of Lattice preservation

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Homomorphism.agda | 53 +++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 51 insertions(+), 2 deletions(-)

diff --git a/Homomorphism.agda b/Homomorphism.agda
index f54fae9..8f567eb 100644
--- a/Homomorphism.agda
+++ b/Homomorphism.agda
@@ -96,5 +96,54 @@ record LatticeHomomorphism (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
         ⊔-homomorphism : SemilatticeHomomorphism _⊔₁_ _⊔₂_
         ⊓-homomorphism : SemilatticeHomomorphism _⊓₁_ _⊓₂_
 
-    open SemilatticeHomomorphism ⊔-homomorphism using (f-preserves-≈)
-    open SemilatticeHomomorphism ⊓-homomorphism renaming (f-⊔-distr to f-⊓-distr)
+    open SemilatticeHomomorphism ⊔-homomorphism using (f-⊔-distr; f-preserves-≈) public
+    open SemilatticeHomomorphism ⊓-homomorphism using () renaming (f-⊔-distr to f-⊓-distr) public
+
+module _ (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+         (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
+         (lh : LatticeHomomorphism _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_)
+         (≈₂-⊔₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
+         (≈₂-⊓₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊓₂ a₃) ≈₂ (a₂ ⊓₂ a₄))
+         (surF : Surjective _≈₁_ _≈₂_ f) where
+
+    open LatticeHomomorphism lh
+
+    transportLattice : IsLattice A _≈₁_ _⊔₁_ _⊓₁_ → IsLattice B _≈₂_ _⊔₂_ _⊓₂_
+    transportLattice lA = record
+        { joinSemilattice = transportSemilattice _⊔₁_ _⊔₂_ (LatticeHomomorphism.⊔-homomorphism lh) ≈₂-⊔₂-cong surF (IsLattice.joinSemilattice lA)
+        ; meetSemilattice = transportSemilattice _⊓₁_ _⊓₂_ (LatticeHomomorphism.⊓-homomorphism lh) ≈₂-⊓₂-cong surF (IsLattice.meetSemilattice lA)
+        ; absorb-⊔-⊓ = λ b₁ b₂ →
+            let (a₁ , fa₁≈b₁) = surF b₁
+                (a₂ , fa₂≈b₂) = surF b₂
+            in
+               begin
+                   b₁ ⊔₂ (b₁ ⊓₂ b₂)
+               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) ⟩
+                   f a₁ ⊔₂ (f a₁ ⊓₂ f a₂)
+               ∼⟨ ≈₂-⊔₂-cong ≈₂-refl (≈₂-sym (f-⊓-distr a₁ a₂)) ⟩
+                   f a₁ ⊔₂ f (a₁ ⊓₁ a₂)
+               ∼⟨ ≈₂-sym (f-⊔-distr a₁ (a₁ ⊓₁ a₂)) ⟩
+                   f (a₁ ⊔₁ (a₁ ⊓₁ a₂))
+               ∼⟨ f-preserves-≈ (IsLattice.absorb-⊔-⊓ lA a₁ a₂) ⟩
+                   f a₁
+               ∼⟨ fa₁≈b₁ ⟩
+                   b₁
+               ∎
+        ; absorb-⊓-⊔ = λ b₁ b₂ →
+            let (a₁ , fa₁≈b₁) = surF b₁
+                (a₂ , fa₂≈b₂) = surF b₂
+            in
+               begin
+                   b₁ ⊓₂ (b₁ ⊔₂ b₂)
+               ∼⟨ ≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) ⟩
+                   f a₁ ⊓₂ (f a₁ ⊔₂ f a₂)
+               ∼⟨ ≈₂-⊓₂-cong ≈₂-refl (≈₂-sym (f-⊔-distr a₁ a₂)) ⟩
+                   f a₁ ⊓₂ f (a₁ ⊔₁ a₂)
+               ∼⟨ ≈₂-sym (f-⊓-distr a₁ (a₁ ⊔₁ a₂)) ⟩
+                   f (a₁ ⊓₁ (a₁ ⊔₁ a₂))
+               ∼⟨ f-preserves-≈ (IsLattice.absorb-⊓-⊔ lA a₁ a₂) ⟩
+                   f a₁
+               ∼⟨ fa₁≈b₁ ⟩
+                   b₁
+               ∎
+        }