# [Agda] Trust me regarding Dan Licata's trick

Martin Escardo m.escardo at cs.bham.ac.uk
Fri Jun 7 22:19:00 CEST 2013

What is disturbing about hpropositional truncation is this:

We want the type (p q : || X ||) -> p == q to be inhabited, where "=="
is propositional equality.

But, if we take ||-|| as primitive, we don't want to have a constant for
that equality: how would we compute with it? What would J do to it?

So the easiest way out seems to add a rule to the theory extended with a
constructor ||-|| stipulating that all elements of ||X|| are
definitionally equal. You are saying that this way out is too
optimistic, as you would get, under univalence,

Unit = (Unit -> Unit)

definitionally, which doesn't sound right, and I agree.

So it seems that adding ||-|| as primitive poses the same problems as
adding functional extensionality or more generally univalence.

(Hence I take back my triviality hope of my previous message.)

You posit equalities that don't come from refl, and at the same time you
want to have J determined by its action on refl.

If not all points of ||X|| are definitionally equal, we are forced to
write equations for the postulated inhabitant of (p q : || X ||) -> p ==
q. I have no clue what they ought to be.

Best,
Martin

On 07/06/13 20:56, Guillaume Brunerie wrote:
> Do you also want the same elimination and computation rules as before?
> Again, that may be problematic when combined with univalence.
> Assuming univalence, the type Contr of small contractible types is a
> proposition.
> Hence you can define a map f from the truncation of Bool to
> Contr sending true to Unit and false to Unit -> Unit.
>
> Then, by the usual computation rule for truncation, you get f | true | =
> Unit.
> But | true | = | false |, hence
>
>    Unit = f | true | = f | false | = Unit -> Unit
>
> (all equalities are definitional here).
>
> It's not a contradiction yet, but having Unit and Unit -> Unit
> definitionally equal is already quite strange.

