
  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 | %pair Σ π1 π2
 14 | 
 15 | public export
 16 | record SigEq (a, b : Σ f s) where
 17 |   constructor MkSigEq
 18 |   fstEq : a.π1 === b.π1
 19 |   sndEq : a.π2 === replace {p = s} (sym fstEq) b.π2
 20 | 
 21 | export
 22 | 0 sigEqToEq : SigEq a b -> a === b
 23 | sigEqToEq {a = _ ## _} {b = _ ## _} (MkSigEq Refl Refl) = Refl
 24 | 
 25 |