Spelling fixes

Author: brendanzab

experiments/idris/src/Fathom/Closed/InductiveRecursive.idr

@@ -2,15 +2,15 @@
 ||| the descriptions and their in-memory representation. This closely matches
 ||| the current implementation of format descriptions in Fathom.
 |||
-||| [Induction recusion](https://en.wikipedia.org/wiki/Induction-recursion) is
+||| [Induction recursion](https://en.wikipedia.org/wiki/Induction-recursion) is
 ||| where an inductive datatype is defined simultaneously with a function that
 ||| operates on that type (see the @Format and @Rep definitions below).
 |||
 ||| The universe is ‘closed’ in the sense tha new format descriptions cannot be
 ||| added to the type theory, although they can be composed out of other formats)
 |||
 ||| This is similar to the approach used when defining type theories with
-||| Tarski-style universes. In-fact inductive-recusrive datatypes as a language
+||| Tarski-style universes. In-fact inductive-recursive datatypes as a language
 ||| feature were apparently originally motivated by this use case (see: [“A
 ||| General Formulation of Simultaneous Inductive-Recursive Definitions in Type
 ||| Theory”](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.4575) by

experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr

@@ -1,4 +1,4 @@
-||| Experimenting with an approach to extending inductive-recusive format
+||| Experimenting with an approach to extending inductive-recursive format
 ||| descriptions with custom formats.
 
 module Fathom.Closed.InductiveRecursiveCustom
@@ -18,7 +18,7 @@ import Fathom.Base
 ||| A custom format description.
 |||
 ||| We’d prefer to just import `Fathom.Open.Record`, but Idris’ imports are a
-||| bit tempramental and result in ambiguities when importing modules that
+||| bit temperamental and result in ambiguities when importing modules that
 ||| contain types of the same name as those defined in the current module.
 public export
 record CustomFormat where

experiments/idris/src/Fathom/Open/Record.idr

@@ -1,11 +1,11 @@
 ||| Open format universe
 |||
 ||| This module defines an open universe of binary format descriptions using
-||| records to define an inderface. By defining formats in this way, the
+||| records to define an interface. By defining formats in this way, the
 ||| universe of formats is open to extension.
 |||
-||| I’m not sure, but this reminds me a little of the ‘coinductive universes’
-||| that [some type theorists were proposing for HoTT](https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-05-12.pdf#page=79),
+||| I’m not sure, but this reminds me a little of the ‘coinductively defined
+||| universes’ that [some type theorists were proposing](https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-05-12.pdf#page=79),
 ||| but I may be mistaken.
 
 module Fathom.Open.Record

experiments/idris/src/Playground.idr

@@ -13,7 +13,7 @@ import Fathom.Open.Record as Record
 -- Experiment with converting between the different styles of format universes
 
 
-||| Convert an inductive-recusive format universe into a record format
+||| Convert an inductive-recursive format universe into a record format
 public export
 format : IndRec.Format -> Record.Format
 format f = Record.MkFormat
@@ -23,7 +23,7 @@ format f = Record.MkFormat
   }
 
 
-||| Conver an indexed-inductive format universe into a record format
+||| Convert an indexed-inductive format universe into a record format
 public export
 formatOf : {Rep : Type} -> Indexed.FormatOf Rep -> Record.Format
 formatOf f = Record.MkFormat