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

[Michael Shulman <shu...@sandiego.edu>]

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.

On Sat, May 26, 2018 at 2:21 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> Triggered by your mails I have tried to recall what I think has to
> be shown for verifying the initiality conjecture.
> Given a type theory with its catgeorical semantics we can construct 2
> models M_a and M_s where M_a is the initial model of the respective
> essentially algebraic theory and M_s is the Lindenbaum-Tarski model
> obtained by factoring syntax modulo provable (judgemental) equality.
> Then we have homomorphism h : M_a -> M_s (by initiality) and h' : M_s
> -> M_a (essential the interpretation function for the theory in M_a).
> Trivially h' \circ h is the identity. For showing that h \circ h' is
> the identity one essentailly shows that interpreting syntax in M_a and
> translating the result back to syntax with variables is the identity.
>
> This last step should be a straightforward induction over syntax.
> Thus the main task is to show that M_s is actually a model. This
> latter task I performed for CoC in my old Thesis. This is fairly
> tedious when performed in detail.
>
> When I wrote my Thesis I didn't think about M_a at all. Instead I used
> the obvious fact that interpreting syntax in M_s just amounts to
> taking equivalence classes modulo provable equivalence. This suffices
> for obtaining the completeness theorem I wanted to have. That M_s is
> initial is then sort of obvious since M_s is term generated and
> interpretation of syntax gives a morphism from M_s to any other model.
>
> So summing up the key is to show that the Lindenbaum-Tarksi construction
> gives rise to a model.
>
> 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.