Sequential limits

src/foundation-core/commuting-squares-of-maps.lagda.md

@@ -40,7 +40,7 @@ coherence-square-maps :
   (top : C → B) (left : C → A) (right : B → X) (bottom : A → X) →
   UU (l3 ⊔ l4)
 coherence-square-maps top left right bottom =
-  (bottom ∘ left) ~ (right ∘ top)
+  bottom ∘ left ~ right ∘ top
 ```
 
 ## Properties

src/foundation-core/commuting-triangles-of-maps.lagda.md

@@ -22,15 +22,20 @@ open import foundation-core.whiskering-homotopies
 A triangle of maps
 
 ```text
- A ----> B
-  \     /
-   \   /
-    V V
-     X
+      top
+   A ----> B
+    \     /
+left \   / right
+      V V
+       X
 ```
 
 is said to commute if there is a homotopy between the map on the left and the
-composite map.
+composite map
+
+```text
+  left ~ right ∘ top.
+```
 
 ## Definitions
 
@@ -43,11 +48,11 @@ module _
 
   coherence-triangle-maps :
     (left : A → X) (right : B → X) (top : A → B) → UU (l1 ⊔ l2)
-  coherence-triangle-maps left right top = left ~ (right ∘ top)
+  coherence-triangle-maps left right top = left ~ right ∘ top
 
   coherence-triangle-maps' :
     (left : A → X) (right : B → X) (top : A → B) → UU (l1 ⊔ l2)
-  coherence-triangle-maps' left right top = (right ∘ top) ~ left
+  coherence-triangle-maps' left right top = right ∘ top ~ left
 ```
 
 ### Concatenation of commuting triangles of maps
@@ -92,3 +97,20 @@ module _
       ( precomp right W)
   precomp-coherence-triangle-maps' H W = htpy-precomp H W
 ```
+
+### Coherences of commuting triangles of maps with fixed vertices
+
+This or its opposite should be the coherence in the characterization of
+identifications of commuting triangles of maps with fixed end vertices.
+
+```agda
+coherence-htpy-triangle-maps :
+  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
+  (left : A → X) (right : B → X) (top : A → B)
+  (left' : A → X) (right' : B → X) (top' : A → B) →
+  coherence-triangle-maps left right top →
+  coherence-triangle-maps left' right' top' →
+  left ~ left' → right ~ right' → top ~ top' → UU (l1 ⊔ l2)
+coherence-htpy-triangle-maps left right top left' right' top' c c' L R T =
+  c ∙h htpy-comp-horizontal T R ~ L ∙h c'
+```

src/foundation-core/equality-dependent-pair-types.lagda.md

@@ -7,6 +7,7 @@ module foundation-core.equality-dependent-pair-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
@@ -51,13 +52,26 @@ module _
   pair-eq-Σ {s} refl = refl-Eq-Σ s
 
   eq-pair-Σ :
-    {s t : Σ A B} (α : pr1 s ＝ pr1 t) →
+    {s t : Σ A B}
+    (α : pr1 s ＝ pr1 t) →
     dependent-identification B α (pr2 s) (pr2 t) → s ＝ t
-  eq-pair-Σ {pair x y} {pair .x .y} refl refl = refl
+  eq-pair-Σ refl refl = refl
 
   eq-pair-Σ' : {s t : Σ A B} → Eq-Σ s t → s ＝ t
   eq-pair-Σ' p = eq-pair-Σ (pr1 p) (pr2 p)
 
+  eq-pair-Σ-eq-pr1 :
+    {x y : A} {s : B x} (p : x ＝ y) → (x , s) ＝ (y , tr B p s)
+  eq-pair-Σ-eq-pr1 refl = refl
+
+  eq-pair-Σ-eq-pr1' :
+    {x y : A} {t : B y} (p : x ＝ y) → (x , tr B (inv p) t) ＝ (y , t)
+  eq-pair-Σ-eq-pr1' refl = refl
+
+  eq-pair-Σ-eq-pr2 :
+    {x : A} {s t : B x} → s ＝ t → (x , s) ＝ (x , t)
+  eq-pair-Σ-eq-pr2 {x} = ap {B = Σ A B} (pair x)
+
   is-retraction-pair-eq-Σ :
     (s t : Σ A B) →
     ((pair-eq-Σ {s} {t}) ∘ (eq-pair-Σ' {s} {t})) ~ id {A = Eq-Σ s t}

src/foundation-core/equivalences.lagda.md

@@ -402,7 +402,7 @@ abstract
 abstract
   is-equiv-is-section :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} →
-    is-equiv f → (f ∘ g) ~ id → is-equiv g
+    is-equiv f → f ∘ g ~ id → is-equiv g
   is-equiv-is-section {B = B} {f = f} {g = g} is-equiv-f H =
     is-equiv-right-factor-htpy id f g (inv-htpy H) is-equiv-f is-equiv-id
 ```

src/foundation-core/fibers-of-maps.lagda.md

@@ -23,9 +23,9 @@ open import foundation-core.transport-along-identifications
 
 ## Idea
 
-Given a map `f : A → B` and a point `b : B`, the fiber of `f` at `b` is the
-preimage of `f` at `b`. In other words, it consists of the elements `a : A`
-equipped with an identification `Id (f a) b`.
+Given a map `f : A → B` and an element `b : B`, the **fiber** of `f` at `b` is
+the preimage of `f` at `b`. In other words, it consists of the elements `a : A`
+equipped with an [identification](foundation-core.identity-types.md) `f a ＝ b`.
 
 ## Definition
 
@@ -403,3 +403,10 @@ reduce-Π-fiber :
   (C : B → UU l3) → ((y : B) → fiber f y → C y) ≃ ((x : A) → C (f x))
 reduce-Π-fiber f C = reduce-Π-fiber' f (λ y z → C y)
 ```
+
+## Table of files about fibers of maps
+
+The following table lists files that are about fibers of maps as a general
+concept.
+
+{{#include tables/fibers-of-maps.md}}

src/foundation-core/homotopies.lagda.md

@@ -7,7 +7,6 @@ module foundation-core.homotopies where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-identifications
@@ -334,8 +333,8 @@ syntax step-homotopy-reasoning p h q = p ~ h by q
 
 ## See also
 
-- We postulate that homotopies characterize identifications in (dependent)
-  function types in the file
+- We postulate that homotopies characterize identifications of (dependent)
+  functions in the file
   [`foundation-core.function-extensionality`](foundation-core.function-extensionality.md).
 - The whiskering operations on homotopies are defined in the file
   [`foundation.whiskering-homotopies`](foundation.whiskering-homotopies.md).