Amélia

Error message from #6017 w/ the current implementation: ``` ~ i₁ ∨ i₁ != (~ i₁ ∨ i₁) ∨ ~ i₂ ∨ i₂ of type I when checking the boundary...

Y'know I was expecting CI to fail on the previous commit but I wasn't expecting it to fail _so fast_

Putting this here as a note to myself: There's a recurring problem that I _really_ need to minimize, but line 278 in `ZCohomology/GroupStructure` always causes unsolved metas when the boundary...

@Mergifyio rebase

#5929 works also with `Sub` (slightly moot point since you get a warning about confluence checking not being implemented to work with `--cubical` yet, but...): ```agda postulate f : {X...

#5837 also happens for the "unit" type defined above: ``` postulate F : Set → “unit” G : “unit” → Set mutual X : Set X = _ solve :...

Part of #6049

Having a normal one with the force pushes, sorry! (It took me a couple tries to remember to do everything that needs to be done to add a test)

Thanks for the ping @ecavallo. This code will essentially be invalid with the changes I want to make to the interval type, and how it's handled in Agda. In particular,...

Whether or not they're in SSet doesn't matter: type checking will still be undecidable if you have non-interval-stuff in your interval. Strictly speaking the interval shouldn't even be a _type_,...