Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Kripke-Joyal Semantics and HoTT
@ 2019-10-08 15:07 Alexander Gietelink Oldenziel
  2019-10-08 16:36 ` Ali Caglayan
  0 siblings, 1 reply; 3+ messages in thread
From: Alexander Gietelink Oldenziel @ 2019-10-08 15:07 UTC (permalink / raw)
  To: Homotopy Type Theory

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

Dear all,

It is my understanding that the interpretation of HoTT inside higher topoi 
is an ongoing field of research. Much of this business involves subtle 
strictness properties and things like contextual and syntactic categories. 
In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These 
semantics are easy to use in practice.  Naively, it seems one could lift 
the Kripke-Joyal semantics by not asking for truth but simply an inhabitant 
of a type. 

Has this been investigated at all? Is it ultimately fruitless?

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.com.

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

^ permalink raw reply	[flat|nested] 3+ messages in thread

end of thread, other threads:[~2019-10-10 21:20 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-10-08 15:07 [HoTT] Kripke-Joyal Semantics and HoTT Alexander Gietelink Oldenziel
2019-10-08 16:36 ` Ali Caglayan
2019-10-10 21:20   ` Michael Shulman

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