diff --git a/Main.agda b/Main.agda
index ca4ecae..af67b7b 100644
--- a/Main.agda
+++ b/Main.agda
@@ -1,11 +1,12 @@
 module Main where
 
 open import IO
-open import Level
+open import Level using (0ℓ)
 open import Data.Nat.Show using (show)
-open import Data.List using (List; _∷_; [])
-open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Data.List using (List; _∷_; []; foldr)
+open import Data.String using (String; _++_) renaming (_≟_ to _≟ˢ_)
 open import Data.Unit using (⊤; tt) renaming (_≟_ to _≟ᵘ_)
+open import Data.Product using (_,_; _×_; proj₁; proj₂)
 open import Data.List.Relation.Unary.All using (_∷_; [])
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl; trans)
 open import Relation.Nullary using (¬_)
@@ -18,13 +19,51 @@ xyzw = "x" ∷ "y" ∷ "z" ∷ "w" ∷ []
 xyzw-Unique : Unique xyzw
 xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ []) (push [] empty)))
 
-open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice)
-open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_  as AB renaming (≈-dec to ≈ᵘ-dec)
-open AB.Plain renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
-open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ)
+open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic)
+open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_  as AB using () renaming (≈-dec to ≈ᵘ-dec)
+open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
+open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
 
 fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
 
+FiniteHeightMap = FiniteHeightTypeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
+
+showAboveBelow : AB.AboveBelow → String
+showAboveBelow AB.⊤ = "⊤"
+showAboveBelow AB.⊥ = "⊥"
+showAboveBelow (AB.[_] tt) = "()"
+
+showMap : ∀ {ks : List String} → FiniteHeightMap ks → String
+showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
+
 fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
 
-main = run {0ℓ} (putStrLn (show (FiniteHeightLattice.height fhlⁱᵖ)))
+open FiniteHeightLattice fhlⁱᵖ using (_≈_; _⊔_; _⊓_; ⊔-idemp; _≼_; ≈-⊔-cong; ≈-refl; ≈-trans; ≈-sym; ⊔-assoc; ⊔-comm; ⊔-Monotonicˡ)
+open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m}) (λ {m₁} {m₂} {m₃} → ≈-trans {m₁} {m₂} {m₃}) -- why am I having to eta-expand here?
+
+smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
+largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
+
+dumb : FiniteHeightMap xyzw
+dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl)
+
+dumbFunction : FiniteHeightMap xyzw → FiniteHeightMap xyzw
+dumbFunction = _⊔_ dumb
+
+dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction
+dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {m₂} m₁≼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ᶠ))