Where is the problem with initiality?

Where is the problem with initiality?

[Michael Shulman]

Thorsten gave a very nice HoTTEST talk a couple weeks ago about his
work with his collaborators on intrinsic syntax as a Quotient
Inductive-Inductive Type.  Since then I have been trying to fit
together a mental picture of exactly how all the different approaches
to syntax are related, but I am still kind of confused.

In an attempt to clarify what I mean by "all the different
approaches", let me describe all the approaches I can think of in the
case of a very simple type theory: non-dependent unary type theory
with product types.  Unary means that the judgments have exactly one
type in the context, x:A |- t:B, and the only type constructor is a
product type A x B, with pairing for an introduction rule and
projections for elimination.  The semantics should be a category with
finite products.  Here are all the ways I can think of to describe
such a type theory:


1. A QIIT that mirrors the semantics, with all the categorical
operations as point-constructors and their axioms as
equality-constructors.

data Ty : Set where
 _x_ : Ty -> Ty -> Ty
[This will be the same in all cases, so I henceforth omit it.]

data Tm : Ty -> Ty -> Set where
  id : {A} -> Tm A A
  _o_ : Tm A B -> Tm B C -> Tm A C
  assoc : h o (g o f) = (h o g) o f
  lid : id o f = f
  rid : f o id = f
  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
  pr1 : Tm (A x B) A
  pr2 : Tm (A x B) B
  beta1 : pr1 o (f , g) = f
  beta2 : pr2 o (f , g) = g
  eta : p = (pr1 o p , pr2 o p)


2. An Inductive-Inductive family of setoids that similarly mirrors the
categorical semantics, with judgmental equality an inductive type
family rather than coinciding with the metatheoretic equality.

data Tm : Ty -> Ty -> Set where
  id : {A} -> Tm A A
  _o_ : Tm A B -> Tm B C -> Tm A C
  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
  pr1 : Tm (A x B) A
  pr2 : Tm (A x B) B

data Eq : Tm A B -> Tm A B -> Set where
  assoc : Eq (h o (g o f)) ((h o g) o f)
  lid : Eq (id o f) f
  rid : Eq 9f o id) f
  beta1 : Eq (pr1 o (f , g)) f
  beta2 : Eq (pr2 o (f , g)) g
  eta : Eq p (pr1 o p , pr2 o p)


3. A QIIT that instead mirrors the usual type-theoretic syntax, with
operations like composition being admissible rather than primitive.
In our simple case it looks like this:

data Tm : Ty -> Ty -> Set where
  id : {A} -> Tm A A
  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
  pr1 : Tm A (B x C) -> Tm A B
  pr2 : Tm A (B x C) -> Tm A C
  beta1 : pr1 (f , g) = f
  beta2 : pr2 (f , g) = g
  eta : p = (pr1 p , pr2 p)


4. Combining 2 and 3, an II family of setoids that mirrors
type-theoretic syntax.

data Tm : Ty -> Ty -> Set where
  id : {A} -> Tm A A
  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
  pr1 : Tm A (B x C) -> Tm A B
  pr2 : Tm A (B x C) -> Tm A C

data Eq : Tm A B -> Tm A B -> Set where
  beta1 : Eq (pr1 (f , g)) f
  beta2 : Eq (pr2 (f , g)) g
  eta : Eq p (pr1 p , pr2 p)


5. A single inductive type of raw terms, together with inductive
predicates over it for the typing judgment and equality judgments.

data Tm : Set where
  var : Tm
  (_,_) : Tm -> Tm -> Tm
  pr1 : Tm -> Tm
  pr2 : Tm -> Tm

data Of : Ty -> Tm -> Ty -> Set where
  of-var : Of A var A
  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
  of-pr1 : Of A t (B x C) -> Of A (pr1 t) B
  of-pr2 : Of A t (B x C) -> Of A (pr2 t) C

data Eq : Ty -> Tm -> Tm -> Ty -> Set where
  beta1 : Of A t B -> Of A s C -> Eq A (pr1 (t , s)) t B
  beta2 : Of A t B -> Of A s C -> Eq A (pr2 (t , s)) t C
  eta : Of A t (B x C) -> Eq A (pr1 t , pr2 t) t (B x C)


6. An II family that defines only the normal forms, via a separate
judgment for "atomic" terms that prevents us from writing down any
beta-redexes, thereby eliminating the need for any equality judgment
(though substitution then becomes more complicated, as it must
essentially incorporate beta-reduction).

data Atom : Ty -> Ty -> Set where
  id : {A} -> Atom A A
  pr1 : Atom A (B x C) -> Atom A B
  pr2 : Atom A (B x C) -> Atom A C

data Tm : Ty -> Ty -> Set where
  atom : Atom A B -> Tm A B
  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)


7. Combining 5 and 6, an inductive type of raw terms and predicates
over it that type only the normal forms.

data Tm : Set where
  var : Tm
  (_,_) : Tm -> Tm -> Tm
  pr1 : Tm -> Tm
  pr2 : Tm -> Tm

data Atom : Ty -> Tm -> Ty -> Set where
  atom-var : Atom A var A
  atom-pr1 : Atom A t (B x C) -> Atom A (pr1 t) B
  atom-pr2 : Atom A t (B x C) -> Atom A (pr2 t) C

data Of : Ty -> Tm -> Ty -> Set where
  of-atom : Atom A t B -> Of A t B
  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)


This is all I can think of right now.  Are there others?  Are there
other choices we can make in the case of dependent type theory that
are not visible in this simple case?

In the above simple case of unary type theory with products, it should
be easy to show that all these definitions construct the initial
category with products.  (There should be some generating/axiomatic
types and terms too, to make the result nontrivial, but I've left them
out for brevity.)  My main question is, where do things become hard in
the case of dependent type theory?

It seems to me that the main difference between (1) and (2), and
between (3) and (4), is convenience; is that right?  Type theory has
no infinitary constructors, so there shouldn't be axiom-of-choice
issues with descending algebraic operations to a quotient; it's just
that the bookkeeping involved in dealing with setoids everywhere
becomes unmanageable in the case of DTT.  Right?

Thorsten said that (1) in the case of dependent type theory is
tautologically the initial CwF, which seems eminently plausible.  I
don't think this solves the "initiality conjecture", but where is the
sticking point?  Is it between (1) and (3), or between (3) and (5)?

(Note that I'm not talking at all about the "h-level problem" that
these QIITs are by definition sets but that for HoTT to "eat itself"
we would want to eliminate out of them into the universe which is not
a set.  I'm only talking about initiality of syntax among *strict*
CwFs; coherence/strictification theorems can wait.  Personally,
though, I like (6)-(7) as potential approaches to coherence.)

Re: Where is the problem with initiality?

[Ambrus Kaposi]

