Sigma.idr 307 Bytes
Newer Older
Nicola Botta's avatar
Nicola Botta committed
1
2
module Sigma.Sigma

Nicola Botta's avatar
Nicola Botta committed
3
{-
Nicola Botta's avatar
Nicola Botta committed
4
5
6
7

public export
data Sigma : (A : Type) -> (P : A -> Type) -> Type where
  MkSigma : {A : Type} -> {P : A -> Type} -> (x : A) -> (pf : P x) -> Sigma A P
Nicola Botta's avatar
Nicola Botta committed
8
9
10
11
12
13
14
15
16
17
18

---}

namespace Sigma
  public export
  record Sigma a (p : a -> Type) where
    constructor MkSigma
    fst : a
    snd : p fst