WorldSEnder

I had a similar issue, although launching took only 6 seconds. HunterPie will report "Auto-Update is disabled. If your HunterPie has any issues or doesn't support the current game version,...

> ```shell > > sed -i "s|img src=.*/svgs|img src=\"/svgs|g" README.md > sed -i "s|\?invert\_in\_darkmode||g" README.md > # find all used svgs > svgs=$(cat README.md | grep -oP "/svgs.*.svg" | sed...

Also you probably don't want to do > ```shell > > git add . > ``` but instead ```shell git add svgs/ README.md ```

I have a very similar problem with my code [here](https://gist.github.com/WorldSEnder/4dc7dd1904db074dbf12be5ad1c30802). Not sure if related. Typechecking seems to go on forever when [the definition on line 298](https://gist.github.com/WorldSEnder/4dc7dd1904db074dbf12be5ad1c30802#file-sets-agda-L298) is given, when instead...

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 argument...

I found an alternative for my file, using no abstracts: On line [290](https://gist.github.com/WorldSEnder/4dc7dd1904db074dbf12be5ad1c30802#file-sets-agda-L290) giving an explicit argument to `Σ≡` also solves the problem: propFibers y (p₁ , m) (p₂ ,...

I came up with a smaller test file. It's not exhibiting the problem since I couldn't come up with a complicated enough term, but with `-v tc.meta.kill:10` the difference in...

Any updates on this?

In my rather naive eyes, the following should define an equivalence, but currently does not due to getting stuck. ``` module _ {ℓ ℓ'} {A : Set ℓ} {B :...

I, too, would appreciate this happening, see also #102