[-- Attachment #1.1: Type: text/plain, Size: 2597 bytes --]

Hi Mike,

This is all I can think of right now.  Are there others?  Are there 
> other choices we can make in the case of dependent type theory that 
> are not visible in this simple case? 
>

I think there are at least the following categories:

Typing can be:
  I. intrinsic (only well-typed terms)
  II. extrinsic (preterms and typing relations).
Conversion can be given:
  1. by equality
  2. by an inductive relation
  3. not given, if we only have normal forms in the syntax (hereditary 
substitution)
Substitution can be:
  A. explicit (substitution is a constructor)
  B. implicit (it is defined recursively)

Your variants are categorised as below:

1 I,1,A
2 I,2,A
3 I,1,B
4 I,2,B
5 II,2,B
6 I,3,B
7 II,3,B

In the extrinsic case, I can think about the following additional choices:
 - Conversion and typing can be merged into a PER
 - use universes a la Russel or Tarski (in the Russel case, types and terms 
are identified)
 - you can have paranoid/relaxed variants of constructors (do you have Pi A 
B or Pi Gamma A B)
 - do you have conversion for contexts or not

In the above simple case of unary type theory with products, it should 
> be easy to show that all these definitions construct the initial 
> category with products.  (There should be some generating/axiomatic 
> types and terms too, to make the result nontrivial, but I've left them 
> out for brevity.)  My main question is, where do things become hard in 
> the case of dependent type theory? 
>
> It seems to me that the main difference between (1) and (2), and 
> between (3) and (4), is convenience; is that right?  Type theory has 
> no infinitary constructors, so there shouldn't be axiom-of-choice 
> issues with descending algebraic operations to a quotient; it's just 
> that the bookkeeping involved in dealing with setoids everywhere 
> becomes unmanageable in the case of DTT.  Right?  


> Thorsten said that (1) in the case of dependent type theory is 
> tautologically the initial CwF, which seems eminently plausible.  I 
> don't think this solves the "initiality conjecture", but where is the 
> sticking point?  Is it between (1) and (3), or between (3) and (5)? 
>

I think the hard part is between (3) and (5). However I haven't seen a 
definition of  (3) for type theory, e.g. CwF+Pi. It is very intricate, you 
have to prove substitution laws mutually with substitution, but you also 
shouldn't depend on the proofs etc.

There is a nice presentation of Streicher's initiality proof using the 
extrinsic, PER encoding 
in http://www.cse.chalmers.se/~peterd/papers/Lmcs-2016.pdf

Cheers,
Ambrus

[-- Attachment #1.2: Type: text/html, Size: 3530 bytes --]

Re: [HoTT] Where is the problem with initiality?

[Thorsten Altenkirch]

Hi Michael,

thank you for your nice summary. You say that

"It seems to me that the main difference between (1) and (2), and
between (3) and (4), is convenience; is that right?"

It seems to me that a lot in Mathematics can be described as convenience.
Sometimes a good (but equivalent) choice of representation can make all
the difference. 

And I may add that there are cases where we don't want to stick to
finitary constructors. For example Ambrus and Andras proposed a theory of
codes to describe QIITs which does use infinitary constructors to allow
indexing by external sets. In this case the setoid approach wouldn't work.

(5) and (7) introduce preterms which I think shouldn't be considered
fundamental in the definition of type theory.

Defining normal forms (6),(7) is an important tool but it shouldn't be the
basic definition of the type theory.

Historically we have used (5) even with the variation that equality is
defined on untyped terms and using only a small step reduction relation.
Substitution is a defined metatheoretic operation. Once you take these
choices you spend a lot of time proving things which should be obvious.
Now, obviously there is not one "best" way to define type theory but I
think we have made a lot of progress. The basic ingredients of this
progress are:

1. Substitution is a term constructor and works on the whole context
(parallel substitution). This issue isn't visible in your examples because
of the restriction to unary.
2. Equality is typed and not derived form small-step reduction.
3. Equality is defined at the same time as typing. (this is especially
relevant for dependent types).
4. We only define typed entities (no preterms).

Being able to do these things relied on developments in type theory
itself. It was clear that we needed inductive-inductive definitions to be
able to avoid preterms but a lot of boilerplate was eliminated by using
QITs. And as I said this also opens the way to have well behaved type
theories with infinitary constructors.

Just to comment on the h-level problem you don't want to discuss yet: it
seems to me that if we want to use something along the line of (6) to
define normal forms for dependent types we face the problem that we need
to define normalisation at the same time as the terms. This is
induction-recursion which on it's own shouldn't be a problem. However, it
seems to me that we have to prove properties of normalisation (e.g.
substitution laws) at the same time which again give rise to coherence
problems. It would be interesting to see a way to avoid these issues, but
then wouldn't we be able to solve the problem to define semi-simlicial
sets (or more general reedy limits) in plain HoTT?


Thorsten

On 22/05/2018, 06:46, "homotopyt...@googlegroups.com on behalf of
Michael Shulman" <homotopyt...@googlegroups.com on behalf of
shu...@sandiego.edu> wrote:

>Thorsten gave a very nice HoTTEST talk a couple weeks ago about his
>work with his collaborators on intrinsic syntax as a Quotient
>Inductive-Inductive Type.  Since then I have been trying to fit
>together a mental picture of exactly how all the different approaches
>to syntax are related, but I am still kind of confused.
>
>In an attempt to clarify what I mean by "all the different
>approaches", let me describe all the approaches I can think of in the
>case of a very simple type theory: non-dependent unary type theory
>with product types.  Unary means that the judgments have exactly one
>type in the context, x:A |- t:B, and the only type constructor is a
>product type A x B, with pairing for an introduction rule and
>projections for elimination.  The semantics should be a category with
>finite products.  Here are all the ways I can think of to describe
>such a type theory:
>
>
>1. A QIIT that mirrors the semantics, with all the categorical
>operations as point-constructors and their axioms as
>equality-constructors.
>
>data Ty : Set where
> _x_ : Ty -> Ty -> Ty
>[This will be the same in all cases, so I henceforth omit it.]
>
>data Tm : Ty -> Ty -> Set where
>  id : {A} -> Tm A A
>  _o_ : Tm A B -> Tm B C -> Tm A C
>  assoc : h o (g o f) = (h o g) o f
>  lid : id o f = f
>  rid : f o id = f
>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>  pr1 : Tm (A x B) A
>  pr2 : Tm (A x B) B
>  beta1 : pr1 o (f , g) = f
>  beta2 : pr2 o (f , g) = g
>  eta : p = (pr1 o p , pr2 o p)
>
>
>2. An Inductive-Inductive family of setoids that similarly mirrors the
>categorical semantics, with judgmental equality an inductive type
>family rather than coinciding with the metatheoretic equality.
>
>data Tm : Ty -> Ty -> Set where
>  id : {A} -> Tm A A
>  _o_ : Tm A B -> Tm B C -> Tm A C
>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>  pr1 : Tm (A x B) A
>  pr2 : Tm (A x B) B
>
>data Eq : Tm A B -> Tm A B -> Set where
>  assoc : Eq (h o (g o f)) ((h o g) o f)
>  lid : Eq (id o f) f
>  rid : Eq 9f o id) f
>  beta1 : Eq (pr1 o (f , g)) f
>  beta2 : Eq (pr2 o (f , g)) g
>  eta : Eq p (pr1 o p , pr2 o p)
>
>
>3. A QIIT that instead mirrors the usual type-theoretic syntax, with
>operations like composition being admissible rather than primitive.
>In our simple case it looks like this:
>
>data Tm : Ty -> Ty -> Set where
>  id : {A} -> Tm A A
>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>  pr1 : Tm A (B x C) -> Tm A B
>  pr2 : Tm A (B x C) -> Tm A C
>  beta1 : pr1 (f , g) = f
>  beta2 : pr2 (f , g) = g
>  eta : p = (pr1 p , pr2 p)
>
>
>4. Combining 2 and 3, an II family of setoids that mirrors
>type-theoretic syntax.
>
>data Tm : Ty -> Ty -> Set where
>  id : {A} -> Tm A A
>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>  pr1 : Tm A (B x C) -> Tm A B
>  pr2 : Tm A (B x C) -> Tm A C
>
>data Eq : Tm A B -> Tm A B -> Set where
>  beta1 : Eq (pr1 (f , g)) f
>  beta2 : Eq (pr2 (f , g)) g
>  eta : Eq p (pr1 p , pr2 p)
>
>
>5. A single inductive type of raw terms, together with inductive
>predicates over it for the typing judgment and equality judgments.
>
>data Tm : Set where
>  var : Tm
>  (_,_) : Tm -> Tm -> Tm
>  pr1 : Tm -> Tm
>  pr2 : Tm -> Tm
>
>data Of : Ty -> Tm -> Ty -> Set where
>  of-var : Of A var A
>  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>  of-pr1 : Of A t (B x C) -> Of A (pr1 t) B
>  of-pr2 : Of A t (B x C) -> Of A (pr2 t) C
>
>data Eq : Ty -> Tm -> Tm -> Ty -> Set where
>  beta1 : Of A t B -> Of A s C -> Eq A (pr1 (t , s)) t B
>  beta2 : Of A t B -> Of A s C -> Eq A (pr2 (t , s)) t C
>  eta : Of A t (B x C) -> Eq A (pr1 t , pr2 t) t (B x C)
>
>
>6. An II family that defines only the normal forms, via a separate
>judgment for "atomic" terms that prevents us from writing down any
>beta-redexes, thereby eliminating the need for any equality judgment
>(though substitution then becomes more complicated, as it must
>essentially incorporate beta-reduction).
>
>data Atom : Ty -> Ty -> Set where
>  id : {A} -> Atom A A
>  pr1 : Atom A (B x C) -> Atom A B
>  pr2 : Atom A (B x C) -> Atom A C
>
>data Tm : Ty -> Ty -> Set where
>  atom : Atom A B -> Tm A B
>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>
>
>7. Combining 5 and 6, an inductive type of raw terms and predicates
>over it that type only the normal forms.
>
>data Tm : Set where
>  var : Tm
>  (_,_) : Tm -> Tm -> Tm
>  pr1 : Tm -> Tm
>  pr2 : Tm -> Tm
>
>data Atom : Ty -> Tm -> Ty -> Set where
>  atom-var : Atom A var A
>  atom-pr1 : Atom A t (B x C) -> Atom A (pr1 t) B
>  atom-pr2 : Atom A t (B x C) -> Atom A (pr2 t) C
>
>data Of : Ty -> Tm -> Ty -> Set where
>  of-atom : Atom A t B -> Of A t B
>  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>
>
>This is all I can think of right now.  Are there others?  Are there
>other choices we can make in the case of dependent type theory that
>are not visible in this simple case?
>
>In the above simple case of unary type theory with products, it should
>be easy to show that all these definitions construct the initial
>category with products.  (There should be some generating/axiomatic
>types and terms too, to make the result nontrivial, but I've left them
>out for brevity.)  My main question is, where do things become hard in
>the case of dependent type theory?
>
>It seems to me that the main difference between (1) and (2), and
>between (3) and (4), is convenience; is that right?  Type theory has
>no infinitary constructors, so there shouldn't be axiom-of-choice
>issues with descending algebraic operations to a quotient; it's just
>that the bookkeeping involved in dealing with setoids everywhere
>becomes unmanageable in the case of DTT.  Right?
>
>Thorsten said that (1) in the case of dependent type theory is
>tautologically the initial CwF, which seems eminently plausible.  I
>don't think this solves the "initiality conjecture", but where is the
>sticking point?  Is it between (1) and (3), or between (3) and (5)?
>
>(Note that I'm not talking at all about the "h-level problem" that
>these QIITs are by definition sets but that for HoTT to "eat itself"
>we would want to eliminate out of them into the universe which is not
>a set.  I'm only talking about initiality of syntax among *strict*
>CwFs; coherence/strictification theorems can wait.  Personally,
>though, I like (6)-(7) as potential approaches to coherence.)
>
>-- 
>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.




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

Re: [HoTT] Where is the problem with initiality?

[Michael Shulman]

Thanks for your response Thorsten!  I did not intend my original email
as a criticism or alternative proposal to your work, only an
informational question as to where the difficulty is in getting from
the "tautological" initiality theorem in your work to the "hard"
initiality theorem that various other people are working on proving
(whatever one's opinion may be about which of them is more important).

That said, I suppose I may as well pick up that gauntlet you left on
the floor...  (-:O

On Wed, May 23, 2018 at 9:26 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> It seems to me that a lot in Mathematics can be described as convenience.
> Sometimes a good (but equivalent) choice of representation can make all
> the difference.

I agree entirely; I didn't mean the word "convenience" to be at all perjorative.

> (5) and (7) introduce preterms which I think shouldn't be considered
> fundamental in the definition of type theory.

I have to disagree here.  In my view, we have to eventually connect
things back to untyped syntax, because untyped syntax is what we write
on the page, and what we enter into a proof assistant.  (We don't need
to go all the way back to character strings -- parsing and lexing are
essentially solved problems in any language -- but we do need to get
back to some kind of untyped *abstract* syntax such as in (5).)  The
various kinds of typed syntax are useful and important intermediate
objects, but at some point there has to be a step that formally
explains how to produce "typed syntax" from untyped syntax.

I suppose you could play word games and call the typed syntax the
"definition of type theory" and the untyped syntax a "technical tool
for presenting terms in type theory" or something like that, but the
point is that the untyped syntax has to be there at some point, or
else our metatheory is incomplete.  And the fact that the initiality
theorem for your typed syntax is trivial while the initiality theorem
for untyped syntax is hard means that this gap has real mathematical
content and can't be dismissed as obvious or not worth worrying about.

> Substitution is a defined metatheoretic operation. Once you take these
> choices you spend a lot of time proving things which should be obvious.
> Now, obviously there is not one "best" way to define type theory but I
> think we have made a lot of progress. The basic ingredients of this
> progress are:
>
> 1. Substitution is a term constructor

I have to disagree here too.  Substitution should *not* be a term
constructor (at least, not in the fundamental definition of type
theory), because *in practice* the terms we write do not contain
explicit substitutions.  When I tell my calculus students to
substitute g(x) for y in f'(y) in the chain rule, I expect them to
write f'(g(x)), not f'(y)[g(x)/y].  Using explicit substitutions in
the syntax makes the semantics easier, but at the expense of "changing
the question" away from the one we wanted to ask in the first place.
In the end we want to interpret the *actual* syntax we write down on
the page.

Of course, in an intermediate step like QIIT typed syntax, we are free
to choose to make substitution explicit; but eventually we need to
make the connection back to a syntax in which substitution is
implicit.

> Just to comment on the h-level problem you don't want to discuss yet: it
> seems to me that if we want to use something along the line of (6) to
> define normal forms for dependent types we face the problem that we need
> to define normalisation at the same time as the terms. This is
> induction-recursion which on it's own shouldn't be a problem.

I actually think it's better to define the graph of hereditary
substitution inductive-inductively along with the terms, but that may
be largely aesthetic; in general I prefer induction-induction over
induction-recursion.

> However, it
> seems to me that we have to prove properties of normalisation (e.g.
> substitution laws) at the same time which again give rise to coherence
> problems.

I agree, both approaches will have to deal with coherence, since they
are essentially proving the same theorem in two different ways.  The
advantage I envision for (6) is that the coherence is all encapsulated
in the *operation* of hereditary substitution and corresponding
"higher operations": the actual *equality* on normal forms coincides
with the metatheoretic equality *without* the need to impose
equality-constructors.  It seems to me that this may be useful when we
come to interpret the untyped syntax into the typed syntax, because it
means there is no "coercion rule" in the typed syntax to worry about
having to apply.

I agree that non-normal forms are important, for the same reason that
untyped syntax is important, namely that we actually write them on the
page.  But since the typed syntax is just an intermediate step between
what we write on the page and its semantic interpretation, I don't see
a problem with performing the normalization in the same step that
interprets untyped syntax into typed syntax.

> It would be interesting to see a way to avoid these issues, but
> then wouldn't we be able to solve the problem to define semi-simlicial
> sets (or more general reedy limits) in plain HoTT?
>
>
> Thorsten
>
> On 22/05/2018, 06:46, "homotopyt...@googlegroups.com on behalf of
> Michael Shulman" <homotopyt...@googlegroups.com on behalf of
> shu...@sandiego.edu> wrote:
>
>>Thorsten gave a very nice HoTTEST talk a couple weeks ago about his
>>work with his collaborators on intrinsic syntax as a Quotient
>>Inductive-Inductive Type.  Since then I have been trying to fit
>>together a mental picture of exactly how all the different approaches
>>to syntax are related, but I am still kind of confused.
>>
>>In an attempt to clarify what I mean by "all the different
>>approaches", let me describe all the approaches I can think of in the
>>case of a very simple type theory: non-dependent unary type theory
>>with product types.  Unary means that the judgments have exactly one
>>type in the context, x:A |- t:B, and the only type constructor is a
>>product type A x B, with pairing for an introduction rule and
>>projections for elimination.  The semantics should be a category with
>>finite products.  Here are all the ways I can think of to describe
>>such a type theory:
>>
>>
>>1. A QIIT that mirrors the semantics, with all the categorical
>>operations as point-constructors and their axioms as
>>equality-constructors.
>>
>>data Ty : Set where
>> _x_ : Ty -> Ty -> Ty
>>[This will be the same in all cases, so I henceforth omit it.]
>>
>>data Tm : Ty -> Ty -> Set where
>>  id : {A} -> Tm A A
>>  _o_ : Tm A B -> Tm B C -> Tm A C
>>  assoc : h o (g o f) = (h o g) o f
>>  lid : id o f = f
>>  rid : f o id = f
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>  pr1 : Tm (A x B) A
>>  pr2 : Tm (A x B) B
>>  beta1 : pr1 o (f , g) = f
>>  beta2 : pr2 o (f , g) = g
>>  eta : p = (pr1 o p , pr2 o p)
>>
>>
>>2. An Inductive-Inductive family of setoids that similarly mirrors the
>>categorical semantics, with judgmental equality an inductive type
>>family rather than coinciding with the metatheoretic equality.
>>
>>data Tm : Ty -> Ty -> Set where
>>  id : {A} -> Tm A A
>>  _o_ : Tm A B -> Tm B C -> Tm A C
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>  pr1 : Tm (A x B) A
>>  pr2 : Tm (A x B) B
>>
>>data Eq : Tm A B -> Tm A B -> Set where
>>  assoc : Eq (h o (g o f)) ((h o g) o f)
>>  lid : Eq (id o f) f
>>  rid : Eq 9f o id) f
>>  beta1 : Eq (pr1 o (f , g)) f
>>  beta2 : Eq (pr2 o (f , g)) g
>>  eta : Eq p (pr1 o p , pr2 o p)
>>
>>
>>3. A QIIT that instead mirrors the usual type-theoretic syntax, with
>>operations like composition being admissible rather than primitive.
>>In our simple case it looks like this:
>>
>>data Tm : Ty -> Ty -> Set where
>>  id : {A} -> Tm A A
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>  pr1 : Tm A (B x C) -> Tm A B
>>  pr2 : Tm A (B x C) -> Tm A C
>>  beta1 : pr1 (f , g) = f
>>  beta2 : pr2 (f , g) = g
>>  eta : p = (pr1 p , pr2 p)
>>
>>
>>4. Combining 2 and 3, an II family of setoids that mirrors
>>type-theoretic syntax.
>>
>>data Tm : Ty -> Ty -> Set where
>>  id : {A} -> Tm A A
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>  pr1 : Tm A (B x C) -> Tm A B
>>  pr2 : Tm A (B x C) -> Tm A C
>>
>>data Eq : Tm A B -> Tm A B -> Set where
>>  beta1 : Eq (pr1 (f , g)) f
>>  beta2 : Eq (pr2 (f , g)) g
>>  eta : Eq p (pr1 p , pr2 p)
>>
>>
>>5. A single inductive type of raw terms, together with inductive
>>predicates over it for the typing judgment and equality judgments.
>>
>>data Tm : Set where
>>  var : Tm
>>  (_,_) : Tm -> Tm -> Tm
>>  pr1 : Tm -> Tm
>>  pr2 : Tm -> Tm
>>
>>data Of : Ty -> Tm -> Ty -> Set where
>>  of-var : Of A var A
>>  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>>  of-pr1 : Of A t (B x C) -> Of A (pr1 t) B
>>  of-pr2 : Of A t (B x C) -> Of A (pr2 t) C
>>
>>data Eq : Ty -> Tm -> Tm -> Ty -> Set where
>>  beta1 : Of A t B -> Of A s C -> Eq A (pr1 (t , s)) t B
>>  beta2 : Of A t B -> Of A s C -> Eq A (pr2 (t , s)) t C
>>  eta : Of A t (B x C) -> Eq A (pr1 t , pr2 t) t (B x C)
>>
>>
>>6. An II family that defines only the normal forms, via a separate
>>judgment for "atomic" terms that prevents us from writing down any
>>beta-redexes, thereby eliminating the need for any equality judgment
>>(though substitution then becomes more complicated, as it must
>>essentially incorporate beta-reduction).
>>
>>data Atom : Ty -> Ty -> Set where
>>  id : {A} -> Atom A A
>>  pr1 : Atom A (B x C) -> Atom A B
>>  pr2 : Atom A (B x C) -> Atom A C
>>
>>data Tm : Ty -> Ty -> Set where
>>  atom : Atom A B -> Tm A B
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>
>>
>>7. Combining 5 and 6, an inductive type of raw terms and predicates
>>over it that type only the normal forms.
>>
>>data Tm : Set where
>>  var : Tm
>>  (_,_) : Tm -> Tm -> Tm
>>  pr1 : Tm -> Tm
>>  pr2 : Tm -> Tm
>>
>>data Atom : Ty -> Tm -> Ty -> Set where
>>  atom-var : Atom A var A
>>  atom-pr1 : Atom A t (B x C) -> Atom A (pr1 t) B
>>  atom-pr2 : Atom A t (B x C) -> Atom A (pr2 t) C
>>
>>data Of : Ty -> Tm -> Ty -> Set where
>>  of-atom : Atom A t B -> Of A t B
>>  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>>
>>
>>This is all I can think of right now.  Are there others?  Are there
>>other choices we can make in the case of dependent type theory that
>>are not visible in this simple case?
>>
>>In the above simple case of unary type theory with products, it should
>>be easy to show that all these definitions construct the initial
>>category with products.  (There should be some generating/axiomatic
>>types and terms too, to make the result nontrivial, but I've left them
>>out for brevity.)  My main question is, where do things become hard in
>>the case of dependent type theory?
>>
>>It seems to me that the main difference between (1) and (2), and
>>between (3) and (4), is convenience; is that right?  Type theory has
>>no infinitary constructors, so there shouldn't be axiom-of-choice
>>issues with descending algebraic operations to a quotient; it's just
>>that the bookkeeping involved in dealing with setoids everywhere
>>becomes unmanageable in the case of DTT.  Right?
>>
>>Thorsten said that (1) in the case of dependent type theory is
>>tautologically the initial CwF, which seems eminently plausible.  I
>>don't think this solves the "initiality conjecture", but where is the
>>sticking point?  Is it between (1) and (3), or between (3) and (5)?
>>
>>(Note that I'm not talking at all about the "h-level problem" that
>>these QIITs are by definition sets but that for HoTT to "eat itself"
>>we would want to eliminate out of them into the universe which is not
>>a set.  I'm only talking about initiality of syntax among *strict*
>>CwFs; coherence/strictification theorems can wait.  Personally,
>>though, I like (6)-(7) as potential approaches to coherence.)
>>
>>--
>>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.
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> --
> 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.

Re: [HoTT] Where is the problem with initiality?

[Thorsten Altenkirch]

>
>Thanks for your response Thorsten!  I did not intend my original email
>as a criticism or alternative proposal to your work, only an
>informational question as to where the difficulty is in getting from
>the "tautological" initiality theorem in your work to the "hard"
>initiality theorem that various other people are working on proving
>(whatever one's opinion may be about which of them is more important).

I didn't view it as criticism - I was just commenting on your email.

>
>That said, I suppose I may as well pick up that gauntlet you left on
>the floor...  (-:O

Ah good. :-)

>>(5) and (7) introduce preterms which I think shouldn't be considered
>> fundamental in the definition of type theory.
>
>I have to disagree here.  In my view, we have to eventually connect
>things back to untyped syntax, because untyped syntax is what we write
>on the page, and what we enter into a proof assistant.  (We don't need
>to go all the way back to character strings -- parsing and lexing are
>essentially solved problems in any language -- but we do need to get
>back to some kind of untyped *abstract* syntax such as in (5).)  The
>various kinds of typed syntax are useful and important intermediate
>objects, but at some point there has to be a step that formally
>explains how to produce "typed syntax" from untyped syntax.

Indeed but also type checking and scoping are solved problems.

We may as well say that parsing, that is relating strings and trees is a
fundamental issue in algebra. It isn't. By the way that isn't so far
fetched as it sounds, in (older?) text books on regular expressions you
find the rule that if E is a regular expression then so is (E). Actually,
you may find the same on lambda calculus.

>
>I suppose you could play word games and call the typed syntax the
>"definition of type theory" and the untyped syntax a "technical tool
>for presenting terms in type theory" or something like that, but the
>point is that the untyped syntax has to be there at some point, or
>else our metatheory is incomplete.

As with the strings...

> And the fact that the initiality
>theorem for your typed syntax is trivial while the initiality theorem
>for untyped syntax is hard means that this gap has real mathematical
>content and can't be dismissed as obvious or not worth worrying about.

Neither can parsing.

>
>> Substitution is a defined metatheoretic operation. Once you take these
>> choices you spend a lot of time proving things which should be obvious.
>> Now, obviously there is not one "best" way to define type theory but I
>> think we have made a lot of progress. The basic ingredients of this
>> progress are:
>>
>> 1. Substitution is a term constructor
>
>I have to disagree here too.  Substitution should *not* be a term
>constructor (at least, not in the fundamental definition of type
>theory), because *in practice* the terms we write do not contain
>explicit substitutions.  When I tell my calculus students to
>substitute g(x) for y in f'(y) in the chain rule, I expect them to
>write f'(g(x)), not f'(y)[g(x)/y].  Using explicit substitutions in
>the syntax makes the semantics easier, but at the expense of "changing
>the question" away from the one we wanted to ask in the first place.
>In the end we want to interpret the *actual* syntax we write down on
>the page.

But doesn't the same apply to beta-redeces? We don't write programs
containing beta-redeces, they only show up when we expand definitions. The
same with substitutions: we don't write them but they show up for example
when we reduced beta redeces.

>Of course, in an intermediate step like QIIT typed syntax, we are free
>to choose to make substitution explicit; but eventually we need to
>make the connection back to a syntax in which substitution is
>implicit.

We only write substitution normal forms as we only write beta normal terms.

>
>> Just to comment on the h-level problem you don't want to discuss yet: it
>> seems to me that if we want to use something along the line of (6) to
>> define normal forms for dependent types we face the problem that we need
>> to define normalisation at the same time as the terms. This is
>> induction-recursion which on it's own shouldn't be a problem.
>
>I actually think it's better to define the graph of hereditary
>substitution inductive-inductively along with the terms, but that may
>be largely aesthetic; in general I prefer induction-induction over
>induction-recursion.
>
>> However, it
>> seems to me that we have to prove properties of normalisation (e.g.
>> substitution laws) at the same time which again give rise to coherence
>> problems.
>
>I agree, both approaches will have to deal with coherence, since they
>are essentially proving the same theorem in two different ways.  The
>advantage I envision for (6) is that the coherence is all encapsulated
>in the *operation* of hereditary substitution and corresponding
>"higher operations": the actual *equality* on normal forms coincides
>with the metatheoretic equality *without* the need to impose
>equality-constructors.  It seems to me that this may be useful when we
>come to interpret the untyped syntax into the typed syntax, because it
>means there is no "coercion rule" in the typed syntax to worry about
>having to apply.
>
>I agree that non-normal forms are important, for the same reason that
>untyped syntax is important, namely that we actually write them on the
>page.  But since the typed syntax is just an intermediate step between
>what we write on the page and its semantic interpretation, I don't see
>a problem with performing the normalization in the same step that
>interprets untyped syntax into typed syntax.
>
>> It would be interesting to see a way to avoid these issues, but
>> then wouldn't we be able to solve the problem to define semi-simlicial
>> sets (or more general reedy limits) in plain HoTT?
>>
>>
>> Thorsten
>>
>> On 22/05/2018, 06:46, "homotopyt...@googlegroups.com on behalf of
>> Michael Shulman" <homotopyt...@googlegroups.com on behalf of
>> shu...@sandiego.edu> wrote:
>>
>>>Thorsten gave a very nice HoTTEST talk a couple weeks ago about his
>>>work with his collaborators on intrinsic syntax as a Quotient
>>>Inductive-Inductive Type.  Since then I have been trying to fit
>>>together a mental picture of exactly how all the different approaches
>>>to syntax are related, but I am still kind of confused.
>>>
>>>In an attempt to clarify what I mean by "all the different
>>>approaches", let me describe all the approaches I can think of in the
>>>case of a very simple type theory: non-dependent unary type theory
>>>with product types.  Unary means that the judgments have exactly one
>>>type in the context, x:A |- t:B, and the only type constructor is a
>>>product type A x B, with pairing for an introduction rule and
>>>projections for elimination.  The semantics should be a category with
>>>finite products.  Here are all the ways I can think of to describe
>>>such a type theory:
>>>
>>>
>>>1. A QIIT that mirrors the semantics, with all the categorical
>>>operations as point-constructors and their axioms as
>>>equality-constructors.
>>>
>>>data Ty : Set where
>>> _x_ : Ty -> Ty -> Ty
>>>[This will be the same in all cases, so I henceforth omit it.]
>>>
>>>data Tm : Ty -> Ty -> Set where
>>>  id : {A} -> Tm A A
>>>  _o_ : Tm A B -> Tm B C -> Tm A C
>>>  assoc : h o (g o f) = (h o g) o f
>>>  lid : id o f = f
>>>  rid : f o id = f
>>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>>  pr1 : Tm (A x B) A
>>>  pr2 : Tm (A x B) B
>>>  beta1 : pr1 o (f , g) = f
>>>  beta2 : pr2 o (f , g) = g
>>>  eta : p = (pr1 o p , pr2 o p)
>>>
>>>
>>>2. An Inductive-Inductive family of setoids that similarly mirrors the
>>>categorical semantics, with judgmental equality an inductive type
>>>family rather than coinciding with the metatheoretic equality.
>>>
>>>data Tm : Ty -> Ty -> Set where
>>>  id : {A} -> Tm A A
>>>  _o_ : Tm A B -> Tm B C -> Tm A C
>>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>>  pr1 : Tm (A x B) A
>>>  pr2 : Tm (A x B) B
>>>
>>>data Eq : Tm A B -> Tm A B -> Set where
>>>  assoc : Eq (h o (g o f)) ((h o g) o f)
>>>  lid : Eq (id o f) f
>>>  rid : Eq 9f o id) f
>>>  beta1 : Eq (pr1 o (f , g)) f
>>>  beta2 : Eq (pr2 o (f , g)) g
>>>  eta : Eq p (pr1 o p , pr2 o p)
>>>
>>>
>>>3. A QIIT that instead mirrors the usual type-theoretic syntax, with
>>>operations like composition being admissible rather than primitive.
>>>In our simple case it looks like this:
>>>
>>>data Tm : Ty -> Ty -> Set where
>>>  id : {A} -> Tm A A
>>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>>  pr1 : Tm A (B x C) -> Tm A B
>>>  pr2 : Tm A (B x C) -> Tm A C
>>>  beta1 : pr1 (f , g) = f
>>>  beta2 : pr2 (f , g) = g
>>>  eta : p = (pr1 p , pr2 p)
>>>
>>>
>>>4. Combining 2 and 3, an II family of setoids that mirrors
>>>type-theoretic syntax.
>>>
>>>data Tm : Ty -> Ty -> Set where
>>>  id : {A} -> Tm A A
>>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>>  pr1 : Tm A (B x C) -> Tm A B
>>>  pr2 : Tm A (B x C) -> Tm A C
>>>
>>>data Eq : Tm A B -> Tm A B -> Set where
>>>  beta1 : Eq (pr1 (f , g)) f
>>>  beta2 : Eq (pr2 (f , g)) g
>>>  eta : Eq p (pr1 p , pr2 p)
>>>
>>>
>>>5. A single inductive type of raw terms, together with inductive
>>>predicates over it for the typing judgment and equality judgments.
>>>
>>>data Tm : Set where
>>>  var : Tm
>>>  (_,_) : Tm -> Tm -> Tm
>>>  pr1 : Tm -> Tm
>>>  pr2 : Tm -> Tm
>>>
>>>data Of : Ty -> Tm -> Ty -> Set where
>>>  of-var : Of A var A
>>>  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>>>  of-pr1 : Of A t (B x C) -> Of A (pr1 t) B
>>>  of-pr2 : Of A t (B x C) -> Of A (pr2 t) C
>>>
>>>data Eq : Ty -> Tm -> Tm -> Ty -> Set where
>>>  beta1 : Of A t B -> Of A s C -> Eq A (pr1 (t , s)) t B
>>>  beta2 : Of A t B -> Of A s C -> Eq A (pr2 (t , s)) t C
>>>  eta : Of A t (B x C) -> Eq A (pr1 t , pr2 t) t (B x C)
>>>
>>>
>>>6. An II family that defines only the normal forms, via a separate
>>>judgment for "atomic" terms that prevents us from writing down any
>>>beta-redexes, thereby eliminating the need for any equality judgment
>>>(though substitution then becomes more complicated, as it must
>>>essentially incorporate beta-reduction).
>>>
>>>data Atom : Ty -> Ty -> Set where
>>>  id : {A} -> Atom A A
>>>  pr1 : Atom A (B x C) -> Atom A B
>>>  pr2 : Atom A (B x C) -> Atom A C
>>>
>>>data Tm : Ty -> Ty -> Set where
>>>  atom : Atom A B -> Tm A B
>>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>>
>>>
>>>7. Combining 5 and 6, an inductive type of raw terms and predicates
>>>over it that type only the normal forms.
>>>
>>>data Tm : Set where
>>>  var : Tm
>>>  (_,_) : Tm -> Tm -> Tm
>>>  pr1 : Tm -> Tm
>>>  pr2 : Tm -> Tm
>>>
>>>data Atom : Ty -> Tm -> Ty -> Set where
>>>  atom-var : Atom A var A
>>>  atom-pr1 : Atom A t (B x C) -> Atom A (pr1 t) B
>>>  atom-pr2 : Atom A t (B x C) -> Atom A (pr2 t) C
>>>
>>>data Of : Ty -> Tm -> Ty -> Set where
>>>  of-atom : Atom A t B -> Of A t B
>>>  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>>>
>>>
>>>This is all I can think of right now.  Are there others?  Are there
>>>other choices we can make in the case of dependent type theory that
>>>are not visible in this simple case?
>>>
>>>In the above simple case of unary type theory with products, it should
>>>be easy to show that all these definitions construct the initial
>>>category with products.  (There should be some generating/axiomatic
>>>types and terms too, to make the result nontrivial, but I've left them
>>>out for brevity.)  My main question is, where do things become hard in
>>>the case of dependent type theory?
>>>
>>>It seems to me that the main difference between (1) and (2), and
>>>between (3) and (4), is convenience; is that right?  Type theory has
>>>no infinitary constructors, so there shouldn't be axiom-of-choice
>>>issues with descending algebraic operations to a quotient; it's just
>>>that the bookkeeping involved in dealing with setoids everywhere
>>>becomes unmanageable in the case of DTT.  Right?
>>>
>>>Thorsten said that (1) in the case of dependent type theory is
>>>tautologically the initial CwF, which seems eminently plausible.  I
>>>don't think this solves the "initiality conjecture", but where is the
>>>sticking point?  Is it between (1) and (3), or between (3) and (5)?
>>>
>>>(Note that I'm not talking at all about the "h-level problem" that
>>>these QIITs are by definition sets but that for HoTT to "eat itself"
>>>we would want to eliminate out of them into the universe which is not
>>>a set.  I'm only talking about initiality of syntax among *strict*
>>>CwFs; coherence/strictification theorems can wait.  Personally,
>>>though, I like (6)-(7) as potential approaches to coherence.)
>>>
>>>--
>>>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.
>>
>>
>>
>>
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please contact the sender and delete the email and
>> attachment.
>>
>> Any views or opinions expressed by the author of this email do not
>> necessarily reflect the views of the University of Nottingham. Email
>> communications with the University of Nottingham may be monitored
>> where permitted by law.
>>
>>
>>
>>
>> --
>> 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.




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

Re: [HoTT] Where is the problem with initiality?

[Ambrus Kaposi]

On Thu, May 24, 2018 at 10:11 AM Thorsten Altenkirch <
Thorsten....@nottingham.ac.uk> wrote:
> >>(5) and (7) introduce preterms which I think shouldn't be considered
> >> fundamental in the definition of type theory.
> >
> >I have to disagree here.  In my view, we have to eventually connect
> >things back to untyped syntax, because untyped syntax is what we write
> >on the page, and what we enter into a proof assistant.  (We don't need
> >to go all the way back to character strings -- parsing and lexing are
> >essentially solved problems in any language -- but we do need to get
> >back to some kind of untyped *abstract* syntax such as in (5).)  The
> >various kinds of typed syntax are useful and important intermediate
> >objects, but at some point there has to be a step that formally
> >explains how to produce "typed syntax" from untyped syntax.

> Indeed but also type checking and scoping are solved problems.

Just to clarify this: you don't need to go through preterms and typing
relations to do type checking. You can write an algorithm which takes
untyped terms (without explicit substitutions) and returns intrinsic
(well-typed) terms. It only needs conversion checking for intrinsic terms
which is also a solved problem. Here is an example implementation:
https://bitbucket.org/akaposi/tt-in-tt/src/HEAD/Typecheck.agda

Re: [HoTT] Where is the problem with initiality?

[Michael Shulman]

On Thu, May 24, 2018 at 2:53 AM, Ambrus Kaposi <kaposi...@gmail.com> wrote:
> Just to clarify this: you don't need to go through preterms and typing
> relations to do type checking. You can write an algorithm which takes
> untyped terms (without explicit substitutions) and returns intrinsic
> (well-typed) terms. It only needs conversion checking for intrinsic terms
> which is also a solved problem. Here is an example implementation:
> https://bitbucket.org/akaposi/tt-in-tt/src/HEAD/Typecheck.agda

This is the sort of thing I was hoping for.  But how far is this from
a translation of (5) to (1)?  Shouldn't a typing derivation in (5) be
essentially a certificate of success for typechecking it?

Re: [HoTT] Where is the problem with initiality?

[Thomas Streicher]

Triggered by your mails I have tried to recall what I think has to
be shown for verifying the initiality conjecture.
Given a type theory with its catgeorical semantics we can construct 2
models M_a and M_s where M_a is the initial model of the respective
essentially algebraic theory and M_s is the Lindenbaum-Tarski model
obtained by factoring syntax modulo provable (judgemental) equality.
Then we have homomorphism h : M_a -> M_s (by initiality) and h' : M_s
-> M_a (essential the interpretation function for the theory in M_a).
Trivially h' \circ h is the identity. For showing that h \circ h' is
the identity one essentailly shows that interpreting syntax in M_a and
translating the result back to syntax with variables is the identity.

This last step should be a straightforward induction over syntax.
Thus the main task is to show that M_s is actually a model. This
latter task I performed for CoC in my old Thesis. This is fairly
tedious when performed in detail.

When I wrote my Thesis I didn't think about M_a at all. Instead I used
the obvious fact that interpreting syntax in M_s just amounts to
taking equivalence classes modulo provable equivalence. This suffices
for obtaining the completeness theorem I wanted to have. That M_s is
initial is then sort of obvious since M_s is term generated and
interpretation of syntax gives a morphism from M_s to any other model.

So summing up the key is to show that the Lindenbaum-Tarksi construction
gives rise to a model.

Thomas

Re: [HoTT] Where is the problem with initiality?

[Michael Shulman]

Thomas, are you saying that the hard part is proving that the syntax
of type theory is a CwF?  I always thought that was perfectly obvious
and the hard part was interpreting the syntax into some other CwF.

On Sat, May 26, 2018 at 2:21 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> Triggered by your mails I have tried to recall what I think has to
> be shown for verifying the initiality conjecture.
> Given a type theory with its catgeorical semantics we can construct 2
> models M_a and M_s where M_a is the initial model of the respective
> essentially algebraic theory and M_s is the Lindenbaum-Tarski model
> obtained by factoring syntax modulo provable (judgemental) equality.
> Then we have homomorphism h : M_a -> M_s (by initiality) and h' : M_s
> -> M_a (essential the interpretation function for the theory in M_a).
> Trivially h' \circ h is the identity. For showing that h \circ h' is
> the identity one essentailly shows that interpreting syntax in M_a and
> translating the result back to syntax with variables is the identity.
>
> This last step should be a straightforward induction over syntax.
> Thus the main task is to show that M_s is actually a model. This
> latter task I performed for CoC in my old Thesis. This is fairly
> tedious when performed in detail.
>
> When I wrote my Thesis I didn't think about M_a at all. Instead I used
> the obvious fact that interpreting syntax in M_s just amounts to
> taking equivalence classes modulo provable equivalence. This suffices
> for obtaining the completeness theorem I wanted to have. That M_s is
> initial is then sort of obvious since M_s is term generated and
> interpretation of syntax gives a morphism from M_s to any other model.
>
> So summing up the key is to show that the Lindenbaum-Tarksi construction
> gives rise to a model.
>
> Thomas
>
> --
> 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.

Re: [HoTT] Where is the problem with initiality?

[stre...]

> Thomas, are you saying that the hard part is proving that the syntax
> of type theory is a CwF?  I always thought that was perfectly obvious
> and the hard part was interpreting the syntax into some other CwF.

That was a misunderstanding on my side. Correctness is also quite an issue.

But I thought you just discussed the initiality problem!
For this the laborious part is indeed showing that Lindenbaum-Tarski gives
a model. I mean this is intuitively clear and without any surprises.
If one is not overly formalist one is happy to believe this. I possibly
was more formalist those days (:-

But formulating the correctness in terms of a partial interpretation
function on raw syntax is a nice unorthodox idea. To perform it is also a
bit dull but getting the idea how to proceed took me some time.

If I had thought in terms of initial models for essentially algebraic
theories I wouldn't have proven my completeness theorem but rather relied
on algebraic and variable syntax as obviously “isomorph“.

Thomas

Re: [HoTT] Where is the problem with initiality?

[Bas Spitters]

One question that recently came up in our work on modal type theory,
https://arxiv.org/abs/1804.05236
is: what is the right notion of morphism for CwF.
In the paper (def 9, thm 10) we propose a notion of weak CwF morphism,
where comprehension is only preserved upto iso.

The notion fits well with the local universe construction, but I
hadn't seen it before.
Peter Lumsdaine later told me that it sees CwFs as discrete
comprehension categories and where one uses pseudo-maps of comp cats.

I also noticed that the literature on categories of models of type
theory seems quite scattered (I guess this complaint is due to
Vladimir).
We know how to translate between different models of type theory, but
I don't know of a convenient place to find all the functorial
properties.

On Sat, May 26, 2018 at 6:47 PM,  <stre...@mathematik.tu-darmstadt.de> wrote:
>> Thomas, are you saying that the hard part is proving that the syntax
>> of type theory is a CwF?  I always thought that was perfectly obvious
>> and the hard part was interpreting the syntax into some other CwF.
>
> That was a misunderstanding on my side. Correctness is also quite an issue.
>
> But I thought you just discussed the initiality problem!
> For this the laborious part is indeed showing that Lindenbaum-Tarski gives
> a model. I mean this is intuitively clear and without any surprises.
> If one is not overly formalist one is happy to believe this. I possibly
> was more formalist those days (:-
>
> But formulating the correctness in terms of a partial interpretation
> function on raw syntax is a nice unorthodox idea. To perform it is also a
> bit dull but getting the idea how to proceed took me some time.
>
> If I had thought in terms of initial models for essentially algebraic
> theories I wouldn't have proven my completeness theorem but rather relied
> on algebraic and variable syntax as obviously “isomorph“.
>
> Thomas
>
> --
> 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.

Re: Where is the problem with initiality?

[Michael Shulman]

I knew this situation seemed familiar: it reminds me of Tom Leinster's
comments about the homotopy hypothesis:
https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html
(scroll down to "What is an n-category?")

The "Homotopy Hypothesis" of higher category theory, first formulated
by Grothendieck, is the claim that "infinity-groupoids are the same as
spaces".  The prevailing approach to this in higher category theory
nowadays is the one that Tom describes as a "joke":

Q.  How do you prove the Homotopy Hypothesis?
A.  Define an infinity-groupoid to be a Kan complex; define a space to
be a Kan complex; done!

Describing this as a joke is not to denigrate the value of such a
"definitional solution"; it's certainly been enormously fruitful for
higher category theory.  But at the same time, Tom's point is that it
doesn't, on its own, answer the question that was originally asked.
He has a nice picture of a spectrum from "algebra" to "topology",
starting with algebraic notions of infinity-groupoid, then moving
through non-algebraic notions of infinity-groupoid, to algebraic
notions of space, and eventually non-algebraic notions of space, with
Kan complexes occupying the fulcum at the middle.  A full-strength
statement of the homotopy hypothesis would then equate fully algebraic
notions of infinity-groupoid with fully non-algebraic notions of
space.

I feel like here we have something similar.  If we call the
"Initiality Hypothesis" something like "type theory is the initial
elementary infinity-topos", then we can make a similar "joke":

Q: How do you prove the Initiality Hypothesis?
A: Define an elementary infinity-topos to be a (suitably structured)
CwF; define type theory to be the initial such CwF; done!

Again, this is not to denigrate the value of such an approach!  It
just doesn't, on its own, answer the original question.  I can imagine
a similar spectrum from "syntax" to "semantics", starting with
"syntactic notions of type theory", then moving through "semantic
notions of type theory", to "syntactic notions of toposes", and
eventually "semantic notions of toposes".  Untyped syntax with
implicit substitution (5) is way over on the syntactic side; locally
cartesian closed quasicategories with appropriate stuff are way over
on the semantic side; CwFs and the initial one as a QIIT are at the
fulcrum in the middle.  And just as Kan complexes can play an
important intermediate role in connecting the disparate ends of the
homotopy-hypothesis spectrum, it seems likely that QIIT syntax can
play a similar intermediate role in connecting the ends of the
initiality-hypothesis spectrum.

Does this seem reasonable?


On Mon, May 21, 2018 at 10:46 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> Thorsten gave a very nice HoTTEST talk a couple weeks ago about his
> work with his collaborators on intrinsic syntax as a Quotient
> Inductive-Inductive Type.  Since then I have been trying to fit
> together a mental picture of exactly how all the different approaches
> to syntax are related, but I am still kind of confused.
>
> In an attempt to clarify what I mean by "all the different
> approaches", let me describe all the approaches I can think of in the
> case of a very simple type theory: non-dependent unary type theory
> with product types.  Unary means that the judgments have exactly one
> type in the context, x:A |- t:B, and the only type constructor is a
> product type A x B, with pairing for an introduction rule and
> projections for elimination.  The semantics should be a category with
> finite products.  Here are all the ways I can think of to describe
> such a type theory:
>
>
> 1. A QIIT that mirrors the semantics, with all the categorical
> operations as point-constructors and their axioms as
> equality-constructors.
>
> data Ty : Set where
>  _x_ : Ty -> Ty -> Ty
> [This will be the same in all cases, so I henceforth omit it.]
>
> data Tm : Ty -> Ty -> Set where
>   id : {A} -> Tm A A
>   _o_ : Tm A B -> Tm B C -> Tm A C
>   assoc : h o (g o f) = (h o g) o f
>   lid : id o f = f
>   rid : f o id = f
>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>   pr1 : Tm (A x B) A
>   pr2 : Tm (A x B) B
>   beta1 : pr1 o (f , g) = f
>   beta2 : pr2 o (f , g) = g
>   eta : p = (pr1 o p , pr2 o p)
>
>
> 2. An Inductive-Inductive family of setoids that similarly mirrors the
> categorical semantics, with judgmental equality an inductive type
> family rather than coinciding with the metatheoretic equality.
>
> data Tm : Ty -> Ty -> Set where
>   id : {A} -> Tm A A
>   _o_ : Tm A B -> Tm B C -> Tm A C
>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>   pr1 : Tm (A x B) A
>   pr2 : Tm (A x B) B
>
> data Eq : Tm A B -> Tm A B -> Set where
>   assoc : Eq (h o (g o f)) ((h o g) o f)
>   lid : Eq (id o f) f
>   rid : Eq 9f o id) f
>   beta1 : Eq (pr1 o (f , g)) f
>   beta2 : Eq (pr2 o (f , g)) g
>   eta : Eq p (pr1 o p , pr2 o p)
>
>
> 3. A QIIT that instead mirrors the usual type-theoretic syntax, with
> operations like composition being admissible rather than primitive.
> In our simple case it looks like this:
>
> data Tm : Ty -> Ty -> Set where
>   id : {A} -> Tm A A
>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>   pr1 : Tm A (B x C) -> Tm A B
>   pr2 : Tm A (B x C) -> Tm A C
>   beta1 : pr1 (f , g) = f
>   beta2 : pr2 (f , g) = g
>   eta : p = (pr1 p , pr2 p)
>
>
> 4. Combining 2 and 3, an II family of setoids that mirrors
> type-theoretic syntax.
>
> data Tm : Ty -> Ty -> Set where
>   id : {A} -> Tm A A
>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>   pr1 : Tm A (B x C) -> Tm A B
>   pr2 : Tm A (B x C) -> Tm A C
>
> data Eq : Tm A B -> Tm A B -> Set where
>   beta1 : Eq (pr1 (f , g)) f
>   beta2 : Eq (pr2 (f , g)) g
>   eta : Eq p (pr1 p , pr2 p)
>
>
> 5. A single inductive type of raw terms, together with inductive
> predicates over it for the typing judgment and equality judgments.
>
> data Tm : Set where
>   var : Tm
>   (_,_) : Tm -> Tm -> Tm
>   pr1 : Tm -> Tm
>   pr2 : Tm -> Tm
>
> data Of : Ty -> Tm -> Ty -> Set where
>   of-var : Of A var A
>   of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>   of-pr1 : Of A t (B x C) -> Of A (pr1 t) B
>   of-pr2 : Of A t (B x C) -> Of A (pr2 t) C
>
> data Eq : Ty -> Tm -> Tm -> Ty -> Set where
>   beta1 : Of A t B -> Of A s C -> Eq A (pr1 (t , s)) t B
>   beta2 : Of A t B -> Of A s C -> Eq A (pr2 (t , s)) t C
>   eta : Of A t (B x C) -> Eq A (pr1 t , pr2 t) t (B x C)
>
>
> 6. An II family that defines only the normal forms, via a separate
> judgment for "atomic" terms that prevents us from writing down any
> beta-redexes, thereby eliminating the need for any equality judgment
> (though substitution then becomes more complicated, as it must
> essentially incorporate beta-reduction).
>
> data Atom : Ty -> Ty -> Set where
>   id : {A} -> Atom A A
>   pr1 : Atom A (B x C) -> Atom A B
>   pr2 : Atom A (B x C) -> Atom A C
>
> data Tm : Ty -> Ty -> Set where
>   atom : Atom A B -> Tm A B
>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>
>
> 7. Combining 5 and 6, an inductive type of raw terms and predicates
> over it that type only the normal forms.
>
> data Tm : Set where
>   var : Tm
>   (_,_) : Tm -> Tm -> Tm
>   pr1 : Tm -> Tm
>   pr2 : Tm -> Tm
>
> data Atom : Ty -> Tm -> Ty -> Set where
>   atom-var : Atom A var A
>   atom-pr1 : Atom A t (B x C) -> Atom A (pr1 t) B
>   atom-pr2 : Atom A t (B x C) -> Atom A (pr2 t) C
>
> data Of : Ty -> Tm -> Ty -> Set where
>   of-atom : Atom A t B -> Of A t B
>   of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>
>
> This is all I can think of right now.  Are there others?  Are there
> other choices we can make in the case of dependent type theory that
> are not visible in this simple case?
>
> In the above simple case of unary type theory with products, it should
> be easy to show that all these definitions construct the initial
> category with products.  (There should be some generating/axiomatic
> types and terms too, to make the result nontrivial, but I've left them
> out for brevity.)  My main question is, where do things become hard in
> the case of dependent type theory?
>
> It seems to me that the main difference between (1) and (2), and
> between (3) and (4), is convenience; is that right?  Type theory has
> no infinitary constructors, so there shouldn't be axiom-of-choice
> issues with descending algebraic operations to a quotient; it's just
> that the bookkeeping involved in dealing with setoids everywhere
> becomes unmanageable in the case of DTT.  Right?
>
> Thorsten said that (1) in the case of dependent type theory is
> tautologically the initial CwF, which seems eminently plausible.  I
> don't think this solves the "initiality conjecture", but where is the
> sticking point?  Is it between (1) and (3), or between (3) and (5)?
>
> (Note that I'm not talking at all about the "h-level problem" that
> these QIITs are by definition sets but that for HoTT to "eat itself"
> we would want to eliminate out of them into the universe which is not
> a set.  I'm only talking about initiality of syntax among *strict*
> CwFs; coherence/strictification theorems can wait.  Personally,
> though, I like (6)-(7) as potential approaches to coherence.)

Re: [HoTT] Re: Where is the problem with initiality?

[Thorsten Altenkirch]

Hi Mike,

you are right there is a genuine content in the initiality theorem. Indeed, we are using the preterm/judgement presentation to construct initial QIITs (jww Ambrus Kaposi, Andras Kovac and Jakob von Raumer) in general. Jakob is currently implementing a plugin for Lean that allows us to define QIITs even though they are not present in Lean’s core theory.

What I am arguing about is the way the syntax of type theory should be presented. The separation of preterms and typing derivation reflects conventional thinking, in the sense that collection and logical reasoning need to be separated. To me one of the important innovations of type theory is not only that they don’t need to be separated, they shouldn’t. If we think that type theory is a good way to present Mathematics then shouldn’t we use it, when we present the syntax of type theory?

The intrinsic presentation also capture the spirit of type theory in the sense that we are only interested in typed objects, I.e. that we don’t need to think about untyped objects first.

There is no contradiction in saying that the initiality theorem is useful: it helps to relate systems which are inspired by the old thinking to the new ideas (in CS we call this “legacy software”). I think QITs and HITs should be primitive and once they are there is no need to present type theory in the extrinsic way. 

Thorsten




On 28/05/2018, 23:39, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:

>I knew this situation seemed familiar: it reminds me of Tom Leinster's
>comments about the homotopy hypothesis:
>https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html
>(scroll down to "What is an n-category?")
>
>The "Homotopy Hypothesis" of higher category theory, first formulated
>by Grothendieck, is the claim that "infinity-groupoids are the same as
>spaces".  The prevailing approach to this in higher category theory
>nowadays is the one that Tom describes as a "joke":
>
>Q.  How do you prove the Homotopy Hypothesis?
>A.  Define an infinity-groupoid to be a Kan complex; define a space to
>be a Kan complex; done!
>
>Describing this as a joke is not to denigrate the value of such a
>"definitional solution"; it's certainly been enormously fruitful for
>higher category theory.  But at the same time, Tom's point is that it
>doesn't, on its own, answer the question that was originally asked.
>He has a nice picture of a spectrum from "algebra" to "topology",
>starting with algebraic notions of infinity-groupoid, then moving
>through non-algebraic notions of infinity-groupoid, to algebraic
>notions of space, and eventually non-algebraic notions of space, with
>Kan complexes occupying the fulcum at the middle.  A full-strength
>statement of the homotopy hypothesis would then equate fully algebraic
>notions of infinity-groupoid with fully non-algebraic notions of
>space.
>
>I feel like here we have something similar.  If we call the
>"Initiality Hypothesis" something like "type theory is the initial
>elementary infinity-topos", then we can make a similar "joke":
>
>Q: How do you prove the Initiality Hypothesis?
>A: Define an elementary infinity-topos to be a (suitably structured)
>CwF; define type theory to be the initial such CwF; done!
>
>Again, this is not to denigrate the value of such an approach!  It
>just doesn't, on its own, answer the original question.  I can imagine
>a similar spectrum from "syntax" to "semantics", starting with
>"syntactic notions of type theory", then moving through "semantic
>notions of type theory", to "syntactic notions of toposes", and
>eventually "semantic notions of toposes".  Untyped syntax with
>implicit substitution (5) is way over on the syntactic side; locally
>cartesian closed quasicategories with appropriate stuff are way over
>on the semantic side; CwFs and the initial one as a QIIT are at the
>fulcrum in the middle.  And just as Kan complexes can play an
>important intermediate role in connecting the disparate ends of the
>homotopy-hypothesis spectrum, it seems likely that QIIT syntax can
>play a similar intermediate role in connecting the ends of the
>initiality-hypothesis spectrum.
>
>Does this seem reasonable?
>
>
>On Mon, May 21, 2018 at 10:46 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>> Thorsten gave a very nice HoTTEST talk a couple weeks ago about his
>> work with his collaborators on intrinsic syntax as a Quotient
>> Inductive-Inductive Type.  Since then I have been trying to fit
>> together a mental picture of exactly how all the different approaches
>> to syntax are related, but I am still kind of confused.
>>
>> In an attempt to clarify what I mean by "all the different
>> approaches", let me describe all the approaches I can think of in the
>> case of a very simple type theory: non-dependent unary type theory
>> with product types.  Unary means that the judgments have exactly one
>> type in the context, x:A |- t:B, and the only type constructor is a
>> product type A x B, with pairing for an introduction rule and
>> projections for elimination.  The semantics should be a category with
>> finite products.  Here are all the ways I can think of to describe
>> such a type theory:
>>
>>
>> 1. A QIIT that mirrors the semantics, with all the categorical
>> operations as point-constructors and their axioms as
>> equality-constructors.
>>
>> data Ty : Set where
>>  _x_ : Ty -> Ty -> Ty
>> [This will be the same in all cases, so I henceforth omit it.]
>>
>> data Tm : Ty -> Ty -> Set where
>>   id : {A} -> Tm A A
>>   _o_ : Tm A B -> Tm B C -> Tm A C
>>   assoc : h o (g o f) = (h o g) o f
>>   lid : id o f = f
>>   rid : f o id = f
>>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>   pr1 : Tm (A x B) A
>>   pr2 : Tm (A x B) B
>>   beta1 : pr1 o (f , g) = f
>>   beta2 : pr2 o (f , g) = g
>>   eta : p = (pr1 o p , pr2 o p)
>>
>>
>> 2. An Inductive-Inductive family of setoids that similarly mirrors the
>> categorical semantics, with judgmental equality an inductive type
>> family rather than coinciding with the metatheoretic equality.
>>
>> data Tm : Ty -> Ty -> Set where
>>   id : {A} -> Tm A A
>>   _o_ : Tm A B -> Tm B C -> Tm A C
>>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>   pr1 : Tm (A x B) A
>>   pr2 : Tm (A x B) B
>>
>> data Eq : Tm A B -> Tm A B -> Set where
>>   assoc : Eq (h o (g o f)) ((h o g) o f)
>>   lid : Eq (id o f) f
>>   rid : Eq 9f o id) f
>>   beta1 : Eq (pr1 o (f , g)) f
>>   beta2 : Eq (pr2 o (f , g)) g
>>   eta : Eq p (pr1 o p , pr2 o p)
>>
>>
>> 3. A QIIT that instead mirrors the usual type-theoretic syntax, with
>> operations like composition being admissible rather than primitive.
>> In our simple case it looks like this:
>>
>> data Tm : Ty -> Ty -> Set where
>>   id : {A} -> Tm A A
>>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>   pr1 : Tm A (B x C) -> Tm A B
>>   pr2 : Tm A (B x C) -> Tm A C
>>   beta1 : pr1 (f , g) = f
>>   beta2 : pr2 (f , g) = g
>>   eta : p = (pr1 p , pr2 p)
>>
>>
>> 4. Combining 2 and 3, an II family of setoids that mirrors
>> type-theoretic syntax.
>>
>> data Tm : Ty -> Ty -> Set where
>>   id : {A} -> Tm A A
>>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>   pr1 : Tm A (B x C) -> Tm A B
>>   pr2 : Tm A (B x C) -> Tm A C
>>
>> data Eq : Tm A B -> Tm A B -> Set where
>>   beta1 : Eq (pr1 (f , g)) f
>>   beta2 : Eq (pr2 (f , g)) g
>>   eta : Eq p (pr1 p , pr2 p)
>>
>>
>> 5. A single inductive type of raw terms, together with inductive
>> predicates over it for the typing judgment and equality judgments.
>>
>> data Tm : Set where
>>   var : Tm
>>   (_,_) : Tm -> Tm -> Tm
>>   pr1 : Tm -> Tm
>>   pr2 : Tm -> Tm
>>
>> data Of : Ty -> Tm -> Ty -> Set where
>>   of-var : Of A var A
>>   of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>>   of-pr1 : Of A t (B x C) -> Of A (pr1 t) B
>>   of-pr2 : Of A t (B x C) -> Of A (pr2 t) C
>>
>> data Eq : Ty -> Tm -> Tm -> Ty -> Set where
>>   beta1 : Of A t B -> Of A s C -> Eq A (pr1 (t , s)) t B
>>   beta2 : Of A t B -> Of A s C -> Eq A (pr2 (t , s)) t C
>>   eta : Of A t (B x C) -> Eq A (pr1 t , pr2 t) t (B x C)
>>
>>
>> 6. An II family that defines only the normal forms, via a separate
>> judgment for "atomic" terms that prevents us from writing down any
>> beta-redexes, thereby eliminating the need for any equality judgment
>> (though substitution then becomes more complicated, as it must
>> essentially incorporate beta-reduction).
>>
>> data Atom : Ty -> Ty -> Set where
>>   id : {A} -> Atom A A
>>   pr1 : Atom A (B x C) -> Atom A B
>>   pr2 : Atom A (B x C) -> Atom A C
>>
>> data Tm : Ty -> Ty -> Set where
>>   atom : Atom A B -> Tm A B
>>   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>
>>
>> 7. Combining 5 and 6, an inductive type of raw terms and predicates
>> over it that type only the normal forms.
>>
>> data Tm : Set where
>>   var : Tm
>>   (_,_) : Tm -> Tm -> Tm
>>   pr1 : Tm -> Tm
>>   pr2 : Tm -> Tm
>>
>> data Atom : Ty -> Tm -> Ty -> Set where
>>   atom-var : Atom A var A
>>   atom-pr1 : Atom A t (B x C) -> Atom A (pr1 t) B
>>   atom-pr2 : Atom A t (B x C) -> Atom A (pr2 t) C
>>
>> data Of : Ty -> Tm -> Ty -> Set where
>>   of-atom : Atom A t B -> Of A t B
>>   of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>>
>>
>> This is all I can think of right now.  Are there others?  Are there
>> other choices we can make in the case of dependent type theory that
>> are not visible in this simple case?
>>
>> In the above simple case of unary type theory with products, it should
>> be easy to show that all these definitions construct the initial
>> category with products.  (There should be some generating/axiomatic
>> types and terms too, to make the result nontrivial, but I've left them
>> out for brevity.)  My main question is, where do things become hard in
>> the case of dependent type theory?
>>
>> It seems to me that the main difference between (1) and (2), and
>> between (3) and (4), is convenience; is that right?  Type theory has
>> no infinitary constructors, so there shouldn't be axiom-of-choice
>> issues with descending algebraic operations to a quotient; it's just
>> that the bookkeeping involved in dealing with setoids everywhere
>> becomes unmanageable in the case of DTT.  Right?
>>
>> Thorsten said that (1) in the case of dependent type theory is
>> tautologically the initial CwF, which seems eminently plausible.  I
>> don't think this solves the "initiality conjecture", but where is the
>> sticking point?  Is it between (1) and (3), or between (3) and (5)?
>>
>> (Note that I'm not talking at all about the "h-level problem" that
>> these QIITs are by definition sets but that for HoTT to "eat itself"
>> we would want to eliminate out of them into the universe which is not
>> a set.  I'm only talking about initiality of syntax among *strict*
>> CwFs; coherence/strictification theorems can wait.  Personally,
>> though, I like (6)-(7) as potential approaches to coherence.)
>
>-- 
>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.



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman]

On Tue, May 29, 2018 at 2:15 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> What I am arguing about is the way the syntax of type theory should be presented.

I think the answer to a question involving "should" depends on what
the goal is.  Certainly there are situations in which an intrinsic
presentation is valuable.  But because of this:

> we have to eventually connect
>things back to untyped syntax, because untyped syntax is what we write
>on the page, and what we enter into a proof assistant.

I believe there are also situations in which an extrinsic presentation
is essential, and not just a "legacy" way of thinking (at least, not
until someone invents a pencil and paper that include HITs as
primitive).

Mike

Re: [HoTT] Re: Where is the problem with initiality?

[Thomas Streicher]

In my eyes the so called initiality problem is not a problem of
semantics of type theory. Models of type theory are essentailly
algebraic objects and thus as observed by Vladimir do admit an initial
one.

Syntax based on categorical combinatorsis fine in principle and useful
for implementaion.

That categorical syntax and ordinary syntax are isomorphic is just a
purely syntactic result allowing one to replace correct algebraic
syntax by one more accessible for the human mind. But it is important
to show that this replacement is faithful w.r.t. the mathematically
correct one.

Thomas

Re: [HoTT] Re: Where is the problem with initiality?

[Thorsten Altenkirch]

On 30/05/2018, 10:33, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote:

    That categorical syntax and ordinary syntax are isomorphic is just a
    purely syntactic result allowing one to replace correct algebraic
    syntax by one more accessible for the human mind.

For the human mind accustomed to the separation of collections and predicates as present in conventional Mathematics.






This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

Re: [HoTT] Re: Where is the problem with initiality?

[Thomas Streicher]

> On 30/05/2018, 10:33, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote:
> 
>     That categorical syntax and ordinary syntax are isomorphic is just a
>     purely syntactic result allowing one to replace correct algebraic
>     syntax by one more accessible for the human mind.
> 
> For the human mind accustomed to the separation of collections and predicates as present in conventional Mathematics.

That we have in TT as well turning a predicate P on A into the type
(Sigma x:A) P(x).

But that's not the issue here. Its rather syntax with variables as
opposed to syntax with combinators.

In topos theory performing arguments within internal language giving
the illusion of elements is much simpler than chasing diagrams. The
former seems closer to how our mind seems to work. But not verything
can be done internally. Mathematics is all internal, it's logic which
can speak also about the external.

Thomas

Re: [HoTT] Re: Where is the problem with initiality?

[Thorsten Altenkirch]

Names are syntactic sugar. 

In the intrinsic syntax ine uses a form of typed de Bruijn. To relate them to name carrying syntax is straight forward.

On 30/05/2018, 11:11, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote:

    But that's not the issue here. Its rather syntax with variables as
    opposed to syntax with combinators.
    
    




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

Re: [HoTT] Re: Where is the problem with initiality?

[Thomas Streicher]

On Wed, May 30, 2018 at 12:08:37PM +0000, Thorsten Altenkirch wrote:
> Names are syntactic sugar. 
> 
> In the intrinsic syntax ine uses a form of typed de Bruijn. To relate them to name carrying syntax is straight forward.

de Bruijn is just one part of the algebraization of syntax

the algebraic language constains much more inclusing an awful lot of
typing information which is usually inferred

Thomas

Re: [HoTT] Re: Where is the problem with initiality?

[Thorsten Altenkirch]

On 30/05/2018, 14:41, "homotopyt...@googlegroups.com on behalf of Thomas Streicher" <homotopyt...@googlegroups.com on behalf of stre...@mathematik.tu-darmstadt.de> wrote:

    On Wed, May 30, 2018 at 12:08:37PM +0000, Thorsten Altenkirch wrote:
    > Names are syntactic sugar. 
    > 
    > In the intrinsic syntax ine uses a form of typed de Bruijn. To relate them to name carrying syntax is straight forward.
    
    de Bruijn is just one part of the algebraization of syntax
    
    the algebraic language constains much more inclusing an awful lot of
    typing information which is usually inferred
    
Actually you can infer the implicit type information of the embedded system, that is I can leave certain parameters implicit (in the sense of implicit parameters in implementations of type theory which reflect mathematical practice).

Ok, you can say but I want to understand this inference. First of all that shouldn't really affect how you present the system, and actually as Ambrus has pointed out you can develop this inference algorithm based on the intrinsic syntax.

  




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

Re: [HoTT] Re: Where is the problem with initiality?

[Alexander Kurz]

> On 30 May 2018, at 10:37, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote:
> 
> On 30/05/2018, 10:33, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote:
> 
>    That categorical syntax and ordinary syntax are isomorphic is just a
>    purely syntactic result allowing one to replace correct algebraic
>    syntax by one more accessible for the human mind.
> 
> For the human mind accustomed to the separation of collections and predicates as present in conventional Mathematics.

I think the problem is not just one of being accustomed or not. 

It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed. 

If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved. 

Alexander

> 
> 
> 
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
> 
> -- 
> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Thorsten Altenkirch]

