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

Guillaume Brunerie guillaume.brunerie at gmail.com
Mon Jan 19 16:43:06 CET 2015


Take any (closed) equivalence e between Nat and Nat, and write   ua e
 for the equality between Nat and Nat induced by that equivalence
(using the univalence axiom).
Then   transport (\X -> X) (ua e) zero   is a closed term of term Nat
which is neither zero or suc N and without beta reductions (whether ua
is defined using primTrustMe or not).

2015-01-19 16:29 GMT+01:00 Alan Jeffrey <ajeffrey at bell-labs.com>:
> 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