Andreas Abel

Thanks for the proof of concept, @caryoscelus ! I do not see any obstacles to add a new flavor to the JS backend, given: 1. The old flavor still works...

@caryoscelus @qlonik Sorry for the delay in handling this issue. In the Agda core team we currently have no developer with a genuine interest in the JS backend. Would one...

Sorry for not getting back. Our last status was that we disagreed on whether to use `I -> Setoid` or `IndexedSetoid`, and on this fundamental issue there was no resolve,...

> using a coercion `c : Set i -> SSet i` sending `A |-> A` It seems like there shouldn't be an identity `Set -> SSet` because then I can...

Can you get absurdity from eliminating fibrant types to non-fibrant ones? If yes, such a proof of false would be nice to have here (but I understand too little of...

> So the easiest fix is to remove the subtyping `Set

> Maybe, the problem is the coercion map, because without it, the problem does not occur. Agda does not eliminate fibrant type unless the target type is also fibrant. I...

I don't have a good idea how to fix this, so I unassign myself. This bug happens in the combination of two experimental features, so it has a very low...

I tried to exploit a similar situation for `Prop True false`, but: ```agda Rohrkrepierer : ⊥ Rohrkrepierer = true≡false tt ``` ``` True _ !=< ⊥ when checking that the...

Thanks for reaching out, @phikal! Here is a few base points: 1. Support policy: We generally strive to support an Ubuntu LTS until its end of life. So we support...