ExistentialsProjections.agda

-- 2010-09-29 Andreas, mail to Ulf

module ExistentialsProjections where

postulate
 .irrelevant : {A : Set} -> .A -> A

record Exists (A : Set) (P : A -> Set) : Set where
  constructor exists
  field
    .fwitness : A
    fcontent : P fwitness

.witness : forall {A P} -> (x : Exists A P) -> A
witness (exists a p) = irrelevant a

-- second projection out of existential is breaking abstraction, so should be forbidden

content : forall {A P} -> (x : Exists A P) -> P (witness x)
content (exists a p) = p  -- should not typecheck!!

{- We have p : P a != P (witness (exists a p)) = P (irrelevant a)
because a != irrelevant a.
-}