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.