Reorganising HITs

[Alizter]

So I know there was a discussion a while back #573, about moving some files out of HITs to other places. The way I see it, there are only a few "real" HITs that have to be specified with axioms. These should stay in HITs, the rest are defined in terms of these so they should be allowed to dwell anywhere, as some already do.

I propose moving files such as Suspension and Pushout into the Homotopy folder. I also propose moving files such as Fibrations and Pullbacks into this folder. Files such as coequalizers however should stay in HITs.

Files such as Spheres and Circle should be moved into the Spaces folder.

I am already splitting up Pointed into multiple files and giving it its own folder. This would be a natural place for future files such as Wedge and Smash to live in. I want to develop constructions with pointed types properly.

I am however unsure about moving Quotients and friends into a Set folder. Though it could be argued this is the correct thing to do. I don't want to spend time doing these things if its not what people want.

What do you think about this proposal?

[spitters]

That seems reasonable. Although I don't have a strong opinion on it.

There are a number of people building on the library, but not contributing to it. E.g. https://github.com/HoTT/HoTT/wiki/Publications-based-on-the-HoTT-library ( And others )

These kind of big changes might break their work. Arguably, that's their responsibility.

[Alizter]

@spitters Thanks for letting me know about those. I think creating a list of changes will help people when they wish to take into account these changes without them having to guess.

[mikeshulman]

That sort of thing seems like a reasonable start. I'm not sure about your proposed move of files into the Homotopy folder, though. I think of the Homotopy folder as being about actual synthetic homotopy theory, whereas the files you mention are really just defining much more basic constructions on types. Maybe they should be in a folder about "limits and colimits" or something.

[Alizter]

@mikeshulman I think I will move results about homotopy groups into folders containing the spaces in question. Spheres and circles will be moved to their own folders in spaces containing various results about them.

The Homotopy folder will contain general things like the hopf fibrations etc.

I am currently trying to finish off the 3x3 lemma, after which I have the real and complex hopf fibrations ready to go. (They are currently waiting for a proof of the associativity of join (which needs 3x3 or patience)). I have a semifinished version of the Quarternionic hopf fibration which shouldn't be too difficult to clean up.

After which I will try and spend some time proving the smash-pointed map adjunction so we can get some coherence results. This will lead to the development of homology and the Gysin sequence, eventually leading to Pi4S3.

Also once we can prove Freudenthal I have branches for Eilenberg-MacLane spaces and PinSn.

And perhaps after this I will try to generalize the definition of spectra past the connective case, and implement some of van Doorn's results.

[mikeshulman]

Let's please have a discussion and a consensus before moving things. While it seems at first reasonable to say that homotopy groups of some space are properties of that space, I think that at least more complicated calculations of, say, homotopy groups of spheres, are more naturally regarded as part of a wider circle of homotopy-theoretic ideas and results, rather than being specifically properties of the some random spaces called "spheres", so I would be inclined to put them in Homotopy as well.

In particular, it would be nice to minimize circular dependencies between folders so there's a clear progression of the order in which the library is compiled and in which it can be read: first Basics, then Types, etc. I recently encountered a problem of circular dependencies between the folders HIT and Modalities: HIT.Truncations requires Modalities.Modality and some other files in HIT require HIT.Truncations, whereas some files in Modalities want to use HITs (e.g. preserving pushouts, or using them to construct examples. I'm not sure what the best solution to this one is, but I'd rather not create a similar circular dependency between, say, Spaces and Homotopy. Let's think about it all together.

What do you mean by "generalize the definition of spectra past the connective case"? The current definition doesn't have to be connective.

[Alizter]

@mikeshulman I agree that a discussion must be had before moving things around. I am not planning to do this any time soon.

Currently spectra are only defined for naturals, I mean to define them for the integers. I have tried doing this in the past but I have found it tricky working with our version of Int since it is a bit underdeveloped currently. I had a lot of trouble defining truncated spectra if I remember correctly. Unless I am misunderstanding, having spectra only defined for the naturals makes them connective no? (Connective meaning no information for negative integers).

