Theorem 3.1.2

[DanGrayson]

Lots of rephrasing needed here.

[DanGrayson]

Ooops, thanks @benediktahrens .

[DanGrayson]

Commit a39baad addresses this.

[DanGrayson]

There's one more issue with the proof -- the last paragraph introduces p and q again, but doesn't use them.

[UlrikBuchholtz]

The last paragraph uses the more general result from the previous paragraph that takes p : f(∙) = g(∙) and q : f(loop) = p⁻¹ · g(loop) · p and produces an identification of f and g. So the last paragraph explains which p and q to use so that this applies to ve(ev(f)) and f.

[bidundas]

I have a problem finding a place I can talk that still has passable wifi (my office mate is unfortunately not gone yet) so don't wait for me and excuse me if I come and go. I only have some thought on some proofs to share today. Bjorn On 9 Sep 2022, at 15:59, Ulrik Buchholtz ***@***.***> wrote:  The last paragraph uses the more general result from the previous paragraph that takes p : f(∙) = g(∙) and q : f(loop) = p⁻¹ · g(loop) · p and produces an identification of f and g. So the last paragraph explains which p and q to use so that this applies to ve(ev(f)) and f. — Reply to this email directly, view it on GitHub<#153 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AKO2SK4NMBMODWGWRULYJ2TV5M7EJANCNFSM6AAAAAAQH3DGZM>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[bidundas]

Hi, it turns out that many have a problem with meeting Thursday September 29. I propose we skip this meeting. Best, Bjorn

…

On Sep 22, 2022, at 16:13, Bjørn Ian Dundas ***@***.***> wrote: I have a problem finding a place I can talk that still has passable wifi (my office mate is unfortunately not gone yet) so don't wait for me and excuse me if I come and go. I only have some thought on some proofs to share today. Bjorn > On 9 Sep 2022, at 15:59, Ulrik Buchholtz ***@***.***> wrote: > >  > > The last paragraph uses the more general result from the previous paragraph that takes p : f(∙) = g(∙) and q : f(loop) = p⁻¹ · g(loop) · p and produces an identification of f and g. So the last paragraph explains which p and q to use so that this applies to ve(ev(f)) and f. > > — > Reply to this email directly, view it on GitHub, or unsubscribe. > You are receiving this because you are subscribed to this thread. >

[DanGrayson]

Sounds good to me.

[DanGrayson]

So, are we skipping tomorrow's meeting?

[bidundas]

Yes, I think so too. Bjorn On 28 Sep 2022, at 18:41, Daniel R. Grayson ***@***.***> wrote:  So, are we skipping tomorrow's meeting? — Reply to this email directly, view it on GitHub<#153 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AKO2SKZLXLZN7OM3M6AZIYDWARYMXANCNFSM6AAAAAAQH3DGZM>. You are receiving this because you commented.Message ID: ***@***.***>