To wrap or not to wrap

[UlrikBuchholtz]

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.

[marcbezem]

Do I understand the idea of the wrapper correctly as to replace the constructor (,) of the (now) Σ-type Group by the single constructor

wrapper: Π(X:U) Π(x:X) isConn(X) -> isSet(x=x) -> Group

of a (new) inductive type Group?

On second thought, @UlrikBuchholtz means probably to have as the domain of the wrapper the current Σ-type Group.

[DanGrayson]

Ulrik, your suggestion is interesting and worth considering. But this idea of a 'wrapper', while almost transparent to us, might be a hurdle to students, especially since such things have not been encountered before. I wonder how we might encounter it earlier.

What about with propositions? In the book we say that a type is called a proposition if it satisfies a certain property. If we consider the type of all propositions, then its elements are not propositions, which is counterintuitive. (An element of the type of propositions is a pair consisting of a proposition and the proof that it is a proposition.) There are two alternatives: define a proposition to be a pair (X,p) where X is a type and p is a proof that X has at most one element; define a proposition to be an element of a new inductive wrapper type with one constructor X ↦ p ↦ P. It may be worth considering the analogy in this discussion.

What we do with "proposition" we also do with "set", "being connected", and "being a groupoid". A connected type is a type, not a tuple. Here is the definition of "connected" so you can verify what I say:

So now look at our definition of group:

The first sentence says that a group G is a pointed connected groupoid. In light of our convention about "groupoid" and "connected", the proofs of the properties are not incorporated into G, and G should be a pair. The second sentence, however, says that G is a tuple (A,a,p,q). So already we make a mistake.

This discussion of "wrappers" may lead to an improvement at that earliest point, for we would start writing G = group(A,a,p,q) instead, and that first sentence of the definition would go away.

I wonder whether the notion of wrapper should be applied earlier and more often.

I also wonder how the notion of "wrapper" can be explained as a mathematical notion to students, as it doesn't look like mathematics -- it looks like syntax, added gratuitously.

Here's another possible problem: suppose you want to prove something about the type of groups. The first step of the proof is likely to be invocation of the equivalence of the type of groups with the corresponding iterated Σ-type, so you can make use of previous lemmas about Σ-types.

[UlrikBuchholtz]

On second thought, @UlrikBuchholtz means probably to have as the domain of the wrapper the current Σ-type Group.

Yes. Certainly, a pointed type should be a single component of the argument. Whether the proofs of connectivity and truncatedness are then Sigma-packaged or curried, I don't think matters that much.

Ulrik, your suggestion is interesting and worth considering. But this idea of a 'wrapper', while almost transparent to us, might be a hurdle to students, especially since such things have not been encountered before. I wonder how we might encounter it earlier.

Here are two analogous situations (not perfectly parallel, though):

1. Negative numbers. Suppose we start with a type of positive numbers, Pos. Then we want to have negative numbers, too. So we introduce a new type Neg. But negative numbers are in one-to-one correspondence with positive ones, so we could have Neg = Pos, definitionally. But that's not what we do: We introduce a wrapper, unary -, a say a negative number is something of the form -p with p a positive number.
2. Polynomials. Polynomials are just lists of coefficients (over a given base ring R). So we could define Poly(R) = List(R) definitionally. Again, we don't do that, because it's then not clear for instance whether the constant term is the first or last element. So when we consider a list as a polynomial, we write it differently, to help us use it properly.

(In case 2 there is an analogy to the (underline) Omega notation, in case R has finite characteristic: A polynomial looks like a polynomial function, but going from a polynomial to a polynomial function loses information in that case.)

What about with propositions? [...] It may be worth considering the analogy in this discussion.

Actually, I think the issue of dropping or adding a propositional component is not a good analogy for this, because we usually don't want to clutter notation with this. (I think) we're perfectly happy to informally have P : Prop be both the pair and the coersion to P : Type, and if BG is a pointed type which we happen to know is a connected groupoid, then also write BG when a pointed connected groupoid is expected.

Here's another possible problem: suppose you want to prove something about the type of groups. The first step of the proof is likely to be invocation of the equivalence of the type of groups with the corresponding iterated Σ-type, so you can make use of previous lemmas about Σ-types.

That's right, but this is worth it in my opinion.

