From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 12 Oct 2017 17:44:49 -0700 (PDT) From: Alexander Altman To: Homotopy Type Theory Message-Id: In-Reply-To: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_15721_787044428.1507855489707" ------=_Part_15721_787044428.1507855489707 Content-Type: multipart/alternative; boundary="----=_Part_15722_1367976364.1507855489708" ------=_Part_15722_1367976364.1507855489708 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable How does outright explicit subtyping play into this? *E.g.*, if you had a= =20 type theory with judgemental subtyping, not just judgemental equality, and= =20 one of the subtyping rules given was that each universe is a subtype of the= =20 next, would that still violate the conditions needed for initiality? On Thursday, October 12, 2017 at 7:09:06 PM UTC-5, Steve Awodey wrote: > > in order to have an (essentially) algebraic notion of type theory, which= =20 > will then automatically have initial algebras, etc., one should have the= =20 > typing of terms be an operation, so that every term has a unique type. In= =20 > particular, your (R1) violates this. Cumulativity is a practical=20 > convenience that can be added to the system by some syntactic conventions= ,=20 > but the real system should have unique typing of terms. > > Steve > > On Oct 12, 2017, at 2:43 PM, Dimitris Tsementzis > wrote: > > Dear all, > > Let=E2=80=99s say a type theory TT is *initial* if its term model C_TT is= initial=20 > among TT-models, where TT-models are models of the categorical semantics = of=20 > type theory (e.g. CwFs/C-systems etc.) with enough extra structure to mod= el=20 > the rules of TT. > > Then we have the following, building on an example of Voevodsky=E2=80=99s= . > > *OBSERVATION*. Any type theory which contains the following rules=20 > (admissible or otherwise)=20 > > =CE=93 |- T *Type* > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (C) > =CE=93 |- B(T) *Type* > > =CE=93 |- t : T > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (R1) > =CE=93 |- t : B(T) > > =CE=93 |- t : T > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (R2) > =CE=93 |- p(t) : B(T) > > together with axioms that there is a type T0 in any context and a term t0= =20 > : T0 in any context, is not initial.=20 > > *PROOF SKETCH.* Let TT be such a type theory. Consider the type theory=20 > TT* which replaces (R1) with the rule > > =CE=93 |- t : T > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (R1*) > =CE=93 |- q(t) : B(T) > > i.e. the rule which adds an =E2=80=9Cannotation=E2=80=9D to a term t from= T that becomes a=20 > term of B(T). Then the category of TT-models is isomorphic (in fact, equa= l)=20 > to the category of TT*-models and in particular the term models C_TT and= =20 > C_TT* are both TT-models. But there are two distinct TT-model homomorphis= ms=20 > from C_TT to C_TT*, one which sends p(t0) to pq(t0) and one which sends= =20 > p(t0) to qp(t0) (where p(t0) is regarded as an element of Tm_{C_TT} (empt= y,=20 > B(B(T0))), i.e. of the set of terms of B(B(T0)) in the empty context as= =20 > they are interpreted in the term model C_TT).=20 > > *COROLLARY. *Any (non-trivial) type theory with a =E2=80=9Ccumulativity" = rule for=20 > universes, i.e. a rule of the form > > =CE=93 |- A : U0 > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (U-cumul) > =CE=93 |- A : U1=20 > > is not initial. In particular, the type theory in the HoTT book is not=20 > initial (because of (U-cumul)), and two-level type theory 2LTT as present= ed=20 > here is not initial (because of the=20 > rule (FIB-PRE)). > > The moral of this small observation, if correct, is not of course that=20 > type theories with the guilty rules cannot be made initial by appropriate= =20 > modifications to either the categorical semantics or the syntax, but rath= er=20 > that a bit of care might be required for this task. One modification woul= d=20 > be to define their categorical semantics to be such that certain identiti= es=20 > hold that are not generally included in the definitions of=20 > CwF/C-system/=E2=80=A6-gadgets (e.g. that the inclusion operation on univ= erses is=20 > idempotent). Another modification would be to add annotations (by replaci= ng=20 > (R1) with (R1*) as above) and extra definitional equalities ensuring that= =20 > annotations commute with type constructors.=20 > > But without some such explicit modification, I think that the claim that= =20 > e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or even= =20 > entirely correct. > > Best, > > Dimitris > > PS: Has something like the above regarding cumulativity rules has been=20 > observed before =E2=80=94 if so can someone provide a relevant reference? > > > > > > --=20 > You received this message because you are subscribed to the Google Groups= =20 > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= =20 > email to HomotopyTypeThe...@googlegroups.com . > For more options, visit https://groups.google.com/d/optout. > > > ------=_Part_15722_1367976364.1507855489708 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
How does outright explicit subtyping play into this? =C2= =A0E.g., if you had a type theory with judgemental subtyping, not ju= st judgemental equality, and one of the subtyping rules given was that each= universe is a subtype of the next, would that still violate the conditions= needed for initiality?