[-- Attachment #1: Type: text/plain, Size: 1825 bytes --]





On 30/05/2018, 11:53, "Alexander Kurz" <axh...@gmail.com> wrote:



    It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed.



I completely disagree. Set theory is untyped and conceptually misleading, to talk about all natural numbers you quantify over all sets singling those out that represent natural numbers. Untyped thinking leads to non-structural Mathematics, to mathematical hacking and a lack of abstraction. Indeed, the impossibility to hide anything in an untyped universe is one of the diseases of contemporary Mathematics.



I am not talking about formalising Mathematics (sure it is hard work) but I am talking about thinking about it.



It is not true that the difficulty of formalisation has anything to do with typedness. To the contrary types help you to structure your development, they provide a good structure to follow and indeed work well with category theory.



    If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved.



The problem is that people still use untyped Mathematics.









This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.





[-- Attachment #2: Type: text/html, Size: 4772 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman]

On Wed, May 30, 2018 at 5:05 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> Set theory is untyped and conceptually misleading, to
> talk about all natural numbers you quantify over all sets singling those out
> that represent natural numbers. Untyped thinking leads to non-structural
> Mathematics, to mathematical hacking and a lack of abstraction. Indeed, the
> impossibility to hide anything in an untyped universe is one of the diseases
> of contemporary Mathematics.
>
> ...
>
> The problem is that people still use untyped Mathematics.

I agree entirely with this.  Some set theorists like to say that the
untypedness of set theory is not a problem because one can still do
"structural" (i.e. typed) mathematics inside set theory.  This is true
-- IF you know what "structural/typed mathematics" means and you know
what you are doing!  The real problem is that if you learn untyped set
theory as "the" foundation of mathematics, then it requires an extra
step of *learning* to work structurally, i.e. to "forget about" the
ability to do untyped things.  Personally, I have noticed this problem
most when I am refereeing papers -- it seems to be a frequent source
of errors to, for instance, make a non-structural definition and then
use it in ways that would only make sense if it were structural.

However, the "typedness of mathematics" is for me a *semantic*
statement: the "real objects" of mathematics are typed, but that
doesn't necessarily mean that the *language we use to talk about them*
must (or even can) be typed.  There are "more semantic" notions of
"typed syntax", but ultimately what we actually write down is untyped,
so somewhere there is a necessary step of "typechecking" it.

Moreover, I currently still believe that we need not just an algorithm
to typecheck untyped syntax into typed syntax, but a full proof of the
initiality theorem for a structure built out of untyped syntax.  The
problem is that I want to be sure I know what is denoted by the
untyped syntax I write down.  Maybe you have a typechecking algorithm
that compiles it into typed syntax and thereby gives it a semantic
meaning, but maybe someone else has a different typechecking algorithm
that produces an *a priori* different typed syntax; how do I know that
the "meaning" of what I write down doesn't depend on which
typechecking algorithm I choose?  The most natural way I can see to be
sure of this is to show that untyped syntax assembles into the same
initial structure that typed syntax does.

>
>
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
> --
> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Thorsten Altenkirch]

It appears somehow inconsequential to say on the one hand that a typed approach to Mathematics is preferable but then when we talk about type theory itself it is preferable to consider untyped objects first. Doesn't solving the initiality problem just means that you have establish a view on the untyped objects which doesn't depend on them? If we apply the idea of structural Mathematics to type theory itself, isn't it clear that we should take the algebraic view as the fundamental definition? And indeed, using the idea of HITs combined with inductive-inductive it turns out that we can just give an inductive definition of the initial object in this algebraic view. This is nice because indeed HITs were not invented for this particular purpose!

And yes we have to relate this abstract initial object to the stuff we write or type in or create by clicking somewhere (indeed linear syntax may be a thing of the past anyway). We can do this by just establishing properties of the typed algebraic syntax, e.g. decidability and type inference in a way similar as we can understand parsing as the partial inverse of printing trees. 

Thorsten


On 30/05/2018, 20:07, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:

    On Wed, May 30, 2018 at 5:05 AM, Thorsten Altenkirch
    <Thorsten....@nottingham.ac.uk> wrote:
    > Set theory is untyped and conceptually misleading, to
    > talk about all natural numbers you quantify over all sets singling those out
    > that represent natural numbers. Untyped thinking leads to non-structural
    > Mathematics, to mathematical hacking and a lack of abstraction. Indeed, the
    > impossibility to hide anything in an untyped universe is one of the diseases
    > of contemporary Mathematics.
    >
    > ...
    >
    > The problem is that people still use untyped Mathematics.
    
    I agree entirely with this.  Some set theorists like to say that the
    untypedness of set theory is not a problem because one can still do
    "structural" (i.e. typed) mathematics inside set theory.  This is true
    -- IF you know what "structural/typed mathematics" means and you know
    what you are doing!  The real problem is that if you learn untyped set
    theory as "the" foundation of mathematics, then it requires an extra
    step of *learning* to work structurally, i.e. to "forget about" the
    ability to do untyped things.  Personally, I have noticed this problem
    most when I am refereeing papers -- it seems to be a frequent source
    of errors to, for instance, make a non-structural definition and then
    use it in ways that would only make sense if it were structural.
    
    However, the "typedness of mathematics" is for me a *semantic*
    statement: the "real objects" of mathematics are typed, but that
    doesn't necessarily mean that the *language we use to talk about them*
    must (or even can) be typed.  There are "more semantic" notions of
    "typed syntax", but ultimately what we actually write down is untyped,
    so somewhere there is a necessary step of "typechecking" it.
    
    Moreover, I currently still believe that we need not just an algorithm
    to typecheck untyped syntax into typed syntax, but a full proof of the
    initiality theorem for a structure built out of untyped syntax.  The
    problem is that I want to be sure I know what is denoted by the
    untyped syntax I write down.  Maybe you have a typechecking algorithm
    that compiles it into typed syntax and thereby gives it a semantic
    meaning, but maybe someone else has a different typechecking algorithm
    that produces an *a priori* different typed syntax; how do I know that
    the "meaning" of what I write down doesn't depend on which
    typechecking algorithm I choose?  The most natural way I can see to be
    sure of this is to show that untyped syntax assembles into the same
    initial structure that typed syntax does.
    
    >
    >
    >
    >
    >
    >
    >
    > This message and any attachment are intended solely for the addressee
    > and may contain confidential information. If you have received this
    > message in error, please contact the sender and delete the email and
    > attachment.
    >
    > Any views or opinions expressed by the author of this email do not
    > necessarily reflect the views of the University of Nottingham. Email
    > communications with the University of Nottingham may be monitored
    > where permitted by law.
    >
    >
    >
    > --
    > 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.
    




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman]

It sounds like Thorsten and are both starting to repeat ourselves, so
we should probably spare the patience of everyone else on the list
pretty soon.  I'll just make my own hopefully-final point by saying
that if "properties of the typed algebraic syntax" can imply that the
untyped stuff we write on the page has a *unique* typed denotation,
independent of a particular typechecking algorithm, as mentioned in my
last email, then I'll (probably) be satisfied.  (But at present I
don't see how it can do that without also essentially implying the
initiality theorem for untyped syntax.)

Thanks everyone for a very interesting discussion!

On Thu, May 31, 2018 at 3:06 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> It appears somehow inconsequential to say on the one hand that a typed approach to Mathematics is preferable but then when we talk about type theory itself it is preferable to consider untyped objects first. Doesn't solving the initiality problem just means that you have establish a view on the untyped objects which doesn't depend on them? If we apply the idea of structural Mathematics to type theory itself, isn't it clear that we should take the algebraic view as the fundamental definition? And indeed, using the idea of HITs combined with inductive-inductive it turns out that we can just give an inductive definition of the initial object in this algebraic view. This is nice because indeed HITs were not invented for this particular purpose!
>
> And yes we have to relate this abstract initial object to the stuff we write or type in or create by clicking somewhere (indeed linear syntax may be a thing of the past anyway). We can do this by just establishing properties of the typed algebraic syntax, e.g. decidability and type inference in a way similar as we can understand parsing as the partial inverse of printing trees.
>
> Thorsten
>
>
> On 30/05/2018, 20:07, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:
>
>     On Wed, May 30, 2018 at 5:05 AM, Thorsten Altenkirch
>     <Thorsten....@nottingham.ac.uk> wrote:
>     > Set theory is untyped and conceptually misleading, to
>     > talk about all natural numbers you quantify over all sets singling those out
>     > that represent natural numbers. Untyped thinking leads to non-structural
>     > Mathematics, to mathematical hacking and a lack of abstraction. Indeed, the
>     > impossibility to hide anything in an untyped universe is one of the diseases
>     > of contemporary Mathematics.
>     >
>     > ...
>     >
>     > The problem is that people still use untyped Mathematics.
>
>     I agree entirely with this.  Some set theorists like to say that the
>     untypedness of set theory is not a problem because one can still do
>     "structural" (i.e. typed) mathematics inside set theory.  This is true
>     -- IF you know what "structural/typed mathematics" means and you know
>     what you are doing!  The real problem is that if you learn untyped set
>     theory as "the" foundation of mathematics, then it requires an extra
>     step of *learning* to work structurally, i.e. to "forget about" the
>     ability to do untyped things.  Personally, I have noticed this problem
>     most when I am refereeing papers -- it seems to be a frequent source
>     of errors to, for instance, make a non-structural definition and then
>     use it in ways that would only make sense if it were structural.
>
>     However, the "typedness of mathematics" is for me a *semantic*
>     statement: the "real objects" of mathematics are typed, but that
>     doesn't necessarily mean that the *language we use to talk about them*
>     must (or even can) be typed.  There are "more semantic" notions of
>     "typed syntax", but ultimately what we actually write down is untyped,
>     so somewhere there is a necessary step of "typechecking" it.
>
>     Moreover, I currently still believe that we need not just an algorithm
>     to typecheck untyped syntax into typed syntax, but a full proof of the
>     initiality theorem for a structure built out of untyped syntax.  The
>     problem is that I want to be sure I know what is denoted by the
>     untyped syntax I write down.  Maybe you have a typechecking algorithm
>     that compiles it into typed syntax and thereby gives it a semantic
>     meaning, but maybe someone else has a different typechecking algorithm
>     that produces an *a priori* different typed syntax; how do I know that
>     the "meaning" of what I write down doesn't depend on which
>     typechecking algorithm I choose?  The most natural way I can see to be
>     sure of this is to show that untyped syntax assembles into the same
>     initial structure that typed syntax does.
>
>     >
>     >
>     >
>     >
>     >
>     >
>     >
>     > This message and any attachment are intended solely for the addressee
>     > and may contain confidential information. If you have received this
>     > message in error, please contact the sender and delete the email and
>     > attachment.
>     >
>     > Any views or opinions expressed by the author of this email do not
>     > necessarily reflect the views of the University of Nottingham. Email
>     > communications with the University of Nottingham may be monitored
>     > where permitted by law.
>     >
>     >
>     >
>     > --
>     > 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.
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> --
> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Alexander Kurz]

