UniMath
Theorem 3.1.2
There's one more issue with the proof -- the last paragraph introduces p and q again, but doesn't use them.
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.
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 GitHubhttps://github.com/UniMath/SymmetryBook/issues/153#issuecomment-1242011574, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SK4NMBMODWGWRULYJ2TV5M7EJANCNFSM6AAAAAAQH3DGZM. You are receiving this because you are subscribed to this thread.Message ID: @.***>
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.
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 GitHubhttps://github.com/UniMath/SymmetryBook/issues/153#issuecomment-1261172352, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SKZLXLZN7OM3M6AZIYDWARYMXANCNFSM6AAAAAAQH3DGZM. You are receiving this because you commented.Message ID: @.***>