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
