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.