From 56c72e1388a71e679b65d3fc8939f86e69715b21 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 9 Mar 2024 14:07:56 -0800 Subject: [PATCH] Delete unused homomorphism proof that was broken by an Agda update. Signed-off-by: Danila Fedorin --- Homomorphism.agda | 149 ---------------------------------------------- 1 file changed, 149 deletions(-) delete mode 100644 Homomorphism.agda 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₁ - ∎ - }