Tesla Zhang‮

I think maybe in the future. Because we are changing language features all the time at this point, it's better to couple the library with the compiler. Once we have...

This requires putting cubical boundary conditions into the constraints... It's blocked by a meta so it's reasonable

Fixed by the new version. Why?

Feature write de good, next second is mine

> Is this fixed? We still do not have a `Prelude` module. It should be loaded upon availability, and not being loaded when the stdlib is missing.

@imkiva

Maybe need to be `isContr A → Fn (x y : A) → isContr (x ＝ y)`? The error has to be handled though.

@imkiva help 😭 Idk how to fix this in a good way

You don't need `\section`, you need `\label`.

> Is it possible to support multiple literate backends? We already do