search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
378 stars 22 forks source link

Theorem 3.1.2 #153

Open DanGrayson opened 2 years ago

DanGrayson commented 2 years ago

Lots of rephrasing needed here.

DanGrayson commented 2 years ago

Ooops, thanks @benediktahrens .

DanGrayson commented 2 years ago

Commit a39baad16fcf4356b313bc485877ffb4b9ea2a1f addresses this.

DanGrayson commented 2 years ago

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

UlrikBuchholtz commented 2 years ago

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 commented 2 years ago

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: @.***>

bidundas commented 2 years ago

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 commented 2 years ago

Sounds good to me.

DanGrayson commented 2 years ago

So, are we skipping tomorrow's meeting?

bidundas commented 2 years ago

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: @.***>