From: Dimitris Tsementzis <dtse...@princeton.edu>
To: "Gaëtan Gilbert" <"gaetan...."@skyskimmer.net>
Cc: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] A question regarding certain rules
Date: Mon, 9 Oct 2017 23:06:53 -0400 [thread overview]
Message-ID: <F0A31C6E-26DF-40CB-BBAA-98921072ABCB@princeton.edu> (raw)
In-Reply-To: <0d00219f-470f-cd84-98de-5eff1c2a4ea4@skyskimmer.net>
Thanks. Yes, this is of course entirely compatible with my description, yet I am not sure it captures what I was after.
I will have to think more about whether your example suffices for my purposes.
Dimitris
> On Oct 9, 2017, at 13:54, Gaëtan Gilbert <gaetan....@skyskimmer.net> wrote:
>
> Does T:=Type0, C(T):=Type1, t:=nat and p(t):=nat->nat count? If so HoTT has this. If not why not?
>
> Gaëtan Gilbert
>
> On 2017-10-09 19:41, Dimitris Tsementzis wrote:
>> Dear all,
>> Is there a type theory that has been considered in the literature which includes *both* the following rules
>> Γ |- t : T
>> ———————— (R1)
>> Γ |- t : C(T)
>> Γ |- t : T
>> ———————— (R2)
>> Γ |- p(t) : C(T)
>> where C(T) is a type expression, p(t) is a term expression, t is a term expression that must appear in p(t), and T is a type expression that may or may not appear in C(T).
>> An example of (R1) is (U-CUMUL) as in the HoTT book, i.e. cumulativity of universes.
>> An example of (R2) is (Nat-intro-2) as in the HoTT book, i.e. the successor for Nat (with C(T) == Nat).
>> Best,
>> Dimitris
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
prev parent reply other threads:[~2017-10-10 3:06 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-10-09 17:41 Dimitris Tsementzis
2017-10-09 17:54 ` [HoTT] " Gaëtan Gilbert
2017-10-10 3:06 ` Dimitris Tsementzis [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=F0A31C6E-26DF-40CB-BBAA-98921072ABCB@princeton.edu \
--to="dtse..."@princeton.edu \
--cc="HomotopyT..."@googlegroups.com \
--cc="gaetan...."@skyskimmer.net \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).