Dear all,

I've posted two papers to the arXiv that might be of interest to people on 
this list, both on path types and identity types.

Identity Types in Algebraic Model Structures and Cubical Sets 
<https://arxiv.org/abs/1808.00915> - a nicer version of my earlier work on 
path types and identity types in algebraic model structures
Separating Path and Identity Types in Presheaf Models of Univalent Type 
Theory <https://arxiv.org/abs/1808.00920> - in some situations it is 
possible to show that path types cannot be used directly as identity types 
(and so some kind of separate construction is strictly necessary)

Comments, questions, corrections etc are welcome.


Best,
Andrew

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.