[HoTT] Re: [Agda] Univalence via Agda's primTrustMe?
Alan Jeffrey
ajeffrey at bell-labs.com
Mon Jan 19 17:19:43 CET 2015
Thanks, this clarifies what the problem is!
A.
On 01/19/2015 10:09 AM, Vladimir Voevodsky 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 <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.
>
More information about the Agda
mailing list