Additions for coherently invertible maps

[fredrik-bakke]

I'm ~just~ adding ~a little~ some infrastructure about coherently invertible maps ref. our discussions ~yesterday~ the other day. Don't worry, I'm not starting a huge refactoring project.

Relevant to #946 and #1021.

Summary

• Add mirror file about coherence squares of homotopies after coherence squares of identifications
• Add some core files for more streamlined proofs in other core files.
• Refactor some proofs for coherently invertible maps
  • is-emb-is-equiv was actually a proof about coherently invertible maps
  • slightly improve readability of is-coherently-invertible-is-invertible
• Prove the following (and corollaries) without "coherent replacement":
  • a coherently invertible map is transpose coherently invertible
  • the inverse of a coherently invertible map is coherently invertible
  • composites of coherently invertible maps are coherently invertible
  • coherently invertible maps are closed under homotopies

[fredrik-bakke]

Okay, so this is like the n'th time the past few months that we undo each others work with regards to avoiding cyclic dependencies, so I think we should sit down and agree on a common decision procedure.

[fredrik-bakke]

I think it is very useful to have a few more core files, and think we should try to have more results in them that don't add more dependencies. This allows us to have more conceptual proofs for core constructions such as, for instance, equivalences. For this to work, however, it is absolutely paramount that the core files try to avoid "junction" files as much as possible, like equivalences and embeddings. For instance, I think it should be possible to reason with squares of homotopies in all the ways I would want to in foundation-core.coherently-invertible-maps. This hinges on the fact that foundation-core.commuting-squares-of-identifications does not import foundation-core.equivalences, but does have the common constructs like pasting and inversions.

[fredrik-bakke]

Maybe one heuristic to go for is that, we should be more inclined to rewrite short proofs to avoid extra dependencies, such as the constructions on commuting squares of identifications, and prioritize making it possible to make the more complicated proofs conceptual, such as showing that the inverse of a coherently invertible map is coherently invertible.

[EgbertRijke]

Damn... :(

What was the original problem that caused you to do this?

[fredrik-bakke]

I want to prove lemma 4.2.2 in the HoTT/UF book by pasting diagrams

[fredrik-bakke]

I don't think foundation/(-core).commuting-squares-of-identifications is that bad

[EgbertRijke]

I think making foundation-core.coherently-invertible-maps dependent on commuting squares is not great. foundation-core.coherently-invertible-maps should have very minimal dependencies, because it is so fundamental in the hierarchy of our library. On top of that, it would have really been easy for you to do that one pasting square by hand.

[fredrik-bakke]

It's three pastings, no? And I must disagree. I think commuting squares come lower in the hierarchy than coherently invertible maps. Indeed, the constructions for commuting diagrams generally tend to depend only on the most basic things, and making them available to the other basic files will allow us to write lots of proofs more conceptually.

[EgbertRijke]

In #1014 I literally worked towards minimizing the dependencies of foundation-core.coherently-invertible-maps. That eased a lot of the tension that generated cyclic dependencies. So I am not at all convinced that the approach that you're taking in this PR is the right one, or an acceptable one.

[fredrik-bakke]

My proposal will not add any more dependencies to foundation-core.coherently-invertible-maps. But it will allow us to write better proofs in this file.

[fredrik-bakke]

Essentially by making most of commuting-squares-of-identifications not depend on equivalences.

[fredrik-bakke]

Of course, I don't mean "doesn't change the import statements" when I say "doesn't add dependencies"

[fredrik-bakke]

I have no clue how this PR got so large

[EgbertRijke]

I have no clue how this PR got so large

It is kind of you to give me some cover for my own large PRs:)

[fredrik-bakke]

I asked like a month or two ago whether coh-horizontal-concat-htpy was true without funext. Turns out it's just a case of naturality of homotopies, and now I actually needed it to be true without funext :)

[fredrik-bakke]

Alright, I'm flagging this one as ready for review. Apologies if I forgot to clean up something.

[fredrik-bakke]

(Currently doing import cleanup)

[EgbertRijke]

BTW I really like the work you have done in this pull request, and I think you are right about it that the commuting squares of identifications and of homotopies can be split up in a part that uses equivalences and a part that doesn't use equivalences. It seems to work well, and given the amount of theory that is being developed in coherently invertible maps it seems to be a really useful change. So thank you for doing that.