You might have already seen this, but I have a paper on so= me related issues at=C2=A0http= s://arxiv.org/abs/1808.00920 . In that paper I didn't look at the o= riginal version of regularity, but a more recent version ("all monomor= phisms are cofibrations")=C2=A0that fits better with the general frame= work of Orton and Pitts. In that case it is definitely equality of objects = that causes problems.

Best,
Andrew

On F= riday, 13 September 2019 08:10:42 UTC+2, Jasper Hugunin wrote:
Hello all,

=
I've been trying to understand better why composition for the= universe does not satisfy regularity.
Since comp^i [ phi |-> = E ] A is defined as (roughly) Glue [ phi |-> equiv^i E ] A, I would expe= ct regularity to follow from two parts:
1. That Glue [ phi |->= equivRefl A ] A reduces to A (a sort of regularity condition for the Glue = type constructor itself)
2. That equiv^i (refl A) reduces to equi= vRefl A
I'm curious as to which (or both) of these parts was = the issue, or if regularity for the universe was supposed to follow from a = different argument.

Context:
I'= ve been studying and using CCHM cubical type theory recently, and often fin= ding myself wishing that J computed strictly.
If I understand cor= rectly, early implementations of ctt did have strict J for Path types, and = this was justified by a "regularity" condition on the composition= operation, but as discussed in=C2=A0this thread on the HoTT mailing list= , the definition of composition for the universe was found to not satisfy r= egularity.
I don't remember seeing the regularity condition d= efined anywhere, but my understanding is that it requires that composition = in a degenerate line of types, with the system of constraints giving the si= des of the box also degenerate in that direction, reduces to just the botto= m of the box. This seems to be closed under the usual type formers, plus Gl= ue, but not the universe with computation defined as in=C2=A0the CCHM paper=C2=A0= (for trivial reasons and non-trivial reasons; it gets stuck at the start wi= th Glue [ phi |-> equiv^i refl ] A not reducing to anything).
=
Best regards,
- Jasper Hugunin

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/16b3b92f-069b-468c-94f8-f3859e152338%40googleg= roups.com.
------=_Part_1514_1197939661.1568548534596-- ------=_Part_1513_667385532.1568548534596--