Prove the transport of 'height lattice' property given an isomorphism

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

Equivalence.agda

@@ -4,8 +4,18 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
 
-record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
+module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
+    IsReflexive : Set a
+    IsReflexive = ∀ {a : A} → a ≈ a
+
+    IsSymmetric : Set a
+    IsSymmetric = ∀ {a b : A} → a ≈ b → b ≈ a
+
+    IsTransitive : Set a
+    IsTransitive = ∀ {a b c : A} → a ≈ b → b ≈ c → a ≈ c
+
+    record IsEquivalence : Set a where
         field
-        ≈-refl : {a : A} → a ≈ a
+            ≈-refl : IsReflexive
-        ≈-sym : {a b : A} → a ≈ b → b ≈ a
+            ≈-sym : IsSymmetric
-        ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c
+            ≈-trans : IsTransitive

Isomorphism.agda

@@ -0,0 +1,61 @@
+module Isomorphism where
+
+open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
+open import Function.Definitions using (Inverseˡ; Inverseʳ; Injective)
+open import Lattice
+open import Equivalence
+open import Relation.Binary.Core using (_Preserves_⟶_ )
+open import Data.Nat using (ℕ)
+open import Data.Product using (_,_)
+open import Relation.Nullary using (¬_)
+
+module TransportFiniteHeight
+         {a b : Level} {A : Set a} {B : Set b}
+         {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
+         {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
+         {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B}
+         {height : ℕ}
+         (fhlA : IsFiniteHeightLattice A height _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_)
+         {f : A → B} {g : B → A}
+         (f-preserves-≈₁ : f Preserves _≈₁_ ⟶  _≈₂_) (g-preserves-≈₂ : g Preserves _≈₂_ ⟶  _≈₁_)
+         (f-⊔-distr : ∀ (a₁ a₂ : A) → f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂)))
+         (g-⊔-distr : ∀ (b₁ b₂ : B) → g (b₁ ⊔₂ b₂) ≈₁ ((g b₁) ⊔₁ (g b₂)))
+         (inverseˡ : Inverseˡ _≈₁_ _≈₂_ f g) (inverseʳ : Inverseʳ _≈₁_ _≈₂_ f g) where
+
+    open IsFiniteHeightLattice fhlA using () renaming (_≺_ to _≺₁_; ≺-cong to ≺₁-cong; ≈-equiv to ≈₁-equiv)
+    open IsLattice lB               using () renaming (_≺_ to _≺₂_; ≺-cong to ≺₂-cong; ≈-equiv to ≈₂-equiv)
+
+    open IsEquivalence ≈₁-equiv using () renaming (≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
+    open IsEquivalence ≈₂-equiv using () renaming (≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans)
+
+    open import Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
+    open import Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
+
+    f-Injective : Injective _≈₁_ _≈₂_ f
+    f-Injective {x} {y} fx≈fy = ≈₁-trans (≈₁-sym (inverseʳ x)) (≈₁-trans (g-preserves-≈₂ fx≈fy) (inverseʳ y))
+
+    g-Injective : Injective _≈₂_ _≈₁_ g
+    g-Injective {x} {y} gx≈gy = ≈₂-trans (≈₂-sym (inverseˡ x)) (≈₂-trans (f-preserves-≈₁ gx≈gy) (inverseˡ y))
+
+    f-preserves-̷≈ : f Preserves (λ x y → ¬ x ≈₁ y) ⟶  (λ x y → ¬ x ≈₂ y)
+    f-preserves-̷≈ x̷≈y = λ fx≈fy → x̷≈y (f-Injective fx≈fy)
+
+    g-preserves-̷≈ : g Preserves (λ x y → ¬ x ≈₂ y) ⟶  (λ x y → ¬ x ≈₁ y)
+    g-preserves-̷≈ x̷≈y = λ gx≈gy → x̷≈y (g-Injective gx≈gy)
+
+    portChain₁ : ∀ {a₁ a₂ : A} {h : ℕ} → Chain₁ a₁ a₂ h → Chain₂ (f a₁) (f a₂) h
+    portChain₁ (done₁ a₁≈a₂) = done₂ (f-preserves-≈₁ a₁≈a₂)
+    portChain₁ (step₁ {a₁} {a₂} (a₁≼a₂ , a₁̷≈a₂) a₂≈a₂' c) = step₂ (≈₂-trans (≈₂-sym (f-⊔-distr a₁ a₂)) (f-preserves-≈₁ a₁≼a₂) , f-preserves-̷≈ a₁̷≈a₂) (f-preserves-≈₁ a₂≈a₂') (portChain₁ c)
+
+    portChain₂ : ∀ {b₁ b₂ : B} {h : ℕ} → Chain₂ b₁ b₂ h → Chain₁ (g b₁) (g b₂) h
+    portChain₂ (done₂ a₂≈a₁) = done₁ (g-preserves-≈₂ a₂≈a₁)
+    portChain₂ (step₂ {b₁} {b₂} (b₁≼b₂ , b₁̷≈b₂) b₂≈b₂' c) = step₁ (≈₁-trans (≈₁-sym (g-⊔-distr b₁ b₂)) (g-preserves-≈₂ b₁≼b₂) , g-preserves-̷≈ b₁̷≈b₂) (g-preserves-≈₂ b₂≈b₂') (portChain₂ c)
+
+    isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
+    isFiniteHeightLattice =
+        let
+            (((a₁ , a₂) , c) , bounded₁) = IsFiniteHeightLattice.fixedHeight fhlA
+        in record
+            { isLattice = lB
+            ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
+            }

Lattice/IterProd.agda

@@ -20,7 +20,7 @@ IterProd k = iterate k (λ t → A × t) B
 -- To make iteration more convenient, package the definitions in Lattice
 -- records, perform the recursion, and unpackage.
 
-private module _ where
+module _ where
     lattice : ∀ {k : ℕ} → Lattice (IterProd k)
     lattice {0} = record
         { _≈_ = _≈₂_