@@ -36,7 +36,8 @@ namespace Builtins
3636 ||| it. Another way to see dependent pairs is as just data - for instance, the
3737 ||| length of a vector paired with that vector.
3838 |||
39− ||| @ a the type of the witness @ P the type of the proof
39+ ||| @ a the type of the witness
40+ ||| @ P the type of the proof
4041 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
4142 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
4243