Additions for coherently invertible maps

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
 ```