Update ObjectClassifier.v and classify maps into BAut.

[jarlg]

In the 1st commit, we expand ObjectClassifier.v to speak about pointed maps into the universe pointed at some type, and into Type_ O pointed at some O-local type. In particular, the former corresponds to the type of fiber sequences, which we may consider to be pointed (equiv_sigma_pfibration) or not (equiv_sigma_fibration_p).

In the 2nd commit, we view X => merely (X <~> F) as a subuniverse to deduce facts about maps into BAut F from the statements about Type_ O in ObjectClassifier.v. Both pType and pForall are made cumulative in order for equiv_pequiv_postcompose to work at the end of BAut.v.

Question: in Truncations/Connectedness.v we added conn_to_trunc_ind, with the naming indicating that this is an induction principle for (n+1)-connected types into n-types. Any suggestions for a better name?

Comment: the interest of #1509 is be to make BAut F definitionally Type_ O for the subuniverse X => merely (X = F), thus letting us simply specialize results in ObjectClassifier.v to BAut F. An alternative is to redefine BAut F to use equivalences, in which case BAut F already would be Type_ O definitionally for subuniverse_merely_equiv. Having these results will help in determining which approach simplifies things.

[Alizter]

LGTM

Perhaps we should find a home for ObjectClassifier.v other than just in theories/. I'm not sure where though.

[mikeshulman]

The diff for the changes to ObjectClassifier is one of those extremely unhelpful ones that intersperses removed lines with added ones that are entirely unrelated to them. Is the old stuff only renamed, or replaced?

[Alizter]

On github, the split review option in the cog menu at the top seems to be easier to read.

[mikeshulman]

Thanks! I need to remember that cog. I wish it were more visible.

[jarlg]

I renamed things according to the suggestions, however some of the comments ObjectClassifier.v still talk about "fibrations". If desired I could rewrite these to refer to "types over" or "bundles over" some type Y, or some better suggestion. Let me know.

[Alizter]

@jarlg I think it would be good to update the documentation while we are at it, but if you don't have time just open an issue.

[jarlg]

Alright, I'll do it -- was mostly wondering if the terminology was fine, which I think it is.

[mikeshulman]

Looks great!