[Agda] Parametricity is inconsistent with classical logic

[Peter Hancock]

On a related matter, if B is some notion of singleton-hood, 
or maybe double negation, or other `modality', and we would like it to interact
with Pi so that

  ((x : X)-> B (F x)) -> B((x : X)-> F x) 

? How should it behave wrt Sigma?  Might that be 

  B X -> ((x : X)-> B (F x)) -> B((Sigma x : X)F x)

? How should it behave wrt B? 

  ???? -> B (B X)

? Hank