diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index a698145..9d79088 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -13,6 +13,7 @@ import DocGen4.Output.NotFound
 import DocGen4.Output.Find
 import DocGen4.Output.SourceLinker
 import DocGen4.Output.ToJson
+import DocGen4.Output.FoundationalTypes
 import DocGen4.LeanInk.Process
 import Lean.Data.HashMap
 
@@ -32,6 +33,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   -- All the doc-gen static stuff
   let indexHtml := ReaderT.run index config |>.toString
   let notFoundHtml := ReaderT.run notFound config |>.toString
+  let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
   let navbarHtml := ReaderT.run navbar config |>.toString
   let docGenStatic := #[
     ("style.css", styleCss),
@@ -43,6 +45,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
     ("instances.js", instancesJs),
     ("importedBy.js", importedByJs),
     ("index.html", indexHtml),
+    ("foundational_types.html", foundationalTypesHtml),
     ("404.html", notFoundHtml),
     ("navbar.html", navbarHtml)
   ]
diff --git a/DocGen4/Output/FoundationalTypes.lean b/DocGen4/Output/FoundationalTypes.lean
new file mode 100644
index 0000000..6112832
--- /dev/null
+++ b/DocGen4/Output/FoundationalTypes.lean
@@ -0,0 +1,50 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Inductive
+
+namespace DocGen4.Output
+
+open scoped DocGen4.Jsx
+
+def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundational Type") do
+  pure <|
+    <div class="docfile">
+      <a id="top"></a>
+      <h1>Foundational Types</h1>
+
+      <p>Some of Lean's types are not defined in any Lean source files (even the <code>prelude</code>) since they come from its foundational type theory. This page provides basic documentation for these types.</p>
+      <p>For a more in-depth explanation of Lean's type theory, refer to
+      <a href="https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html">TPiL</a>.</p>
+      
+      
+      <h2 id="codesort-ucode"><code>Sort u</code></h2>
+      <p><code>Sort u</code> is the type of types in Lean, and <code>Sort u : Sort (u + 1)</code>.</p>
+      {← instancesForToHtml `_builtin_sortu}
+    
+      <h2 id="codetype-ucode"><code>Type u</code></h2>
+      <p><code>Type u</code> is notation for <code>Sort (u + 1)</code>.</p>    
+      {← instancesForToHtml `_builtin_typeu}
+      
+      <h2 id="codepropcode"><code>Prop</code></h2>
+      <p><code>Prop</code> is notation for <code>Sort 0</code>.</p>    
+      {← instancesForToHtml `_builtin_prop}
+    
+      <h2 id="pi-types-codeπ-a--α-β-acode">Pi types, <code>{"Π a : α, β a"}</code></h2>
+      <p>The type of dependent functions is known as a pi type.
+      Non-dependent functions and implications are a special case.</p>
+      <p>Note that these can also be written with the alternative notations:</p>
+      <ul>
+      <li><code>∀ a : α, β a</code>, conventionally used where <code>β a : Prop</code>.</li>
+      <li><code>α → γ</code>, possible only if <code>β a = γ</code> for all <code>a</code>.</li>
+      </ul>
+      <p>Lean also permits ASCII-only spellings of the three variants:</p>
+      <ul>
+      <li><code>Pi a : A, B a</code> for <code>{"Π a : α, β a"}</code></li>
+      <li><code>forall a : A, B a</code> for <code>{"∀ a : α, β a"}</code></li>
+      <li><code>A -&gt; B</code>, for <code>α → β</code></li>
+      </ul>
+      <p>Note that despite not itself being a function, <code>(→)</code> is available as infix notation for
+      <code>{"λ α β, α → β"}</code>.</p>    
+      -- TODO: instnaces for pi types 
+    </div>
+
+end DocGen4.Output
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index b12f125..7d27cc3 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -8,7 +8,7 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean
 
-def instancesForToHtml (typeName : Name) : HtmlM Html := do
+def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
   pure
     <details «class»="instances">
         <summary>Instances For</summary>
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index 5952b6d..f5d2612 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -69,6 +69,7 @@ def navbar : BaseHtmlM Html := do
         <nav class="nav">
           <h3>General documentation</h3>
           <div class="nav_link"><a href={s!"{←getRoot}"}>index</a></div>
+          <div class="nav_link"><a href={s!"{←getRoot}foundational_types.html"}>foundational types</a></div>
           /-
           TODO: Add these in later
           <div class="nav_link"><a href={s!"{←getRoot}tactics.html"}>tactics</a></div>