Prove that a finite height lattice is bounded below

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

Lattice.agda

@@ -442,3 +442,46 @@ module IsFiniteHeightLatticeInstances where
                                                             (proj₂ (IsFiniteHeightLattice.fixedHeight lB) b₁b₂))
                 )
             }
+
+module FixedHeightLatticeIsBounded {a} {A : Set a} {h : ℕ}
+    {_≈_ : A → A → Set a}
+    {_⊔_ : A → A → A} {_⊓_ : A → A → A}
+    (decA : IsDecidable _≈_)
+    (lA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_) where
+
+    open IsFiniteHeightLattice lA using (_≼_; _≺_; fixedHeight; ≈-equiv; ≈-refl; ≈-sym; ≈-trans; ≼-refl; ≼-cong; ≺-cong; ≈-⊔-cong; absorb-⊔-⊓; ⊔-comm; ⊓-comm)
+    open IsDecidable decA using () renaming (R-dec to ≈-dec)
+    open NatProps using (+-comm; m+1+n≰m)
+    module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
+
+    A-BoundedBelow : Σ A (λ ⊥ᴬ → ∀ (a : A) → ⊥ᴬ ≼ a)
+    A-BoundedBelow = (⊥ᴬ , ⊥ᴬ≼)
+        where
+            ⊥ᴬ : A
+            ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))
+
+            ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
+            ⊥ᴬ≼ a
+                with ≈-dec a ⊥ᴬ
+            ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
+            ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
+            ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = (a , ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ)))
+            ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = absurd (m+1+n≰m h h+1≤h)
+                            where
+                                ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
+                                ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
+
+                                x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ
+                                x≺⊥ᴬ = ((⊥ᴬ , ≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a))) , ⊥ᴬ⊓a̷≈⊥ᴬ)
+
+                                h+1≤h : h + 1 ≤ h
+                                h+1≤h rewrite (+-comm h 1) = proj₂ fixedHeight (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight)))
+
+module FixedPoint {a} {A : Set a}
+                  (h : ℕ)
+                  (_≈_ : A → A → Set a)
+                  (_⊔_ : A → A → A) (_⊓_ : A → A → A)
+                  (isFiniteHeightLattice : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
+                  (f : A → A) (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ isFiniteHeightLattice)
+                                                      (IsFiniteHeightLattice._≼_ isFiniteHeightLattice) f) where
+    open IsFiniteHeightLattice isFiniteHeightLattice