renamed Fibrations.v to HFiber.v

[Alizter]

closes #1303

[Alizter]

@mikeshulman are you able to review this?

[mikeshulman]

Thanks for this, and sorry for the delay. My main goal here is to make it intuitive which file one needs to import to get a particular result. For instance, it makes sense that to get results about hfibers you need to import HFiber. However, there are a few results currently in this file for which I don't think it's intuitive that you have to import HFiber, notably isequiv_from_functor_sigma and those involving IsTruncMap. Is there somewhere else we could put those results that would make them easier to find? I almost feel like those are such basic results that they should be in Basics or Types somewhere.

[Alizter]

@mikeshulman What about moving HFiber to Types? Then we will never have to worry about importing it.

[Alizter]

OK, I have rebased and reorganised HFiber. I've moved the "hfiber of functor" results to Types also.

[mikeshulman]

This is good, thanks! It might also be worth looking through the library to see if there are some unnecessary imports of HFiber now that some stuff has been moved into Types.

[Alizter]

They require the fcontr results which rely on Types/Sigma. Maybe we should kove fcontr to Basics?

…

On Wed, 1 Apr 2020 at 13:05, Mike Shulman ***@***.***> wrote: ***@***.**** approved this pull request. This is good, thanks! It might also be worth looking through the library to see if there are some unnecessary imports of HFiber now that some stuff has been moved into Types. ------------------------------ In theories/Types/Equiv.v <#1304 (comment)>: > @@ -164,4 +164,25 @@ Section AssumeFunext. : (A <~> B) <~> (B <~> A) := Build_Equiv _ _ ***@***.***_inverse A B) _. + (** If [functor_sigma idmap g] is an equivalence then so is g *) Why are these here rather than in Types/Sigma? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#1304 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACBXFE7DEZOK3V2BUD4V5O3RKMUYZANCNFSM4LJP2BOA> .

[mikeshulman]

Ah right. That's probably okay, but maybe we should add a comment in Types/Sigma pointing the reader to Types/Equiv to find them.

[Alizter]

Alright before we merge I will have a look for unnecessary imports.

[Alizter]

OK, I've removed the unnecessary imports of HFiber.v

[mikeshulman]

CI is unhappy?

[Alizter]

The CI is having trouble installing dependencies. I've restarted a few times but still a few (sometimes different) jobs fail.

[Alizter]

So the ubuntu repositories are being hosted on azure. I've heard rumors that azure is under a lot of strain due to current events. It will probably go away tomorrow.

[Alizter]

@mikeshulman Are we good to merge now?