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

Dan Licata drl at cs.cmu.edu
Fri Nov 23 14:54:18 CET 2012

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:

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


More information about the Agda mailing list