More typo fixes

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>

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>

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>
 

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>

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

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.

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>