Data.Sigma

Definitions

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

  Dependent pairs

Totality: total
Visibility: public export
Constructor: 

(##) : (p1 : a) -> b p1 -> Σ a b

Projections:

.p1 : Σ a b -> a

  First projection of sigma

.p2 : ({rec:0} : Σ a b) -> b (p1 {rec:0})

  Second projection of sigma

.p1 : Σ a b -> a

  First projection of sigma

Visibility: public export

p1 : Σ a b -> a

  First projection of sigma

Visibility: public export

.p2 : ({rec:0} : Σ a b) -> b (p1 {rec:0})

  Second projection of sigma

Visibility: public export

p2 : ({rec:0} : Σ a b) -> b (p1 {rec:0})

  Second projection of sigma

Visibility: public export

Sigma : (a : Type) -> (a -> Type) -> Type

Visibility: public export

π1 : Σ a b -> a

Visibility: public export

.π1 : Σ a b -> a

Visibility: public export

π2 : (x : Σ a b) -> b (x .p1)

Visibility: public export

.π2 : (x : Σ a b) -> b (x .p1)

Visibility: public export

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

Visibility: public export