On Thursday, October 12, 2017 at 7:09:06 PM = UTC-5, Steve Awodey wrote:
in orde= r to have an (essentially) algebraic notion of type theory, which will then= automatically have initial algebras, etc., one should have the typing of t= erms be an operation, so that every term has a unique type. In particular, = your (R1) violates this. Cumulativity is a practical convenience that can b= e added to the system=C2=A0by some syntactic conventions, but the real syst= em should have unique typing of terms.

Steve
On Oct 12, 2017, at 2:43 PM, Dimitris = Tsementzis <dts...@princeton.edu> wrote:

Dear all,

Let=E2=80=99s say a type = theory TT is initial if its term model C_TT is initial among TT-mode= ls, where TT-models are models of the categorical semantics of type theory = (e.g. CwFs/C-systems etc.) with enough extra structure to model the rules o= f TT.

Then we have the following, building on an e= xample of Voevodsky=E2=80=99s.

OBSERVATION. A= ny type theory which contains the following rules (admissible or otherwise)= =C2=A0

=CE=93 |- T Type
=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =C2=A0(C)
=CE= =93 |- B(T) Type

=CE=93 |- t : T
=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =C2=A0(R= 1)
=CE=93 |- t : B(T)

=CE=93 |- t : T
=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =C2=A0(R2)
=CE=93 |- p(= t) : B(T)

together with axioms that there is a typ= e T0 in any context and a term t0 : T0 in any context, is not initial.=C2= =A0

PROOF SKETCH. Let TT be such= a type theory. Consider the type theory TT* which replaces (R1) with the r= ule

=CE=93 |- t : T
=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =C2=A0(R1*)
=CE=93 |- q(t)= : B(T)

i.e. the rule which adds an =E2=80=9Cannot= ation=E2=80=9D to a term t from T that becomes a term of B(T). Then the cat= egory of TT-models is isomorphic (in fact, equal) to the category of TT*-mo= dels and in particular the term models C_TT and C_TT* are both TT-models. B= ut there are two distinct TT-model homomorphisms from C_TT to C_TT*, one wh= ich sends p(t0) to pq(t0) and one which sends p(t0) to qp(t0) (where p(t0) = is regarded as an element of Tm_{C_TT} (empty, B(B(T0))), i.e. of the set o= f terms of B(B(T0)) in the empty context as they are interpreted in the ter= m model C_TT).=C2=A0

COROLLARY. Any (= non-trivial) type theory with a =E2=80=9Ccumulativity" rule for univer= ses, i.e. a rule of the form

=CE=93 |- A : U0
= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = =C2=A0(U-cumul)
=CE=93 |- A : U1=C2=A0

is not i= nitial. In particular, the type theory in the HoTT book is not initial (bec= ause of (U-cumul)), and two-level type theory 2LTT as presented=C2=A0here=C2=A0is not initial (because of the rule (FIB-PRE)).

The moral of this small observation, if correct, is n= ot of course that type theories with the guilty rules cannot be made initia= l by appropriate modifications to either the categorical semantics or the s= yntax, but rather that a bit of care might be required for this task. One m= odification would be to define their categorical semantics to be such that = certain identities hold that are not generally included in the definitions = of CwF/C-system/=E2=80=A6-gadgets (e.g. that the inclusion operation on uni= verses is idempotent). Another modification would be to add annotations (by= replacing (R1) with (R1*) as above) and extra definitional equalities ensu= ring that annotations commute with type constructors.=C2=A0

<= /div>
But without some such explicit modification, I think that the cla= im that e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or = even entirely correct.

Best,

<= div>Dimitris

PS: Has something like the above rega= rding cumulativity rules has been observed before =E2=80=94 if so can someo= ne provide a relevant reference?




--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/= d/optout.

------=_Part_15722_1367976364.1507855489708-- ------=_Part_15721_787044428.1507855489707--