> Guillaume
>
> On Jun 7, 2013 4:13 PM, "Martin Escardo" <m.escardo at cs.bham.ac.uk
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
>
>     Summary of discussion:
>     ---------------------
>
>     * primTrustMe doesn't do what I wanted.
>
>     I wanted to identify all elements of any given type, definitionally,
>     so as to get an Agda implementation of hpropositional truncation
>     that fully computes, by replacing a postulate in Dan's trick with
>     primTrustMe.
>
>     For my purposes, I will use Dan's trick, as originally stated by
>     him, with a postulate for identifying all points of || X ||.
>
>     * Advantage (Dan's original point in
>     http://homotopytypetheory.org/__2011/04/23/running-circles-__around-in-your-proof-__assistant/
>     <http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/>):
>
>
>          The elimination-rule equation for hpropositional truncation holds
>          definitionally rather than just propositionally.
>
>     This is precisely what I need to get my proofs accepted. (And what
>     he and other people needed to get their proofs accepted in the
>     presence of higher-inductive types (HIT's) for lines, circles,
>     spheres etc.)
>
>     * Disadvantage (again in Dan's original post):
>
>           We lose canonicity if we use || - ||, because there is a
>           postulate. (And we may gain SegFault if we attempt to fix this by
>           using primTrustMe).
>
>     I can live with that, using a postulate as Dan originally did,
>     rather than my failed attempt with primTrustMe, waiting for the
>     computational open problems in univalent foundations to be sorted
>     out. primTrustMe can't solve them in this particular case, it seems.
>
>     But I have the feeling that it should be trivial to extend Agda with
>     a type constructor for hpropositional truncation so that canonicity
>     is preserved (but primTrustMe doesn't seem to be the answer).
>
>     Best,
>     Martin
>
>
>     On 07/06/13 13:00, Guillaume Brunerie wrote:
>
>
>         On Jun 7, 2013 5:40 AM, "Martin Escardo"
>         <m.escardo at cs.bham.ac.uk <mailto:m.escardo at cs.bham.ac.uk>
>         <mailto:m.escardo at cs.bham.ac.__uk
>         <mailto:m.escardo at cs.bham.ac.uk>>> wrote:
>           >
>           >
>           >
>           > On 06/06/13 19:57, Guillaume Brunerie wrote:
>           >>
>           >> This is a natural number which should normalise to 0 if you
>         have
>           >> canonicity, but it doesn't, even if you use primTrustMe.
>           >> (on the other hand if you *compile* it, then it will
>         compute to 0,
>           >
>           >
>           > It is a bit disturbing that the normalization for type
>         checking is
>         different from the normalization given by compilation for
>         running terms.
>
>         One difference between normalization and compilation is that
>         when you
>         run a program you are guaranteed to be in the empty context whereas
>         normalization also happens in non empty contexts.
>
>           >> but
>           >> combining that with univalence you can easily get a segfault)
>           >
>           >
>           > I want to understand this more precisely, because univalence is
>         compatible with hpropositional truncation. Perhaps you are just
>         saying
>         that we cannot have all points of the truncation to be
>         definitionally
>         equal under univalence: the type checking is right (because it
>         doesn't
>         believe me when I ask to be trusted), but the compilation is
>         wrong (for
>         univalent foundations).
>
>         Univalence is compatible with truncation but not with primTrustMe.
>         PrimTrustMe is based on the fact that in the empty context the only
>         proof of equality should be refl, which is not compatible with
>         univalence.
>
>         Here is how I think you can get a segfault using the interval (I
>         haven't
>         managed to actually get the segfault because I don't understand
>         how to
>         compile an Agda program yet). You can probably adapt it to
>         truncations
>         if you want.
>
>         Assuming univalence, the types Unit and Unit -> Unit are equivalent.
>         Hence there is a dependent type over I whose fiber over 0 is
>         Unit and
>         whose fiber over 1 is Unit -> Unit.
>         Then you can take the canonical element tt of Unit, transport it
>         along
>         the path of the interval (so that you get a function of type Unit ->
>         Unit) and apply it to tt.
>         What I think will happen if you try to compile it is that the
>         path of
>         the interval will be compiled to refl, hence the transport is
>         just the
>         identity so the program will try to apply the "function" tt to the
>         argument tt, which is obviously problematic.
>
>           > Anyway, if trustMe does work as a postulate as claimed
>         earlier, why
>         is it needed/useful at all?
>
>         My impression is that it can be used to get some unsafe coercion
>         between
>         arbitrary types, like Obj.magic in OCaml.
>
>         Guillaume
>
>           >> On Jun 6, 2013 3:20 PM, "Martin Escardo"
>         <m.escardo at cs.bham.ac.uk <mailto:m.escardo at cs.bham.ac.uk>
>         <mailto:m.escardo at cs.bham.ac.__uk <mailto:m.escardo at cs.bham.ac.uk>>
>           >> <mailto:m.escardo at cs.bham.ac.__uk
>         <mailto:m.escardo at cs.bham.ac.uk>
>         <mailto:m.escardo at cs.bham.ac.__uk
>         <mailto:m.escardo at cs.bham.ac.uk>>>>
>         wrote:
>           >>
>           >>
>           >>
>           >>     On 06/06/13 16:16, Guillaume Brunerie wrote:
>           >>
>           >>         Are you planning to compile such code?
>           >>
>           >>
>           >>     Not necessarily, but I want to normalize closed terms
>         of e.g.
>           >>     natural number type.
>           >>
>           >>     When I say that I want a definition that computes, I
>         mean that the
>           >>     addition of this construction should preserve
>         canonicity (say for
>           >>     closed terms of natural number type).
>           >>
>           >>         It doesn't really seem safe to me to compile all
>           >>         truncation-is-hprop to
>           >>         refl, especially when combined with univalence.
>           >>         As far as I understand, it only affects the
>         compiler (not the
>           >>         normalisation procedure in the type checker), so
>         maybe it's safe
>           >>         if you
>           >>         just want to type-check code.
>           >>
>           >>
>           >>     If I wanted to just type check, then postulates would
>         be enough.
>           >>
>           >>         For the interval, given that the two endpoints are not
>           >>         definitionally
>           >>         equal, I don't think there is any difference with
>         the version
>           >>         using a
>           >>         postulate (unless you compile the code, in which case
>         strange things
>           >>         might happen)
>           >>
>           >>
>           >>     Well, I would be very surprised if it works, because
>         the interval
>           >>     gives you functional extensionality, and it would be
>         too easy to get
>           >>     that from data abstraction + primTrustMe in such a way that
>           >>     canonicity is preserved.
>           >>
>           >>     Best,
>           >>     Martin
>           >>
>           >>
>           >>
>           >>         On Jun 6, 2013 8:35 AM, "Martin Escardo"
>           >>         <m.escardo at cs.bham.ac.uk
>         <mailto:m.escardo at cs.bham.ac.uk>
>         <mailto:m.escardo at cs.bham.ac.__uk <mailto:m.escardo at cs.bham.ac.uk>>
>         <mailto:m.escardo at cs.bham.ac.__uk
>         <mailto:m.escardo at cs.bham.ac.uk>
>         <mailto:m.escardo at cs.bham.ac.__uk <mailto:m.escardo at cs.bham.ac.uk>>>
>           >>         <mailto:m.escardo at cs.bham.ac
>         <mailto:m.escardo at cs.bham.ac>. <mailto:m.escardo at cs.bham.ac
>         <mailto:m.escardo at cs.bham.ac>.>____uk
>           >>
>           >>         <mailto:m.escardo at cs.bham.ac.__uk
>         <mailto:m.escardo at cs.bham.ac.uk>
>         <mailto:m.escardo at cs.bham.ac.__uk
>         <mailto:m.escardo at cs.bham.ac.uk>>>>> wrote:
>           >>
>           >>              Hi Dan,
>           >>
>           >>              On 05/06/13 17:41, Dan Licata wrote:
>           >>
>           >>                  As far as I understand it,
>           >>                  primTrustMe is a way of asserting an
>         equality, which is
>           >>         slightly
>           >>                  better
>           >>                  than a postulate because when it has type
>         x = x , it
>           >>         reduces to
>           >>                  refl.
>           >>
>           >>               > [...]
>           >>
>           >>                  I would guess that what you're doing below
>         is OK:  For
>           >>         the usual
>           >>                  definition of ∥ X ∥ as a higher inductive
>         type,
>           >>
>           >>                  (x : ∥ X ∥) (p : Id x x) -> Id p refl
>           >>
>           >>                  will be propositionally true, (∥ X ∥ is an
>         hprop, and
>           >>         therefore an
>           >>                  hset).
>           >>
>           >>
>           >>              Yes, that's precisely my intuition. But this
>         intuition
>           >>         would work
>           >>              for the interval too, because it is an hprop
>         and hence an
>           >>         hset, but
>           >>              I don't think this trick would work for the
>         interval. Or
>           >>         would it?
>           >>
>           >>                  Using primTrustMe will strictify certain
>         instances of
>           >>         this (the
>           >>                  ones where p is constructed by applying
>           >>         truncation-is-hprop to
>           >>                  definitionally equal arguments) to
>         definitional
>           >>         equalities.  Off the
>           >>                  top of my head, I don't see why that would
>         go wrong.
>           >>
>           >>
>           >>              I agree. But it would be nice to hear from
>         those who
>           >>         designed and
>           >>              implemented the feature.
>           >>
>           >>                  On the other hand, using primTrustMe to
>         implement the
>           >>         circle or
>           >>                  something like that would be bad: if loop
>         : Id{S1} base
>           >>         base
>           >>                  is defined to be primTrustMe, it will
>         reduce to refl.
>           >>
>           >>
>           >>              I agree too.
>           >>
>           >>              Best,
>           >>              Martin
>           >>
>           >>
>           >>                  -Dan
>           >>
>           >>                  On Jun05, Martin Escardo wrote:
>           >>
>           >>
>           >>                      On 05/06/13 03:12, Guillaume Brunerie
>         wrote:
>           >>
>           >>                          I’m not sure I understand what you
>         are trying
>           >>         to do.
>           >>
>           >>
>           >>                      I am trying to use an unsound Agda
>         feature to
>           >>         implement a sound
>           >>                      construction (hpropositional reflection or
>         truncation).
>           >>
>           >>                          I don’t really know what
>         primTrustMe is,
>           >>
>           >>
>           >>                      Me neither, and this is why I asked
>         the question
>           >>         here. The
>           >>                      documentation
>           >>
>           >>
>           >>
>           >>
>           >>
>           >>
>           >>                      says:
>           >>
>           >>                          "Note that the compiler replaces
>         all uses of
>           >>         primTrustMe
>           >>                      with the
>           >>                          REFL builtin, without any check for
>         definitional
>           >>                      equality. Incorrect
>           >>                          uses of primTrustMe can
>           >>         segfaults or
>           >>                      similar
>           >>                          problems."
>           >>
>           >>                      However, It Doesn't say what the
>         correct uses are
>           >>         meant to be.
>           >>
>           >>                          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.
>           >>
>           >>
>           >>                      Yes, but notice that I use it privately,
>         hopefully in a
>           >>                      sound way.
>           >>
>           >>                          What are you trying to achieve
>         exactly?
>           >>
>           >>
>           >>                      I am trying to (soundly) implement
>         hpropositional
>           >>         truncation
>           >>                      that
>           >>                      computes, without *any* postulate at all.
>           >>
>           >>                      Voevodsky's Coq implementation uses
>         type-in-type (also
>           >>                      unsound in
>           >>                      general, but backed by sound resizing
>         axioms in
>           >>         this case) and
>           >>                      additionally postulates the axiom of
>         function
>           >>         extensionality
>           >>                      to show
>           >>                      that the truncation really is an
>         hproposition.
>           >>
>           >>                      Here is an improved version of what I sent
>           >>         yesterday, with more
>           >>                      explanations, and the main question
>         repeated.
>           >>
>           >>                      Best,
>           >>                      Martin
>           >>
>           >>
>         ------------------------------______--------------------------__--__--__-------
>           >>
>           >>                      Here is what we want to achieve:
>           >>
>           >>                      Given a type X, we want to construct a
>         type ∥ X ∥:
>           >>
>           >>                                   X type
>           >>                                 ----------
>           >>                                  ∥ X ∥ type
>           >>
>           >>                      We want any two elements of ∥ X ∥ to be
>         propositionally
>           >>                      equal, written
>           >>                      hprop ∥ X ∥.
>           >>
>           >>                      We have the introduction rule:
>           >>
>           >>                                       x : X
>           >>                                  ---------------
>           >>                                    ∣ x ∣ :  ∥ X ∥
>           >>
>           >>                      The elimination rule or induction
>         principle, for
>           >>         any P : ∥ X
>           >>                      ∥ → Set:
>           >>
>           >>                             g : (h : ∥ X ∥) → hprop(P h)  f
>         : ((x : X) →
>           >>         P ∣ x ∣)
>           >>
>           >>
>         ------------------------------______------------------------
>           >>
>           >>                                   elim g f : (h : ∥ X ∥) → P h
>           >>
>           >>                      The computation rule:
>           >>
>           >>                             elim g f ∣ x ∣ = f x
>           >>
>           >>                      Thus this is a bracket type that
>         allows us to get
>           >>         out of it,
>           >>                      provided
>           >>                      the target has at most one element (is an
>           >>         hproposition).
>           >>
>           >>                      Here is the tentative implementation:
>           >>
>           >>                      \begin{code}
>           >>
>           >>                      module
>         hpropositionalTruncationTentat______ive where
>           >>
>           >>
>           >>                      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 #-}
>           >>
>           >>                      \end{code}
>           >>
>           >>                      This is unsound, but we try to use it
>         to perform a
>           >>         sound
>           >>                      construction:
>           >>
>           >>                      \begin{code}
>           >>
>           >>                      private
>           >>                         primitive
>           >>                           primTrustMe : ∀{ℓ} {X : Set ℓ} {x
>         y : X} →
>         x ≡ y
>           >>
>           >>                      \end{code}
>           >>
>           >>                      Notice that we keep the above private
>         to the
>           >>         module, so that the
>           >>                      unsoundness doesn't leak to modules
>         that use this
>           >>         module but no
>           >>                      unsound Agda features.
>           >>
>           >>                      The first part is Dan Licata's trick. We
>         implement the
>           >>                      hpropositional
>           >>                      truncation of ∥ X ∥ as X itself, or
>         rather its
>           >>         isomorphic
>           >>                      copy ∥ X
>           >>                      ∥',
>           >>                      which is kept private to the module:
>           >>
>           >>                      \begin{code}
>           >>
>           >>                      private
>           >>                          data ∥_∥' (X : Set) : Set where
>           >>                            ∣_∣' : X → ∥ X ∥'
>           >>
>           >>                      ∥_∥ : Set → Set
>           >>                      ∥_∥ = ∥_∥'
>           >>
>           >>                      ∣_∣ : {X : Set} → X → ∥ X ∥
>           >>                      ∣_∣ = ∣_∣'
>           >>
>           >>                      hprop : Set → Set
>           >>                      hprop X = (x y : X) → x ≡ y
>           >>
>           >>                      truncation-rec : {X P : Set} → hprop P
>         → (X → P) →
>           >>         ∥ X ∥ → P
>           >>                      truncation-rec _ f ∣ x ∣' = f x
>           >>
>           >>                      truncation-ind : {X : Set} {P : ∥ X ∥
>         → Set} → ((h
>           >>         : ∥ X ∥)
>           >>                                       → hprop(P h)) → ((x :
>         X) → P ∣ x
>           >>         ∣) → (h : ∥ X
>           >>                      ∥) → P h
>           >>                      truncation-ind _ f ∣ x ∣' = f x
>           >>
>           >>                      \end{code}
>           >>
>           >>                      The above -rec and -ind are the
>         non-dependent and
>           >>         dependent
>           >>                      elimination rules respectively.
>           >>
>           >>                      The crucial requirement is that ∥ X ∥
>         is to be an
>           >>                      hproposition. We can
>           >>                      achieve this with a postulate, but
>         postulates don't
>           >>         compute.
>           >>                      To try to
>           >>                      get an implementation that fully
>         computes, we
>           >>         privately use
>           >>                      the above
>           >>                      generally unsound feature:
>           >>
>           >>                      \begin{code}
>           >>
>           >>                      truncation-is-hprop : {X : Set} →
>         hprop ∥ X ∥
>           >>                      truncation-is-hprop _ _ = primTrustMe
>           >>
>           >>                      \end{code}
>           >>
>           >>                      Is that sound? The semantics of
>         primTrustMe is not
>           >>         clearly
>           >>                      given in
>           >>                      the documentation.
>           >>
>           >>                      NB. Of course, we can make one
>         parameter of the
>           >>         elimination rule
>           >>                      computationally irrelevant:
>           >>
>           >>                      \begin{code}
>           >>
>           >>                      Truncation-elim' : {X P : Set} →
>         .(hprop P) → (X →
>           >>         P) → ∥ X ∥
>           >>                      → P
>           >>                      Truncation-elim' _ f ∣ x ∣' = f x
>           >>
>           >>                      Truncation-elim : {X : Set} {P : ∥ X ∥
>         → Set} →
>           >>         .((h : ∥ X ∥)
>           >>                      → hprop(P h)) → ((x : X) → P ∣ x ∣) →
>         (h : ∥ X
>         ∥) → P h
>           >>                      Truncation-elim _ f ∣ x ∣' = f x
>           >>
>           >>                      \end{code}
>           >>
>           _____________________________________________________
>           >>
>           >>                      Agda mailing list
>           >> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>>
>           >>         <mailto:Agda at lists.chalmers.se
>         <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se
>         <mailto:Agda at lists.chalmers.se>__>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se
>         <mailto:Agda at lists.chalmers.se>__>>__>
>           >> https://lists.chalmers.se/______mailman/listinfo/agda
>         <https://lists.chalmers.se/____mailman/listinfo/agda>
>           >>
>         <https://lists.chalmers.se/____mailman/listinfo/agda
>         <https://lists.chalmers.se/__mailman/listinfo/agda>>
>           >>
>           <https://lists.chalmers.se/____mailman/listinfo/agda
>         <https://lists.chalmers.se/__mailman/listinfo/agda>
>           >>         <https://lists.chalmers.se/__mailman/listinfo/agda
>         <https://lists.chalmers.se/mailman/listinfo/agda>>>
>           >>
>           >>
>           >>
>           _____________________________________________________
>           >>
>           >>              Agda mailing list
>           >> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>>
>           >>         <mailto:Agda at lists.chalmers.se
>         <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se
>         <mailto:Agda at lists.chalmers.se>__>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se
>         <mailto:Agda at lists.chalmers.se>__>>__>
>           >> https://lists.chalmers.se/______mailman/listinfo/agda
>         <https://lists.chalmers.se/____mailman/listinfo/agda>
>           >>
>         <https://lists.chalmers.se/____mailman/listinfo/agda
>         <https://lists.chalmers.se/__mailman/listinfo/agda>>
>           >>
>           >>
>           <https://lists.chalmers.se/____mailman/listinfo/agda
>         <https://lists.chalmers.se/__mailman/listinfo/agda>
>           >>         <https://lists.chalmers.se/__mailman/listinfo/agda
>         <https://lists.chalmers.se/mailman/listinfo/agda>>>
>           >>
>           >>     ___________________________________________________
>           >>     Agda mailing list
>           >> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>>
>           >> https://lists.chalmers.se/____mailman/listinfo/agda
>         <https://lists.chalmers.se/__mailman/listinfo/agda>
>           >>     <https://lists.chalmers.se/__mailman/listinfo/agda
>         <https://lists.chalmers.se/mailman/listinfo/agda>>
>           >>
>           > _________________________________________________
>           > Agda mailing list
>           > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>__>
>           > https://lists.chalmers.se/__mailman/listinfo/agda
>         <https://lists.chalmers.se/mailman/listinfo/agda>
>
>     _________________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/__mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>