diff --git a/src/HTML.agda b/src/HTML.agda
index c4d894e..441c09f 100644
--- a/src/HTML.agda
+++ b/src/HTML.agda
@@ -1,16 +1,70 @@
 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.Nat
 open import Data.Bool
 
+import Data.String as S
+import Data.Char as C
+import Data.List as L
+open S using (String)
+open C using (Char)
+open L using (List)
+
 open import Base
 
 module HTML where
 
+private
+  _≤ᶜ_ : Char → Char → Bool
+  c₀ ≤ᶜ c₁ = C.toℕ c₀ ≤ᵇ C.toℕ c₁
+
+
+
+valid-attribute-name : String → Bool
+valid-attribute-name x = L.all valid-attribute-char (S.toList x)
+  where
+    valid-attribute-char : Char → Bool
+    valid-attribute-char c =
+      ('a' ≤ᶜ c) ∧ (c ≤ᶜ 'z') ∨
+      ('A' ≤ᶜ c) ∧ (c ≤ᶜ 'Z')
+
+valid-tag-name : String → Bool
+valid-tag-name x = L.all valid-tag-char (S.toList x)
+  where
+    valid-tag-char : Char → Bool
+    valid-tag-char c =
+      ('a' ≤ᶜ c) ∧ (c ≤ᶜ 'z') ∨
+      ('A' ≤ᶜ c) ∧ (c ≤ᶜ 'Z') ∨
+      ('0' ≤ᶜ c) ∧ (c ≤ᶜ '9')
+
+record Attribute : Type where
+  field
+    name : String
+    value : String
+    {name-is-valid}: T (valid-attribute-name name)
+
+instance
+  open Attribute
+  EqAttribute : Eq Attribute
+  EqAttribute ._==_ x y = x .name == y .name ∧ x .value == y .value
+
+record HTMLTag : Type where
+  field
+    name : String
+    attributes : List Attribute
+    {name-is-valid}: T (valid-tag-name name)
+
+instance
+  open HTMLTag
+
+  EqTag : Eq HTMLTag
+  EqTag ._==_ x y = x .name == y .name ∧ x .attributes == y .attributes
+
+data Element : Type where
+  textnode : String → Element
+  node : HTMLTag → List Element → Element
+
+{-
 data HTMLTag : Type where
   html head meta title body : HTMLTag
   div p a span : HTMLTag
@@ -42,29 +96,24 @@ instance
   ShowHTMLTag .show span = "span"
   ShowHTMLTag .show (h n) = "h" ++ˢ show n
 
-data AttributeName : Type where
-  lang src name content href style : AttributeName
+data Attr : Type where
+  lang= src= name= content= href= style= : String → Attr
 
-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"
+attr-name : Attr → String
+attr-name (lang=    _) = "lang"
+attr-name (src=     _) = "src"
+attr-name (name=    _) = "name"
+attr-name (content= _) = "content"
+attr-name (href=    _) = "href"
+attr-name (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 } ∷ []
+attr-value : Attr → String
+attr-value (lang=    x) = x
+attr-value (src=     x) = x
+attr-value (name=    x) = x
+attr-value (content= x) = x
+attr-value (href=    x) = x
+attr-value (style=   x) = x
 
 mutual
   DOM : Type
@@ -72,7 +121,7 @@ mutual
 
   data Element : Type where
     textnode : String → Element
-    element : HTMLTag → AttrList → DOM → Element
+    element : HTMLTag → List Attr → DOM → Element
 
 record Listable (T L : Type) : Type where
   field
@@ -80,30 +129,29 @@ record Listable (T L : Type) : Type where
 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)
+  ListListable : {T : Type} → Listable (List T) T
+  ListListable .enlist x = x
 
-infixr 10 _,_
+  IdListable : {T : Type} → Listable T T
+  IdListable .enlist x = x ∷ []
 
-<_&_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → AttrList → D → (y : HTMLTag) → {T (x == y)} → DOM
-< tag & attrs > inner </ tag′ > = element tag attrs (enlist inner) ∷ []
+  PairListable : {T L : Type} → ⦃ Listable T L ⦄ → Listable (L × T) L
+  PairListable .enlist (x , y) = x ∷ enlist y
 
-<_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → D → (y : HTMLTag) → {T (x == y)} → DOM
-< tag > inner </ tag′ > = element tag [] (enlist inner) ∷ []
+<_&_>_</_> : {Es As : Type} → ⦃ Listable Es Element ⦄ → ⦃ Listable As Attr ⦄ → (x : HTMLTag) → As → Es → (y : HTMLTag) → {T (x == y)} → Element
+< tag & attrs > inner </ tag′ > = element tag (enlist attrs) (enlist inner)
 
