[HoTT] Re: [Agda] Univalence via Agda's primTrustMe?
Vladimir Voevodsky
vladimir at ias.edu
Mon Jan 19 17:09:52 CET 2015
>> 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 <ajeffrey at bell-labs.com> 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 <jasongross9 at gmail.com
>>> <mailto:jasongross9 at gmail.com>> wrote:
>>>
>>>
>>>
>>> On Sun, Jan 18, 2015 at 12:18 AM, Alan Jeffrey <ajeffrey at bell-labs.com
>>> <mailto:ajeffrey at bell-labs.com>> 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"
>>> <ajeffrey at bell-labs.com <mailto:ajeffrey at bell-labs.com>
>>> <mailto:ajeffrey at bell-labs.com
>>> <mailto:ajeffrey at bell-labs.com>__>> 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/>> 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
>>> 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>
>>>
>>>
>>>
>>> --
>>> 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
>>> <mailto:HomotopyTypeTheory+unsubscribe at googlegroups.com>.
>>> For more options, visit 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
>> <mailto:HomotopyTypeTheory+unsubscribe at googlegroups.com>.
>> For more options, visit 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.
> For more options, visit https://groups.google.com/d/optout.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150119/a903962c/signature.bin
More information about the Agda
mailing list