Data.Sigma

Definitions

record Σ : (a : Type) -> (a -> Type) -> Type

  Dependent pairs

Totality: total
Visibility: public export
Constructor: 

(##) : (π1 : a) -> b π1 -> Σ a b

Projections:

.π1 : Σ a b -> a

  First projection of sigma

.π2 : ({rec:0} : Σ a b) -> b (π1 {rec:0})

  Second projection of sigma

.π1 : Σ a b -> a

  First projection of sigma

Visibility: public export

π1 : Σ a b -> a

  First projection of sigma

Visibility: public export

.π2 : ({rec:0} : Σ a b) -> b (π1 {rec:0})

  Second projection of sigma

Visibility: public export

π2 : ({rec:0} : Σ a b) -> b (π1 {rec:0})

  Second projection of sigma

Visibility: public export

projBoth : (x : Σ a b) -> x .π1 ## x .π2 = x

Visibility: public export