diff --git a/Main.agda b/Main.agda
index af67b7b..99ae755 100644
--- a/Main.agda
+++ b/Main.agda
@@ -56,14 +56,4 @@ dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {
 
 open import Fixedpoint {0ℓ} {FiniteHeightMap xyzw} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
 
--- module Fixedpoint {a} {A : Set a}
---                   {h : ℕ}
---                   {_≈_ : A → A → Set a}
---                   {_⊔_ : A → A → A} {_⊓_ : A → A → A}
---                   (≈-dec : IsDecidable _≈_)
---                   (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
---                   (f : A → A)
---                   (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
---                                           (IsFiniteHeightLattice._≼_ flA) f) where
-
 main = run {0ℓ} (putStrLn (showMap aᶠ))