Here is note which should be connected to this message. It contains first a self contained presentation of the cubical set model, and then a notion of “Bishop set” which corresponds to the fact that any two paths between the same end points are -judgmentally- equal. One defines a subpresheaf of the universe which classifies these sets, and one notices that this notion is closed by the Kan filling operation of the universe (because this is defined in term of glueing, and this notion is closed by the glueing operation), and hence it is fibrant (and univalent). If this is correct, one expects a corresponding type system with decidable type-checking, and connections with what has been done in observational type theory (and it will be interesting to see if this can also be connected to the more recent work of Thorsten et al.) while staying in a univalent theory. Thierry On 23 Feb 2017, at 15:47, Vladimir Voevodsky > wrote: Just a thought… Can we devise a version of the HTS where exact equality types are not available for the universes such that, even with the exact equality, HTS would remain a univalent theory. Maybe only some types should be equipped with the exact equality and this should be a special quality of types. Vladimir. PS If there are higher inductive types then the exact equality should not be available for them either. -- 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.