diff --git a/opetopic-play/app/views/docs/categories.scala.html b/opetopic-play/app/views/docs/categories.scala.html
index 0a3affdf..2dc6d43b 100644
--- a/opetopic-play/app/views/docs/categories.scala.html
+++ b/opetopic-play/app/views/docs/categories.scala.html
@@ -68,7 +68,7 @@ <h3 class="ui dividing header">Comparison with Baez-Dolan Opetopic Categories</h
       in a model category.  We think this makes the axiom reasonable
       from a theoretical point of view.  In compensation for this 
       strengthening of the axioms for a category, our definition of
-      universal properties are weaker that those given by Baez-Dolan.
+      universal properties are weaker than those given by Baez-Dolan.
       We will show later that under this stronger definition of category,
       we can recover the full strength of Baez-Dolan style universal cells.
     </p>
@@ -82,9 +82,9 @@ <h3 class="ui dividing header">Comparison with Baez-Dolan Opetopic Categories</h
       </div>
       <div class="right menu">
 	<div class="item">
-	  <a href="/docs/categories/categories" class="ui right labeled icon button">
+	  <a href="/docs/theory/units" class="ui right labeled icon button">
     	    <i class="right arrow icon"></i>
-    	    Next: Categories
+    	    Next: Identities and Units
 	  </a>
 	</div>
       </div>
diff --git a/opetopic-play/app/views/docs/complexes.scala.html b/opetopic-play/app/views/docs/complexes.scala.html
index 0e30fea5..de0ccf20 100644
--- a/opetopic-play/app/views/docs/complexes.scala.html
+++ b/opetopic-play/app/views/docs/complexes.scala.html
@@ -123,7 +123,7 @@ <h3 class="ui dividing header">Atomic Diagrams</h3>
 	  edge tree.
 	</div>
 	<div class="item">
-	  The box and edge trees are each <em>rooted</em>
+	  The box and edge trees are each <em>rooted</em>.
 	</div>
       </div>
     </div>
diff --git a/opetopic-play/app/views/docs/eqvs.scala.html b/opetopic-play/app/views/docs/eqvs.scala.html
index 85fd3713..024cd770 100644
--- a/opetopic-play/app/views/docs/eqvs.scala.html
+++ b/opetopic-play/app/views/docs/eqvs.scala.html
@@ -113,7 +113,7 @@ <h3 class="ui dividing header">Proof: ⇒</h3>
     @svg("eqvs/eta-tu.svg")
 
     <p>
-      Futhermore, since η is a unary, target universal cell, we conclude
+      Furthermore, since η is a unary, target universal cell, we conclude
       that it is an equivalence by the coinductive hypothesis.
     </p>
 
diff --git a/opetopic-play/app/views/docs/geometry.scala.html b/opetopic-play/app/views/docs/geometry.scala.html
index 2c569ec4..f4082122 100644
--- a/opetopic-play/app/views/docs/geometry.scala.html
+++ b/opetopic-play/app/views/docs/geometry.scala.html
@@ -50,7 +50,7 @@ <h3 class="ui dividing header">Dimension 1</h3>
     <h3 class="ui dividing header">Dimension 2</h3>
 
     <p>
-      Dimension 2 becomes more intersting: we already have infinitely
+      Dimension 2 becomes more interesting: we already have infinitely
       many opetopes of dimension two, one for each natural number
       which counts the number of source arrows.
     </p>
diff --git a/opetopic-play/app/views/docs/intro.scala.html b/opetopic-play/app/views/docs/intro.scala.html
index b2f06f53..16465903 100644
--- a/opetopic-play/app/views/docs/intro.scala.html
+++ b/opetopic-play/app/views/docs/intro.scala.html
@@ -25,7 +25,7 @@ <h2 class="ui dividing header">Introduction</h2>
       higher categories based on a collection of shapes called the
       <em>opetopes</em>.  It is probably fair to say that among the
       currently available approaches to higher category theory, the
-      opeoptic one is the among least well known.  This is not without
+      opetopic one is the among least well known.  This is not without
       some justification: indeed, finding a sufficiently rigorous
       definition of the opetopes has occupied a number of different
       authors, and the subtleties involved might leave one with the
diff --git a/opetopic-play/app/views/docs/opetopes.scala.html b/opetopic-play/app/views/docs/opetopes.scala.html
index aad88c33..8651fa89 100644
--- a/opetopic-play/app/views/docs/opetopes.scala.html
+++ b/opetopic-play/app/views/docs/opetopes.scala.html
@@ -111,7 +111,7 @@ <h3 class="ui header">Face</h3>
     <p>
       First of all, as you pass your mouse cursor over one of the cells,
       you will notice that a number of lower dimensional cells are highlighted.
-      These are exactly the faces of the face you are pointing at.  Futhermore
+      These are exactly the faces of the face you are pointing at.  Furthermore
       if you click on one of the faces, its opetopic structure will be 
       "extracted" into the bottom region, where you can verify that it also
       is an opetope in the sense defined above.
diff --git a/opetopic-play/app/views/docs/srccoh.scala.html b/opetopic-play/app/views/docs/srccoh.scala.html
index 1256c707..79c9c0da 100644
--- a/opetopic-play/app/views/docs/srccoh.scala.html
+++ b/opetopic-play/app/views/docs/srccoh.scala.html
@@ -80,7 +80,7 @@ <h3 class="ui dividing header">Proof</h3>
       From here, you have a bit of work, but it seems pretty likely
       that α and α-inv can be cancelled, resulting in just f and
       β as the exterior.  The result should now be that t, being
-      universal for this configuation admits a map to/from g ∘ γ.
+      universal for this configuration admits a map to/from g ∘ γ.
     </p>
 
   </div>