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