[Agda] Re: Agda Digest, Vol 87, Issue 24

[Dan Licata]

On Nov21, Martin Escardo wrote:
> In HoTT, and even before HoTT, people define a "proposition" not to be a 
> type, but instead a type with at most one element (suitably formulated). 
> One also considers the "propositional reflection" of any type (similar to 
> so-called bracket types), which hides (some part of the) computational 
> content. Denote the propositional reflection of a type X by X* or [X]. 
> Intuitively, X* is empty if X is empty, and X* has just one element if X* 
> is inhabited (the trick is how to say this without using excluded middle).

Just a HoTT-related terminological note: There's been some pushback on
using the word "proposition" exclusively to mean "hprop" (where a type A
is an hprop iff there is a term of type (x y : A) -> Id x y), which is
what Martin is doing above.  Mike Shulman has a nice summary here:
http://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html

The reason is that both the proof-relevant interpretation of logic
(forall=Pi/exists=Sigma) and the hprop interpretation of logic (using
bracket types for exists) are useful, and it's linguistically helpful to
use logical terminology for both.  And while it's very important to be
clear about which of the two you mean in a given context, I think it's a
bad idea to accomploish this by using logical terminology only for the
hprop interpretation.  I think Mike's suggestion of adverbs is much
better.

-Dan