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
397 stars 23 forks source link

"merely" #148

Open DanGrayson opened 2 years ago

DanGrayson commented 2 years ago

After our discussion of \eq and \eqto, I think this make no sense at all:

Screen Shot 2022-08-25 at 8 13 42 AM

How can we have a English adjectival phrase encoded by a type that is not a proposition? For example, to have an element involves existence of an element, and existence already involves propositional truncation. And here the usage of "merely" seems to be redundant:

Screen Shot 2022-08-25 at 8 17 46 AM

Maybe we should throw out the words purely and merely.

bidundas commented 2 years ago

That may be, but a certain redundancy makes natural language (as well as code) more robust, so it may still serve a purpose.

Bjorn

On 25 Aug 2022, at 14:18, Daniel R. Grayson @.***> wrote:



After our discussion of \eq and \eqto, I think this make no sense at all:

[Screen Shot 2022-08-25 at 8 13 42 AM]https://user-images.githubusercontent.com/700228/186661682-f44bb344-fea1-42b0-b903-b0fe5e5a00d9.png

How can we have a English adjectival phrase encoded by a type that is not a proposition? For example, to have an element involves existence of an element, and existence already involves propositional truncation. And here the usage of "merely" seems to be redundant:

[Screen Shot 2022-08-25 at 8 17 46 AM]https://user-images.githubusercontent.com/700228/186662323-e243975f-f59c-4a5b-90e4-7d2099c36810.png

Maybe we should throw out the words purely and merely.

— Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/148, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SK2AJ56HERP6JDQ34T3V25QBTANCNFSM57S4FCHQ. You are receiving this because you are subscribed to this thread.Message ID: @.***>

DanGrayson commented 2 years ago

Can you come up with any examples where adding "merely" to a sentence makes it more robust?

bidundas commented 2 years ago

I’m not sure if I follow your objection, but to me, if $A$ is a connected type, saying that ”any two terms in $A$ are merely equal” is fine (and true - The alternative is to evoke truncations explicitly, which gives a sentence I don’t want to write), whereas the sentence ”any two terms in $A$ are equal” is less robust and may (intentionally?) kill $A$ (if this is the intention I prefer to say so explicitly, but you never know what ideology you’re exposed to).

Bjorn

On Aug 25, 2022, at 14:41, Daniel R. Grayson @.***> wrote:

Can you come up with any examples where adding "merely" to a sentence makes it more robust?

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you commented.

bidundas commented 2 years ago

Ah, I found the problem. New computer and old zoom. I’m upgrading

On Aug 25, 2022, at 15:22, Bjørn Ian Dundas @.***> wrote:

I’m not sure if I follow your objection, but to me, if $A$ is a connected type, saying that ”any two terms in $A$ are merely equal” is fine (and true - The alternative is to evoke truncations explicitly, which gives a sentence I don’t want to write), whereas the sentence ”any two terms in $A$ are equal” is less robust and may (intentionally?) kill $A$ (if this is the intention I prefer to say so explicitly, but you never know what ideology you’re exposed to).

Bjorn

On Aug 25, 2022, at 14:41, Daniel R. Grayson @.***> wrote:

Can you come up with any examples where adding "merely" to a sentence makes it more robust?

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you commented.

DanGrayson commented 2 years ago

As agreed: I'll come up with a proposed definition of merely for next time, and remove the use of purely, which seems totally redundant.