Start on the homomorphism / isomorphism proofs

Homomorphism.agda

@@ -0,0 +1,100 @@
+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-preserves-≈)
+    open SemilatticeHomomorphism ⊓-homomorphism renaming (f-⊔-distr to f-⊓-distr)