[Agda] Parametricity is inconsistent with classical logic
Peter Hancock
hancock at spamcop.net
Thu May 10 13:08:25 CEST 2012
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
More information about the Agda
mailing list