
  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 |   p1 : a
 10 |   ||| Second projection of sigma
 11 |   p2 : b p1
 12 | 
 13 | public export
 14 | Sigma : (a : Type) -> (b : a -> Type) -> Type
 15 | Sigma = Σ
 16 | 
 17 | public export
 18 | π1 : Σ a b -> a
 19 | π1 = p1
 20 | 
 21 | public export
 22 | (.π1) : Σ a b -> a
 23 | (.π1) = p1
 24 | 
 25 | public export
 26 | π2 : (x : Σ a b) -> b x.p1
 27 | π2 = p2
 28 | 
 29 | public export
 30 | (.π2) : (x : Σ a b) -> b x.p1
 31 | (.π2) = p2
 32 | 
 33 | public export
 34 | projBoth : (x : Σ a b) -> x.π1 ## x.π2 = x
 35 | projBoth (p1 ## p2) = Refl
 36 | 
 37 |