diff --git a/Homomorphism.agda b/Homomorphism.agda
deleted file mode 100644
index 8f567eb..0000000
--- a/Homomorphism.agda
+++ /dev/null
@@ -1,149 +0,0 @@
-open import Equivalence
-
-module Homomorphism {a b} (A : Set a) (B : Set b)
-    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
-    (≈₂-equiv : IsEquivalence B _≈₂_)
-    (f : A → B) where
-
-open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
-open import Function.Definitions using (Surjective)
-open import Relation.Binary.Core using (_Preserves_⟶_ )
-open import Data.Product using (_,_)
-open import Lattice
-
-open IsEquivalence ≈₂-equiv using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; ≈-refl to ≈₂-refl)
-open import Relation.Binary.Reasoning.Base.Single _≈₂_ ≈₂-refl ≈₂-trans
-
-infixl 20 _∙₂_
-_∙₂_ = ≈₂-trans
-
-record SemilatticeHomomorphism (_⊔₁_ : A → A → A)
-                               (_⊔₂_ : B → B → B) : Set (a ⊔ℓ b) where
-    field
-        f-preserves-≈ : f Preserves _≈₁_ ⟶  _≈₂_
-        f-⊔-distr : ∀ (a₁ a₂ : A) → f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂))
-
-module _ (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
-         (sh : SemilatticeHomomorphism _⊔₁_ _⊔₂_)
-         (≈₂-⊔₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
-         (surF : Surjective _≈₁_ _≈₂_ f) where
-
-    open SemilatticeHomomorphism sh
-
-    transportSemilattice : IsSemilattice A _≈₁_ _⊔₁_ → IsSemilattice B _≈₂_ _⊔₂_
-    transportSemilattice sA = record
-        { ≈-equiv = ≈₂-equiv
-        ; ≈-⊔-cong = ≈₂-⊔₂-cong
-        ; ⊔-assoc = λ b₁ b₂ b₃ →
-            let (a₁ , fa₁≈b₁) = surF b₁
-                (a₂ , fa₂≈b₂) = surF b₂
-                (a₃ , fa₃≈b₃) = surF b₃
-            in
-               begin
-                   (b₁ ⊔₂ b₂) ⊔₂ b₃
-               ∼⟨ ≈₂-⊔₂-cong (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) (≈₂-sym fa₃≈b₃) ⟩
-                   (f a₁ ⊔₂ f a₂) ⊔₂ f a₃
-               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym (f-⊔-distr a₁ a₂)) ≈₂-refl ⟩
-                   f (a₁ ⊔₁ a₂) ⊔₂ f a₃
-               ∼⟨ ≈₂-sym (f-⊔-distr (a₁ ⊔₁ a₂) a₃) ⟩
-                   f ((a₁ ⊔₁ a₂) ⊔₁ a₃)
-               ∼⟨ f-preserves-≈ (IsSemilattice.⊔-assoc sA a₁ a₂ a₃) ⟩
-                   f (a₁ ⊔₁ (a₂ ⊔₁ a₃))
-               ∼⟨ f-⊔-distr a₁ (a₂ ⊔₁ a₃) ⟩
-                   f a₁ ⊔₂ f (a₂ ⊔₁ a₃)
-               ∼⟨ ≈₂-⊔₂-cong ≈₂-refl (f-⊔-distr a₂ a₃) ⟩
-                   f a₁ ⊔₂ (f a₂ ⊔₂ f a₃)
-               ∼⟨ ≈₂-⊔₂-cong fa₁≈b₁ (≈₂-⊔₂-cong fa₂≈b₂ fa₃≈b₃) ⟩
-                   b₁ ⊔₂ (b₂ ⊔₂ b₃)
-               ∎
-        ; ⊔-comm = λ b₁ b₂ →
-            let (a₁ , fa₁≈b₁) = surF b₁
-                (a₂ , fa₂≈b₂) = surF b₂
-            in
-               begin
-                   b₁ ⊔₂ b₂
-               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂) ⟩
-                   f a₁ ⊔₂ f a₂
-               ∼⟨ ≈₂-sym (f-⊔-distr a₁ a₂) ⟩
-                   f (a₁ ⊔₁ a₂)
-               ∼⟨ f-preserves-≈ (IsSemilattice.⊔-comm sA a₁ a₂) ⟩
-                   f (a₂ ⊔₁ a₁)
-               ∼⟨ f-⊔-distr a₂ a₁ ⟩
-                   f a₂ ⊔₂ f a₁
-               ∼⟨ ≈₂-⊔₂-cong fa₂≈b₂ fa₁≈b₁ ⟩
-                   b₂ ⊔₂ b₁
-               ∎
-        ; ⊔-idemp = λ b →
-            let (a , fa≈b) = surF b
-            in
-               begin
-                   b ⊔₂ b
-               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa≈b) (≈₂-sym fa≈b) ⟩
-                   f a ⊔₂ f a
-               ∼⟨ ≈₂-sym (f-⊔-distr a a) ⟩
-                   f (a ⊔₁ a)
-               ∼⟨ f-preserves-≈ (IsSemilattice.⊔-idemp sA a) ⟩
-                   f a
-               ∼⟨ fa≈b ⟩
-                   b
-               ∎
-        }
-
-
-record LatticeHomomorphism (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
-                           (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) : Set (a ⊔ℓ b) where
-    field
-        ⊔-homomorphism : SemilatticeHomomorphism _⊔₁_ _⊔₂_
-        ⊓-homomorphism : SemilatticeHomomorphism _⊓₁_ _⊓₂_
-
-    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₁
-               ∎
-        }