[Agda] Trust me regarding Dan Licata's trick

[Guillaume Brunerie]

Hi Martin,

I’m not sure I understand what you are trying to do.
I don’t really know what primTrustMe is, but it seems to be some kind
of postulate that every type is an hprop, which seems much worse than
just postulating that a single type is an hprop.

What are you trying to achieve exactly?

Guillaume

2013/6/4 Martin Escardo <m.escardo at cs.bham.ac.uk>:
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda