Re: Where is the problem with initiality?

[Ambrus Kaposi <kaposi...@gmail.com>]

[-- 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 --]