Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Two Papers on Path Types and Identity Types
@ 2018-08-03 10:33 Andrew Swan
  0 siblings, 0 replies; only message in thread
From: Andrew Swan @ 2018-08-03 10:33 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 989 bytes --]

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.

[-- Attachment #1.2: Type: text/html, Size: 1341 bytes --]

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2018-08-03 10:33 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-08-03 10:33 [HoTT] Two Papers on Path Types and Identity Types Andrew Swan

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).