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