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>> https://groups.google.com/d/msgid/Homotop= yTypeTheory/16b3b92f-069b-468c-94f8-f3859e152338%40googlegroups.com <htt= ps://groups.google.com/d/msgid/HomotopyTypeTheory/16b3b92f-069b-468c-94f8-f= 3859e152338%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter&g= t;.>> --> You received this message because you are subscribed to the Go= ogle Groups "Homotopy Type Theory" group.> To unsubscribe from this group and stop receiving emails fro= m it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.

=> To view this discussion on the= web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/80a2be3b-af= aa-4106-9c69-0df6567ec709%40www.fastmail.com.--

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/afe67df2-7f4a-4e51-abc9-3f8e3a985623%40www.fas= tmail.com.

--18654bdf4b6a4ca7b87c475527c9d9b6--