If my note was correct, it describes in the cubical set model two univalent universes
(subpresheaf of the first universe) that satisfy
(1) if A : sSet and p : Path A a b then a = b : A and p is the constant path a
(equality reflection rule)
(2) if A : bSet and p and q of type Path A a b then p = q : Path A a b
(judgemental form of UIP)
Maybe (1) or (2) could be used instead of HTS (and we would remain in an univalent
theory, where all types are fibrant)
For testing this, one question is: can we define semi-simplicial types in (1)? in (2)?
Best regards,
Thierry
So the answer was yes, right? Problem solved?
On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v 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
HomotopyTypeTheory+unsu...@googlegroups.com.
For more options, visit
https://groups.google.com/d/optout.