Commit cd5b4820 authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup

parent 9b914900
module Sigma.Operations
import Sigma.Sigma
public export
outl : {A : Type} -> {P : A -> Type} -> Sigma A P -> A
outl (MkSigma a _) = a
public export
outr : {A : Type} -> {P : A -> Type} -> (s : Sigma A P) -> P (outl s)
outr (MkSigma _ p) = p
module Sigma.Sigma
{-
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
---}
namespace Sigma
public export
record Sigma a (p : a -> Type) where
constructor MkSigma
fst : a
snd : p fst
> module Sigma.Sigma
> namespace Sigma
> public export
> record Sigma (A : Type) (P : A -> Type) where
> constructor MkSigma
> outl : A
> outr : P outl
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment