On Oct 13, 2017, at 11:50 AM, Michael Shulman <shu...@sandiego.edu> wrote:

On Thu, Oct 12, 2017 at 5:09 PM, Steve Awodey <steve...@gmail.com> wrote:

in order to have an (essentially) algebraic notion of type theory, which
will then automatically have initial algebras, etc., one should have the
typing of terms be an operation, so that every term has a unique type. In
particular, your (R1) violates this. Cumulativity is a practical convenience
that can be added to the system by some syntactic conventions, but the real
system should have unique typing of terms.

I'm not convinced of that.  When we define the syntactic model, a
morphism from A to B (say) is defined to be a term x:A |- t:B, where
the types A and B are given.  So it's not clear that it matters
whether the same syntactic object t can also be typed as belonging to
some other type.  I thought that the fundamental structure that we
induct over to prove initiality is the *derivation* of a typing
judgment, which includes the type that the term belongs to: two
derivations of x:A |- t:B and x:A |- t:C will necessarily be different
if B and C are different.  In an ideal world, a judgment x:A |- t:B
would have at most one derivation, so that we could induct on
derivations and still consider the syntactic model to be built out of
terms rather than derivations.  If not, then we need a separate step
of showing that different derivations of the same judgment yield the
same interpretation; but still, it's not clear to me that the
simultaneous derivability of x:A |- t:C is fatal.

Moreover, I'm not an expert in this, but my understanding is that type
theorists often think of typing as having two "modes": type checking,
in which t and B are both given and a derivation of t:B is to be
found, and type synthesis or inference, in which t is given and B has
to be found along with a derivation of t:B.  Which mode you are in at
which point in an algorithm depends on the structure of t and B.  This
is not irrelevant to the question of initiality, since this sort of
"bidirectional type checking" can also be encoded in the judgmental
structure.

Mike

Steve


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

Dear all,

Let’s say a type theory TT is initial if its term model C_TT is initial
among TT-models, 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 of TT.

Then we have the following, building on an example of Voevodsky’s.

OBSERVATION. Any type theory which contains the following rules (admissible
or otherwise)

Γ |- T Type
————————  (C)
Γ |- B(T) Type

Γ |- t : T
————————  (R1)
Γ |- t : B(T)

Γ |- t : T
————————  (R2)
Γ |- p(t) : B(T)

together with axioms that there is a type T0 in any context and a term t0 :
T0 in any context, is not initial.

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

Γ |- t : T
————————  (R1*)
Γ |- q(t) : B(T)

i.e. the rule which adds an “annotation” to a term t from T that becomes a
term of B(T). Then the category of TT-models is isomorphic (in fact, equal)
to the category of TT*-models and in particular the term models C_TT and
C_TT* are both TT-models. But there are two distinct TT-model homomorphisms
from C_TT to C_TT*, one which 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 of terms of B(B(T0)) in the empty context as they
are interpreted in the term model C_TT).

COROLLARY. Any (non-trivial) type theory with a “cumulativity" rule for
universes, i.e. a rule of the form

Γ |- A : U0
————————  (U-cumul)
Γ |- A : U1

is not initial. In particular, the type theory in the HoTT book is not
initial (because of (U-cumul)), and two-level type theory 2LTT as presented
here is not initial (because of the rule (FIB-PRE)).

The moral of this small observation, if correct, is not of course that type
theories with the guilty rules cannot be made initial by appropriate
modifications to either the categorical semantics or the syntax, but rather
that a bit of care might be required for this task. One modification 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/…-gadgets (e.g. that the inclusion operation on universes is
idempotent). Another modification would be to add annotations (by replacing
(R1) with (R1*) as above) and extra definitional equalities ensuring that
annotations commute with type constructors.

But without some such explicit modification, I think that the claim that
e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or even
entirely correct.

Best,

Dimitris

PS: Has something like the above regarding cumulativity rules has been
observed before — if so can someone provide a relevant reference?





--
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.


--
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.

-- 
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.