> module Sigma.Sigma > namespace Sigma > public export > record Sigma (A : Type) (P : A -> Type) where > constructor MkSigma > outl : A > outr : P outl
