From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 22 May 2018 09:47:37 -0700 (PDT) From: Ambrus Kaposi To: Homotopy Type Theory Message-Id: <73f16935-63b3-4ebe-a13b-35ccd4e4bf53@googlegroups.com> In-Reply-To: References: Subject: Re: Where is the problem with initiality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_26201_1263155399.1527007658023" ------=_Part_26201_1263155399.1527007658023 Content-Type: multipart/alternative; boundary="----=_Part_26202_1942680772.1527007658023" ------=_Part_26202_1942680772.1527007658023 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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 ------=_Part_26202_1942680772.1527007658023 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Hi Mike,

This is all I can think of right now. =C2=A0Are there others? =C2=A0Are = 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 followi= ng categories:

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

Your variants are categorised as bel= ow:

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 followin= g additional choices:
=C2=A0- Conversion and typing can be me= rged into a PER
=C2=A0- use universes a la Russel or Tarski (= in the Russel case, types and terms are identified)
=C2=A0- y= ou can have paranoid/relaxed variants of constructors (do you have Pi A B o= r Pi Gamma A B)
=C2=A0- do you have conversion for contexts or no= t

In t= he 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. =C2=A0(There should be some generating/axiomati= c
types and terms too, to make the result nontrivial, but I've left t= hem
out for brevity.) =C2=A0My main question is, where do things become har= d 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? =C2=A0Type theory h= as
no infinitary constructors, so there shouldn't be axiom-of-choice
issues with descending algebraic operations to a quotient; it's jus= t
that the bookkeeping involved in dealing with setoids everywhere
becomes unmanageable in the case of DTT. =C2=A0Right? =C2=A0

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

I think the hard part is between (3) a= nd (5). However I haven't seen a definition of =C2=A0(3) for type theor= y, e.g. CwF+Pi. It is very intricate, you have to prove substitution laws m= utually 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=C2=A0http://www.cs= e.chalmers.se/~peterd/papers/Lmcs-2016.pdf

Cheers,=
Ambrus
------=_Part_26202_1942680772.1527007658023-- ------=_Part_26201_1263155399.1527007658023--