agda-unimath icon indicating copy to clipboard operation
agda-unimath copied to clipboard

Published 20 hours ago • verified publisher icon UniMath

sequences large preorders/posets

Open malarbol opened this issue 7 months ago • 1 comments

We can discuss how much of https://github.com/UniMath/agda-unimath/pull/1388/ we want in large posets. I guess one of the main example would be sequences of real numbers so I'll try to keep that in mind. When we merge https://github.com/UniMath/agda-unimath/pull/1371/ I could work on arithmetic sequences of positive real numbers.

malarbol avatar Apr 07 '25 01:04 malarbol

Hey @fredrik-bakke. If you see anything reviewing #1388 that you think should be transposed here, feel free to make a list and I'll do my best to fill the blanks.

malarbol avatar Apr 12 '25 16:04 malarbol