@@ -788,7 +788,7 @@ as “sigma types”:
788788.. code-block:: idris
789789
790790 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
791− MkSigma : {P : A -> Type} -> (x : a) -> P x -> Sigma a P
791+ MkSigma : {P : a -> Type} -> (x : a) -> P x -> Sigma a P
792792
793793Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
794794of a pair of A and P, where the name ``a`` can occur inside ``P``.