Re: [HoTT] Where is the problem with initiality?

[Bas Spitters <b.a.w.s...@gmail.com>]

One question that recently came up in our work on modal type theory,
https://arxiv.org/abs/1804.05236
is: what is the right notion of morphism for CwF.
In the paper (def 9, thm 10) we propose a notion of weak CwF morphism,
where comprehension is only preserved upto iso.

The notion fits well with the local universe construction, but I
hadn't seen it before.
Peter Lumsdaine later told me that it sees CwFs as discrete
comprehension categories and where one uses pseudo-maps of comp cats.

I also noticed that the literature on categories of models of type
theory seems quite scattered (I guess this complaint is due to
Vladimir).
We know how to translate between different models of type theory, but
I don't know of a convenient place to find all the functorial
properties.

On Sat, May 26, 2018 at 6:47 PM,  <stre...@mathematik.tu-darmstadt.de> wrote:
>> Thomas, are you saying that the hard part is proving that the syntax
>> of type theory is a CwF?  I always thought that was perfectly obvious
>> and the hard part was interpreting the syntax into some other CwF.
>
> That was a misunderstanding on my side. Correctness is also quite an issue.
>
> But I thought you just discussed the initiality problem!
> For this the laborious part is indeed showing that Lindenbaum-Tarski gives
> a model. I mean this is intuitively clear and without any surprises.
> If one is not overly formalist one is happy to believe this. I possibly
> was more formalist those days (:-
>
> But formulating the correctness in terms of a partial interpretation
> function on raw syntax is a nice unorthodox idea. To perform it is also a
> bit dull but getting the idea how to proceed took me some time.
>
> If I had thought in terms of initial models for essentially algebraic
> theories I wouldn't have proven my completeness theorem but rather relied
> on algebraic and variable syntax as obviously “isomorph“.
>
> Thomas
>
> --
> 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.