[Agda] Trust me regarding Dan Licata's trick
drl at cs.cmu.edu
Sat Jun 15 14:44:44 CEST 2013
On Jun10, Martin Escardo wrote:
> hPropositionally truncated types are also known as bracket types in
> NuPrl, a well-known implementation of extensional type theory. You may
> wish to check Awodey and Bauer's paper "Propositions as [types]" for a
> theoretical treatment of bracket types in extensional type theory.
> It comes to me as a shock that introducing bracket types in
> intensional type theory so that canonicity is preserved is at least as
> hard, if not more, than introducing the axiom of function
> extensionality for dependent functions so that canonicity is
Interesting! That kind of makes sense, in retrospect, because bracket
types can be thought of as quotienting by the full relation, and, if I
recall correctly, quotients give you function extensionality.
(What kinds of quotients are used in the known proofs of this fact?)
Also, I think that some of the issues in this thread are related to the
1) hprops, or types where any two elements are propositionally equal
2) what one might call "strict hprops", or types where any two elements
are definitionally equal.
The rules for hprop-truncations that we use in HoTT are the "best way of
making any type into an hprop, in the sense of (1)". I think what you
have noticed in this thread is that a similar construct for "the best
way of making any type into a strict hprop, in the sense of (2)" has
some unexpected consequences.
More information about the Agda