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:

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 AI'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--