Ayberk Tosun

@nad > How do you know that Agda does not terminate (given enough time and space)? I should have maybe said "Agda takes an unreasonable amount of time to typecheck"...

> I might be able to reduce the size of the test case to some extent, but I don't think it will be possible to reduce it substantially @nad I...

Tried converting things to postulates one by one, and it seems that the problem is fixed when all the lemmas defined in the where clause in the definition of `downwnard-subset-poset`...

I managed to solve the problem by marking `

> In my file, when I make [this definition](https://gist.github.com/WorldSEnder/4dc7dd1904db074dbf12be5ad1c30802#file-sets-agda-L297-L298) abstract, everything type checks "instantly". I believe this is connected to [`rigidVarsNotContainedIn`](https://github.com/agda/agda/blob/b1ecc72a0718de1173cd8b888b332ad94cef74fe/src/full/Agda/TypeChecking/MetaVars/Occurs.hs#L718) fully reducing a complicated term that appears as an...

I still experience this problem quite often by the way. It's usually hard to determine what needs to marked as `abstract` to circumvent it. Would anyone have any suggestions for...

@anuyts I almost always have this issue in the development I'm currently working on (that has got quite big). The only solution I've found is to use the `--experimental-lossy-unification` flag...

Use: `propext-funext-give-prop-ua`.

@UlrikBuchholtz thanks for the suggestions. > Which definition are you planning to use? Probably, some kind of Dedekind reals are a good start, but perhaps parametrized by an arbitrary σ-frame,...

I guess #116 is a dependency (operations on rationals).