SymmetryBook
SymmetryBook copied to clipboard
UniMath
This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
section?
Do you want to use the word "section" for an f : \prod_{x:A} B(x) ? We also have "family of elements" f(x) : B(x), for all x:A. If yes, we...
What about skipping the Galois group and introducing the Galois groupoid, instead? Is there any reason to artificially single out a particular splitting field?
I've now closed issue #45 as settled. This means we should now go through Ch. 4+5 and update the exposition where needed. (Dan already fixed a lot of the formulas.)
Re: _"(I think) we're perfectly happy to informally have P : Prop be both the pair and the coersion to P : Type"_ Currently, a proposition is neither of those...
Consider this: I propose to start more gently, with words, and to say that a subgroup of G is a monomorphism from a group to G. After that, to introduce...
Wouldn't it make sense for quotient groups to be defined in the way strictly dual to the way subgroups are defined? Here are the two definitions: Then the connection with...
Look at this: I think we need more coercions if we want the type `\bn n` to be regarded as an element of all three of those types.
Is there a definition of "Cayley diagram" in the literature that makes the last sentence of this paragraph true? (This is about ZTors.tex.)
Our E3 in 2.3 is based path induction, and this is fine. With p: a=b I see that E3 is sometimes referred to as "induction on b and p". I...
Dan, Peter, and Marc have been discussing when to use = and when to use \equiv between types. Here is our temporary conclusion: For any types A and B, if...