... don't seem to work:

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.

Request: I need set coequalizer (p88 4.7)

I'll replace uses of the bulky pt_G = pt_G with U G, after the place where it's defined.

The diagrams made with tikz have ugly artifacts in them:

These changes may prompt comment: 6d042d1

In Ch. 3, after the introduction of LPO, there are two occurrences of "decidable":

(1) "decidable set map f: A->C" and (2) "g ... is injective and decidable".

It took me some time to see that they mean different things:
(1) each fiber of f is a set with decidable equality;
(2) each fiber of g is a decidable proposition.
With this understanding I could follow the ensuing argument.

The use under (2) is presently not defined. If you agree I can define it somewhere.

Marc

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.)

In this text:

the first statement is perfectly precise, so it's not possible for something to be more precise than it. Moreover, the second statement is a different statement, not a more precise version of the first one.

I think the second statement should be part of the proof, not part of the statement.

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 an element of A=B can be constructed (sic) without UA, then use A=B, otherwise use A \equiv B.

The reason is that we would like to avoid unnecessary use of UA, in particular as the last and only step in the construction (sic) of an element of type A=B.

It turned out that I needed a number of constructions related to subgroups for stating and proving the 2nd and 3rd Sylow theorems. Since the proofs will depend on the formulations it means that I have started to write this down even if that wasn't my plan. All of it things that obviously ought to be included somewhere, so that is some sense good.. Currently this is in section 4.11-4.13, but much of it will move elsewhere when finalized.

This means that:

1. if you need stuff like kernel, pullback, normal... please check whether it is there before starting to implement it anew
2. while the material is in flux (shaped and reshaped by how I get the best overall exposition), comments are very welcome

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 the type of subgroups, but using "being a monomorphism" as the property. If that particular form of the property (

) is needed somewhere, then we should add a fourth condition to this lemma:

Calling latexmk -pdf book yields

[10] [11]
! Undefined control sequence.
<recently read> \trp 
                     
