[Agda] Trust me regarding Dan Licata's trick

[Martin Escardo]

This is a suggestion/question regarding Dan Licata's trick in Agda:

http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/

I am interested in applying (and perhaps improving) Dan's trick to the
following situation.

Given a type X, we want to convert it into a type ||X|| which has the
same elements as X, but all of them become equal in
||X||. Intuitively, we quotient X by the indiscrete equivalence
relation that (propositionally) equates any two elements of X. This is
called the hpropositional truncation of X.

In particular, if 0 is the type with no elements, and 1 is the type
with one element, then ||X|| is isomorphic to 1 if X is inhabited, and
isomorphic to 0 otherwise. Because we don't have excluded middle, we
can't say that ||X|| is isomorphic to either 0 or 1, of course. But we
can (constructively) say that ||X|| has at most one element, in the
sense that any two of its elements are equal.

Cutting a long story short, this can be achieved via Licata's trick as
follows, where I use the notation of the HoTT Book for this
"truncation operation" (https://github.com/HoTT/book):

data _≡_ {X : Set} : X → X → Set where
   refl : {x : X} → x ≡ x

hprop : Set → Set
hprop X = (x y : X) → x ≡ y

private
   data ∥_∥' (X : Set) : Set where
     ∣_∣' : X → ∥ X ∥'

∥_∥ : Set → Set
∥_∥ = ∥_∥'

∣_∣ : {X : Set} → X → ∥ X ∥
∣_∣ = ∣_∣'

postulate
   hprop-|| : {X : Set} → (h k : ∥ X ∥) → h ≡ k

hinhabited-elim' : {X P : Set} → hprop P → (X → P) → ∥ X ∥ → P
hinhabited-elim' _ f ∣ x ∣' = f x

hinhabited-elim : {X : Set} {P : ∥ X ∥ → Set} → ((h : ∥ X ∥) → hprop(P 
h)) → ((x : X) → P ∣ x ∣) → (h : ∥ X ∥) → P h
hinhabited-elim _ f ∣ x ∣' = f x

This is very good, but we have one postulate left (as in Dan's
technique).

Can we get rid of this postulate?

Trust me, of rather primTrustMe, that we can:

http://code.haskell.org/Agda/doc/release-notes/2-2-6.txt
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism
http://www.cse.chalmers.se/~nad/listings/lib-0.7/Relation.Binary.PropositionalEquality.TrustMe.html

Unfortunately I can't be as concise as above, because primTrustMe
requires to both have universe levels declared and equality defined in
a particular way with particular pragmas, but still the following
should be somewhat readable:

private
  postulate Level : Set
  postulate zero : Level
  postulate suc  : Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}

data _≡_ {ℓ} {X : Set ℓ} (x : X) : X → Set ℓ where
   refl : x ≡ x

{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

private
  primitive
    primTrustMe : ∀{ℓ} {X : Set ℓ} {x y : X} → x ≡ y

hprop : Set → Set
hprop X = (x y : X) → x ≡ y

private
   data ∥_∥' (X : Set) : Set where
     ∣_∣' : X → ∥ X ∥'

∥_∥ : Set → Set
∥_∥ = ∥_∥'

∣_∣ : {X : Set} → X → ∥ X ∥
∣_∣ = ∣_∣'

truncation-is-hprop : {X : Set} → (h k : ∥ X ∥) → h ≡ k
truncation-is-hprop h k = primTrustMe

hinhabited-elim' : {X P : Set} → hprop P → (X → P) → ∥ X ∥ → P
hinhabited-elim' _ f ∣ x ∣' = f x

hinhabited-elim : {X : Set} {P : ∥ X ∥ → Set} → ((h : ∥ X ∥) → hprop(P 
h)) → ((x : X) → P ∣ x ∣) → (h : ∥ X ∥) → P h
hinhabited-elim _ f ∣ x ∣' = f x


So indeed it seems we can do away with postulates in our application
of Dan's trick.  However, the semantics of primTrustMe is barely
hinted in the Agda documentation.

So don't trust me.

Perhaps the designers of this Agda feature can explain to what extent
I am trustworthy in the above removal of a postulate from Dan's trick.

Clearly, this primTrustMe trick can also be blindly applied to Dan's
example in the above link. But does that make sense?

Best,
Martin
PS. I also hope I've managed to send this message with the right 
character encoding so that you are able to read it.