UniMath
"merely"
After our discussion of \eq and \eqto, I think this make no sense at all:
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:
Maybe we should throw out the words purely and merely.
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: @.***>
Can you come up with any examples where adding "merely" to a sentence makes it more robust?
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.
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.
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.