diff --git a/.gitignore b/.gitignore
index 3fb4cf6cb..03d669448 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 .lake/
 docbuild/lake-manifest.json
 docbuild/lean-toolchain
-html/
\ No newline at end of file
+html/
+/KernelHomManual.lean
\ No newline at end of file
diff --git a/KernelHom/Tactic/Hom/KernelDiagram.lean b/KernelHom/Tactic/Hom/KernelDiagram.lean
index 9c5de7478..d8c1eb20f 100644
--- a/KernelHom/Tactic/Hom/KernelDiagram.lean
+++ b/KernelHom/Tactic/Hom/KernelDiagram.lean
@@ -60,10 +60,6 @@ def Node.toPenroseVar_kernel (n : Node) : MetaM PenroseVar := do
       pure n.e
   return ⟨"E", [n.vPos, n.hPosSrc, n.hPosTar], expr⟩
 
-def Strand.toPenroseVar_kernel (s : Strand) : MetaM PenroseVar := do
-  let expr := Expr.const ``True []
-  return ⟨"f", [s.vPos, s.hPos], expr ⟩
-
 open scoped Jsx in
 /-- Construct a kernelized string diagram from a Penrose `sub`stance program and
 expressions `embeds` to display as labels in the diagram. -/
@@ -88,7 +84,7 @@ def mkKernelDiagram (nodes : List (List Node)) (strands : List (List Strand)) :
   /- Add 1-morphisms as strings. -/
   for l in strands do
     for s in l do
-      StringDiagram.addConstructor "Mor1" (← s.toPenroseVar_kernel)
+      StringDiagram.addConstructor "Mor1" s.toPenroseVar
         "MakeString" [← s.startPoint.toPenroseVar_kernel, ← s.endPoint.toPenroseVar_kernel]
 
 end Mathlib.Tactic.Widget.StringDiagram
diff --git a/Verso/KernelHomManual/Front.lean b/KernelHomManual/Front.lean
similarity index 100%
rename from Verso/KernelHomManual/Front.lean
rename to KernelHomManual/Front.lean
diff --git a/Verso/KernelHomManual.lean b/KernelHomManual/Manual.lean
similarity index 100%
rename from Verso/KernelHomManual.lean
rename to KernelHomManual/Manual.lean
diff --git a/Verso/KernelHomManual/Pages/CatTactics.lean b/KernelHomManual/Pages/CatTactics.lean
similarity index 100%
rename from Verso/KernelHomManual/Pages/CatTactics.lean
rename to KernelHomManual/Pages/CatTactics.lean
diff --git a/Verso/KernelHomManual/Pages/Examples.lean b/KernelHomManual/Pages/Examples.lean
similarity index 100%
rename from Verso/KernelHomManual/Pages/Examples.lean
rename to KernelHomManual/Pages/Examples.lean
diff --git a/Verso/KernelHomManual/Pages/HomKernel.lean b/KernelHomManual/Pages/HomKernel.lean
similarity index 100%
rename from Verso/KernelHomManual/Pages/HomKernel.lean
rename to KernelHomManual/Pages/HomKernel.lean
diff --git a/Verso/KernelHomManual/Pages/KernelHom.lean b/KernelHomManual/Pages/KernelHom.lean
similarity index 100%
rename from Verso/KernelHomManual/Pages/KernelHom.lean
rename to KernelHomManual/Pages/KernelHom.lean
diff --git a/Verso/KernelHomManual/Pages/MonoidalComp.lean b/KernelHomManual/Pages/MonoidalComp.lean
similarity index 100%
rename from Verso/KernelHomManual/Pages/MonoidalComp.lean
rename to KernelHomManual/Pages/MonoidalComp.lean
diff --git a/Verso/KernelHomManual/Pages/Universe.lean b/KernelHomManual/Pages/Universe.lean
similarity index 100%
rename from Verso/KernelHomManual/Pages/Universe.lean
rename to KernelHomManual/Pages/Universe.lean
diff --git a/Verso/KernelHomManual/Papers.lean b/KernelHomManual/Papers.lean
similarity index 100%
rename from Verso/KernelHomManual/Papers.lean
rename to KernelHomManual/Papers.lean
diff --git a/Verso/KernelHomManual/Tools/Assets/infoview-shim.js b/KernelHomManual/Tools/Assets/infoview-shim.js
similarity index 100%
rename from Verso/KernelHomManual/Tools/Assets/infoview-shim.js
rename to KernelHomManual/Tools/Assets/infoview-shim.js
diff --git a/Verso/KernelHomManual/Tools/Assets/string-diagram-host.js b/KernelHomManual/Tools/Assets/string-diagram-host.js
similarity index 100%
rename from Verso/KernelHomManual/Tools/Assets/string-diagram-host.js
rename to KernelHomManual/Tools/Assets/string-diagram-host.js
diff --git a/Verso/KernelHomManual/Tools/Assets/string-diagram-loader.js b/KernelHomManual/Tools/Assets/string-diagram-loader.js
similarity index 100%
rename from Verso/KernelHomManual/Tools/Assets/string-diagram-loader.js
rename to KernelHomManual/Tools/Assets/string-diagram-loader.js
diff --git a/Verso/KernelHomManual/Tools/Assets/string-diagram-widget.js b/KernelHomManual/Tools/Assets/string-diagram-widget.js
similarity index 100%
rename from Verso/KernelHomManual/Tools/Assets/string-diagram-widget.js
rename to KernelHomManual/Tools/Assets/string-diagram-widget.js
diff --git a/Verso/KernelHomManual/Tools/LeanDecl.lean b/KernelHomManual/Tools/LeanDecl.lean
similarity index 100%
rename from Verso/KernelHomManual/Tools/LeanDecl.lean
rename to KernelHomManual/Tools/LeanDecl.lean
diff --git a/Verso/KernelHomManual/Tools/VersoKernelDiagram.lean b/KernelHomManual/Tools/VersoKernelDiagram.lean
similarity index 98%
rename from Verso/KernelHomManual/Tools/VersoKernelDiagram.lean
rename to KernelHomManual/Tools/VersoKernelDiagram.lean
index ffa3979aa..dde260371 100644
--- a/Verso/KernelHomManual/Tools/VersoKernelDiagram.lean
+++ b/KernelHomManual/Tools/VersoKernelDiagram.lean
@@ -111,7 +111,7 @@ block_extension Block.stringDiagramWidget (payload : StringDiagramPayload) where
         match FromJson.fromJson? (α := StringDiagramPayload) data with
         | .ok payload => pure payload
         | .error err =>