[marcbezem]

Why can't we achieve this with some more flexibility in the name of the constructor of a Σ-type? A wrapper inductive type with one constructor with the Σ-type as domain seems too complicated. Sometimes one sees AxB inductively defined with a constructor pair: A -> B -> AxB, and (pair a b) then denoted as (a,b). By our convention, and that of the HoTT book, to stick to uncurried notation, one would also have the notation pair(a,b), which is not meant to wrap (a,b).

I have nothing at all against a Σ-type with a constructor called "group". We could denote such a Σ-type by "groupΣ". We need convenient conventions in place for tuples (we need those anyway, since we are using them; it's on my list for Chapter 2). We should also be allowed to use tuples of variables to quantify over Σ-types (with/out fancy constructor names). E.g., U := Σ{X:U} X (no fancy constructor name, but see below), GROUP := groupΣ{(X,x):U} isConn(X) & isSet(x=x) (fancy constructor name). Elements of type GROUP would read group((X,x),(p,q)), or group(X,x,p,q) if you wish. We need conventions to disambiguate projections.

This is flexible: let's say we want the first projection to return the classifying type. Then: CLT := cltΣ{X:U} X (now with fancy constructor name), GROUP := groupΣ{clt(X,x):CLT} isConn(X) & isSet(x=x). Elements of type GROUP would now read group(clt(X,x),(p,q)), or group(clt(X,x),p,q) if you wish.

In proving something about the type of groups one would not have to invoke a "wrapper equivalence" first, one would just invoke the lemmas about "xyzΣ" types, that are the same as those of Σ-types. So I'm not convinced we need wrappers.

[UlrikBuchholtz]

Why can't we achieve this with some more flexibility in the name of the constructor of a Σ-type? A wrapper inductive type with one constructor with the Σ-type as domain seems too complicated.

Personally, I don't see much difference (but see below), so I'm open to this, if you convince me it's really simpler.

I have nothing at all against a Σ-type with a constructor called "group". We could denote such a Σ-type by "groupΣ".

Now this seems more complicated than what I was suggesting, because there we don't need arbitrary parameters in the Σ-type for Group.

We need convenient conventions in place for tuples (we need those anyway, since we are using them; it's on my list for Chapter 2). We should also be allowed to use tuples of variables to quantify over Σ-types (with/out fancy constructor names). E.g., U := Σ{X:U} X (no fancy constructor name, but see below), GROUP := groupΣ{(X,x):U} isConn(X) & isSet(x=x) (fancy constructor name).

Do I understand you correctly, that the difference is between the inductive types:

1. (no parameters), constructor group : prod_{(X,x):U*} -> isConn(X) -> isSet(x=x) -> Group
2. (parameters A:U, B:A->U), constructor group : prod_{a:A} B(a) -> GroupΣ(A,B)

Is it just me, or is 1 not simpler? Also, with 2, we have many other GroupΣ that have nothing to do with groups. This seems to me like unnecessary clutter.

(NB 1 is a special case of a ternary Σ-type)

BTW. I realize my polynomial example is not quite right (we need to quotient by zero-extension), but I hope the analogy is still enlightening.

[marcbezem]

Not sure we understand each other. I mean:

Σ(a:A) B(a) is the inductive type with constructor (,): Π(a:A) B(a) -> Σ_(a:A) B(a)

fooΣ(a:A) B(a) is the inductive type with constructor foo: Π(a:A) B(a) -> fooΣ_(a:A) B(a)

This idea we apply in creative ways to achieve what you do with a wrapper (if I understand that correctly).

[UlrikBuchholtz]

I think I understood you, but I'm suggesting to simplify matters by specializing the parameters of fooΣ to avoid clutter.

This idea we apply in creative ways to achieve what you do with a wrapper (if I understand that correctly).

This is actually then more or less exactly my idea of the wrapper. (Every Σ-type is in fact a wrapper, if you like, but I'm indeed requesting that we special-case this one for pedagogical/notational/expository/type-checking reasons.)

[marcbezem]

That my whole point, Σ-types are wrappers and we should not need an extra wrapper around them!

[UlrikBuchholtz]

That my whole point, Σ-types are wrappers and we should not need an extra wrapper around them!

OK, then you're OK with having Group be a special-purpose Σ-type. That does achieve what I wanted for Group, which was to notationally (and type-checkingly) distinguish groups from pointed connected types, so I'll be happy with that, as long as we can keep the usual convention of eliding propositional arguments when convenient, i.e., at some point we can write mkGroup X for short, instead of mkGroup(X,p,q), or whatever we end up calling the constructor, for a pointed type X.

One concern I have (albeit minor) is about separation of concerns: We already have Σ-types for tupling several components, so there's really no need to repurpose them for this other purpose, and for exposition, it might be useful to have a short section anyway about inductive types T whose only constructor is mkT : A -> T. We could say once and for all that mkT and its inverse are inverse in a strong sense (up to definitional equality), so transporting results and constructions from A to T is particularly transparent.

Also, in the case of Hom, I'd slightly prefer to have mkHom : (BG -> BH) -> Hom(G,H) rather than mkHom : prod_(Bf : BG -> BG) (pt = Bf pt) -> Hom(G,H). (Or worse, mkHom : (BG -> BH) -> True -> Hom(G,H), in order for it to be a special Σ-type.)

But these concerns are indeed quite minor, so if you much prefer to avoid inductive types of the above form, I think we can manage with the special-purpose Σ-types.

[DanGrayson]

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.

[UlrikBuchholtz]

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.

Hm, if X : Type satisfies the property of being a proposition, then there is p : isProp(X), so (X,p) : Prop, so the first projection fst(X,p) is back to X : Type (so the second of the above). Or did you want to say that X can be a proposition even when we don't have p : isProp(X), e.g., perhaps something like X = True + "The Riemann Hypothesis", and that's the difference?

BTW, coming back to your:

There are two alternatives: define a proposition to be a pair (X,p) where X is a type and p is a proof that X has at most one element; define a proposition to be an element of a new inductive wrapper type with one constructor X ↦ p ↦ P. It may be worth considering the analogy in this discussion.

Maybe I didn't understand your suggestion (where does P come from in your example?).

Is the suggestion that we have a constructor for subtypes (as in Def. 2.11.1) where the constructor takes two arguments t : T and p : P(t), but we write this constructor application simply as t : T_P to conform with informal practice? So if pressed, we can say, “Really, it's not just a t you see there left of the colon, there's actually an invisible constructor symbol and a p we've left implicit, that's how we end up in T_P”. I kinda like that! (Conversely, if t : T_P, then we also have t : T, using fst as a coercion.)

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.

Oh right, that's true if you use inductive. (Coq has Record for this case which gives the eta rule.) We probably don't actually need this, however. (But if we do, it's a quite harmless assumption in this case.)

[pierrecagne]

Just to be a little nitpicking on Dan's remark about connected types, or propositions and the like. In the beginning of section 2.10, we are making clear than the English language is used constructively: in particular, if we say "A is a type such that P holds" where P is a proposition, it means A together with an element of P (we just don't name this element as we will never need definitional equality for it, and propositionally it only matters that it exists).

Hence, for me, a proposition is indeed a type P together with an element of isProp(P). A connected type is indeed a type A together with an element of (trunc A) and (x,y:A)->trunc(x=y).

Did I misunderstood something about our convention with the English language?

[DanGrayson]

Re: "(I think) we're perfectly happy to informally have P : Prop be both the pair and the coercion to P : Type" Currently, a proposition is neither of those things -- currently it's a type that satisfies a property.

Hm, if X : Type satisfies the property of being a proposition, then there is p : isProp(X), so (X,p) : Prop, so the first projection fst(X,p) is back to X : Type (so the second of the above). Or did you want to say that X can be a proposition even when we don't have p : isProp(X), e.g., perhaps something like X = True + "The Riemann Hypothesis", and that's the difference?

I wasn't clear. Currently the pair (P,p) is not mentioned at all when we define "proposition". Here's the definition:

Actually, that definition is inadequate, because it refers to "such a type" at a time when we haven't yet posited that P has the property.

Calling both P and (P,p) propositions might lead to confusion, for then later, when we say "let P be a proposition", it won't be clear what we mean.

BTW, coming back to your:

There are two alternatives: define a proposition to be a pair (X,p) where X is a type and p is a proof that X has at most one element; define a proposition to be an element of a new inductive wrapper type with one constructor X ↦ p ↦ P. It may be worth considering the analogy in this discussion.

Maybe I didn't understand your suggestion (where does P come from in your example?).

Here P is the value returned by the constructor, to be thought of as (X,p).

Is the suggestion that we have a constructor for subtypes (as in Def. 2.11.1) where the constructor takes two arguments t : T and p : P(t), but we write this constructor application simply as t : T_P to conform with informal practice? So if pressed, we can say, “Really, it's not just a t you see there left of the colon, there's actually an invisible constructor symbol and a p we've left implicit, that's how we end up in T_P”. I kinda like that! (Conversely, if t : T_P, then we also have t : T, using fst as a coercion.)

Nope, I wasn't thinking along those lines.

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.

Oh right, that's true if you use inductive. (Coq has Record for this case which gives the eta rule.) We probably don't actually need this, however. (But if we do, it's a quite harmless assumption in this case.)

Ah, yes, Coq has the eta rule for records, but only if you turn it on with Set Primitive Projections. UniMath does that, by the way. So, yes, we could introduce the eta rule in this context, and it would be innocent.

[DanGrayson]

I have fixed the definition of "proposition" in commit d8601032f5e624d6a115b33e7d3dad4724ee5206. Here it is now:

[DanGrayson]

Just to be a little nitpicking on Dan's remark about connected types, or propositions and the like. In the beginning of section 2.10, we are making clear than the English language is used constructively: in particular, if we say "A is a type such that P holds" where P is a proposition, it means A together with an element of P (we just don't name this element as we will never need definitional equality for it, and propositionally it only matters that it exists).

Hence, for me, a proposition is indeed a type P together with an element of isProp(P). A connected type is indeed a type A together with an element of (trunc A) and (x,y:A)->trunc(x=y).

Did I misunderstood something about our convention with the English language?

Could you show me where in the text we adopt that convention?

Actually, I can't understand from what you say about it, what the convention actually is. Could you clarify?

[pierrecagne]

I understand from that excerpt that if I say "a type A satifsying P", it means the pair of A and the non-named element of P. And the definition of the types Set and Prop seems to validate that:

So as for now a proposition is actually defined as a pair (that we coerce silently to its first projection when needed). Same goes for the other subtypes.

[DanGrayson]

The first excerpt you showed us does not use the word "pair", so it's not possible to infer that it has anything to do with pairs.

The second excerpt seems incorreclty phrased, because a type that is a proposition is not a pair, either.

[pierrecagne]

But isn't just an effect of the language that we can even "define" something in between the full pair and the bare type? In fully formal type theory, "a widget is defined as a guizmo A such that there is an inhabitant of P" is just an English sentence for the definition of the type of widgets as sum_{A:guizmo}P.

But this is a side debate and one can just be clearer in the introduction of propositions to make explicit that a proposition is a pair (with silent coercion introduced immediately after). It doesn't solve the issue raised by Ulrik and I think your remark holds indeed (the one that call for a wrapper for propositions if we need one for groups).

[UlrikBuchholtz]

But this is a side debate and one can just be clearer in the introduction of propositions to make explicit that a proposition is a pair (with silent coercion introduced immediately after). It doesn't solve the issue raised by Ulrik and I think your remark holds indeed (the one that call for a wrapper for propositions if we need one for groups).

I still don't understand the need for a wrapper for propositions, can you explain that again?

Maybe it helps if I try to sum up where we are with respect to subtypes (& propositions) and groups (and mutatis mutandis, homomorphisms), as I see it, in terms of three tenable positions:

1. For a type T with P : T -> Prop, defining the subtype T_P, we can very carefully distinguish between elements t : T such that P(t) holds via some p : P(t), and pair (t,p) : T_P. We maintain a distinction between groups G = (A,a,p,q) and their classifying types BG = (A,a), which happen to be connected (q) and truncated (p).

2. For the subtype T_P, we move without much further ado between t : T with p : P(t) and the pair (t,p) : T_P. For instance, we may (somewhat abusively) write t : T_P, if the situation calls for it.

   a. A group is a pointed, connected groupoid, period. To avoid confusion, we remove all mentions of classifying types, since otherwise G = BG, which is a mess. The integers as a group is the circle, period.

   b. We maintain a distinction between G and BG by saying that a group is anything of the form Ω BG, where BG is a pointed, connected groupoid. The type of groups is by definition the Ω-wrapped copy of the type of pointed, connected groupoids. The integers as a group is Ω S^1 (the group given by the circle).

I think frankly that 1 is only barely tenable, though it's mostly where we are now. I find it hard to write prose for, and difficult to read (but proof assistants love it!). (E.g., I wasn't even careful enough above: A subtype of T is determined not by P : T -> Prop, but by P : T -> U such that we have on the side some q : prod_(t:T) isProp(P(t)) – did you catch that on the first reading?)

I think 2.a is interesting and tenable, but veers quite a bit from standard practice. My vote is for 2.b. (I'm actually quite excited about it, and I hope to convince you all that this is the way.)

[pierrecagne]

I still don't understand the need for a wrapper for propositions, can you explain that again?

Probably best if Dan answers himself so that I don't speculate on what he meant to begin with.

I think frankly that 1 is only barely tenable, though it's mostly where we are now. I find it hard to write prose for, and difficult to read (but proof assistants love it!). (E.g., I wasn't even careful enough above: A subtype of T is determined not by P : T -> Prop, but by P : T -> U such that we have on the side some q : prod_(t:T) isProp(P(t)) – did you catch that on the first reading?)

I think 2.a is tenable, but veers quite a bit from standard practice. My vote is for 2.b. (I'm actually quite excited about it, and I hope to convince you all that this is the way.)

I agree that 1 is not tenable all the way through. Although I think it is pedagogically a good idea to start with 1 and gradually shift to 2. This is what is done about proposition, equivalences, etc. in the book, or even for univalence (the first few sections after introduction of the concept, one must take care of the reader and take all the steps with him/her, but after some time he/she must be able to jump transparently from a path p between types to an equivalence and then to the underlying function in order to evaluate p at a point for example). I think 2a is not really a problem: we adopt this convention with propositions as you said, yet we refrain to write confusing stuff like P=fst(P) even if it would make sense with the use of the coercion. Maybe a rule of thumb if to use coercion "linearly": if a group G is coerced to its underlying pointed type in an expression, then every occurrences of G in that expression is coerced. (Then stuff like G=BG does not make sense anymore.)

I also agree that 2b is a good option, but I think it would be confusing, at least at first. As a student your first question is: "wait it seems like underline omega is a one-to-one correspondence between pointed connected groupoids and what they call groups... what's the point?". The concept of a wrapper as definition is usually confusing. You wouldn't imagine the number of question we find on math.stackexchange about "how is the morphism f^{op} constructed in the opposite category?" for example. By the way, don't we already have the wrapper a posteriori in some way: given a pointed connected groupoid (A,a), the group is referred as AutA(a), never as (A,a) directly. Example 4.1.9 is careful to define the integers as Aut{S^1}(\base) and not as (S^1,\base), etc.

I think it kind of match your example about polynomials in a way. (Sorry for the ramble, I'm thinking as I'm writing.) If I recall my first bachelor class on algebra, polynomials have been defined as eventually null sequences of elements of a ring, and immediately after the notation with X is introduced. There is an immediate connection that the students make with the functions they are manipulating from high-school and before. So polynomials were not introduced through a wrapper but as a synonym for something else, that is denoted in a specific manner to be sure not to confuse them with the original object they are synonym with (at least for me, but France higher education in mathematics is very bourbakian so it might be that also... I mean, the concept of a matrix is usually introduced after the concept of a fully abstract vector space and linear morphism between them and I probably learn about kernel decomposition theorem before I saw any matrix reduction in action). I see the group stuff in the book the same way, with Aut replacing the X-notation.

So to sum up: I agree that stuff as G=BG should not appear, I agree that a wrapper is a good and necessary idea but I would introduce it a posteriori, I also agree that defining groups through a wrapper is completely tenable and is probably technically better but also would be confusing for readers that have no background in type theory (or more generally in foundational stuff).

[DanGrayson]

But isn't just an effect of the language that we can even "define" something in between the full pair and the bare type? In fully formal type theory, "a widget is defined as a guizmo A such that there is an inhabitant of P" is just an English sentence for the definition of the type of widgets as sum_{A:guizmo}P.

No, I don't think so. If you want to say that something is a pair, you should say it.

[DanGrayson]

I still don't understand the need for a wrapper for propositions, can you explain that again?

Probably best if Dan answers himself so that I don't speculate on what he meant to begin with.

I'm pretty sure I never said we need to have wrappers for propositions, but was just drawing a comparison with that case and considering the possibility as a topic of discussion.

[marcbezem]

I'm catching up with this (very interesting) discussion, and here is a comment to an older comment by @DanGrayson, which comments on even older posts of mine.

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

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

In the book we can simply say: analogously if the constructor of the Σ-type has another name. Similarly for wrapper types.

In Coq, it would be unpleasant to have to redo all lemmas for each reincarnation of a Σ-type. The same would be true for all reincarnations of a wrapper type (but they are fewer/simpler). We have no such thing as "constructor polymorphism" (imperfect metaphor).

BUT: perhaps the simplest of all syntax hacks could be used in Coq (not in the book!). Just add a syntax rule saying that "group" is a synonym of "pair", or whatever the official name of the constructor of a Σ-type in Coq may be. (If I remember well, (,) is also just syntactic sugar). Continue to use the Σ-type as officially defined, and denote its elements by group(X,x,p,q). No new lemmas required! If this works, it can of course also be used for wrappers.

[DanGrayson]

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

If our wrapper has just one argument, which is a tuple then my comment above doesn't apply. In the comment I was thinking of having the wrapper be another inductive type that mimics the Sigma-type, and having to prove things about it. In the case of a one-argument one-constructor wrapper, it we can deduce that the wrap and unwrap operations are inverse equivalences by citing a theorem we already cite.

[DanGrayson]

I'm convinced by Ulrik that 2b is the way to go.

[marcbezem]

Let me elaborate a bit. BTW @UlrikBuchholtz dropped groupoid in 2b, writing type instead.

2b1. Ω : (Σ_Xxpq) -> GROUP, inductively. Let's call the inverse B. For G,H: GROUP, I guess you would like to have, for any G,H: GROUP, Ω _GH : (BG->*BH) -> Hom(G,H), inductively.

2b2. group : Π_Xxpq GROUP, inductively. Define B(group(Xxpq))=(X,x): U. I would probably like, for any G,H: GROUP, hom_GH : (BG->BH) -> Hom(G,H), inductively (wrapper, not Σ-type).

How do they compare? 2b1 is more systematic, and exposes Ω as a functor. 2b2 has slimmer BG,BH, cleaned from redundant p,q.

Any comments?

[DanGrayson]

I think what I said before reveals that I prefer 2b1 to 2b2: "If our wrapper has just one argument, which is a tuple then my comment above doesn't apply. In the comment I was thinking of having the wrapper be another inductive type that mimics the Sigma-type, and having to prove things about it. In the case of a one-argument one-constructor wrapper, it we can deduce that the wrap and unwrap operations are inverse equivalences by citing a theorem we already cite."

[UlrikBuchholtz]

Although I think it is pedagogically a good idea to start with 1 and gradually shift to 2.

Agreed. As you said, we already do that in Chapter 2.

I think 2a is not really a problem: we adopt this convention with propositions as you said, yet we refrain to write confusing stuff like P=fst(P) even if it would make sense with the use of the coercion.

Maybe it's just me, but I don't particularly mind P=fst(P), because in my mind I insert a coercion on the left, because it's clear the identity type in question must be that of U. On the other hand, I don't want G=BG to type-check even after applying coercions.

Maybe a rule of thumb if to use coercion "linearly": if a group G is coerced to its underlying pointed type in an expression, then every occurrences of G in that expression is coerced.

I think this would be very confusing.

I also agree that 2b is a good option, but I think it would be confusing, at least at first. As a student your first question is: "wait it seems like underline omega is a one-to-one correspondence between pointed connected groupoids and what they call groups... what's the point?".

I agree it'll take some expository finesse, which I'll be happy to try my hand at. I propose to bring in the positive/negative numbers example. Yes, negative numbers are in one-to-one correspondence with positive numbers, but we write them wrapped with a minus sign, which tells us how they are used, and helps us make sense of contexts where both are used together. (Unless anyone can think of a better example.)

The concept of a wrapper as definition is usually confusing. You wouldn't imagine the number of question we find on math.stackexchange about "how is the morphism f^{op} constructed in the opposite category?" for example.

Interesting. I still think not having the wrapper is more confusing, but this point does emphasize the need for good exposition overall.

By the way, don't we already have the wrapper a posteriori in some way: given a pointed connected groupoid (A,a), the group is referred as Aut_A(a), never as (A,a) directly.

Sure, and this is pretty good, but there are two issues: (1) AutA(a) is currently definitionally equal to Ω(A,a) when A is connected and to Ω(A(a),a) otherwise, cf. Rem. 4.1.8. (2) More importantly, it doesn't solve the type-checking problem.

I think it would be a better idea to introduce Aut_A(a) as a notation for Ω(A,a), when A is connected, so that we can define Aut_A(a) uniformly. This also gives us parallel notations for the cases where the point is specified separately and where we have a pointed type.

BTW @UlrikBuchholtz dropped groupoid in 2b, writing type instead.

Thanks for catching that error: I fixed my comment above.

How do they compare? (2b1 and 2b2)

For technical and expository reasons, I agree with Dan that 2b1 is better.

[pierrecagne]

Maybe it's just me, but I don't particularly mind P=fst(P), because in my mind I insert a coercion on the left, because it's clear the identity type in question must be that of U. On the other hand, I don't want G=BG to type-check even after applying coercions.

So what is bothering you is not the implicit coercion of a pointed connected groupoid to its underlying pointed type. Your quarrel is about the fact that a group could be thought directly as a pointed connected groupoid? Then why is not bothering to think of a proposition as directly a type? I am willing to get on board, but I don't see how it is morally wrong to take a group directly as a pointed connected groupoid, but in the same time ok to take a proposition directly as a type.

Maybe a rule of thumb if to use coercion "linearly": if a group G is coerced to its underlying pointed type in an expression, then every occurrences of G in that expression is coerced.

I think this would be very confusing.

I meant an informal rule for us writer, not something to write as an explicit rule in the book. I'm almost sure anyway that we already apply this principle without thinking about it most of the time with other subtypes.

I agree it'll take some expository finesse, which I'll be happy to try my hand at. I propose to bring in the positive/negative numbers example. Yes, negative numbers are in one-to-one correspondence with positive numbers, but we write them wrapped with a minus sign, which tells us how they are used, and helps us make sense of contexts where both are used together. (Unless anyone can think of a better example.)

I can't think of a better example for now but I'll keep that in mind.

Sure, and this is pretty good, but there are two issues: (1) AutA(a) is currently definitionally equal to Ω(A,a) when A is connected and to Ω(A(a),a) otherwise, cf. Rem. 4.1.8. (2) More importantly, it doesn't solve the type-checking problem.

The first point is solved by always defining Aut_A(a) as the group induced by the connected component of a, as we never use the definitional equality if I'm not mistaken. The second point is clearly related to the beginning of the post.

(By the way, I have nothing against Omega instead of Aut (underlined or not), but I thought we were to avoid notations that collide with the homotopical interpretation of HoTT to keep "clear" of the topological realm at least for the first 4/5 chapters.)

[DanGrayson]

I like the negative numbers idea as a way of introducing wrappers, Ulrik. I bet it will work.

By the way, it occurs to me that if we had wrappers around the positive numbers introduced in ZFC, then that would solve some problems, too, because then irrelevant statements such as 2 ∈ 3 would not be true.

Also by the way, one might imagine have two sorts of wrappers, so that -2 and +2 are integers and 2 is still a natural number. Why not do that, too?

Pierre, there is a big difference between coercing proposition pairs to proposition types and coercing groups to pointed types that makes the former a convenience and the latter simply confusing to the student. As Ulrik has observed right at the start, we don't want to think of ℤ as a circle. One reason is that the circle, in topology, is a topological group in its own right!

Rather, we want to think of ℤ as the circle, together with an announced intention that we are poised to consider the binary operation that is composition of loops from the base point to the base point.

Think of the operation of direct sum of a family of abelian groups. The important part of that operation is what it does to the fundamental groups of the pointed types in the family, not what it does to the types themselves, which may be rather mysterious.

With a proposition type P, the intention we announce when we pair it with a proof p that it is a proposition, is that we are poised to remember that any two elements of P are equal, but as far as the intended use goes, it is the same : assertion of (P,p) amounts to assertion of P, disjunction of (P,p) and (P',p') amounts to disjunction of P and P', and so on. Of course, new proofs have to be manufactured for the results of logical operations, but they just go along for the ride in an obvious way.

The motto could be that a wrapper is a way of divorcing an object from its intended uses to make it more convenient to attach new uses. The same can be said for negative numbers: -2 × 3 is different from 2 × 3. The minus sign serves to divorce -2 from 2 for the purpose of multiplying it in a different way.

I prefer Omega to Aut.

[pierrecagne]

I think I understand a little better your point of view. You actually want to convey the idea that groups are fundamental groups of some types (and then I understand better the Omega choice), and that the paths are the relevant data.

I'll wait the first commit on that and see how it feels.

[marcbezem]

@DanGrayson could you pls elaborate on "we can deduce that the wrap and unwrap operations are inverse equivalences by citing a theorem we already cite."

[UlrikBuchholtz]

So what is bothering you is not the implicit coercion of a pointed connected groupoid to its underlying pointed type. Your quarrel is about the fact that a group could be thought directly as a pointed connected groupoid? Then why is not bothering to think of a proposition as directly a type? I am willing to get on board, but I don't see how it is morally wrong to take a group directly as a pointed connected groupoid, but in the same time ok to take a proposition directly as a type.

It's only a problem when connected with the established conventions and language, where we have a coercion from groups to sets given by the elements. Different conventions and modes of speech are possible, which is why I mentioned option 2.a. It's just quite ingrained to speak about “the integers” and mean variously both the set, the lift to the (additive) group structure, the lift to the ring structure, etc, which I take to mean that the projections Ring -> AbGroup -> Group -> Set are natural coercions.

(BTW I hope it was clear, via the reference to Eugenia's note, that the talk of morality is somewhat tongue-in-cheek. She gives, as one of her examples, “This notation does work, but morally, it's absurd!”)

@DanGrayson could you pls elaborate on "we can deduce that the wrap and unwrap operations are inverse equivalences by citing a theorem we already cite."

I think Dan meant the logical implication from bi-invertible map to contractible fibers from the HoTT book (Thm. 4.23 + 4.2.6).

[DanGrayson]

@DanGrayson could you pls elaborate on "we can deduce that the wrap and unwrap operations are inverse equivalences by citing a theorem we already cite."

This one:

[UlrikBuchholtz]

I've now updated the definitions of group, infinity-group, and homomorphism to reflect our decision. I've introduced macros for italicized variables BG, BH, Bf, Bi, etc., etc. The macro for the group constructor is \mkgroup, that of homomorphisms is \mkhom, but they print the same currently.

I'm going to stop updating these chapters (4–) for a while, so feel free to change the exposition, make further adaptations, etc.

[DanGrayson]

Here are some comments, as pdf file annotations:

book comments page 44 45.pdf book comments page 22.pdf book chap 4 comments.pdf

[DanGrayson]

Here is the definition of "Copy":

One disadvantage of it is that there is no way to make two different copies. For example, what if you want one copy of N for the negative integers and another copy of N for the positive integers? The intention would be for +3 to be a positive integer and for -3 to be a negative integer. So you copy N twice. But then the two copies are the same, and +3 is the same as -3. Too bad!

A possible solution: each time we copy a type, we do it again, by introducing a new inductive definition. That gives a different copy each time, and it also allows us to give the constructor and destructor a different name each time.

[UlrikBuchholtz]

One disadvantage of it is that there is no way to make two different copies. For example, what if you want one copy of N for the negative integers and another copy of N for the positive integers? The intention would be for +3 to be a positive integer and for -3 to be a negative integer. So you copy N twice. But then the two copies are the same, and +3 is the same as -3. Too bad!

A possible solution: each time we copy a type, we do it again, by introducing a new inductive definition. That gives a different copy each time, and it also allows us to give the constructor and destructor a different name each time.

I agree it's better that way. When I reorganize around Sec. 2.6, I'll write something to that effect.

[DanGrayson]

Okay, thanks.