Require bottom element to actually be bottom; finish proof

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

Lattice.agda

@@ -260,6 +260,12 @@ record IsFiniteHeightLattice {a} (A : Set a)
 
     open MyChain.Height fixedHeight using (⊥; ⊤) public
 
+    Known-⊥ : Set a
+    Known-⊥ = ∀ (a : A) → ⊥ ≼ a
+
+    Known-⊤ : Set a
+    Known-⊤ = ∀ (a : A) → a ≼ ⊤
+
     -- If the equality is decidable, we can prove that the top and bottom
     -- elements of the chain are least and greatest elements of the lattice
     module _ {{≈-Decidable : IsDecidable _≈_}} where
@@ -267,7 +273,7 @@ record IsFiniteHeightLattice {a} (A : Set a)
 
         open MyChain.Height fixedHeight using (bounded; longestChain)
 
-        ⊥≼ : ∀ (a : A) → ⊥ ≼ a
+        ⊥≼ : Known-⊥
         ⊥≼ a with ≈-dec a ⊥
         ...   | yes a≈⊥ = ≼-cong a≈⊥ ≈-refl (≼-refl a)
         ...   | no a̷≈⊥ with ≈-dec ⊥ (a ⊓ ⊥)

Lattice/Builder.agda

@@ -607,7 +607,7 @@ record Graph : Set where
                 ; absorb-⊓-⊔ = absorb-⊓-⊔
                 }
 
-    module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set FiniteHeightLattice) where
+    module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set λ L → Σ (FiniteHeightLattice L) λ fhl → FiniteHeightLattice.Known-⊥ fhl × FiniteHeightLattice.Known-⊤ fhl) where
         open Basic noCycles total-⊔ total-⊓ using () renaming (_⊔_ to _⊔ᵇ_; _⊓_ to _⊓ᵇ_; ⊔-idemp to ⊔ᵇ-idemp; ⊔-comm to ⊔ᵇ-comm; ⊔-assoc to ⊔ᵇ-assoc; _≼_ to _≼ᵇ_; isJoinSemilattice to isJoinSemilatticeᵇ; isMeetSemilattice to isMeetSemilatticeᵇ; isLattice to isLatticeᵇ)
 
         open IsLattice isLatticeᵇ using () renaming (≈-⊔-cong to ≡-⊔ᵇ-cong; x≼x⊔y to x≼ᵇx⊔ᵇy; ≼-antisym to ≼ᵇ-antisym; ⊔-Monotonicʳ to ⊔ᵇ-Monotonicʳ)
@@ -619,7 +619,10 @@ record Graph : Set where
         LatticeT n = proj₁ (𝓛 n)
 
         FHL : (n : Node) → FiniteHeightLattice (LatticeT n)
-        FHL n = proj₂ (𝓛 n)
+        FHL n = proj₁ (proj₂ (𝓛 n))
+
+        ⊥≼x : ∀ {n : Node} (l : LatticeT n) → FiniteHeightLattice._≼_ (FHL n) (FiniteHeightLattice.⊥ (FHL n)) l
+        ⊥≼x {n} = proj₁ (proj₂ (proj₂ (𝓛 n)))
 
         data _≈_ : Elem → Elem → Set where
             ≈-lift : ∀ {n : Node} {l₁ l₂ : LatticeT n} →
@@ -779,7 +782,7 @@ record Graph : Set where
                     with n₁₂ ← n₁ ⊔ᵇ n₂
                     with n₃ ≟ n₁₂
             ...       | no n₃≢n₁₂ = ≈-refl
-            ...       | yes refl rewrite d₁ rewrite d₂ = {!!} -- TODO: need ⊥ ⊔ n₃ ≡ n₃
+            ...       | yes refl rewrite d₁ rewrite d₂ = ≈-lift (⊥≼x l₃) -- TODO: need ⊥ ⊔ n₃ ≡ n₃
             Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
                   | no n≢n₁ | no n≢n₂ | no n≢n₃
                     with n₁₂ ← n₁ ⊔ᵇ n₂
@@ -825,7 +828,7 @@ record Graph : Set where
                     with n₂₃ ← n₂ ⊔ᵇ n₃
                     with n₁ ≟ n₂₃
             ...       | no n₁≢n₂₃ = ≈-refl
-            ...       | yes refl rewrite d₂ rewrite d₃ = {!!} -- TODO: need ⊥ ⊔ n₃ ≡ n₃
+            ...       | yes refl rewrite d₂ rewrite d₃ = ≈-lift (FiniteHeightLattice.≈-trans (FHL n₁) (FiniteHeightLattice.⊔-comm (FHL n₁) _ _) (⊥≼x l₁))
             Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
                   | no n₂≢n₁ | yes refl | yes refl
                     rewrite ⊔ᵇ-idemp n₂