-          Verso.Doc.Html.HtmlT.logError s!"Could not deserialize string diagram payload: {err}"
+          Verso.reportError s!"Could not deserialize string diagram payload: {err}"
           pure {
             html := Json.null,
             diagramHash := 0,
diff --git a/build_manual.sh b/build_manual.sh
index b1bdd7487..558c9c349 100755
--- a/build_manual.sh
+++ b/build_manual.sh
@@ -1,9 +1,9 @@
 set -x -e
 
-rm -rf _out html
+rm -rf _out html KernelHomManual.lean
 lake exe manual
 mkdir html
 mv _out/html-multi/* html/
 rm -rf _out
 mkdir -p html/static
-cp Verso/static_files/* html/static
\ No newline at end of file
+cp verso_static_files/* html/static
\ No newline at end of file
diff --git a/lakefile.toml b/lakefile.toml
index 76adaf1c8..bae7f44aa 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -27,10 +27,9 @@ globs = ["KernelHomTests.+"]
 
 [[lean_lib]]
 name = "KernelHomManual"
-srcDir = "Verso/"
-root = "KernelHomManual"
+globs = ["KernelHomManual.+"]
 
 [[lean_exe]]
 name = "manual"
-srcDir = "Verso/"
-root = "KernelHomManual"
+srcDir = "KernelHomManual/"
+root = "Manual"
diff --git a/Verso/static_files/FiraCode-Regular.ttf b/verso_static_files/FiraCode-Regular.ttf
similarity index 100%
rename from Verso/static_files/FiraCode-Regular.ttf
rename to verso_static_files/FiraCode-Regular.ttf
diff --git a/Verso/static_files/diagram.svg b/verso_static_files/diagram.svg
similarity index 100%
rename from Verso/static_files/diagram.svg
rename to verso_static_files/diagram.svg
diff --git a/Verso/static_files/favicon.svg b/verso_static_files/favicon.svg
similarity index 100%
rename from Verso/static_files/favicon.svg
rename to verso_static_files/favicon.svg
diff --git a/Verso/static_files/scripts.js b/verso_static_files/scripts.js
similarity index 100%
rename from Verso/static_files/scripts.js
rename to verso_static_files/scripts.js
diff --git a/Verso/static_files/style.css b/verso_static_files/style.css
similarity index 100%
rename from Verso/static_files/style.css
rename to verso_static_files/style.css