[Agda] Trust me regarding Dan Licata's trick
Dan Licata
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
> preserved.
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
distinction between:
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.
-Dan
More information about the Agda
mailing list