
  0 | module Data.Sigma
  1 | 
  2 | import Data.Ops
  3 | 
  4 | ||| Dependent pairs
  5 | public export
  6 | record Σ (a : Type) (b : a -> Type) where
  7 |   constructor (##)
  8 |   ||| First projection of sigma
  9 |   π1 : a
 10 |   ||| Second projection of sigma
 11 |   π2 : b π1
 12 | 
 13 | public export
 14 | projBoth : (x : Σ a b) -> x.π1 ## x.π2 = x
 15 | projBoth (p1 ## p2) = Refl
 16 | 
 17 |