-<_&_/> :  (x : HTMLTag) → AttrList → DOM
-< tag & attrs /> = element tag attrs [] ∷ []
-
-<_/> : (x : HTMLTag) → DOM
-< tag /> = element tag [] [] ∷ []
+<_>_</_> : {Es : Type} → ⦃ Listable Es Element ⦄ → (x : HTMLTag) → Es → (y : HTMLTag) → {T (x == y)} → Element
+< tag > inner </ tag′ > = element tag [] (enlist inner)
 
+<_&_/> :  {As : Type} → ⦃ Listable As Attr ⦄ → (x : HTMLTag) → As → Element
+< tag & attrs /> = element tag (enlist attrs) []
 
+<_/> : (x : HTMLTag) → Element
+< tag /> = element tag [] []
 
 encode : List Char → String → String
 encode escapes text = fromList (concatMap (λ x → toList (escape-char x)) (toList text))
@@ -119,8 +167,8 @@ private
               ≡ "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)
+render-attr : Attr → String
+render-attr x = show (attr-name x) ++ˢ "=" ++ˢ encode (toList "\t\n\r \"'=<>`") (attr-value x)
 
 {-# TERMINATING #-} -- TODO: we should eliminate the tree as a traversable instead of doing it like this
 render-element : Element → String
@@ -130,16 +178,13 @@ render-element (element tag attrlist inner) =
   ++ˢ concatˢ (map render-element inner)
   ++ˢ "</" ++ˢ show tag ++ˢ ">"
 
-render-dom : DOM → String
-render-dom x = concatˢ (map render-element x)
-
-sample-dom : DOM
+sample-dom : Element
 sample-dom =
-  < html & lang ＝ "en" >
+  < 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" />
+      < meta & name= "description" , content= "Simple webpage rendered in Agda DSL" /> ,
+      < meta & name= "author" , content= "xenia" />
     </ head > ,
     < body >
       < p > "hello" </ p > ,
@@ -149,3 +194,5 @@ sample-dom =
       </ div >
     </ body >
   </ html >
+
+-}
diff --git a/src/HTML/Render.agda b/src/HTML/Render.agda
new file mode 100644
index 0000000..3bd219b
--- /dev/null
+++ b/src/HTML/Render.agda
@@ -0,0 +1,42 @@
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.Bool
+
+import Data.String as S
+import Data.List as L
+import Data.Char as C
+open S using (String)
+open L using (List)
+open C using (Char)
+
+open import HTML
+open import Base
+
+module HTML.Render where
+
+private
+  -- encodes using HTML decimal escapes (&#621;)
+  encode : List Char → String → String
+  encode escapes text = S.fromList (L.concatMap (λ x → S.toList (escape-char x)) (S.toList text))
+    where
+      escape-char : Char → String
+      escape-char ch =
+        if L.any (_== ch) escapes
+          then "&#" S.++ show (C.toℕ ch) S.++ ";"
+          else S.fromChar ch
+
+render-attr : Attribute → String
+render-attr x = x .name S.++ "=" S.++ encode (S.toList "\t\n\r \"'=<>`") (x .value)
+  where
+    open Attribute
+
+{-# 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 (S.toList "</>") x -- we don't technically need to escape all these characters, but it's easier to do this
+render-element (node tag inner) =
+  "<" S.++ tag .name S.++ S.concat (L.map (λ attr → " " S.++ render-attr attr) (tag .attributes)) S.++ ">"
+  S.++ S.concat (L.map render-element inner)
+  S.++ "</" S.++ tag .name S.++ ">"
+  where
+    open HTMLTag
+
diff --git a/src/HTML/Syntax.agda b/src/HTML/Syntax.agda
new file mode 100644
index 0000000..84a9f5b
--- /dev/null
+++ b/src/HTML/Syntax.agda
@@ -0,0 +1,103 @@
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.Product
+open import Data.Bool hiding (_<_)
+
+import Data.String as S
+import Data.List as L
+open S using (String)
+open L using (List)
+
+open import Base
+
+open import HTML
+
+module HTML.Syntax where
+
+module Attributes where
+  open HTMLTag
+  mkAttr : (name : String) → {T (valid-attribute-name name)} → HTMLTag → String → HTMLTag
+  mkAttr attr-name {attr-name-is-valid} tag value =
+    record tag
+    { attributes = record
+        { name = attr-name
+        ; value = value
+        ; name-is-valid = attr-name-is-valid
+        }
+        L.∷ tag .attributes
+    ; name = tag .name
+    ; name-is-valid = tag .name-is-valid
+    }
+
+  _id=_ = mkAttr "id"
+  infixl 20 _id=_
+  _class=_ = mkAttr "class"
+  infixl 20 _class=_
+  _style=_ = mkAttr "style"
+  infixl 20 _style=_
+  _lang=_ = mkAttr "lang"
+  infixl 20 _lang=_
+  _src=_ = mkAttr "src"
+  infixl 20 _src=_
+  _href=_ = mkAttr "href"
+  infixl 20 _href=_
+  _name=_ = mkAttr "name"
+  infixl 20 _name=_
+  _content=_ = mkAttr "content"
+  infixl 20 _content=_
+
+open Attributes hiding (mkAttr) public
+
+module Tags where
+  mkTag : (name : String) → {T (valid-tag-name name)} → HTMLTag
+  mkTag name {name-is-valid} = record { name = name ; attributes = L.[]; name-is-valid = name-is-valid }
+
+  html = mkTag "html"
+  body = mkTag "body"
+  head = mkTag "head"
+  meta = mkTag "meta"
+  title = mkTag "title"
+  img = mkTag "img"
+  p = mkTag "p"
+  span = mkTag "span"
+  footer = mkTag "footer"
+
+  open import Data.Nat
+  open import Relation.Binary.PropositionalEquality
+  postulate
+    h-is-valid : (x : ℕ) → T (valid-tag-name ("h" S.++ show x)) -- :3
+  h : ℕ → HTMLTag
+  h x = record
+    { name = "h" S.++ show x
+    ; attributes = L.[]
+    ; name-is-valid = h-is-valid x
+    }
+
+open Tags hiding (mkTag) public
+
+record DOMAble (T : Type) : Type where
+  field
+    endom : T → List Element
+open DOMAble ⦃...⦄
+
+instance
+  TextnodeDOMAble : DOMAble String
+  TextnodeDOMAble .endom x = textnode x L.∷ L.[]
+
+  ElementDOMAble : DOMAble Element
+  ElementDOMAble .endom e = e L.∷ L.[]
+
+  ListDOMAble : {T : Type} → ⦃ DOMAble T ⦄ → DOMAble (List T)
+  ListDOMAble .endom x = L.concatMap endom x
+
+  PairDOMAble : {T₀ T₁ : Type} → ⦃ DOMAble T₀ ⦄ → ⦃ DOMAble T₁ ⦄ → DOMAble (T₀ × T₁)
+  PairDOMAble .endom (x , y) = endom x L.++ endom y
+
+module Syntax where
+  open HTMLTag
+  <_>_</_> : {D : Type} → ⦃ DOMAble D ⦄ → (t₀ : HTMLTag) → D → (t₁ : HTMLTag) → {T (t₀ .name == t₁ .name)} → Element
+  < t₀ > sub </ t₁ > = node t₀ (endom sub)
+
+  <_/> : HTMLTag → Element
+  <_/> t = node t L.[]
+open Syntax public
diff --git a/src/Main.agda b/src/Main.agda
index 8e41683..95608bb 100644
--- a/src/Main.agda
+++ b/src/Main.agda
@@ -8,7 +8,7 @@ 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.Product using (_×_; proj₁; proj₂; _,_)
 open import Data.Nat hiding (_<_; _>_)
 open import Data.Unit using (⊤; tt)
 open import Data.Bool
@@ -23,7 +23,9 @@ open import NonEmpty
 open import Parse-HTTP
 open import Parse-HTTP.URL hiding (_/_)
 open import Parse-HTTP.Methods
-import HTML
+open import HTML
+import HTML.Syntax
+import HTML.Render
 import UTF-8
 
 response-with-content : ℕ → S.String → String → List Byte → List Byte
@@ -60,23 +62,29 @@ response-without-content status-code status =
 module Pages where
   open HTML
 
-  render-index : Maybe S.String → HTML.DOM
+  render-index : Maybe S.String → HTML.Element
   render-index query =
-    < html & lang ＝ "en" , style ＝ "color: yellow; background: black; padding: 1em;" >
+    < html lang= "en" style= "color: white; 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" />
+        < title > "henttp index" </ title > ,
+        < meta name= "description" content= "Simple webpage rendered in Agda DSL" /> ,
+        < meta name= "author" content= "xenia" />
       </ head > ,
       < body >
-        < h 1 > "hi" </ h 1 > ,
+        < h 1 >
+          < span style= "color: yellow;" > "hen" </ span > ,
+          < span style= "color: purple;" > "ttp" </ span >
+        </ h 1 > ,
         < p >
-          "welcome to the " ,
-          < span & style ＝ "color: white;" > "index" </ span > ,
-          (((λ q → < span & style ＝ "color: fuchsia;" > " (query = " , q , ")" </ span >) <$> query) or-else L.[])
-          </ p >
-      </ body >
+          "what is this?"
+        </ p >
+      </ body > ,
+      < footer >
+        "meow"
+      </ footer >
     </ html >
+    where
+      open HTML.Syntax
 
 handle-request : Request → IO (List Byte)
 handle-request req =
@@ -85,7 +93,7 @@ handle-request req =
       200-ok
         "text/html"
         (UTF-8.encode-string (S.toList (
-          HTML.render-dom (Pages.render-index (req .target .query))
+          HTML.Render.render-element (Pages.render-index (req .target .query))
         )))
       )
     else pure 404-not-found