Initial.

Exists/Operations.lidr

+> module Exists.Operations
+
+
+> import Pairs.Operations
+
+
+> %default total
+
+> %access public export
+
+
+> |||
+> outl : {A : Type} -> {P : A -> Type} -> Exists {a = A} P -> A
+> outl = getWitness
+
+
+> |||
+> outr : {A : Type} -> {P : A -> Type} -> (s : Exists {a = A} P) -> P (outl s)
+> outr = getProof
+
+