Apostolis / is on Nostr

Mathématichien

Last Notes

2024-11-30 13:18:59

- reply

@nprofile…y6g5 in the case where rules are picked out of order, any two rules can be non-deterministicly chosen, both forward and in reverse, if you change the elements in the bag 🛍️.
For example
A : _ _ -> 🦆
B : _ _ -> 🐔
With 🛍️:
🦆
This is réversible.
With 🛍️:
🦆 🐔
It is not réversible.
Thus, maybe reversibility should be regarded in context.
Maybe in the ordered case, things are simpler, I do not know.

2024-11-28 22:15:52

- reply

@nprofile…y6g5 if you ask someone if the sun 🌞 is yellow, and you receive no answer, would you assume that the sun is not yellow.
The semantics of multisets are about the existence or not of objects, but nothing is told about the meaning of the object itself.

2024-11-05 18:21:25

- reply

@npub1qu5…4evr Yea, I was thinking if the position was also part of the symbol. (you could have both types, both with position and not).
Let me see if you can pull this off, to have a picture move on top.

2024-11-05 18:18:28

- reply

@npub1qu5…4evr Not multiset anymore? Do they have specific positions?
I wonder if you can move a photo on top of the scrollbar.
You would have to introduce a token that represents "ANY" value.

2023-09-03 04:14:56

- reply

@npub1ez3…xnxl what about Higher inductive types?

2023-09-03 03:56:49

- reply

@npub1ez3…xnxl @npub1jd8…t4jc So which library written in Agda does that? I want to switch from Cubical to HoTT/UF while still being able to compile a program, when that will be possible in agda.

2023-09-03 03:56:49

- reply

@npub1ez3…xnxl @npub1jd8…t4jc So which library written in Agda does that? I want to switch from Cubical to HoTT/UF while still being able to compile a program, when that will be possible in agda.