> On 31 May 2018, at 12:05, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> It sounds like Thorsten and are both starting to repeat ourselves, so
> we should probably spare the patience of everyone else on the list
> pretty soon.  I'll just make my own hopefully-final point by saying
> that if "properties of the typed algebraic syntax" can imply that the
> untyped stuff we write on the page has a *unique* typed denotation,
> independent of a particular typechecking algorithm, as mentioned in my
> last email, then I'll (probably) be satisfied.  

I am interested in this question of translating the untyped stuff we write on the page into type theory. 

To give a concrete example of what I am thinking of as untyped, but nevertheless conceptual and structural mathematics, I would point at Tom Leinster’s elegant description of the solution to the problem of Buffon’s needle, see the first paragraphs of the section “What is category theory?” at https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html

I call this argument type free because I see no obvious or canonical way to make the types precise enough in order to implement the proof in, say, Agda. Even if this can be done, it is still important that mathematicians can discuss this argument first without having to make the types precise. So there will always be mathematics outside of type theory.

If we want to routinely translate this kind of mathematics into type theory, we need to develop software that is either doing this automatically, or, more realistically, at least helps the mathematician to do this translation quickly enough, without decreasing their productivity by orders of magnitude.

As far as I can see, we are very far away from this. Is anybody aware of research trying to solve this problem?

I would imagine that one needs for example automatic (or semi-automatic) translations between the natural language that mathematicians use and the language of type theory. Automatic type annotation is only part of the problem. Googling shows up a little bit here and there, but I would be interested to know if anybody knows of serious ongoing work in this direction.

All the best,

Alexander



> (But at present I
> don't see how it can do that without also essentially implying the
> initiality theorem for untyped syntax.)
> 
> Thanks everyone for a very interesting discussion!
> 
> On Thu, May 31, 2018 at 3:06 AM, Thorsten Altenkirch
> <Thorsten....@nottingham.ac.uk> wrote:
>> It appears somehow inconsequential to say on the one hand that a typed approach to Mathematics is preferable but then when we talk about type theory itself it is preferable to consider untyped objects first. Doesn't solving the initiality problem just means that you have establish a view on the untyped objects which doesn't depend on them? If we apply the idea of structural Mathematics to type theory itself, isn't it clear that we should take the algebraic view as the fundamental definition? And indeed, using the idea of HITs combined with inductive-inductive it turns out that we can just give an inductive definition of the initial object in this algebraic view. This is nice because indeed HITs were not invented for this particular purpose!
>> 
>> And yes we have to relate this abstract initial object to the stuff we write or type in or create by clicking somewhere (indeed linear syntax may be a thing of the past anyway). We can do this by just establishing properties of the typed algebraic syntax, e.g. decidability and type inference in a way similar as we can understand parsing as the partial inverse of printing trees.
>> 
>> Thorsten
>> 
>> 
>> On 30/05/2018, 20:07, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:
>> 
>>    On Wed, May 30, 2018 at 5:05 AM, Thorsten Altenkirch
>>    <Thorsten....@nottingham.ac.uk> wrote:
>>> Set theory is untyped and conceptually misleading, to
>>> talk about all natural numbers you quantify over all sets singling those out
>>> that represent natural numbers. Untyped thinking leads to non-structural
>>> Mathematics, to mathematical hacking and a lack of abstraction. Indeed, the
>>> impossibility to hide anything in an untyped universe is one of the diseases
>>> of contemporary Mathematics.
>>> 
>>> ...
>>> 
>>> The problem is that people still use untyped Mathematics.
>> 
>>    I agree entirely with this.  Some set theorists like to say that the
>>    untypedness of set theory is not a problem because one can still do
>>    "structural" (i.e. typed) mathematics inside set theory.  This is true
>>    -- IF you know what "structural/typed mathematics" means and you know
>>    what you are doing!  The real problem is that if you learn untyped set
>>    theory as "the" foundation of mathematics, then it requires an extra
>>    step of *learning* to work structurally, i.e. to "forget about" the
>>    ability to do untyped things.  Personally, I have noticed this problem
>>    most when I am refereeing papers -- it seems to be a frequent source
>>    of errors to, for instance, make a non-structural definition and then
>>    use it in ways that would only make sense if it were structural.
>> 
>>    However, the "typedness of mathematics" is for me a *semantic*
>>    statement: the "real objects" of mathematics are typed, but that
>>    doesn't necessarily mean that the *language we use to talk about them*
>>    must (or even can) be typed.  There are "more semantic" notions of
>>    "typed syntax", but ultimately what we actually write down is untyped,
>>    so somewhere there is a necessary step of "typechecking" it.
>> 
>>    Moreover, I currently still believe that we need not just an algorithm
>>    to typecheck untyped syntax into typed syntax, but a full proof of the
>>    initiality theorem for a structure built out of untyped syntax.  The
>>    problem is that I want to be sure I know what is denoted by the
>>    untyped syntax I write down.  Maybe you have a typechecking algorithm
>>    that compiles it into typed syntax and thereby gives it a semantic
>>    meaning, but maybe someone else has a different typechecking algorithm
>>    that produces an *a priori* different typed syntax; how do I know that
>>    the "meaning" of what I write down doesn't depend on which
>>    typechecking algorithm I choose?  The most natural way I can see to be
>>    sure of this is to show that untyped syntax assembles into the same
>>    initial structure that typed syntax does.
>> 
>>> 
>>> 
>>> 
>>> 
>>> 
>>> 
>>> 
>>> This message and any attachment are intended solely for the addressee
>>> and may contain confidential information. If you have received this
>>> message in error, please contact the sender and delete the email and
>>> attachment.
>>> 
>>> Any views or opinions expressed by the author of this email do not
>>> necessarily reflect the views of the University of Nottingham. Email
>>> communications with the University of Nottingham may be monitored
>>> where permitted by law.
>>> 
>>> 
>>> 
>>> --
>>> 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.
>> 
>> 
>> 
>> 
>> 
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please contact the sender and delete the email and
>> attachment.
>> 
>> Any views or opinions expressed by the author of this email do not
>> necessarily reflect the views of the University of Nottingham. Email
>> communications with the University of Nottingham may be monitored
>> where permitted by law.
>> 
>> 
>> 
>> 
>> --
>> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Martin Escardo]

On 31/05/18 20:02, Alexander Kurz wrote:

> I am interested in this question of translating the untyped stuff we write on the page into type theory.
> 
> To give a concrete example of what I am thinking of as untyped, but nevertheless conceptual and structural mathematics, I would point at Tom Leinster’s elegant description of the solution to the problem of Buffon’s needle, see the first paragraphs of the section “What is category theory?” at https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html
> 
> I call this argument type free because I see no obvious or canonical way to make the types precise enough in order to implement the proof in, say, Agda. Even if this can be done, it is still important that mathematicians can discuss this argument first without having to make the types precise. So there will always be mathematics outside of type theory.

I don't understand why you call this argument untyped. Do you feel that 
a formalization in set theory, which is untyped, would be easier than a 
formalization in type theory? How is untypedness helping with this argument?

Martin

Re: [HoTT] Re: Where is the problem with initiality?

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 1831 bytes --]



On Thursday, 31 May 2018 20:02:51 UTC+1, Alexander Kurz wrote:
>
>
> > On 31 May 2018, at 12:05, Michael Shulman <shu...@sandiego.edu 
> <javascript:>> wrote: 
> > 
> > It sounds like Thorsten and are both starting to repeat ourselves, so 
> > we should probably spare the patience of everyone else on the list 
> > pretty soon.  I'll just make my own hopefully-final point by saying 
> > that if "properties of the typed algebraic syntax" can imply that the 
> > untyped stuff we write on the page has a *unique* typed denotation, 
> > independent of a particular typechecking algorithm, as mentioned in my 
> > last email, then I'll (probably) be satisfied.   
>
> I am interested in this question of translating the untyped stuff we write 
> on the page into type theory. 
>
> To give a concrete example of what I am thinking of as untyped, but 
> nevertheless conceptual and structural mathematics, I would point at Tom 
> Leinster’s elegant description of the solution to the problem of Buffon’s 
> needle, see the first paragraphs of the section “What is category theory?” 
> at 
> https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html 
>
> I call this argument type free because I see no obvious or canonical way 
> to make the types precise enough in order to implement the proof in, say, 
> Agda. Even if this can be done, it is still important that mathematicians 
> can discuss this argument first without having to make the types precise. 
> So there will always be mathematics outside of type theory. 
>

 I don't understand why you call this argument untyped. Do you feel that a 
formalization in set theory, which is untyped, would be easier than a 
formalization in type theory? How is untypedness helping with this 
argument? 

Martin 


