@@ -72,7 +72,7 @@ A type that is true is inhabited, that is, it can be constructed. An equality ty
72 onePlusOne : 1+1=2
72 onePlusOne : 1+1=2
73 onePlusOne = Refl
73 onePlusOne = Refl
75−So how can Refl, which is a constructor without any parameters, construct and equality type? If we type it on its own then it can't:
75+So how can Refl, which is a constructor without any parameters, construct an equality type? If we type it on its own then it can't:
77.. code-block:: idris
77.. code-block:: idris