Additions for coherently invertible maps (#1024)

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

src/category-theory/adjunctions-large-precategories.lagda.md

@@ -160,7 +160,7 @@ module _
       ( map-inv-equiv-is-adjoint-pair-Large-Precategory H X2 Y2)
   naturality-inv-equiv-is-adjoint-pair-Large-Precategory
     H {X1 = X1} {X2} {Y1} {Y2} f g =
-    coherence-square-maps-inv-equiv-horizontal
+    horizontal-inv-equiv-coherence-square-maps
       ( equiv-is-adjoint-pair-Large-Precategory H X1 Y1)
       ( λ h →
         comp-hom-Large-Precategory D

src/finite-group-theory/delooping-sign-homomorphism.lagda.md

@@ -85,7 +85,7 @@ open import univalent-combinatorics.standard-finite-types
 ## Ideas
 
 The delooping of a group homomorphism `f : G → H` is a pointed map
-`Bf : BG → BH` equiped with an homotopy witnessing that the following square
+`Bf : BG → BH` equiped with a homotopy witnessing that the following square
 commutes :
 
 ```text

src/foundation-core.lagda.md

@@ -10,6 +10,7 @@ open import foundation-core.cartesian-product-types public
 open import foundation-core.coherently-invertible-maps public
 open import foundation-core.commuting-prisms-of-maps public
 open import foundation-core.commuting-squares-of-homotopies public
+open import foundation-core.commuting-squares-of-identifications public
 open import foundation-core.commuting-squares-of-maps public
 open import foundation-core.commuting-triangles-of-maps public
 open import foundation-core.constant-maps public
@@ -59,4 +60,6 @@ open import foundation-core.type-theoretic-principle-of-choice public
 open import foundation-core.univalence public
 open import foundation-core.universal-property-pullbacks public
 open import foundation-core.universal-property-truncation public
+open import foundation-core.whiskering-homotopies-concatenation public
+open import foundation-core.whiskering-identifications-concatenation public
 ```