[-- Attachment #1.2: Type: text/html, Size: 2872 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Eric Finster]

[-- Attachment #1: Type: text/plain, Size: 3910 bytes --]

Hi All,

I just had a chance to catch up and watch the video which
prompted this disucussion last night.  I'm a huge fan of the idea
of trying to understand and make precise the notion of "higher
category with families" and what that might say about the syntax
of type theory.  So my question is probably mostly directed at
Thorsten, but I am curious to hear other people's responses as
well.

I guess my question is pretty simple: why should we insist,
as Thorsten seems to, that the "intrinsic" syntax of type
theory form a set?

I can, I think, anticipate the first response: well, we want to
have a type-checking algorithm.  And, in light of the conversion
rule, this typically means that we will have to reduce type
expressions to a normal form and check if they are equal.  Hence,
if we don't have decidability of the syntax, we cannot have
decidability of typechecking.  Am I right that this is the principle
motivation for having decidable syntax?

But, then, this seems to be a statement about *extrinsic* syntax.  If,
as Thorsten advocates, we somehow manage to produce a highly
structured, internal description of the syntax of type theory,
then typechecking for this syntax is, by definition, unnecessary!  After
all,
the whole point is that in such a setup, only the well-typed terms
even make sense (i.e., are typeable in the meta-language).

So from an internal perspective, I cannot think of any reason to
insist on decidability.  And consequently, insisting that an
internal higher category with families be univalent does not seem
in any way strange to me.

But maybe there is some other objection that I'm not seeing?

Eric

On Fri, Jun 1, 2018 at 7:07 PM Martín Hötzel Escardó <
escardo...@gmail.com> wrote:

>
>
> On Thursday, 31 May 2018 20:02:51 UTC+1, Alexander Kurz wrote:
>
>>
>> > On 31 May 2018, at 12:05, Michael Shulman <shu...@sandiego.edu> wrote:
>> >
>> > It sounds like Thorsten and are both starting to repeat ourselves, so
>> > we should probably spare the patience of everyone else on the list
>> > pretty soon.  I'll just make my own hopefully-final point by saying
>> > that if "properties of the typed algebraic syntax" can imply that the
>> > untyped stuff we write on the page has a *unique* typed denotation,
>> > independent of a particular typechecking algorithm, as mentioned in my
>> > last email, then I'll (probably) be satisfied.
>>
>> I am interested in this question of translating the untyped stuff we
>> write on the page into type theory.
>>
>> To give a concrete example of what I am thinking of as untyped, but
>> nevertheless conceptual and structural mathematics, I would point at Tom
>> Leinster’s elegant description of the solution to the problem of Buffon’s
>> needle, see the first paragraphs of the section “What is category theory?”
>> at
>> https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html
>>
>> I call this argument type free because I see no obvious or canonical way
>> to make the types precise enough in order to implement the proof in, say,
>> Agda. Even if this can be done, it is still important that mathematicians
>> can discuss this argument first without having to make the types precise.
>> So there will always be mathematics outside of type theory.
>>
>
>  I don't understand why you call this argument untyped. Do you feel that a
> formalization in set theory, which is untyped, would be easier than a
> formalization in type theory? How is untypedness helping with this
> argument?
>
> Martin
>
> --
> 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.
>

[-- Attachment #2: Type: text/html, Size: 5970 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 317 bytes --]



On Friday, 1 June 2018 18:45:42 UTC+1, Eric Finster wrote:
>
> I guess my question is pretty simple: why should we insist,
> as Thorsten seems to, that the "intrinsic" syntax of type
> theory form a set?
>

I like this question. If the syntax is supposed to be the initial model, 
then it can't be a set.

 Martin


[-- Attachment #1.2: Type: text/html, Size: 659 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[András Kovács]

[-- Attachment #1: Type: text/plain, Size: 1692 bytes --]

>
> I like this question. If the syntax is supposed to be the initial model,
> then it can't be a set.


Why? The syntax being a set doesn't imply that models also need to be sets.
As I understand, the goal of higher models for TT is to get rid of
set-truncation but still have a syntax which is a set.

But, then, this seems to be a statement about *extrinsic* syntax.  If,
> as Thorsten advocates, we somehow manage to produce a highly
> structured, internal description of the syntax of type theory,
> then typechecking for this syntax is, by definition, unnecessary!
>

Type checking must be performed in any case, at some level. If we use
intrinsic embedded syntaxes, then the implementation of the metalanguage
(in a meta-metalanguage) does the type checking. Hence, if we intend to
formalize a syntax of type theory which is intended as a metatheoretical
setting for mathematics, then I think decidability is quite important.


2018-06-01 21:55 GMT+02:00 Martín Hötzel Escardó <escardo...@gmail.com>:

>
>
> On Friday, 1 June 2018 18:45:42 UTC+1, Eric Finster wrote:
>>
>> I guess my question is pretty simple: why should we insist,
>> as Thorsten seems to, that the "intrinsic" syntax of type
>> theory form a set?
>>
>
> I like this question. If the syntax is supposed to be the initial model,
> then it can't be a set.
>
>  Martin
>
> --
> 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.
>

[-- Attachment #2: Type: text/html, Size: 6289 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 258 bytes --]



On Friday, 1 June 2018 21:59:28 UTC+1, András Kovács wrote:
>
> I like this question. If the syntax is supposed to be the initial model, 
>> then it can't be a set.
>
>
> Why? 
>

I don't think the initial model is a set. Is it?

Martin
 

[-- Attachment #1.2: Type: text/html, Size: 1440 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman]

On Fri, Jun 1, 2018 at 2:06 PM, Martín Hötzel Escardó
<escardo...@gmail.com> wrote:
> I don't think the initial model is a set. Is it?

This is the big conjecture that Thorsten and I actually agree on: that
the initial infinity-CwF in fact happens to be a 1-CwF.  Thorsten
wants to prove this by explicitly constructing the initial
infinity-CwF and then proving that it is a 1-CwF; my preference would
be to construct the initial 1-CwF in a careful way (e.g. with only
normal forms and hereditary substitution) so that one can prove that
it is in fact the initial infinity-CwF as well.  But in both cases the
conjectured result is the same, and even the important ingredient in
the expected proof is roughly the same: the existence of normal forms
and normalization.

Re: [HoTT] Re: Where is the problem with initiality?

[Eric Finster]

[-- Attachment #1: Type: text/plain, Size: 1375 bytes --]

> > I don't think the initial model is a set. Is it?
>
> This is the big conjecture that Thorsten and I actually agree on: that
> the initial infinity-CwF in fact happens to be a 1-CwF.  Thorsten
> wants to prove this by explicitly constructing the initial
> infinity-CwF and then proving that it is a 1-CwF; my preference would
> be to construct the initial 1-CwF in a careful way (e.g. with only
> normal forms and hereditary substitution) so that one can prove that
> it is in fact the initial infinity-CwF as well.  But in both cases the
> conjectured result is the same, and even the important ingredient in
> the expected proof is roughly the same: the existence of normal forms
> and normalization.
>
>
Right, and I think I'm more or less on board with the conjecture.
Although as you start adding more structure to your CwF, things get a bit
murkier...
Is it still okay with dependent products ... umm ... and what about if I
add a class of HIT's?
To take things really far: if there is such a thing as the free elementary
infty-topos, is it a 1-category?
This somehow seems dubious, no?

So it seems to me at some point, something has to break in our notion of
what syntax for higher algebraic objects *is* in the first place.
Which is why I would not want to make the assumption from the outset that
syntax must necessarily be decidable.

[-- Attachment #2: Type: text/html, Size: 1721 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman]

My intuition is that the conjecture should be true for any categorical
structure whose corresponding type theory satisfies normalization /
cut-elimination.  With my suggested approach the idea is that if there
is normalization, then you can define the initial 1-structure using
*only* the normal forms, so that there is no need to add
path-constructors at all.  Then instead of a HIIT/QIIT you have just a
normal IIT, which will be a set as long as all its parameters are
(this being necessary, as Jasper pointed out); and you can
nevertheless define maps out of it into higher types using its
induction principle.

In essence the situation is similar to how the free oo-group on one
generator (the integers) happens to be a set, because we can define
"normal forms" for integers as positive or negative unary natural
numbers.  This sort of thing is also known to happen elsewhere in
higher category theory; for instance, the free bicategory on a
directed graph happens to be a 1-category, because instead of
constructing it by throwing in all binary composites, associativity
isomorphisms, and so on, we can normalize all bracketed composites to
be (say) left-associated.  This is essentially cut-elimination for
unary simple type theory.

So, if we have a type theory for elementary infinity-toposes that has
normalization (perhaps some form of cubical type theory), then I would
believe the conjecture should hold fo them too.  Note that this
doesn't mean that the *objects* of the free elementary infinity-topos
are *internally* sets -- that would certainly be false since it
contains universes.  Instead, it means that the free elementary
infinity-topos can be *presented* by a structure (e.g. a CwF) that is
*externally* a set, just as the model category of simplicial sets is
itself a 1-category despite containing objects that are "internally"
(in the model-categorical sense) not sets.

It seems to me that the question of whether syntax should be decidable
seems to be just a question of definition as to where you draw the
line separating syntax from semantics.  Does a HIIT initial
infinity-categorical structure that is not decidable count as
"syntax"?  Is it "syntax with a heavy flavor of semantics", or is it
"semantics with a heavy flavor of syntax"?  Whatever we call them,
such things are certainly interesting!  But I'm dubious that we could
use them as a foundation for mathematics unless there is also an
untyped extrinsic syntax that can be typechecked into them (which
might or might not require them to be decidable).


On Fri, Jun 1, 2018 at 2:53 PM, Eric Finster <ericf...@gmail.com> wrote:
>
>>
>> > I don't think the initial model is a set. Is it?
>>
>> This is the big conjecture that Thorsten and I actually agree on: that
>> the initial infinity-CwF in fact happens to be a 1-CwF.  Thorsten
>> wants to prove this by explicitly constructing the initial
>> infinity-CwF and then proving that it is a 1-CwF; my preference would
>> be to construct the initial 1-CwF in a careful way (e.g. with only
>> normal forms and hereditary substitution) so that one can prove that
>> it is in fact the initial infinity-CwF as well.  But in both cases the
>> conjectured result is the same, and even the important ingredient in
>> the expected proof is roughly the same: the existence of normal forms
>> and normalization.
>>
>
> Right, and I think I'm more or less on board with the conjecture.
> Although as you start adding more structure to your CwF, things get a bit
> murkier...
> Is it still okay with dependent products ... umm ... and what about if I add
> a class of HIT's?
> To take things really far: if there is such a thing as the free elementary
> infty-topos, is it a 1-category?
> This somehow seems dubious, no?
>
> So it seems to me at some point, something has to break in our notion of
> what syntax for higher algebraic objects *is* in the first place.
> Which is why I would not want to make the assumption from the outset that
> syntax must necessarily be decidable.
>
>
> --
> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Eric Finster]

[-- Attachment #1: Type: text/plain, Size: 4047 bytes --]

> In essence the situation is similar to how the free oo-group on one
> generator (the integers) happens to be a set, because we can define
> "normal forms" for integers as positive or negative unary natural
> numbers.  This sort of thing is also known to happen elsewhere in
> higher category theory; for instance, the free bicategory on a
> directed graph happens to be a 1-category, because instead of
> constructing it by throwing in all binary composites, associativity
> isomorphisms, and so on, we can normalize all bracketed composites to
> be (say) left-associated.  This is essentially cut-elimination for
> unary simple type theory.
>
>
Yes, and there are of course other examples.
Like finite sets and bijections being the free symmetric monoidal category
on an object.
And Delta as the free monoidal category with a monoid.
Both of these statements are true whether I consider their higher versions
or not.
So I am aware of this phenomenon, which is why I believe the conjecture.


> So, if we have a type theory for elementary infinity-toposes that has
> normalization (perhaps some form of cubical type theory), then I would
> believe the conjecture should hold fo them too.  Note that this
> doesn't mean that the *objects* of the free elementary infinity-topos
> are *internally* sets -- that would certainly be false since it
> contains universes.  Instead, it means that the free elementary
> infinity-topos can be *presented* by a structure (e.g. a CwF) that is
> *externally* a set, just as the model category of simplicial sets is
> itself a 1-category despite containing objects that are "internally"
> (in the model-categorical sense) not sets.
>

Hmmm.  But isn't this situation different from the previous one?
Assuming there is an infinity category of elementary infinity-topoi, then I
can ask the same question as before: is the initial such guy a 1-category.
This is what, to me, the previous conjecture about categories with families
was about.
But now this time you use the word "presented", so I'm not sure if you are
making a similar statement or not.
For example, if this really were the case, wouldn't it rule out effectivity
of (even finite) colimits?
You'll have to remind me, but I think epis are still regular in an
elementary 1-topos....
So in the infinity case, wouldn't this be making kind of a big concession?

It seems to me that the question of whether syntax should be decidable
> seems to be just a question of definition as to where you draw the
> line separating syntax from semantics.  Does a HIIT initial
> infinity-categorical structure that is not decidable count as
> "syntax"?  Is it "syntax with a heavy flavor of semantics", or is it
> "semantics with a heavy flavor of syntax"?


Right, completely agreed.
I guess my position would be that, if we don't allow ourselves to think of
a HIT presentation as syntax for a higher object, if we insist that the
word syntax be reserved for set level objects, then higher objects *don't
have syntax by definition*!
That seems surprising, since the point of this list seems to be that we
have found ways to manipulate them syntactically.  :)

Moreover, there's another reason that this would be strange:
I mean, after all, kind of the whole point of introducing higher algebraic
objects is that these objects carry explicit witnesses for all of the
relations they satisfy.
And our usual way of equipping objects with this kind of witness is to
invent syntax for it.
So shouldn't it somehow be exactly the opposite: shouldn't we think of
higher objects as *more* syntactic than their set theoretic counterparts?

Whatever we call them,
> such things are certainly interesting!  But I'm dubious that we could
> use them as a foundation for mathematics unless there is also an
> untyped extrinsic syntax that can be typechecked into them (which
> might or might not require them to be decidable).
>

Yes, indeed.  Interesting and puzzling.
And I get your point here.

E.

[-- Attachment #2: Type: text/html, Size: 5074 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman]

On Sat, Jun 2, 2018 at 8:06 AM, Eric Finster <ericf...@gmail.com> wrote:
> Assuming there is an infinity category of elementary infinity-topoi, then I
> can ask the same question as before: is the initial such guy a 1-category.
> This is what, to me, the previous conjecture about categories with families
> was about.
> But now this time you use the word "presented", so I'm not sure if you are
> making a similar statement or not.

Right, presentation is the crucial point.  Let me try to say the same
thing again.

There are three kinds of structures under discussion:

1. 1-categories with families / fibration 1-categories
2. oo-categories with families / fibration oo-categories
3. oo-categories

There is an evident inclusion of (1) into (2), and also an "inclusion"
of (3) into (2) by taking the families to be arbitrary objects in
slices.  And there is also a sort of "reflection" operation from (2)
back into (3) that creates new higher cells out of arrows into path
objects, which I would expect to be some kind of left adjoint to the
"inclusion".  I'm not being precise about what extra structure these
things have, and what the functors between them are, so this is really
just a heuristic that I would expect to be true for any well-behaved
"doctrine" of extra structure that we could add to them.

If the doctrine in question includes things like effective oo-colimits
or univalent universes, then the initial object of (3) will not be a
1-category.  However, the initial object of (1) will always be a
1-category by definition.  The big conjecture is that the inclusion of
(1) into (2) preserves this initial object.  The "reflection", being a
"left adjoint", ought then to preserve initial objects, and therefore
take this initial structured 1-CwF (regarded as a structured oo-CwF)
to the initial structured oo-category -- in particular, making it no
longer a 1-category by adding higher cells coming from arrows into
path objects.

Of course, there will also be *other* objects of (2) that are also
reflected onto the inital object of (3), such as for instance the
inclusion of that initial object itself into (2).  The point is that
the initial object of (3) *can be presented by* the initial object of
(2), which *happens to coincide with* the initial object of (1).

Does that help?

> I guess my position would be that, if we don't allow ourselves to think of a
> HIT presentation as syntax for a higher object, if we insist that the word
> syntax be reserved for set level objects, then higher objects *don't have
> syntax by definition*!
> That seems surprising, since the point of this list seems to be that we have
> found ways to manipulate them syntactically.  :)

Right -- the way that we manipulate them syntactically is by
*presenting* free/initial ones with set-level objects.

> Moreover, there's another reason that this would be strange:
> I mean, after all, kind of the whole point of introducing higher algebraic
> objects is that these objects carry explicit witnesses for all of the
> relations they satisfy.
> And our usual way of equipping objects with this kind of witness is to
> invent syntax for it.
> So shouldn't it somehow be exactly the opposite: shouldn't we think of
> higher objects as *more* syntactic than their set theoretic counterparts?
>
>> Whatever we call them,
>> such things are certainly interesting!  But I'm dubious that we could
>> use them as a foundation for mathematics unless there is also an
>> untyped extrinsic syntax that can be typechecked into them (which
>> might or might not require them to be decidable).
>
>
> Yes, indeed.  Interesting and puzzling.
> And I get your point here.
>
> E.
>
> --
> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Thomas Streicher]

> > I like this question. If the syntax is supposed to be the initial model, 
> >> then it can't be a set.
> >
> >
> > Why? 

It's a decidable prediacte on N and thus a set.

Thomas

Re: [HoTT] Re: Where is the problem with initiality?

[Jasper Hugunin]

[-- Attachment #1: Type: text/plain, Size: 1428 bytes --]

On Friday, 1 June 2018 18:45:42 UTC+1, Eric Finster wrote:

> But, then, this seems to be a statement about *extrinsic* syntax.  If,
> as Thorsten advocates, we somehow manage to produce a highly
> structured, internal description of the syntax of type theory,
> then typechecking for this syntax is, by definition, unnecessary!


On Fri, Jun 1, 2018 at 1:59 PM András Kovács <putta...@gmail.com> wrote:

> Type checking must be performed in any case, at some level. If we use
> intrinsic embedded syntaxes, then the implementation of the metalanguage
> (in a meta-metalanguage) does the type checking. Hence, if we intend to
> formalize a syntax of type theory which is intended as a metatheoretical
> setting for mathematics, then I think decidability is quite important.
>

 If we don't intend our type theory to be used as a metatheoretical setting
for mathematics, it seems interesting to consider for example a type theory
with a family of base types indexed by the circle, the syntax of which I
think would not form a set.
That is, if we have a way to represent dependent type theory in Coq, what
happens if we add a constructor `a_circle_of_types : circle -> type` to our
syntax (for a postulated circle, or HIT)? This should be consistent, to add
a family of uninterpreted types, but I believe equality is no longer
decidable (since equality of circle is not decidable).

- Jasper Hugunin

[-- Attachment #2: Type: text/html, Size: 2669 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Eric Finster]

[-- Attachment #1: Type: text/plain, Size: 1734 bytes --]

> Type checking must be performed in any case, at some level. If we use
>> intrinsic embedded syntaxes, then the implementation of the metalanguage
>> (in a meta-metalanguage) does the type checking. Hence, if we intend to
>> formalize a syntax of type theory which is intended as a metatheoretical
>> setting for mathematics, then I think decidability is quite important.
>>
>
>  If we don't intend our type theory to be used as a metatheoretical
> setting for mathematics, it seems interesting to consider for example a
> type theory with a family of base types indexed by the circle, the syntax
> of which I think would not form a set.
> That is, if we have a way to represent dependent type theory in Coq, what
> happens if we add a constructor `a_circle_of_types : circle -> type` to our
> syntax (for a postulated circle, or HIT)? This should be consistent, to add
> a family of uninterpreted types, but I believe equality is no longer
> decidable (since equality of circle is not decidable).
>
>
Yes, exactly, I have the same objection.
Even if the conjecture Mike alluded to is true, that the free higher
category with families is equivalent to a 1-category, I can certainly
*force* it to be false by considering the "free higher category with
families with some random extra 2-cell".
Don't we expect this thing to *also* have some kind of "syntax" presenting
it?



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

[-- Attachment #2: Type: text/html, Size: 3055 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Matt Oliveri]

[-- Attachment #1.1: Type: text/plain, Size: 594 bytes --]

On Friday, June 1, 2018 at 1:45:42 PM UTC-4, Eric Finster wrote:
>
> So from an internal perspective, I cannot think of any reason to
> insist on decidability.
>

I agree with this. And in particular, I think QIITs can define intrinsic 
syntax of (fully-annotated) extensional type theroy just fine. Equality 
reflection would be an extra equality constructor. Isn't that right? What 
do Thorsten and team think of that? Is it an infelicity of QIITs, perhaps 
because they're hSet truncated? Or is there a problem with ETT that 
structuralism doesn't shed light on? Or is ETT maybe not so bad?

[-- Attachment #1.2: Type: text/html, Size: 812 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Ambrus Kaposi]

On Fri, Jun 1, 2018 at 11:27 PM Matt Oliveri <atm...@gmail.com> wrote:
>
> On Friday, June 1, 2018 at 1:45:42 PM UTC-4, Eric Finster wrote:
>>
>> So from an internal perspective, I cannot think of any reason to
>> insist on decidability.
>
> I agree with this. And in particular, I think QIITs can define intrinsic syntax of (fully-annotated) extensional type theroy just fine. Equality reflection would be an extra equality constructor. Isn't that right? What do Thorsten and team think of that? Is it an infelicity of QIITs, perhaps because they're hSet truncated? Or is there a problem with ETT that structuralism doesn't shed light on? Or is ETT maybe not so bad?

Yes, the syntax for extensional type theory can be defined as a QIIT.

For me, the problem with it is that there is no easy way to input
terms in the computer: starting with a string, lexing, parsing it and
getting an untyped term, then typechecking the untyped term. During
bidirectional typechecking, we need that types in the QIIT have
decidable equality. See e.g.
https://bitbucket.org/akaposi/tt-in-tt/src/HEAD/Typecheck.agda
Equality of types is not decidable in ETT, even if we can normalise
terms (use it for programming).

But maybe there are other ways to build terms in this QIIT in a
convenient way (the NuPRL, Andromeda people know this), and then I
also don't see why we would insist on decidability of equality.

Re: [HoTT] Re: Where is the problem with initiality?

[Thomas Streicher]

People introduced intensional type theory for having syntax decidable
because that's necessary for convenient implementation.

But any theory appears quotient of N by some r.e. equivalence relation
on N. And isn't the respective quotient always a set?

Thomas

Re: [HoTT] Re: Where is the problem with initiality?

[Thorsten Altenkirch]

[-- Attachment #1: Type: text/plain, Size: 6466 bytes --]


I just had a chance to catch up and watch the video which
prompted this disucussion last night.  I'm a huge fan of the idea
of trying to understand and make precise the notion of "higher
category with families" and what that might say about the syntax
of type theory.  So my question is probably mostly directed at
Thorsten, but I am curious to hear other people's responses as
well.

I guess my question is pretty simple: why should we insist,
as Thorsten seems to, that the "intrinsic" syntax of type
theory form a set?

I am a bit late and it seems that Mike has already given a nice answer. In a computational reasonable version of type theory we should be able to compute normal forms and be able to show that the terms (with a non-trivial equality) are equivalent and hence the terms form a set. This also entails important properties for an implementation which is one of the reasons that we are interested in a computationally adequate type theory. If we define a version of higher type theory which we can't normalize then maybe there is something missing. But actually I think that a naïve version of higher type theory (using (infinity,1)-version of the usual definition) should be fine and we should eb able to transfer the usual normalisation by evaluation construction to this setting.

Now, there are interesting type theories that are not computationally adequate. Extensional type theory (ETT) was already mentioned. In a higher setting the equality reflection principle of ETT should actually become that propositional equality and judgemental equality are equivalent. The type theory (o.e. the initial algebra) that also features univalence and maybe HITs will not be a set. I think it should be possible to relate such a semantic (extensional) theory to a computational (intensional) one via a conservativity theorem along the lines of Martin Hofmann's conservativity theorem that showed that ETT is conservative over ITT with functional extensionality and uniqueness of equality proofs.

I can, I think, anticipate the first response: well, we want to
have a type-checking algorithm.  And, in light of the conversion
rule, this typically means that we will have to reduce type
expressions to a normal form and check if they are equal.  Hence,
if we don't have decidability of the syntax, we cannot have
decidability of typechecking.  Am I right that this is the principle
motivation for having decidable syntax?

But, then, this seems to be a statement about *extrinsic* syntax.

You can relate explicit syntax (I.e. term trees) to intrinsic syntax and type checking is the problem to decide wether a given tree is the underlying representation of a derivation. This is actually similar to the problem of parsing where we can print a tree and the problem is given a string to find a tree that prints as the term.

  If,
as Thorsten advocates, we somehow manage to produce a highly
structured, internal description of the syntax of type theory,
then typechecking for this syntax is, by definition, unnecessary!  After all,
the whole point is that in such a setup, only the well-typed terms
even make sense (i.e., are typeable in the meta-language).

So from an internal perspective, I cannot think of any reason to
insist on decidability.  And consequently, insisting that an
internal higher category with families be univalent does not seem
in any way strange to me.

But maybe there is some other objection that I'm not seeing?

Eric

On Fri, Jun 1, 2018 at 7:07 PM Martín Hötzel Escardó <escardo...@gmail.com<mailto:escardo...@gmail.com>> wrote:


On Thursday, 31 May 2018 20:02:51 UTC+1, Alexander Kurz wrote:

> On 31 May 2018, at 12:05, Michael Shulman <shu...@sandiego.edu> wrote:
>
> It sounds like Thorsten and are both starting to repeat ourselves, so
> we should probably spare the patience of everyone else on the list
> pretty soon.  I'll just make my own hopefully-final point by saying
> that if "properties of the typed algebraic syntax" can imply that the
> untyped stuff we write on the page has a *unique* typed denotation,
> independent of a particular typechecking algorithm, as mentioned in my
> last email, then I'll (probably) be satisfied.

I am interested in this question of translating the untyped stuff we write on the page into type theory.

To give a concrete example of what I am thinking of as untyped, but nevertheless conceptual and structural mathematics, I would point at Tom Leinster’s elegant description of the solution to the problem of Buffon’s needle, see the first paragraphs of the section “What is category theory?” at https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html

I call this argument type free because I see no obvious or canonical way to make the types precise enough in order to implement the proof in, say, Agda. Even if this can be done, it is still important that mathematicians can discuss this argument first without having to make the types precise. So there will always be mathematics outside of type theory.

 I don't understand why you call this argument untyped. Do you feel that a formalization in set theory, which is untyped, would be easier than a formalization in type theory? How is untypedness helping with this argument?

Martin


--
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<mailto: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<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.





[-- Attachment #2: Type: text/html, Size: 9718 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Jon Sterling]

I fear that this veers off topic---but let me say that this is hardly a serious problem for structural / typed foundations, considering the fact that you can always embed an untyped mathematical universe into a typed one in an easy way (for instance, using Aczel's interpretation of constructive set theory into type theory), whereas it is much harder to move in the other direction without inheriting the pathologies of set theory.

With that said, maybe we can get back to the original question. Where really is the problem with initiality? As Thomas said, the problem surely does not at all lie in the difference between "human syntax" and syntax based on categorical gadgets (it's easy to see that these are the same). Returning to Thomas's email about M_a and M_s (lindenbaum-tarski model), it sounds as if the problem has almost nothing to do with initiality at all, if the hard part is really to show that M_s is a model at all.

Am I misunderstanding Thomas's email?


On Wed, May 30, 2018, at 3:53 AM, Alexander Kurz wrote:
> 
> 
> > On 30 May 2018, at 10:37, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote:
> > 
> > On 30/05/2018, 10:33, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote:
> > 
> >    That categorical syntax and ordinary syntax are isomorphic is just a
> >    purely syntactic result allowing one to replace correct algebraic
> >    syntax by one more accessible for the human mind.
> > 
> > For the human mind accustomed to the separation of collections and predicates as present in conventional Mathematics.
> 
> I think the problem is not just one of being accustomed or not. 
> 
> It is crucial that informal mathematics is untyped. The untypedness is 
> what makes it flexible enough for practical purposes. Formalising 
> mathematics in a proof assistant is hard work. And to a large extent 
> this is due to the fact that everything has to be typed. 
> 
> If we ever want to get mathematicians to use proof assistants as 
> casually as they use latex, the problem of untyped vs typed mathematics 
> needs to be solved. 
> 
> Alexander
> 
> > 
> > 
> > 
> > 
> > 
> > 
> > This message and any attachment are intended solely for the addressee
> > and may contain confidential information. If you have received this
> > message in error, please contact the sender and delete the email and
> > attachment. 
> > 
> > Any views or opinions expressed by the author of this email do not
> > necessarily reflect the views of the University of Nottingham. Email
> > communications with the University of Nottingham may be monitored 
> > where permitted by law.
> > 
> > 
> > 
> > 
> > -- 
> > 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Andrej Bauer]

Dear Alexander,


On Wed, May 30, 2018 at 12:53 PM, Alexander Kurz <axh...@gmail.com> wrote:
>
> It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed.
>
> If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved.

I think you made there a coiple of intellectual jumps. In order for
your statements to have some weight, you need to consider the
following questions:

(a) What if formalization of mathematics in existing proof assistants
is hard for some reason other than typedness?

(b) Most proof assistants that have a large user base are typed. Is
this is a big conspiracy on part of the designers, or could it be
understood as evidence that typed proof assistants have a certain
advantage over the untyped ones?

(c) You offer LaTeX as an example of good design. I beg to differ.

(d) Informal mathematics is very obviously typed, as witnessed by the
fact that authors are always carefully explain the types of various
symbols they use (or rely on the culturally accepted notations).

The Buffon needle example presents absolutely no obstacle to typing.
Perhaps you are mixing up *informal* nature of human mathematics with
untypedness? Formalizing Buffon's needle requires a great amount of
precision (what is a curve? what does it mean to "throw a needle"? how
do we cuunt crossings when there are infinitely many?) which is
unavoidable so long as we subbscribe to the mathematical method.
Typedness has nothing to do with this fact.

With kind regards,

Andrej

Re: [HoTT] Re: Where is the problem with initiality?

[David Roberts]

There is an... "interesting" discussion going on at the fom mailing
list at present, the usual suspects included, about set theory-based
proof assistants, which might provide either a source of entertainment
or frustration. It is enlightening when considering what people think
about typed vs untyped.

Univalent foundations gets a mention here:
https://cs.nyu.edu/pipermail/fom/2018-May/021012.html
The 'ideal proof assistant' is described as being based on ZFC here:
https://cs.nyu.edu/pipermail/fom/2018-May/021026.html
Friedman proclaims he is completely ignorant of the issues and that he
has never gotten close to getting dirty with details, but is happy to
weigh in: https://cs.nyu.edu/pipermail/fom/2018-May/021023.html
The discussion continues this month here:
https://cs.nyu.edu/pipermail/fom/2018-June/021030.html

David
David Roberts
http://ncatlab.org/nlab/show/David+Roberts


On 5 June 2018 at 17:22, Andrej Bauer <andrej...@andrej.com> wrote:
> Dear Alexander,
>
>
> On Wed, May 30, 2018 at 12:53 PM, Alexander Kurz <axh...@gmail.com> wrote:
>>
>> It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed.
>>
>> If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved.
>
> I think you made there a coiple of intellectual jumps. In order for
> your statements to have some weight, you need to consider the
> following questions:
>
> (a) What if formalization of mathematics in existing proof assistants
> is hard for some reason other than typedness?
>
> (b) Most proof assistants that have a large user base are typed. Is
> this is a big conspiracy on part of the designers, or could it be
> understood as evidence that typed proof assistants have a certain
> advantage over the untyped ones?
>
> (c) You offer LaTeX as an example of good design. I beg to differ.
>
> (d) Informal mathematics is very obviously typed, as witnessed by the
> fact that authors are always carefully explain the types of various
> symbols they use (or rely on the culturally accepted notations).
>
> The Buffon needle example presents absolutely no obstacle to typing.
> Perhaps you are mixing up *informal* nature of human mathematics with
> untypedness? Formalizing Buffon's needle requires a great amount of
> precision (what is a curve? what does it mean to "throw a needle"? how
> do we cuunt crossings when there are infinitely many?) which is
> unavoidable so long as we subbscribe to the mathematical method.
> Typedness has nothing to do with this fact.
>
> With kind regards,
>
> Andrej
>
> --
> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Gabriel Scherer]

Conversely, I think that we could leave the discussion of preterms,
typed/untyped representations, etc., out of the present discussion.
Instead of trying to argue, a priori, which representations gives the
more important initiality statement, we should be able to see, given
initiality proofs for each representation (assuming that the proofs
are as clean as they can), which ones contain the important, tasty
bits, and which ones can be factorized from the others by adding a
trivial or heavy-but-already-well-understood (parsing, for example)
step.
In particular, someone feeling that a given representation is "less
important" from an initiality perspective should be able to prove
themselves correct by deriving the result, while if they are missing
something of mathematical interest it would be apparent in the
difficulty to establish the result.

(It is not clear that the absolute importance of various
representation choices can be assessed solely from their initiality
properties; but initiality properties is what is discussed here.)




On Tue, Jun 5, 2018 at 10:37 AM, David Roberts <drobert...@gmail.com> wrote:
> There is an... "interesting" discussion going on at the fom mailing
> list at present, the usual suspects included, about set theory-based
> proof assistants, which might provide either a source of entertainment
> or frustration. It is enlightening when considering what people think
> about typed vs untyped.
>
> Univalent foundations gets a mention here:
> https://cs.nyu.edu/pipermail/fom/2018-May/021012.html
> The 'ideal proof assistant' is described as being based on ZFC here:
> https://cs.nyu.edu/pipermail/fom/2018-May/021026.html
> Friedman proclaims he is completely ignorant of the issues and that he
> has never gotten close to getting dirty with details, but is happy to
> weigh in: https://cs.nyu.edu/pipermail/fom/2018-May/021023.html
> The discussion continues this month here:
> https://cs.nyu.edu/pipermail/fom/2018-June/021030.html
>
> David
> David Roberts
> http://ncatlab.org/nlab/show/David+Roberts
>
>
> On 5 June 2018 at 17:22, Andrej Bauer <andrej...@andrej.com> wrote:
>> Dear Alexander,
>>
>>
>> On Wed, May 30, 2018 at 12:53 PM, Alexander Kurz <axh...@gmail.com> wrote:
>>>
>>> It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed.
>>>
>>> If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved.
>>
>> I think you made there a coiple of intellectual jumps. In order for
>> your statements to have some weight, you need to consider the
>> following questions:
>>
>> (a) What if formalization of mathematics in existing proof assistants
>> is hard for some reason other than typedness?
>>
>> (b) Most proof assistants that have a large user base are typed. Is
>> this is a big conspiracy on part of the designers, or could it be
>> understood as evidence that typed proof assistants have a certain
>> advantage over the untyped ones?
>>
>> (c) You offer LaTeX as an example of good design. I beg to differ.
>>
>> (d) Informal mathematics is very obviously typed, as witnessed by the
>> fact that authors are always carefully explain the types of various
>> symbols they use (or rely on the culturally accepted notations).
>>
>> The Buffon needle example presents absolutely no obstacle to typing.
>> Perhaps you are mixing up *informal* nature of human mathematics with
>> untypedness? Formalizing Buffon's needle requires a great amount of
>> precision (what is a curve? what does it mean to "throw a needle"? how
>> do we cuunt crossings when there are infinitely many?) which is
>> unavoidable so long as we subbscribe to the mathematical method.
>> Typedness has nothing to do with this fact.
>>
>> With kind regards,
>>
>> Andrej
>>
>> --
>> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 1760 bytes --]



On Tuesday, 5 June 2018 09:37:41 UTC+1, David Roberts wrote:
>
> There is an... "interesting" discussion going on at the fom mailing 
> list at present, the usual suspects included, about set theory-based 
> proof assistants, which might provide either a source of entertainment 
> or frustration. It is enlightening when considering what people think 
> about typed vs untyped. 
>
> Univalent foundations gets a mention here: 
> https://cs.nyu.edu/pipermail/fom/2018-May/021012.html 
> The 'ideal proof assistant' is described as being based on ZFC here: 
> https://cs.nyu.edu/pipermail/fom/2018-May/021026.html 
> Friedman proclaims he is completely ignorant of the issues and that he 
> has never gotten close to getting dirty with details, but is happy to 
> weigh in: https://cs.nyu.edu/pipermail/fom/2018-May/021023.html 
> The discussion continues this month here: 
> https://cs.nyu.edu/pipermail/fom/2018-June/021030.html 
>
>
May I humbly say that the FOM list is mainly concerned with the foundations 
of mathematics of hlevel 2, or 0-types. 

And that they are concerned with "how much" a foundation can prove, rather 
than "what" a foundation talks about *natively*?  (As opposed to via 
ZFC-set avatars.)

What univalent mathematics proposes is that infty-groupoids are the 
primitive objects of mathematics, rather than ZFC sets (imprecisely 
mirrored by 1-groupoids). 

We call these things types (bad terminology, inherited from history). 

From this point of view, the above FOM discussion is completely misguided. 
(As you already know.)

The point of univalent foundations is that we should be able to talk about 
the objects we have in mind directly as they are, rather than via ZFC 
avatars.  

It is not that we worship types.

Martin


[-- Attachment #1.2: Type: text/html, Size: 4320 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 2013 bytes --]

("Imprecisely mirrored by 0-groupoids" - apologies for the typo.)

On Tuesday, 5 June 2018 23:19:20 UTC+1, Martín Hötzel Escardó wrote:
>
>
>
> On Tuesday, 5 June 2018 09:37:41 UTC+1, David Roberts wrote:
>>
>> There is an... "interesting" discussion going on at the fom mailing 
>> list at present, the usual suspects included, about set theory-based 
>> proof assistants, which might provide either a source of entertainment 
>> or frustration. It is enlightening when considering what people think 
>> about typed vs untyped. 
>>
>> Univalent foundations gets a mention here: 
>> https://cs.nyu.edu/pipermail/fom/2018-May/021012.html 
>> The 'ideal proof assistant' is described as being based on ZFC here: 
>> https://cs.nyu.edu/pipermail/fom/2018-May/021026.html 
>> Friedman proclaims he is completely ignorant of the issues and that he 
>> has never gotten close to getting dirty with details, but is happy to 
>> weigh in: https://cs.nyu.edu/pipermail/fom/2018-May/021023.html 
>> The discussion continues this month here: 
>> https://cs.nyu.edu/pipermail/fom/2018-June/021030.html 
>>
>>
> May I humbly say that the FOM list is mainly concerned with the 
> foundations of mathematics of hlevel 2, or 0-types. 
>
> And that they are concerned with "how much" a foundation can prove, rather 
> than "what" a foundation talks about *natively*?  (As opposed to via 
> ZFC-set avatars.)
>
> What univalent mathematics proposes is that infty-groupoids are the 
> primitive objects of mathematics, rather than ZFC sets (imprecisely 
> mirrored by 1-groupoids). 
>
> We call these things types (bad terminology, inherited from history). 
>
> From this point of view, the above FOM discussion is completely misguided. 
> (As you already know.)
>
> The point of univalent foundations is that we should be able to talk about 
> the objects we have in mind directly as they are, rather than via ZFC 
> avatars.  
>
> It is not that we worship types.
>
> Martin
>
>

[-- Attachment #1.2: Type: text/html, Size: 4620 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Richard Williamson]

Alexander is getting a fair bit of stick! I just wanted to add a
note of support to one aspect of the point I think he is making:
there is a reason that languages such as Python are widely used
by perfectly competent programmers who fully understand the
benefits of typing.

I share the view that there has to be something rather more
Python-like in syntax than the currently available syntaxes if
one is to have any hope of having something usable in practise by
people who just want to get on with the mathematics. I am not
convinced that this is a purely engineering problem as opposed to
a theoretical one.

(Yes, Python is not untyped either, but I think the point
stands).

On Tue, Jun 05, 2018 at 09:52:26AM +0200, Andrej Bauer wrote:
> Dear Alexander,
>
>
> On Wed, May 30, 2018 at 12:53 PM, Alexander Kurz <axh...@gmail.com> wrote:
> >
> > It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed.
> >
> > If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved.
>
> I think you made there a coiple of intellectual jumps. In order for
> your statements to have some weight, you need to consider the
> following questions:
>
> (a) What if formalization of mathematics in existing proof assistants
> is hard for some reason other than typedness?
>
> (b) Most proof assistants that have a large user base are typed. Is
> this is a big conspiracy on part of the designers, or could it be
> understood as evidence that typed proof assistants have a certain
> advantage over the untyped ones?
>
> (c) You offer LaTeX as an example of good design. I beg to differ.
>
> (d) Informal mathematics is very obviously typed, as witnessed by the
> fact that authors are always carefully explain the types of various
> symbols they use (or rely on the culturally accepted notations).
>
> The Buffon needle example presents absolutely no obstacle to typing.
> Perhaps you are mixing up *informal* nature of human mathematics with
> untypedness? Formalizing Buffon's needle requires a great amount of
> precision (what is a curve? what does it mean to "throw a needle"? how
> do we cuunt crossings when there are infinitely many?) which is
> unavoidable so long as we subbscribe to the mathematical method.
> Typedness has nothing to do with this fact.
>
> With kind regards,
>
> Andrej
>
> --
> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Thorsten Altenkirch]

On 06/06/2018, 00:12, "homotopyt...@googlegroups.com on behalf of
Richard Williamson" <homotopyt...@googlegroups.com on behalf of
rwilli...@gmail.com> wrote:

>Alexander is getting a fair bit of stick! I just wanted to add a
>note of support to one aspect of the point I think he is making:
>there is a reason that languages such as Python are widely used
>by perfectly competent programmers who fully understand the
>benefits of typing.

Actually I am teaching Python (by choice) hence I agree to a point.
However, first of all we can express "untyped" constructions in a typed
setting (e.g. an untyped object is a pair of a type code and an element of
the corresponding type). And second the untyped version is only the first
step before I understand what I am doing at which point I am able to make
the concepts involved more precise. In particular in a mathematical
development I would expect that the objects involved are understood and
hence can be given a specific type.

>
>I share the view that there has to be something rather more
>Python-like in syntax than the currently available syntaxes if
>one is to have any hope of having something usable in practise by
>people who just want to get on with the mathematics. I am not
>convinced that this is a purely engineering problem as opposed to
>a theoretical one.
>
>(Yes, Python is not untyped either, but I think the point
>stands).

Actually, Python is dynamically typed, which is why I always compare it to
set theory. Python has predicates to test wether an object belongs to an
arbitrary type. This corresponds to the element relation in set theory. In
contrast, strongly typed languages don't have predicates like this because
you know statically what the type of an object is. In the same way in Type
Theory typing is static hence it doesn't make sense to have an element
relation.

I would think that once I understand the concepts involved in my
construction I should be able to assign static types to them. That is
certainly the case in programming but even more so for mathematical
constructions. 


>
>On Tue, Jun 05, 2018 at 09:52:26AM +0200, Andrej Bauer wrote:
>> Dear Alexander,
>>
>>
>> On Wed, May 30, 2018 at 12:53 PM, Alexander Kurz <axh...@gmail.com>
>>wrote:
>> >
>> > It is crucial that informal mathematics is untyped. The untypedness
>>is what makes it flexible enough for practical purposes. Formalising
>>mathematics in a proof assistant is hard work. And to a large extent
>>this is due to the fact that everything has to be typed.
>> >
>> > If we ever want to get mathematicians to use proof assistants as
>>casually as they use latex, the problem of untyped vs typed mathematics
>>needs to be solved.
>>
>> I think you made there a coiple of intellectual jumps. In order for
>> your statements to have some weight, you need to consider the
>> following questions:
>>
>> (a) What if formalization of mathematics in existing proof assistants
>> is hard for some reason other than typedness?
>>
>> (b) Most proof assistants that have a large user base are typed. Is
>> this is a big conspiracy on part of the designers, or could it be
>> understood as evidence that typed proof assistants have a certain
>> advantage over the untyped ones?
>>
>> (c) You offer LaTeX as an example of good design. I beg to differ.
>>
>> (d) Informal mathematics is very obviously typed, as witnessed by the
>> fact that authors are always carefully explain the types of various
>> symbols they use (or rely on the culturally accepted notations).
>>
>> The Buffon needle example presents absolutely no obstacle to typing.
>> Perhaps you are mixing up *informal* nature of human mathematics with
>> untypedness? Formalizing Buffon's needle requires a great amount of
>> precision (what is a curve? what does it mean to "throw a needle"? how
>> do we cuunt crossings when there are infinitely many?) which is
>> unavoidable so long as we subbscribe to the mathematical method.
>> Typedness has nothing to do with this fact.
>>
>> With kind regards,
>>
>> Andrej
>>
>> --
>> 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.




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

Re: [HoTT] Re: Where is the problem with initiality?

[Richard Williamson]

> Actually I am teaching Python (by choice)

Nice!

> And second the untyped version is only the first step before I
> understand what I am doing at which point I am able to make the
> concepts involved more precise.

Interesting! If I understood you correctly, I would say that I
program in Python in the opposite way: I always have the types in
my mind, and these guide the code, even though I do not write
them down explicitly. In other words, I think that I program in
the way as you have in mind in the following sentence, but there
are benefits (flexibility, development time, etc) to me in
writing the code in Python rather than in a statically typed
language.

> In particular in a mathematical development I would expect that
> the objects involved are understood and hence can be given a
> specific type.

I like the following analogy...

> Actually, Python is dynamically typed, which is why I always compare it to
> set theory. Python has predicates to test wether an object belongs to an
> arbitrary type. This corresponds to the element relation in set theory. In
> contrast, strongly typed languages don't have predicates like this because
> you know statically what the type of an object is. In the same way in Type
> Theory typing is static hence it doesn't make sense to have an element
> relation.

...and the following is also true...

> I would think that once I understand the concepts involved in my
> construction I should be able to assign static types to them. That is
> certainly the case in programming but even more so for mathematical
> constructions.

...but I disagree with the implied conclusion that one will
always wish to write down those static types.

Suppose I wish to formalise a quick argument involving words in a
free group for instance. Does it really matter to me whether I am
actually working in a free group? Maybe any group would do for my
present purposes. Indeed, maybe any monoid would do. It is going
to save me a lot of time, and give more flexibility with regard
to how I incorporate my argument in a larger argument later, if I
can just jump in and start manipulating those words without
worrying yet about what type they have, even if I have a
particular type, or more than one type, in mind.

One might even argue that such a view is philosophically closer
to much mathematical practise, especially that influenced by
category theory: we are typically concerned with the properties
of an object (what we can do with it), not exactly with what it
is. To misappropriate the classic slogan: if it quacks like a
free group, it might as well be a free group.

Re: [HoTT] Re: Where is the problem with initiality?

[Jon Sterling]

Hi all,

The point about the homotopy hypothesis is well-taken, but I cannot help but think that there is something of quite a different nature going on with the initiality conjecture. I hope to be corrected by those who know more than I, but it seems like the gap between the "definitional solution" and the full sequence of mathematical practice which the homotopy hypothesis hopes to account for must be vastly greater than the gap between type theory qua preterms + raw judgments, and type theory qua the generalized algebraic theory (for which the initiality conjecture is essentially something that one observes, rather than proves AFAICT).

Somehow for the last 50 years what we type theorists were doing was not so far away from the 'definitional solution'---there is definitely a gap, but ever since Lawvere's devastating and decisive rectification campaign of algebra in the 1960s, preceding the development of modern type theory, it has not been the case that a more abstract notion of syntax has been alien to type theorists; the development of logical frameworks (in the tradition of De Bruijn and Martin-Loef) reflects this. [Ask me sometime what I think about the claim that using the logical framework is "defining away" the question!]

Because I don't know much about homotopy theory, I can't go into depth there, but as a type theorist, I would like to say that this gap (between preterms and the generalized algebraic theory) is not uniform, but comprises multiple distinct components, not limited to the following:

1. There is the question of implicit vs explicit substitution. Mathematical accounts of type theory usually use explicit substitution, because it is the most natural, and it can be phrased without reference to preterms or set-theoretic hacking. Explicit substitution is superior, because it is more abstract, but on the other hand there is indeed a question of whether we have 'solved the problem' if we have not explained implicit substitutions. I would argue that this is in some sense not a significant problem, because if you are "inside" type theory / using type theory to do mathematics, there is really no way to observe whether you are using implicit or explicit substitutions: the question is analogous to the matter of allowing beta redexes vs forcing a canonical-forms representation as in modern LF. It is in some sense an implementation detail.

2. There is the fact that type theories "in the wild" are generally not algebraic. That is to say, they do not have unique types (consider universe cumulativity), and even in cases where it would be possible to achieve uniqueness of typing, it is actually highly undesirable from a practical perspective---the unique typing calculi contain so many unnecessary annotations, and to check types in such a setting is highly inefficient. It can of course be argued that implementation is a different matter from the mathematics, but I want to argue that to a certain extent, we should expect practice to be the leading aspect, and that theory should somehow reflect it.

If "wild" type theories are not algebraic, what do we mean by "model" and "initiality"? Surely we can come up with answers to these questions, but I think somehow it is not the right question.

There is a desire for the mathematics to explain in one fell swoop exactly the full gamut of type theories that we use in daily life, but I think that this apparently 'down to earth' point of view actually forces us to give short shrift on one of the most interesting and under-studied parts of type theory, which is the matter of elaboration and of coherence.

To phrase initiality in terms of an already-suitably-algebraic notion of type theory is not, in my opinion, to "define away" the problem; instead, it is to resist drawing the problem outside its range of significance.

Far from being a result which might hold or fail about "type theories" (what are those, specifically?), I think that initiality is a purely definitive principle by which we can measure any attempt at formulating an algebraic notion of type theory (and there is no reason a priori to expect this to explain type theory as it exists in the wild, because the latter kind of type theory was never intended to be algebraic).

The gap between algebraic type theory and the pre-term-presented version of type theory which still has unique types etc. is a purely bureaucratic gap, and of course we can make it appear as though it has more and more scientific content by choosing to use a less and less structured representation of syntax. For instance, we can say "Aha, we are hardly solving the problem if we use de bruijn indices instead of fixing an infinite set of names, like our grandparents taught us to!" And then, we can increase the appearance of difficulty by threading through the entire construction the bureaucratic issues of name binding which were resolved decades ago. We can also increase the appearance of difficulty, as Thorsten satirically argues, by threading through the construction the *parsing* of sequences of tokens into structured syntax; we could take a step further and thread through the construction the *lexing* of sequences of characters into tokens... But to me this is all beside the point.

I believe that the interesting gap that we should study (using tools from the study of elaboration, coercions, coherence, etc.) is the one between "wild" type theory (where you you have subtyping, implicit coercion, etc.) and algebraic type theory. 

[Cubical type theory brings up numerous other analogous questions; for instance, in cubical type theory one constructs a partial element of a type by going under a "restriction", but another possible representation which is more structured and somehow more type-theoretically natural (but less strict) is to actually pattern match on the "proof" of a cofibration formula (this is in fact exactly what one does in the agda formalizations of the Orton-Pitts-Licata style internal presentation of cubical type theory). There is an interesting connection here with the difficulty question of definitional equivalence which supports the full universal property of coproducts, and there may be a coherence theorem to prove.]

Best,
Jon

P.S. Over the past few years my opinions on the questions have changed a lot, and I expect that they will continue to change, hopefully as a result of this very interesting discussion. Thanks!






On Mon, May 28, 2018, at 3:39 PM, Michael Shulman wrote:
> I knew this situation seemed familiar: it reminds me of Tom Leinster's
> comments about the homotopy hypothesis:
> https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html
> (scroll down to "What is an n-category?")
> 
> The "Homotopy Hypothesis" of higher category theory, first formulated
> by Grothendieck, is the claim that "infinity-groupoids are the same as
> spaces".  The prevailing approach to this in higher category theory
> nowadays is the one that Tom describes as a "joke":
> 
> Q.  How do you prove the Homotopy Hypothesis?
> A.  Define an infinity-groupoid to be a Kan complex; define a space to
> be a Kan complex; done!
> 
> Describing this as a joke is not to denigrate the value of such a
> "definitional solution"; it's certainly been enormously fruitful for
> higher category theory.  But at the same time, Tom's point is that it
> doesn't, on its own, answer the question that was originally asked.
> He has a nice picture of a spectrum from "algebra" to "topology",
> starting with algebraic notions of infinity-groupoid, then moving
> through non-algebraic notions of infinity-groupoid, to algebraic
> notions of space, and eventually non-algebraic notions of space, with
> Kan complexes occupying the fulcum at the middle.  A full-strength
> statement of the homotopy hypothesis would then equate fully algebraic
> notions of infinity-groupoid with fully non-algebraic notions of
> space.
> 
> I feel like here we have something similar.  If we call the
> "Initiality Hypothesis" something like "type theory is the initial
> elementary infinity-topos", then we can make a similar "joke":
> 
> Q: How do you prove the Initiality Hypothesis?
> A: Define an elementary infinity-topos to be a (suitably structured)
> CwF; define type theory to be the initial such CwF; done!
> 
> Again, this is not to denigrate the value of such an approach!  It
> just doesn't, on its own, answer the original question.  I can imagine
> a similar spectrum from "syntax" to "semantics", starting with
> "syntactic notions of type theory", then moving through "semantic
> notions of type theory", to "syntactic notions of toposes", and
> eventually "semantic notions of toposes".  Untyped syntax with
> implicit substitution (5) is way over on the syntactic side; locally
> cartesian closed quasicategories with appropriate stuff are way over
> on the semantic side; CwFs and the initial one as a QIIT are at the
> fulcrum in the middle.  And just as Kan complexes can play an
> important intermediate role in connecting the disparate ends of the
> homotopy-hypothesis spectrum, it seems likely that QIIT syntax can
> play a similar intermediate role in connecting the ends of the
> initiality-hypothesis spectrum.
> 
> Does this seem reasonable?
> 
> 
> On Mon, May 21, 2018 at 10:46 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> > Thorsten gave a very nice HoTTEST talk a couple weeks ago about his
> > work with his collaborators on intrinsic syntax as a Quotient
> > Inductive-Inductive Type.  Since then I have been trying to fit
> > together a mental picture of exactly how all the different approaches
> > to syntax are related, but I am still kind of confused.
> >
> > In an attempt to clarify what I mean by "all the different
> > approaches", let me describe all the approaches I can think of in the
> > case of a very simple type theory: non-dependent unary type theory
> > with product types.  Unary means that the judgments have exactly one
> > type in the context, x:A |- t:B, and the only type constructor is a
> > product type A x B, with pairing for an introduction rule and
> > projections for elimination.  The semantics should be a category with
> > finite products.  Here are all the ways I can think of to describe
> > such a type theory:
> >
> >
> > 1. A QIIT that mirrors the semantics, with all the categorical
> > operations as point-constructors and their axioms as
> > equality-constructors.
> >
> > data Ty : Set where
> >  _x_ : Ty -> Ty -> Ty
> > [This will be the same in all cases, so I henceforth omit it.]
> >
> > data Tm : Ty -> Ty -> Set where
> >   id : {A} -> Tm A A
> >   _o_ : Tm A B -> Tm B C -> Tm A C
> >   assoc : h o (g o f) = (h o g) o f
> >   lid : id o f = f
> >   rid : f o id = f
> >   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
> >   pr1 : Tm (A x B) A
> >   pr2 : Tm (A x B) B
> >   beta1 : pr1 o (f , g) = f
> >   beta2 : pr2 o (f , g) = g
> >   eta : p = (pr1 o p , pr2 o p)
> >
> >
> > 2. An Inductive-Inductive family of setoids that similarly mirrors the
> > categorical semantics, with judgmental equality an inductive type
> > family rather than coinciding with the metatheoretic equality.
> >
> > data Tm : Ty -> Ty -> Set where
> >   id : {A} -> Tm A A
> >   _o_ : Tm A B -> Tm B C -> Tm A C
> >   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
> >   pr1 : Tm (A x B) A
> >   pr2 : Tm (A x B) B
> >
> > data Eq : Tm A B -> Tm A B -> Set where
> >   assoc : Eq (h o (g o f)) ((h o g) o f)
> >   lid : Eq (id o f) f
> >   rid : Eq 9f o id) f
> >   beta1 : Eq (pr1 o (f , g)) f
> >   beta2 : Eq (pr2 o (f , g)) g
> >   eta : Eq p (pr1 o p , pr2 o p)
> >
> >
> > 3. A QIIT that instead mirrors the usual type-theoretic syntax, with
> > operations like composition being admissible rather than primitive.
> > In our simple case it looks like this:
> >
> > data Tm : Ty -> Ty -> Set where
> >   id : {A} -> Tm A A
> >   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
> >   pr1 : Tm A (B x C) -> Tm A B
> >   pr2 : Tm A (B x C) -> Tm A C
> >   beta1 : pr1 (f , g) = f
> >   beta2 : pr2 (f , g) = g
> >   eta : p = (pr1 p , pr2 p)
> >
> >
> > 4. Combining 2 and 3, an II family of setoids that mirrors
> > type-theoretic syntax.
> >
> > data Tm : Ty -> Ty -> Set where
> >   id : {A} -> Tm A A
> >   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
> >   pr1 : Tm A (B x C) -> Tm A B
> >   pr2 : Tm A (B x C) -> Tm A C
> >
> > data Eq : Tm A B -> Tm A B -> Set where
> >   beta1 : Eq (pr1 (f , g)) f
> >   beta2 : Eq (pr2 (f , g)) g
> >   eta : Eq p (pr1 p , pr2 p)
> >
> >
> > 5. A single inductive type of raw terms, together with inductive
> > predicates over it for the typing judgment and equality judgments.
> >
> > data Tm : Set where
> >   var : Tm
> >   (_,_) : Tm -> Tm -> Tm
> >   pr1 : Tm -> Tm
> >   pr2 : Tm -> Tm
> >
> > data Of : Ty -> Tm -> Ty -> Set where
> >   of-var : Of A var A
> >   of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
> >   of-pr1 : Of A t (B x C) -> Of A (pr1 t) B
> >   of-pr2 : Of A t (B x C) -> Of A (pr2 t) C
> >
> > data Eq : Ty -> Tm -> Tm -> Ty -> Set where
> >   beta1 : Of A t B -> Of A s C -> Eq A (pr1 (t , s)) t B
> >   beta2 : Of A t B -> Of A s C -> Eq A (pr2 (t , s)) t C
> >   eta : Of A t (B x C) -> Eq A (pr1 t , pr2 t) t (B x C)
> >
> >
> > 6. An II family that defines only the normal forms, via a separate
> > judgment for "atomic" terms that prevents us from writing down any
> > beta-redexes, thereby eliminating the need for any equality judgment
> > (though substitution then becomes more complicated, as it must
> > essentially incorporate beta-reduction).
> >
> > data Atom : Ty -> Ty -> Set where
> >   id : {A} -> Atom A A
> >   pr1 : Atom A (B x C) -> Atom A B
> >   pr2 : Atom A (B x C) -> Atom A C
> >
> > data Tm : Ty -> Ty -> Set where
> >   atom : Atom A B -> Tm A B
> >   (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
> >
> >
> > 7. Combining 5 and 6, an inductive type of raw terms and predicates
> > over it that type only the normal forms.
> >
> > data Tm : Set where
> >   var : Tm
> >   (_,_) : Tm -> Tm -> Tm
> >   pr1 : Tm -> Tm
> >   pr2 : Tm -> Tm
> >
> > data Atom : Ty -> Tm -> Ty -> Set where
> >   atom-var : Atom A var A
> >   atom-pr1 : Atom A t (B x C) -> Atom A (pr1 t) B
> >   atom-pr2 : Atom A t (B x C) -> Atom A (pr2 t) C
> >
> > data Of : Ty -> Tm -> Ty -> Set where
> >   of-atom : Atom A t B -> Of A t B
> >   of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
> >
> >
> > This is all I can think of right now.  Are there others?  Are there
> > other choices we can make in the case of dependent type theory that
> > are not visible in this simple case?
> >
> > In the above simple case of unary type theory with products, it should
> > be easy to show that all these definitions construct the initial
> > category with products.  (There should be some generating/axiomatic
> > types and terms too, to make the result nontrivial, but I've left them
> > out for brevity.)  My main question is, where do things become hard in
> > the case of dependent type theory?
> >
> > It seems to me that the main difference between (1) and (2), and
> > between (3) and (4), is convenience; is that right?  Type theory has
> > no infinitary constructors, so there shouldn't be axiom-of-choice
> > issues with descending algebraic operations to a quotient; it's just
> > that the bookkeeping involved in dealing with setoids everywhere
> > becomes unmanageable in the case of DTT.  Right?
> >
> > Thorsten said that (1) in the case of dependent type theory is
> > tautologically the initial CwF, which seems eminently plausible.  I
> > don't think this solves the "initiality conjecture", but where is the
> > sticking point?  Is it between (1) and (3), or between (3) and (5)?
> >
> > (Note that I'm not talking at all about the "h-level problem" that
> > these QIITs are by definition sets but that for HoTT to "eat itself"
> > we would want to eliminate out of them into the universe which is not
> > a set.  I'm only talking about initiality of syntax among *strict*
> > CwFs; coherence/strictification theorems can wait.  Personally,
> > though, I like (6)-(7) as potential approaches to coherence.)
> 
> -- 
> 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.

Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman]

Thanks, Jon, for that very detailed and thoughtful response.

I agree that there are significant differences between the Homotopy
Hypothesis spectrum and the Initiality Hypothesis spectrum -- how
could there not be?  But I don't think those differences invalidate
the analogy.  The gap in the homotopy hypothesis is not uniform
either: for instance, in addition to algebraic vs nonalgebraic, it
comprises cell shape (globular vs simplicial), and there are other
dimensions too such as whether a definition can be phrased in an
ambient homotopy theory or whether it has to be built out of sets.  In
other words, the "spectrum" is actually multidimensional in both
cases.  And non-algebraic notions of higher category were not alien to
category theorists either; indeed, the very first proposed general
definition of omega-category (due to Ross Street) was non-algebraic!

I'm grateful to you, Thorsten, and others, for trying to help me get
over my hangups about explicit substitution.  I guess that
fundamentally what matters is the existence of normal forms and of a
terminating normalization algorithm, and that applies to
beta-reduction as well as to substitution-reduction.  I personally
find it more elegant to regard the normal forms as the "fundamental"
objects with things like application and substitution as defined
operations on them, rather than regarding application and substitution
as term constructors and then having to quotient by beta-reduction and
substitution reduction -- why introduce flab only to quotient it out
later?  And I have an easier time with explicit applications than with
explicit substitutions, because I see the former but not the latter
all the time in everyday mathematics.  But I can see that the other
approach has advantages as well.

On Tue, May 29, 2018 at 7:00 AM, Jon Sterling <j...@jonmsterling.com> wrote:
> Far from being a result which might hold or fail about "type theories" (what are those, specifically?),

I take it that your parenthetical refers to the lack of a general
definition of "type theory".  But to me, such a lack is itself a gap
in the literature -- how can we really consider "type theory" a
respectable mathematical subject if we don't even have definitions of
the things it studies?  The lack of such a definition is not a reason
not to study type theories in general, rather the opposite -- studying
type theories in general will help move us towards being able to
formulate such definitions (note the plural -- I don't necessarily
expect there to ever be *one* definition encompassing *all* type
theories).

> I think that initiality is a purely definitive principle by which we can measure any attempt at formulating an algebraic notion of type theory (and there is no reason a priori to expect this to explain type theory as it exists in the wild, because the latter kind of type theory was never intended to be algebraic).

I don't think the fact that "wild type theories" (interesting
associativity there with the biological notion of "wild type") were
"never intended to be algebraic" is a reason not to study their
algebraicity.  In fact it's *more* exciting when something that wasn't
*intended* to be algebraic turns out nevertheless to be (equivalent
to) something algebraic!  Such unintended coincidences are what
mathematics thrives on; indeed HoTT itself arose from a gigantic
unintended coincidence between intensional type theory and homotopy
theory.

> The gap between algebraic type theory and the pre-term-presented version of type theory which still has unique types etc. is a purely bureaucratic gap

I don't think that's a fair characterization, because it seems
(likely) to depend on fundamental features of a particular type
theory.  In his talk Thorsten mentioned that the proof of decidability
of equality for QIIT syntax uses a normalization, and the alternative
argument I proposed using hereditary substitution also depends on the
existence of the latter, which is essentially a normalization
property.  I wouldn't call something "bureaucratic" if it depends on
essential features of a particular situation and doesn't generalize to
slightly modified situations.

> I believe that the interesting gap that we should study (using tools from the study of elaboration, coercions, coherence, etc.) is the one between "wild" type theory (where you you have subtyping, implicit coercion, etc.) and algebraic type theory.

I agree that elaboration is an important problem that we should study,
but I don't think it is "the" problem we should study -- other
problems can also be interesting and important!

Thanks again for the interesting discussion!

Best,
Mike

Re: [HoTT] Re: Where is the problem with initiality?

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 1397 bytes --]



On Wednesday, 30 May 2018 23:35:57 UTC+1, Michael Shulman wrote:
>
>
> On Tue, May 29, 2018 at 7:00 AM, Jon Sterling <j....@jonmsterling.com 
> <javascript:>> wrote: 
> > Far from being a result which might hold or fail about "type theories" 
> (what are those, specifically?), 
>
> I take it that your parenthetical refers to the lack of a general 
> definition of "type theory".  But to me, such a lack is itself a gap 
> in the literature -- how can we really consider "type theory" a 
> respectable mathematical subject if we don't even have definitions of 
> the things it studies?  The lack of such a definition is not a reason 
> not to study type theories in general, rather the opposite -- studying 
> type theories in general will help move us towards being able to 
> formulate such definitions (note the plural -- I don't necessarily 
> expect there to ever be *one* definition encompassing *all* type 
> theories). 
>
>
Of course, as you know, people did a lot of group theory before there was a 
definition of group. And the theory of groups helped to formulate the 
notion of a group. The same happened with topology, where formulations of 
notions of space came after a lot of work on topology had already been 
done. Is the study of type theories mature enough to admit a general 
definition of a type theory, of which the ones we are looking at are a 
particular case?

Martin

[-- Attachment #1.2: Type: text/html, Size: 1861 bytes --]

Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman]

On Thu, May 31, 2018 at 3:48 AM, Martín Hötzel Escardó
<escardo...@gmail.com> wrote:
> Is the
> study of type theories mature enough to admit a general definition of a type
> theory, of which the ones we are looking at are a particular case?

Well, we won't know whether it is unless we try.  Various of the
people working on the initiality theorem are approaching it by way of
formulating such definitions, either syntactically (collections of
rules) or semantically (structure on a CwF).  And I spoke about
another class of general definitions-in-progress in my own HoTTEST
talk (jww Dan Licata and Mitchell Riley).