[mikeshulman]

No, the usual definition of spectra is over the naturals. The space X_0 has information in all positive dimensions already. Each positive shift in the spectrum indexing shifts the dimension lower, so X_{-1} has information in dimensions >= -1, then X_{-2} has information in dimensions >- -2, etc. Remind me what the purpose is of indexing on Int? I do seem to recall that maybe Floris found it more convenient for some reason, but it doesn't change the meaning of spectrum up to homotopy.

[Alizter]

@mikeshulman Looking through Floris's thesis I realise now why I was so confused when I read it. Floris found it more convenient when defining homotopy groups of specrtra since he didn't have to case match on lower dimensions.

All this time I was under the impression that our definition of spectra was inadequate to formalise spectral sequences.

Thank you for clearing up my legendary ignorance.

[mikeshulman]

No worries; guess you are one of today's lucky ten thousand! (Suitably scaled to the relevant definition of "everyone"... (-: )

[mikeshulman]

Generally I think Floris was quite good about finding convenient definitions for formalization, so if he found it easier to define spectra on the integers, maybe we should too.

Is his definition of Int the same as ours? I wonder whether it would be advantageous to use the definition of Int as the HIT freely generated by a point and an automorphism.

[mikeshulman]

BTW, if you mean "we should have a discussion about whether to do X", it would probably ruffle fewer feathers if you don't start off the discussion by saying "I think I will do X".

[Alizter]

@mikeshulman Shouldn't there be some sort of "Universal property of the integers", i.e. an ideal induction principle so that the exact definition doesn't matter. (Perhaps this is what mathclasses was trying to achieve?).

Regarding Floris' thesis, the integers are not defined. The definition in lean is the same as ours without the padding for zero.

I have been viewing the development of cubical agda where they have several definitions of the integers. Here is a new one (for me at least) that is particularly nice:

HIT Int
 | diff : Nat -> Nat -> Int
 | glue : diff a b = diff (S a) (S b)

You can define all the usual integer functions from this. It would be interesting to try all of these as agda/cubical have been doing.

And finally, point taken on ruffling feathers.

[mikeshulman]

I suspect that "the HIT freely generated by a point and an automorphism" gives a reasonable induction principle for the integers.

[Alizter]

@mikeshulman OK stupid question time. How exactly does the circle given an induction principle from its loop space?

[mikeshulman]

Sorry, I couldn't parse that question; can you rephrase it?

[Alizter]

@mikeshulman You say that

"the HIT freely generated by a point and an automorphism" gives a reasonable induction principle for the integers.

Can you elaborate?

How can I define a function Z_ind : forall x : loops S1, P x? I don't see how this just "falls out" of the definition of S1.

[mikeshulman]

I don't have time to explain further right now, but you can check out https://arxiv.org/abs/1901.06022 for a more general framework.

[Alizter]

@mikeshulman I see what you mean now. This clears things up. :-)

[Alizter]

Here is a proposal that I would be willing to carry out:

1. Create two new folders called Colimits and Diagrams
2. Move colimity files in HIT/Colimits into Colimits and move Suspension, Pushout, Flattening etc. from HIT into Colimits
3. Move files about diagrams into Diagrams, this will also include stuff about commutative squares and other misc. diagrams in the future.
4. In the HIT/Colimits library we have files like Coequalizer and Pushout. We should merge these with their HIT counterparts.

The advantage of this is we will have a clear library of diagrams which can pave the way for a limits library too.

What do you all think?

EDIT: And when doing all of this I can clean up the naming convention in the HIT/Colimits library and make it easier to use and maintain.

[mikeshulman]

That's worth a try. I'm not sure how useful it will be to try to merge HIT/Colimits/ files with HIT/ files, but feel free to give it a go.