Jacques Carette

So what do you think a `Quantity` *is*? I agree that a `QDefinition` pairs a 'quantity' with a 'defining formula'. The real question: is the 'defining formula' a mere annotation,...

> I think of 'QDefinition's as specific solutions to calculating a quantity. i.e., its nature is about calculation, not about defining a symbol. That a priori makes sense. Though I...

'5 apples' is a quantity (of apples); '(n+k+3) apples' represents a quantity of apples. One is immediate knowledge, one is future knowledge. That's not the only difference, but it's a...

Given how Drasil works, we *need* to define π *somewhere*. It should indeed be included in some kind of 'background theory' (a sort of `Prelude`) that we implicitly assume. Such...

We might want to have a "proto design" document that would (currently) be completely unstructured, but would at least display the extra knowledge that we need. Of course, we don't...

Attempting to verify an impossible requirement is... stupid. Verification is great. Unachievable requirements are bad.

This is also equivalent to the more general version using `Inverse`, no? If you're not going to pursue further, close?

A `Permutation` is a special case (for finite types) of a type isomorphism, i.e. the case for `Fin n`. The category (Nat, Permutation) is the skeleton of (FinSet, Isomorphism). (In...

> but did you mean rig-isomorphic ? I meant *naturally isomorphic as rig categories* (though I did omit 'in the presence of the axiom of choice').

Having said that: there are strong reasons for having *many* different representations of permutations in `stdlib`. They have their (powerful, disparate) pros and cons. Where it is not always clear...