[HoTT] Re: [Agda] Univalence via Agda's primTrustMe?

Alan Jeffrey ajeffrey at bell-labs.com
Thu Jan 22 00:54:23 CET 2015


Yes, take any type A with an equivalence (e : A ≃ Nat) and (a : A) then:

   ap (ua e) a : Nat

but unless there's a beta-reduction, for example:

   ap (ua e) a  -->  e(a)

then this is a closed term with no beta reductions which isn't zero or 
suc. There is a propositional equivalence:

   ap (ua e) a = e(a)

but it's not a beta-reduction.

A.

On 01/21/2015 02:41 AM, maxim.budaev at googlemail.com wrote:
>>a term of type nat build using univalence
>
> Have you any examples of such terms?
>
> In my understanding the nat is a first order entity but output of
> univalence is higher order entity(equivalency classes/types).
> Is it possible at all?
>
> Thanks.
>
> Max
>
> On Monday, January 19, 2015 at 10:10:01 PM UTC+6, v v wrote:
>
>      >> If so, would it be good enough to show strong normalization, plus:
>      >>
>      >>  For every closed term M of type nat, either
>      >>  a) M has a beta reduction,
>      >>  b) M is zero, or
>      >>  c) M is suc N for some closed term N of type nat
>
>     The term of type nat is assumed to be closed (empty context, other
>     than the univalence axiom).
>
>     The strong normalization comes from the ambient theory (CIC or
>     whatever version of it one considers).
>
>     But there are many terms of type nat that are in the normal form and
>     are not O or a successor. Basically any term constructed using
>     univalence.
>     This is what makes the conjecture difficult.
>
>
>     Vladimir.
>
>
>
>      > On Jan 19, 2015, at 10:29 AM, Alan Jeffrey <ajef... at bell-labs.com
>     <javascript:>> wrote:
>      >
>      > Hi Vladimir,
>      >
>      > In the conjecture, can we assume the term of type nat is closed?
>      >
>      > If so, would it be good enough to show strong normalization, plus:
>      >
>      >  For every closed term M of type nat, either
>      >  a) M has a beta reduction,
>      >  b) M is zero, or
>      >  c) M is suc N for some closed term N of type nat
>      >
>      > To get the conjecture, for any M, use SN to find an N with no
>     beta reductions, such that M beta reduces to N (and so is
>     propositionally equal to it) which must be of the form (suc^n zero)
>     by (b) and (c) above.
>      >
>      > I'm not sure whether this constitutes an algorithm as required by
>     the conjecture, as it includes an appeal to SN.
>      >
>      > A.
>      >
>      > On 01/17/2015 09:10 PM, Vladimir Voevodsky wrote:
>      >> There is my conjecture: to construct an algorithm that takes a
>     term of
>      >> type nat build using univalence and computes a numeral from it
>     and a
>      >> propositional equality from this numeral to the original term.
>      >>
>      >> The cubical type theory is supposed to have univalence terms among
>      >> constructors and still satisfy the canonicity for nat. By
>     interpreting
>      >> MLTT into cubical type theory one will get a proof of  a
>     slightly weaker
>      >> form of the conjecture where instead of propositional equality
>     term one
>      >> will get a proof that the numeral represents the same natural
>     number as
>      >> the original term after application of an interpretation into, say,
>      >> simplicial sets.
>      >>
>      >> Vladimir.
>      >>
>      >>
>      >>> On Jan 17, 2015, at 9:40 PM, Jason Gross <jason... at gmail.com
>     <javascript:>
>      >>> <mailto:jason... at gmail.com <javascript:>>> wrote:
>      >>>
>      >>>
>      >>>
>      >>> On Sun, Jan 18, 2015 at 12:18 AM, Alan Jeffrey
>     <ajef... at bell-labs.com <javascript:>
>      >>> <mailto:ajef... at bell-labs.com <javascript:>>> wrote:
>      >>>
>      >>>    Thanks! Are there good "victory conditions" for a computational
>      >>>    interpretation of univalence? Other than "I know it when I
>     see it" :-)
>      >>>
>      >>>
>      >>> If every function defined by pattern matching on a path
>      >>> reduces judgmentally when applied to univalence (i.e., if the
>     strong
>      >>> normal form of a term contains no pattern matching on univalence),
>      >>> then we've won.  I don't know anything better than that.
>      >>>
>      >>> -Jason
>      >>>
>      >>>
>      >>>    A.
>      >>>
>      >>>    On 01/17/2015 07:11 AM, Jason Gross wrote:
>      >>>
>      >>>        I'm cc'ing the homotopy type theory list as well.
>      >>>
>      >>>        To answer some of your questions:
>      >>>        (a) I've not seen this before.  It seems pretty neat!
>      >>>        (c) This is, in some sense, the simplest part of
>     computational
>      >>>        univalence.  All of the thoughts I've had about
>     computational
>      >>>        univalence
>      >>>        go top down, saying what should happen when you do path
>      >>>        induction on an
>      >>>        equality from univalence.  But it's cool to see what you
>     can
>      >>>        do bottom-up.
>      >>>
>      >>>        -Jason
>      >>>
>      >>>        On Jan 17, 2015 2:33 AM, "Alan Jeffrey"
>      >>>        <ajef... at bell-labs.com <javascript:>
>     <mailto:ajef... at bell-labs.com <javascript:>>
>      >>>        <mailto:ajef... at bell-labs.com <javascript:>
>      >>>        <mailto:ajef... at bell-labs.com <javascript:>>__>> wrote:
>      >>>
>      >>>            Hi everyone,
>      >>>
>      >>>            In the Agda development of Homotopy Type Theory at
>      >>> https://github.com/HoTT/HoTT-____Agda/
>     <https://github.com/HoTT/HoTT-____Agda/>
>      >>>        <https://github.com/HoTT/HoTT-__Agda/
>     <https://github.com/HoTT/HoTT-__Agda/>>
>      >>>
>      >>>            <https://github.com/HoTT/HoTT-__Agda/
>     <https://github.com/HoTT/HoTT-__Agda/>
>      >>>        <https://github.com/HoTT/HoTT-Agda/
>     <https://github.com/HoTT/HoTT-Agda/>>> the univalence axiom is
>      >>>        given
>      >>>            by three postulates (the map from (A ≃ B) to (A ≡ B)
>     and
>      >>>        its β and η
>      >>>            rules).
>      >>>
>      >>>            I wonder whether these postulates could be replaced
>     by uses of
>      >>>            primTrustMe?
>      >>>
>      >>>            As a reminder, primTrustMe is a trusted function which
>      >>>        inhabits the
>      >>>            type (M ≡ N) for any M and N. It is possible to
>     introduce
>      >>>            contradictions (e.g. 0 ≡ 1) in the same way as with
>      >>>        postulates, so
>      >>>            it has to be handled with care. The semantics is as for
>      >>>        postulates,
>      >>>            but with an extra beta reduction:
>      >>>
>      >>>               primTrustMe M M → refl
>      >>>
>      >>>            In the attached Agda code, primTrustMe is used to
>     define:
>      >>>
>      >>>               private
>      >>>                 trustme : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (∃ q ∙
>      >>>        ((≡-to-≃ q)
>      >>>            ≡ p))
>      >>>                 trustme p = ⟨ primTrustMe , primTrustMe ⟩
>      >>>
>      >>>            from which we get the map from (A ≃ B) to (A ≡ B)
>     and its
>      >>>        β rule:
>      >>>
>      >>>               ≃-to-≡ : ∀ {ℓ} {A B : Set ℓ} → (A ≃ B) → (A ≡ B)
>      >>>               ≃-to-≡ p with trustme p
>      >>>               ≃-to-≡ .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl
>      >>>
>      >>>               ≃-to-≡-β : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (≡-to-≃
>      >>>        (≃-to-≡ p) ≡ p)
>      >>>               ≃-to-≡-β p with trustme p
>      >>>               ≃-to-≡-β .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl
>      >>>
>      >>>            Interestingly, the η rule and the coherence property
>     for β
>      >>>        and η
>      >>>            then become trivial:
>      >>>
>      >>>               ≃-to-≡-η : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → (≃-to-≡
>      >>>        (≡-to-≃ p) ≡ p)
>      >>>               ≃-to-≡-η refl = refl
>      >>>
>      >>>               ≃-to-≡-τ : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) →
>      >>>                 (cong ≡-to-≃ (≃-to-≡-η p) ≡ ≃-to-≡-β (≡-to-≃ p))
>      >>>               ≃-to-≡-τ refl = refl
>      >>>
>      >>>            Note there's some hoop-jumping with private
>     declarations
>      >>>        to hide
>      >>>            trustme from users, because:
>      >>>
>      >>>               (fst (trustme p)) → refl  (for any p : (A ≃ A))
>      >>>
>      >>>            that is, all proofs of (A ≃ A) would be identified
>     if we were
>      >>>            allowed unfettered access to trustme. Instead, we only
>      >>>        allow (≃-to-≡
>      >>>            p) to reduce to refl when (trustme p) reduces to ⟨
>     refl ,
>      >>>        refl ⟩,
>      >>>            that is not only do we have (A ≃ A) but also that p
>     must
>      >>>        be the
>      >>>            trivial proof that (A ≃ A).
>      >>>
>      >>>            Now, this isn't a conservative extension of HOTT
>     because it
>      >>>            introduces extra beta reductions that were
>     previously just
>      >>>            propositional equalities, in particular:
>      >>>
>      >>>               (≃-to-≡ (≡-to-≃ refl)) → refl
>      >>>               (≃-to-≡-β (≡-to-≃ refl)) → refl
>      >>>               (≃-to-≡-η refl) → refl
>      >>>               (≃-to-≡-τ refl) → refl
>      >>>
>      >>>            So questions... a) Is this re-inventing the wheel?
>     b) Is
>      >>>        this sound?
>      >>>            c) Is there a connection between this and a
>     computational
>      >>>            interpretation of univalence?
>      >>>
>      >>>            Alan.
>      >>>
>      >>>            _________________________________________________
>      >>>            Agda mailing list
>      >>> Ag... at lists.chalmers.se <javascript:>
>     <mailto:Ag... at lists.chalmers.se <javascript:>>
>      >>>        <mailto:Ag... at lists.chalmers.se <javascript:>
>     <mailto:Ag... at lists.chalmers.se <javascript:>>__>
>      >>> 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>>
>      >>>
>      >>>
>      >>>
>      >>> --
>      >>> You received this message because you are subscribed to the Google
>      >>> Groups "Homotopy Type Theory" group.
>      >>> To unsubscribe from this group and stop receiving emails from
>     it, send
>      >>> an email to HomotopyTypeTheory+unsubscribe at googlegroups.com
>     <javascript:>
>      >>> <mailto:HomotopyTypeTheory+unsubscribe at googlegroups.com
>     <javascript:>>.
>      >>> For more options, visit https://groups.google.com/d/optout
>     <https://groups.google.com/d/optout>.
>      >>
>      >> --
>      >> You received this message because you are subscribed to the Google
>      >> Groups "Homotopy Type Theory" group.
>      >> To unsubscribe from this group and stop receiving emails from
>     it, send
>      >> an email to HomotopyTypeTheory+unsubscribe at googlegroups.com
>     <javascript:>
>      >> <mailto:HomotopyTypeTheory+unsubscribe at googlegroups.com
>     <javascript:>>.
>      >> For more options, visit https://groups.google.com/d/optout
>     <https://groups.google.com/d/optout>.
>      >
>      > --
>      > You received this message because you are subscribed to the
>     Google Groups "Homotopy Type Theory" group.
>      > To unsubscribe from this group and stop receiving emails from it,
>     send an email to HomotopyTypeTheory+unsubscribe at googlegroups.com
>     <javascript:>.
>      > For more options, visit https://groups.google.com/d/optout
>     <https://groups.google.com/d/optout>.
>


More information about the Agda mailing list