WIP Fix some namings according to style guidelines

[fredrik-bakke]

Notes:

• emb-is-equiv was already proven (with a different name) in 04-half-adjoint-equivalences, so I removed the proof in 08-families-of-maps
• The stuff about pullback-homotopy in 08-families-of-maps doesn't seem to be used anywhere, and isn't it just a special case of the fact that transport is an equivalence of fibers?

Builds on #39 and #40, progresses #14.

[fredrik-bakke]

Do you prefer the name fibered-arr-free-arr, or the name map-Σ-hom-arr, or perhaps something else, for the following map?

  (A : U)
  : (arr A) → (Σ (x : A) , (Σ (y : A) , hom A x y))
  := \ f → (f 0₂ , (f 1₂ , f))

[emilyriehl]

Hey @fredrik-bakke I'm back on line. Thanks for all this.

I wrote the pullback-homotopy stuff thinking I needed it for something (I've forgotten) then realized after I've done it that it wasn't necessary actually. So yes that can all be deleted.

Now that the embeddings stuff is earlier can we move the 2-of-3 for is-equiv earlier as well? It felt out of place here.

[fredrik-bakke]

Welcome back! Sure, I'll try to complete this refactoring work soon :)

[fredrik-bakke]

Wow, time really flies! I'll sit down and finish this PR tomorrow. Sorry for the delay.

[emilyriehl]

Hey @fredrik-bakke actually I'm trying to complete the merge now if you don't mind. I attempted the refactoring and decided it didn't quite work (since we use the fundamental theorem of identity types to prove equivalences are embeddings).

Because @jonweinb were doing some other work at the same time we created some merge conflicts that I'm in the process of resolving (I hope). So if you don't object, I'll fix up my mess and then go ahead and merge this. I'm excited to have it as part of the main branch.

[fredrik-bakke]

Oh, alright, that works! I can follow up on any loose ends in a new PR. I think I did some more refactoring locally that didn't make it online, but if the current version of this PR type checks, you should be golden

[fredrik-bakke]

Hmm, when I try and type check this branch, rzk gets stuck on

[ 18 out of 77 ] Checking #define is-natural-in-object-yon

though I'm using a slightly outdated version (0.5.3)

[emilyriehl]

Hopefully I didn't mess any of that up. Merging now!

[fredrik-bakke]

Great! I hope the changes don't make too much of a mess for you. I'll have a look over things tomorrow anyway, and if I end up writing a new PR I'll make sure to make it more self-contained.