Jacques Carette
Jacques Carette
My instinct here is that design smells strongly of classical-math / set-theoretical thinking, and may not lead to improvements in MLTT.
Hoping that @TOTBWF will opine here - he's done more work on this than I have (Order, PER, etc).
I agree that more documentation would have been helpful. From what I can see from the code: 1. I really want this capability, 2. but not as a modification of...
> does the change-of-base construction give you what you want? Quite likely. But the devil's in the details for such things, thus my hedging.
On the 'what else', Yasmine Sharoda's [PhD Thesis](https://github.com/ysharoda/PhD-Thesis) has a nice list of things that are well-enough understood that our original plan was to generate them all. Eventually [our code](https://github.com/ysharoda/Deriving-Definitions)...
So I was going to reply, unhelpfully, that a textbook written in the classical style, even if by spectacular scholars, might not give quite the right definition -- mathematicians tend...
This reminds me that I really have to get the whole `Fam` v `Pow` approach sunk into my brain much more deeply. Right now, this requires active thinking, while it...
Also added to agenda for discussion, in case we don't manage to hash it out here.
I'm pretty sure Conor and I have code for this somewhere. A direct proof is horrible. There's a proof via symmetric difference and a worker helper that does a rather...
I had done Lehmer codes, up to (but not including) composition. I could never quite figure out `Split`. Scoured the internet, asked on forums - nothing. So: yay to Patrik!...