Jacques Carette

To me, the biggest advantage of `cast` over `subst` is that `cast` computes regardless of the actual proof of equality, while `subst` only reduces for `refl`. Working `--without-K` and with...

Seems to me that all of @conal 's questions have been answered, so that this could be closed?

You're likely to want to define R-module over a (commutative?) ring first. That's fully constructive. Vector Space over a Field is... hard.

> Have you been down that particular road before? Not this exact one, but close enough to know that this way lies much pain. > Oh, shoot! The new multiplicative...

It's easy enough to hand-code something, but that feels like cheating (and non-scalable). I do have a more level-polymorphic `RawFunctor`, but `RawApplicative` has resisted all my attempts at generalization.

I don't necessarily see the problem as `README.agda` not typechecking where it is, but being in the repo at all: it's a generated file. It's useful to generate the web...

Wouldn't it be even better to fix the positivity checker? Being able to go through layers of descriptions (shades of a current twitter conversation) is quite useful.

I'm all for this proposal too. One naming question though: `Equality` or `Equivalence` ? [Sorry to bring this up, but better to discuss it now rather than later. I mildly...

`Equivalence.Equality.Propositional`? `Equivalence.Propositional.Equality` ? Or even `Equivalence.PropositionalEquality`.

I don't think anyone has spoken against having a top-level `Order` (nor questioned its name). I don't think anyone has spoken against top-level "equality" hierarchy, just its name. My read...