[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