diff --git a/src/HTML.agda b/src/HTML.agda
new file mode 100644
index 0000000..c4d894e
--- /dev/null
+++ b/src/HTML.agda
@@ -0,0 +1,151 @@
+open import Agda.Primitive renaming (Set to Type)
+
+open import Relation.Binary.PropositionalEquality
+open import Data.List hiding (head; span)
+open import Data.Nat using (ℕ; _<ᵇ_)
+open import Data.String hiding (_==_; show; head) renaming (_++_ to _++ˢ_; concat to concatˢ)
+open import Data.Char hiding (_==_; show)
+open import Data.Bool
+
+open import Base
+
+module HTML where
+
+data HTMLTag : Type where
+  html head meta title body : HTMLTag
+  div p a span : HTMLTag
+  h : (n : ℕ) → {T (n <ᵇ 7)} → HTMLTag
+
+instance
+  EqHTMLTag : Eq HTMLTag
+  EqHTMLTag ._==_ html html = true
+  EqHTMLTag ._==_ head head = true
+  EqHTMLTag ._==_ meta meta = true
+  EqHTMLTag ._==_ title title = true
+  EqHTMLTag ._==_ body body = true
+  EqHTMLTag ._==_ div div = true
+  EqHTMLTag ._==_ p p = true
+  EqHTMLTag ._==_ a a = true
+  EqHTMLTag ._==_ span span = true
+  EqHTMLTag ._==_ (h n) (h m) = n == m
+  EqHTMLTag ._==_ _ _ = false
+
+  ShowHTMLTag : Show HTMLTag
+  ShowHTMLTag .show html = "html"
+  ShowHTMLTag .show head = "head"
+  ShowHTMLTag .show meta = "meta"
+  ShowHTMLTag .show title = "title"
+  ShowHTMLTag .show body = "body"
+  ShowHTMLTag .show div = "div"
+  ShowHTMLTag .show a = "a"
+  ShowHTMLTag .show p = "p"
+  ShowHTMLTag .show span = "span"
+  ShowHTMLTag .show (h n) = "h" ++ˢ show n
+
+data AttributeName : Type where
+  lang src name content href style : AttributeName
+
+instance
+  ShowAttributeName : Show AttributeName
+  ShowAttributeName .show lang = "lang"
+  ShowAttributeName .show src = "src"
+  ShowAttributeName .show name = "name"
+  ShowAttributeName .show content = "content"
+  ShowAttributeName .show href = "href"
+  ShowAttributeName .show style = "style"
+
+record Attribute : Type where
+  field
+    attrname : AttributeName
+    value : String -- maybe string ? how to handle syntax?
+open Attribute
+
+AttrList : Type
+AttrList = List Attribute
+
+_＝_ : AttributeName → String → AttrList
+attrname ＝ value = record { attrname = attrname ; value = value } ∷ []
+
+mutual
+  DOM : Type
+  DOM = List Element
+
+  data Element : Type where
+    textnode : String → Element
+    element : HTMLTag → AttrList → DOM → Element
+
+record Listable (T L : Type) : Type where
+  field
+    enlist : T → List L
+open Listable ⦃...⦄
+
+instance
+  ListListable : {T : Type} → Listable (List T) T
+  ListListable .enlist l = l
+
+  StringDOMAble : Listable String Element
+  StringDOMAble .enlist x = textnode x ∷ []
+
+_,_ : {D₁ D₂ L : Type} → ⦃ Listable D₁ L ⦄ → ⦃ Listable D₂ L ⦄ → D₁ → D₂ → List L
+x , y = (enlist x) Data.List.++ (enlist y)
+
+infixr 10 _,_
+
+<_&_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → AttrList → D → (y : HTMLTag) → {T (x == y)} → DOM
+< tag & attrs > inner </ tag′ > = element tag attrs (enlist inner) ∷ []
+
+<_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → D → (y : HTMLTag) → {T (x == y)} → DOM
+< tag > inner </ tag′ > = element tag [] (enlist inner) ∷ []
+
+<_&_/> :  (x : HTMLTag) → AttrList → DOM
+< tag & attrs /> = element tag attrs [] ∷ []
+
+<_/> : (x : HTMLTag) → DOM
+< tag /> = element tag [] [] ∷ []
+
+
+
+encode : List Char → String → String
+encode escapes text = fromList (concatMap (λ x → toList (escape-char x)) (toList text))
+  where
+    escape-char : Char → String
+    escape-char ch =
+      if any (_== ch) escapes
+        then "&#" ++ˢ show (toℕ ch) ++ˢ ";"
+        else fromChar ch
+
+private
+  encode-test : encode (toList "</>") "hi <3 </p>"
+              ≡ "hi &#60;3 &#60;&#47;p&#62;"
+  encode-test = refl
+
+render-attr : Attribute → String
+render-attr x = show (x .attrname) ++ˢ "=" ++ˢ encode (toList "\t\n\r \"'=<>`") (x .value)
+
+{-# TERMINATING #-} -- TODO: we should eliminate the tree as a traversable instead of doing it like this
+render-element : Element → String
+render-element (textnode x) = encode (toList "</>") x -- we don't technically need to escape all these characters, but it's easier to do this
+render-element (element tag attrlist inner) =
+  "<" ++ˢ show tag ++ˢ concatˢ (map (λ attr → " " ++ˢ render-attr attr) attrlist) ++ˢ ">"
+  ++ˢ concatˢ (map render-element inner)
+  ++ˢ "</" ++ˢ show tag ++ˢ ">"
+
+render-dom : DOM → String
+render-dom x = concatˢ (map render-element x)
+
+sample-dom : DOM
+sample-dom =
+  < html & lang ＝ "en" >
+    < head >
+      < title > "Test page in Agda" </ title > ,
+      < meta & name ＝ "description" , content ＝ "Simple webpage rendered in Agda DSL" /> ,
+      < meta & name ＝ "author" , content ＝ "xenia" />
+    </ head > ,
+    < body >
+      < p > "hello" </ p > ,
+      < p > "world" </ p > ,
+      < div >
+        < p > "hi from within the div" </ p >
+      </ div >
+    </ body >
+  </ html >
diff --git a/src/Main.agda b/src/Main.agda
index 8c8f5bb..75ac46d 100644
--- a/src/Main.agda
+++ b/src/Main.agda
@@ -3,48 +3,81 @@
 module main where
 
 open import Agda.Primitive renaming (Set to Type)
-import Data.String as String
-import Data.Char as Char
-open import Data.Product
-open import Data.Nat
+import Data.String as S
+import Data.Vec as V
+import Data.List as L
+open S using (String)
+open L using (List)
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to _,,,_)
+open import Data.Nat hiding (_<_; _>_)
 open import Data.Unit using (⊤; tt)