l.136 $\trp
           (X,P,a,b,e)$. We often use less verbose phrases such as `by trans...

? 

I am happy about leaving the tilde on top of the H in G\ltimes H. It conforms with current practice where one remembers the action (often as a subscript on the \ltimes, but why not at the top of H?).

Remember to define the homomorphism H(pt_G)-> G\ltimes\tilde H (and show that it is the kernel)

Eventually, when the book is large, we'll want to be able to compile one chapter at a time.
See

https://www.overleaf.com/learn/latex/Multi-file_LaTeX_projects#The_subfiles_package

I'm a little dissatisfied with this discussion:

because, a priori, there may be multiple functions of type ( ∏ (x:X), ( f(x) = g(x) )) → f=g.

What if we introduce g:G as notation for g:pt=pt, when G is a group? We currently aren't using it.

Move the stuff about what a symmetry is from chapter 3 to 2.

Given a subgroup N which is a fixed point under the conjugation action on the type of subgroups of G, give a geometric and elegant construction of G->G/N (or rather, of BG->_*B(G/N)).

In particular without resorting to delooping the abstract quotient (ie, the classical algebraic proof).

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 would prefer to say "(path) induction on p". For me the induction "on b" is at best confusing,but actually incorrect, in particular if the type of b is an inductive type.

the first time "isSet" appears is on page 32 preceded by "We recall the following definitions." Can the one working in that chapter please make it into a definition (and label it \label{def:isSet})?

Perhaps I can rewrite this to use a path over instead of transport. If not, at least refer to the appropriate statement about paths between pairs.

I wonder whether to write a chapter on crystallographic groups. Here are some references:

https://www.jstor.org/stable/2974820
https://www.amazon.com/X-ray-Crystallography-Gregory-S-Girolami/dp/1891389777
https://en.wikipedia.org/wiki/Space_group

How I state later stuff depends on the implementation - I'm not asking for things to be implemented now, I just want to know how one intends to so that I can comply.

1 I need to refer to the normalizer. Ideally in a form reflecting that (classically speaking) if H is a subgroup of G, then the fixed points [G/H]^H is a group whose preimage in G is called N_G(H) (and of course that N_G(H)->[G/H]^H is a group homomorphism).

2. I also refer to Burnside's lemma, but the only thing I'll actually need is that if G is finite and X is a finite G-set, then X consists of the G-fixed points and the nontrivial orbits and that the cardinality of the latter divides the order of G.

Perhaps something like this notation will work:

We need a license for the new book! I propose CC-BY 4.0, which is very permissive.

https://creativecommons.org/licenses/by/4.0/

We should be consistent in calling types either of level at most n+2, or n-types.

The alternative notions of proposition, set and groupoid can be used, in addition to one other method of counting and phrasing.

We should reserve the phrase "nothing but" for judgmental equalities, not equivalences, as here:

In connection with working on the section on semidirect products, I'd like add some cases to these lemmas, if no one minds:

Replacing \cite by \autocite had a bad effect here:

@UlrikBuchholtz

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 normal subgroups would be drawn.

And quotient groups could have their own chapter, too, since subgroups do.

... is a problem:

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 things -- currently it's a type that satisfies a property.

Re: "A wrapper inductive type with one constructor with the Σ-type as domain seems too complicated."and "That my whole point, Σ-types are wrappers and we should not need an extra wrapper around them!"

That's simpler than the other way, because one doesn't have to discuss the properties of Σ-types twice.

Re: "The constructor and B form a pair of functions that are each others' inverse up to definitional equality."and "We could say once and for all that mkT and its inverse are inverse in a strong sense (up to definitional equality)"

This is not true in Coq -- there you need to examine cases to show that wrap (unwrap x) = x.

Originally posted by @DanGrayson in #45 (comment)

The word "subsymmetries" occurs just three times, here, without definition, in a discussion about it having arisen elsewhere, when it hasn't:

It needs to be rephrased.

@bidundas -- I think it's your text.

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 should add this terminology in 2.4.

Marc

At the point where we introduce the Peano axioms for the natural numbers, we should offer a comparison with Peano's original axioms, and tell the student to expect that these numbers are what they are used to (distinct, etc.).

Instead of this:

it would be better to define what a covering of B is. It's a type A, a map f:A->B, etc.

are you ok with letting labels be visible in the pdf-file while we are working on the text?

That way cross-referencing can be implemented much more efficiently (I find the thing I want to refer to in the pdf file, and presto!)

If the type below is not a proposition, perhaps it is not good to say that we "prove" it:

There is a gigantic section of group.tex that is commented out and appears to be duplicated in subgroup.tex. Can I delete it?

This notation will conflict with x+y:

We have this:

I was going to change the second phrase to "any symmetry is a symmetry of a set", since a symmetry of \Set would be a path from \Set to \Set in the next universe, but it's still not a good translation of the first phrase, which refers to a symmetry group, not to one symmetry in it.

Actually, the first phrase should really be "any group is a subgroup of a permutation group", so it's not clear what the corresponding phrase should be here. Maybe none.

At several places we have defined types in higher universes than necessary. For example, the definition of Fin in 2.16.4, where the sum type is taken over Set, where it could be taken over U. As it stands, Fin is in U_2, and so are all the Fin_n. To get these in U_1 there are two options:

1. Replace \sum_{X:Set} ... by \sum_{X:U} isSet(X) \times ... This works always, and has an analogue for \prod_{X:Set}.

2. Use Lemma 2.16.3. This only works if one has such a lemma.

I have no problem with implicitly using that X is a set if X: Fin, after a remark that we do so.
I think the extra universe level is not a good idea. In ZF Fin is a proper class, but not worse.
(Fin is not a set since if it were we would have Fin \in {Fin} \in Fin which contradicts foundation,
similarly for all Fin_n apart from Fin_0.)

I am in favor of economizing on universe levels whenever this is easy, with proper conventions to simplify terminology.

Introduce macros for going back and forth using univalence: p ↦ \tilde p and w ↦ \bar w and encourage their use

It seems we define the group Aut_A(a) only when A is a group and a is the basepoint, which is strange. It should be defined for any element a of any type A such that a=a is a set.

Then the last sentence here would not be needed:

It would also give a meaning to the right hand side here:

I find that the current conventions regarding groups and homomorphisms, while technically correct, are morally wrong. I know I promoted them initially, but they rely on a certain sophistication to be used correctly, which (undergraduate) readers may struggle with. I think the following proposal allows us to stay true to all the good aspects, while ameliorating some bad.

With our current Definition 4.1.5 (Group), it is technically correct to say that the group of integers is the circle. I think we are very careful not to do that, emphasizing that the (pointed) circle is the classifying type, but with the current definition, it's a bit awkward, and readers may be tempted to say and write things that are, while technically (according to the definition) correct, nevertheless morally wrong.

I therefore propose that we change the definitions of Group and Hom(G,H) to introduce a wrapper around the old definientia. According to the new definitions, these types are officially single-constructor inductive types (records). My preferred choice of constructor name would be (underlined Omega), but that's perhaps a separate issue.

This small change has several benefits:

1. The notation and technical implementation now matches better the existing prose, while preventing readers from leaping to wrong conclusions.
2. We can have a standing convention that if a variable G : Group is introduced, then we immediately do a case analysis and name the exposed variable BG. (Mutatis mutandis for H,K,etc.) This variable is then italicized (like all variables).
3. The inverse of the constructor is written upright B, but now it's not just a notational convention, but an actual operation. (The constructor and B form a pair of functions that are each others' inverse up to definitional equality.)
4. It is now a type-error (and not just very bad style), to write BG : Group, or, for Y a pointed simply-connected 2-type, Omega Y : Group. Instead, (underline Omega) BG : Group and (underline Omega) Omega Y : Group, which looks much more reasonable.

I think point 4 is important: A key benefit of type theory is exactly this kind of type-checking.

Finally, some remarks on the name (underlined Omega) for the constructor: We want to say that a group is a set of self-identifications/symmetries, hence something of the form Omega X for X a pointed connected groupoid, but Omega X itself doesn't remember the structure (identity and composition). Hence we introduce the formal expression (underline Omega) X : Group, which does remember everything, and the forgetful map Group -> Set simply maps (underline Omega) X to Omega X. (Forget the underline!) I think this is cute and suggestive, so it's my proposal. Another option is Aut, but it looks a bit weird, because we expect $\Aut_X(x)$ instead.

With Pierre we work on making the notations more systematic. The current proposal is as below,
followed by some examples. Please let us know what you think.

% Should these be sans serif, roman or italic?
% Rule (under discussion): constructors italic, defined elements roman, typeformers sf

\newcommand{\constructor}[1]{\mathit{#1}}
\newcommand{\function}[1]{\mathrm{#1}}
\newcommand{\typeformer}[1]{\mathsf{#1}}

% Typeformers

\newcommand{\bool}{\typeformer{Bool}}

% Constructors

\newcommand{\yes}{\constructor{yes}}
\newcommand{\no}{\constructor{no}}

% Functions and defined elements

\newcommand{\id}{\mathord{\function{id}}}
\newcommand{\pt}{\function{pt}}

We should avoid using variables as English words, as they can't be read. Here is an example:

Better than "on an A" would be "on an element of A".

Is there a definition of "Cayley diagram" in the literature that makes the last sentence of this paragraph true?

(This is about ZTors.tex.)