Hello all,

2. That equiv^i (refl A) reduces to equivRefl A

I've been trying to=
understand better why composition for the universe does not satisfy regula=
rity.

Since comp^i [ phi |-> E ] A is defined as (roughly) Glu=
e [ phi |-> equiv^i E ] A, I would expect 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)

I'm curious=
as to which (or both) of these parts was the issue, or if regularity for t=
he universe was supposed to follow from a different argument.

Context:

I've been studying and using CCHM c=
ubical type theory recently, and often finding myself wishing that J comput=
ed strictly.

If I understand correctly, early implementations of =
ctt did have strict J for Path types, and this was justified by a "reg=
ularity" 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=
regularity.

I don't remember seeing the regularity condition=
defined anywhere, but my understanding is that it requires that compositio=
n in a degenerate line of types, with the system of constraints giving the =
sides of the box also degenerate in that direction, reduces to just the bot=
tom of the box. This seems to be closed under the usual type formers, plus =
Glue, but not the universe with computation defined as in=C2=A0the CCH=
M paper=C2=A0(for trivial reasons and non-trivial reasons; it gets stuc=
k at the start with Glue [ phi |-> equiv^i refl ] A not reducing to anyt=
hing).

Best regards,

- Jaspe=
r 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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8fo4FKCLiCVCYm6AGeVc%3Dq= B8QNUZ3Weho6kLT8NXtc-Q%40mail.gmail.com.

--0000000000000dc3820592691dc6--