-open import Data.Vec using (fromList)
-open import Data.List hiding (take; [_])
 
 open import Base
-open import Bits-and-Bytes
+open import Bits-and-Bytes using (Byte)
 open import SysIO
 open import Socket
 open import Indexed
 open import Parsing (Byte)
 open import NonEmpty
-open import Parse-HTTP
+open import Parse-HTTP hiding (_/_)
+open import HTML
 import UTF-8
 
-200-ok : String.String → List Byte → List Byte
-200-ok content-type content = UTF-8.encode-string (String.toList (headers String.++ "\r\n\r\n")) ++ content
+200-ok : S.String → List Byte → List Byte
+200-ok content-type response-data = UTF-8.encode-string (S.toList (headers S.++ "\r\n\r\n")) L.++ response-data
   where
-    headers : String.String
-    headers = "HTTP/1.1 200 OK\r\nContent-Type: " String.++ content-type String.++ "; charset=utf-8\r\nContent-Length: " String.++ (show (length content))
+    headers : String
+    headers = "HTTP/1.1 200 OK\r\nContent-Type: " S.++ content-type S.++ "; charset=utf-8\r\nContent-Length: " S.++ (show (L.length response-data))
 
-mk-response : (Path × Maybe String.String) → String.String
-mk-response req = "hiii from agda‼ \nmjau mjau mjau :3 <^_^> ∷3\nyou queried the path " String.++ show (proj₁ req) String.++ " :)\n"
+400-bad-request : List Byte
+400-bad-request = UTF-8.encode-string (S.toList "400 Bad Request\r\n\r\n")
 
+render-page : (Path × Maybe String) → DOM
+render-page (path ,,, mquery) =
+  < html & lang ＝ "en" , style ＝ "color: yellow; background: black; padding: 1em;" >
+    < head >
+      < title > "Test page in Agda" </ title > ,
+      < meta & name ＝ "description" , content ＝ "Simple webpage rendered in Agda DSL" /> ,
+      < meta & name ＝ "author" , content ＝ "xenia" />
+    </ head > ,
+    < body >
+      < h 1 > "hi" </ h 1 > ,
+      < p >
+        "you requested " ,
+        < span & style ＝ "color: white;" > show path </ span > ,
+        ((λ q → < span & style ＝ "color: fuchsia;" > "?" , q </ span >) <$> mquery or-else L.[])
+        </ p >
+    </ body >
+  </ html >
+
+handle-request : (Path × Maybe String) → IO (List Byte)
+handle-request req =
+  pure (
+    200-ok
+      "text/html"
+      (UTF-8.encode-string (S.toList (
+        render-dom (render-page req)
+      )))
+  )
 
 handle : Socket → IO (List Byte)
 handle sock = do
   putStrLn "handle: new connection‼"
   let got = get-bytes sock
 
-  let parsed = parse-get-request .parse (fromList got)
+  let parsed = parse-get-request .parse (V.fromList got)
 
   case parsed of λ where
-    (real res) → putStrLn ("handle: path = " String.++ show (proj₁ (res .result)) String.++ ", query = " String.++ proj₂ (res .result) or-else "(no query)")
-    cake → putStrLn "handle: parser died"
-
-  case parsed of λ where
-    (real res) → pure (200-ok "text/plain" (UTF-8.encode-string (String.toList (mk-response (res .result)))))
-    cake → pure (UTF-8.encode-string (String.toList "epic fail\n"))
+    (real ⟨ req@(path ,,, mquery) , _ , _ ⟩) →
+      (do
+        putStrLn ("handle: path = " S.++ show path S.++ ", query = " S.++ mquery or-else "(no query)")
+        handle-request req
+      )
+    cake →
+      (do
+        putStrLn "Got an invalid request"
+        pure 400-bad-request
+      )
 
 run-port : ℕ
 run-port = 1337
@@ -52,5 +85,5 @@ run-port = 1337
 main : IO ⊤
 main = do
   putStrLn "main: starting"
-  putStrLn ("main: running on port " String.++ show run-port)
+  putStrLn ("main: running on port " S.++ show run-port)
   run-server "localhost" run-port handle