Thanks Steve!

On Sun, Sep 15, 2019, at 9:38 PM, steve awodey wrote:
It does: the rel= f term is always a weak equivalence by 3 for 2, and it=E2=80=99s monic beca= use it=E2=80=99s a section.

Sent from my iPhone
=

> On Sep 15, 2019, at 21:04, Jon Sterling <jon@jonmsterling.com>= ; wrote:

> Hi Andrew,

> D= oes "all monomorphisms are cofibrations" imply that identity and path types= coincide? or only the other way around?

> Thanks,=
> Jon

= >
>> On Sun, Sep = 15, 2019, at 7:55 AM, Andrew Swan wrote:
>> You might have already seen this, but I have a paper on s= ome related
>> issue= s at https://arxiv.org/abs/1808.00920 . In that paper I didn't
>> look at the original version = of regularity, but a more recent version
>> ("all monomorphisms are cofibrations") that fits be= tter with the
>> gen= eral framework of Orton and Pitts. In that case it is definitely
<= /div>
>> equality of objects that ca= uses problems.
>>
>> Best,
>> Andrew
>>
>>&= gt; On Friday, 13 September 2019 08:10:42 UTC+2, Jasper Hugunin wrote:
<= /div>
>>> Hello all,
>>>
>>> I've been trying to understand better why co= mposition for the universe does not satisfy regularity.
>>> Since comp^i [ phi |-> E ] A is def= ined as (roughly) Glue [ phi |-> equiv^i E ] A, I would expect regularit= y 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= equivRefl A
>>> I'm cu= rious 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 t= heory recently, and often finding myself wishing that J computed strictly.<= br>
>>> 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 this thread on the HoTT mailing list <https://grou= ps.google.com/d/msg/homotopytypetheory/oXQe5u_Mmtk/3HEDk5g5uq4J>, the de= finition of composition for the universe was found to not satisfy regularit= y.
>>> I don't remember= seeing the regularity condition defined anywhere, but my understanding is = that it requires that composition in a degenerate line of types, with the s= ystem of constraints giving the sides of the box also degenerate in that di= rection, reduces to just the bottom of the box. This seems to be closed und= er the usual type formers, plus Glue, but not the universe with computation= defined as in the CCHM paper <http://www.cse.chalmers.se/~coquand/cubic= altt.pdf> (for trivial reasons and non-trivial reasons; it gets stuck at= the start with Glue [ phi |-> equiv^i refl ] A not reducing to anything= ).
>>>
<= div style=3D"font-family:Arial;">>>> Best regards,
>>> - Jasper Hugunin
>>
>> --
>&= gt; You received this message because you are subscribed to the Google = ;
>> Groups "Homotopy Type= Theory" group.
>> To unsu= bscribe from this group and stop receiving emails from it, send
>> an email to HomotopyTypeTheo= ry+unsubscribe@googlegroups.com.
>> To view this discussion on the web visit