diff --git a/src/foundation-core/commuting-squares-of-maps.lagda.md b/src/foundation-core/commuting-squares-of-maps.lagda.md
index 1ab84850da..de050e312c 100644
--- a/src/foundation-core/commuting-squares-of-maps.lagda.md
+++ b/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
diff --git a/src/foundation-core/commuting-triangles-of-maps.lagda.md b/src/foundation-core/commuting-triangles-of-maps.lagda.md
index 30a6c78e5f..ac2c483faa 100644
--- a/src/foundation-core/commuting-triangles-of-maps.lagda.md
+++ b/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'
+```
diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md
index f80cefffdd..4c48dcb81a 100644
--- a/src/foundation-core/equality-dependent-pair-types.lagda.md
+++ b/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}
diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md
index fe08804f1a..de2d471030 100644
--- a/src/foundation-core/equivalences.lagda.md
+++ b/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
 ```
diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md
index 788aea7aef..255a9c8c24 100644
--- a/src/foundation-core/fibers-of-maps.lagda.md
+++ b/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}}
diff --git a/src/foundation-core/homotopies.lagda.md b/src/foundation-core/homotopies.lagda.md
index 4e09b01772..98d62c6957 100644
--- a/src/foundation-core/homotopies.lagda.md
+++ b/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).
diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md
index 56822e160a..d55e6c6ba7 100644
--- a/src/foundation-core/pullbacks.lagda.md
+++ b/src/foundation-core/pullbacks.lagda.md
@@ -14,7 +14,6 @@ open import foundation.equality-cartesian-product-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-fibers-of-maps
 open import foundation.identity-types
-open import foundation.morphisms-cospans
 open import foundation.structure-identity-principle
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.type-theoretic-principle-of-choice
@@ -35,47 +34,49 @@ open import foundation-core.universal-property-pullbacks
 
 ## Definitions
 
-### The canonical pullback of a cospan
+### The standard pullback of a cospan
 
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
   where
 
-  canonical-pullback : UU ((l1 ⊔ l2) ⊔ l3)
-  canonical-pullback = Σ A (λ x → Σ B (λ y → f x ＝ g y))
+  standard-pullback : UU (l1 ⊔ l2 ⊔ l3)
+  standard-pullback = Σ A (λ x → Σ B (λ y → f x ＝ g y))
 
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {f : A → X} {g : B → X}
   where
 
-  π₁ : canonical-pullback f g → A
-  π₁ = pr1
+  vertical-map-standard-pullback : standard-pullback f g → A
+  vertical-map-standard-pullback = pr1
 
-  π₂ : canonical-pullback f g → B
-  π₂ t = pr1 (pr2 t)
+  horizontal-map-standard-pullback : standard-pullback f g → B
+  horizontal-map-standard-pullback t = pr1 (pr2 t)
 
-  π₃ : (f ∘ π₁) ~ (g ∘ π₂)
-  π₃ t = pr2 (pr2 t)
+  coherence-square-standard-pullback :
+    ( f ∘ vertical-map-standard-pullback) ~
+    ( g ∘ horizontal-map-standard-pullback)
+  coherence-square-standard-pullback t = pr2 (pr2 t)
 ```
 
-### The cone at the canonical pullback
+### The cone at the standard pullback
 
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
   where
 
-  cone-canonical-pullback : cone f g (canonical-pullback f g)
-  pr1 cone-canonical-pullback = π₁
-  pr1 (pr2 cone-canonical-pullback) = π₂
-  pr2 (pr2 cone-canonical-pullback) = π₃
+  cone-standard-pullback : cone f g (standard-pullback f g)
+  pr1 cone-standard-pullback = vertical-map-standard-pullback
+  pr1 (pr2 cone-standard-pullback) = horizontal-map-standard-pullback
+  pr2 (pr2 cone-standard-pullback) = coherence-square-standard-pullback
 ```
 
-### The gap-map into the canonical pullback
+### The gap map into the standard pullback
 
-The gap map of a square is the map fron the vertex of the cone into the
-canonical pullback.
+The **gap map** of a square is the map fron the vertex of the
+[cone](foundation.cones-over-cospans.md) into the standard pullback.
 
 ```agda
 module _
@@ -83,17 +84,19 @@ module _
   (f : A → X) (g : B → X)
   where
 
-  gap : cone f g C → C → canonical-pullback f g
+  gap : cone f g C → C → standard-pullback f g
   pr1 (gap c z) = vertical-map-cone f g c z
   pr1 (pr2 (gap c z)) = horizontal-map-cone f g c z
   pr2 (pr2 (gap c z)) = coherence-square-cone f g c z
 ```
 
-### The `is-pullback` property
+### The property of being a pullback
 
-The proposition `is-pullback` is the assertion that the gap map is an
-equivalence. Note that this proposition is small, whereas the universal property
-is a large proposition.
+The [proposition](foundation-core.propositions.md) `is-pullback` is the
+assertion that the gap map is an [equivalence](foundation-core.equivalences.md).
+Note that this proposition is [small](foundation-core.small-types.md), whereas
+[the universal property](foundation-core.universal-property-pullbacks.md) is a
+large proposition.
 
 ```agda
 module _
@@ -105,86 +108,60 @@ module _
   is-pullback c = is-equiv (gap f g c)
 ```
 
-### Functoriality of canonical pullbacks
-
-```agda
-module _
-  {l1 l2 l3 l1' l2' l3' : Level}
-  {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
-  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X')
-  where
-
-  map-canonical-pullback :
-    hom-cospan f' g' f g → canonical-pullback f' g' → canonical-pullback f g
-  pr1 (map-canonical-pullback (hA , _) (a' , _)) = hA a'
-  pr1 (pr2 (map-canonical-pullback (hA , hB , _) (a' , b' , _))) = hB b'
-  pr2 (pr2 (map-canonical-pullback (hA , hB , hX , HA , HB) (a' , b' , p'))) =
-    (HA a') ∙ ((ap hX p') ∙ (inv (HB b')))
-
-  map-is-pullback :
-    {l4 l4' : Level} {C : UU l4} {C' : UU l4'} →
-    (c : cone f g C) (c' : cone f' g' C') →
-    is-pullback f g c → is-pullback f' g' c' →
-    hom-cospan f' g' f g → C' → C
-  map-is-pullback c c' is-pb-c is-pb-c' h x =
-    map-inv-is-equiv is-pb-c (map-canonical-pullback h (gap f' g' c' x))
-```
-
 ## Properties
 
-### Characterization of the identity type of the canonical pullback
+### Characterization of the identity type of the standard pullback
 
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
   where
 
-  Eq-canonical-pullback : (t t' : canonical-pullback f g) → UU (l1 ⊔ l2 ⊔ l3)
-  Eq-canonical-pullback (a , bp) t' =
-    let b = pr1 bp
-        p = pr2 bp
-        a' = pr1 t'
-        b' = pr1 (pr2 t')
-        p' = pr2 (pr2 t')
-    in
-    Σ (a ＝ a') (λ α → Σ (b ＝ b') (λ β → ((ap f α) ∙ p') ＝ (p ∙ (ap g β))))
-
-  refl-Eq-canonical-pullback :
-    (t : canonical-pullback f g) → Eq-canonical-pullback t t
-  pr1 (refl-Eq-canonical-pullback (a , b , p)) = refl
-  pr1 (pr2 (refl-Eq-canonical-pullback (a , b , p))) = refl
-  pr2 (pr2 (refl-Eq-canonical-pullback (a , b , p))) = inv right-unit
-
-  Eq-eq-canonical-pullback :
-    (s t : canonical-pullback f g) → s ＝ t → Eq-canonical-pullback s t
-  Eq-eq-canonical-pullback s .s refl = refl-Eq-canonical-pullback s
-
-  extensionality-canonical-pullback :
-    (t t' : canonical-pullback f g) → (t ＝ t') ≃ Eq-canonical-pullback t t'
-  extensionality-canonical-pullback (a , b , p) =
+  Eq-standard-pullback : (t t' : standard-pullback f g) → UU (l1 ⊔ l2 ⊔ l3)
+  Eq-standard-pullback (a , b , p) (a' , b' , p') =
+    Σ (a ＝ a') (λ α → Σ (b ＝ b') (λ β → ap f α ∙ p' ＝ p ∙ ap g β))
+
+  refl-Eq-standard-pullback :
+    (t : standard-pullback f g) → Eq-standard-pullback t t
+  pr1 (refl-Eq-standard-pullback (a , b , p)) = refl
+  pr1 (pr2 (refl-Eq-standard-pullback (a , b , p))) = refl
+  pr2 (pr2 (refl-Eq-standard-pullback (a , b , p))) = inv right-unit
+
+  Eq-eq-standard-pullback :
+    (s t : standard-pullback f g) → s ＝ t → Eq-standard-pullback s t
+  Eq-eq-standard-pullback s .s refl = refl-Eq-standard-pullback s
+
+  extensionality-standard-pullback :
+    (t t' : standard-pullback f g) → (t ＝ t') ≃ Eq-standard-pullback t t'
+  extensionality-standard-pullback (a , b , p) =
     extensionality-Σ
       ( λ {a'} bp' α →
-        Σ (b ＝ pr1 bp') (λ β → (ap f α ∙ pr2 bp') ＝ (p ∙ ap g β)))
+        Σ (b ＝ pr1 bp') (λ β → ap f α ∙ pr2 bp' ＝ p ∙ ap g β))
       ( refl)
       ( refl , inv right-unit)
       ( λ x → id-equiv)
       ( extensionality-Σ
-        ( λ {b'} p' β → p' ＝ (p ∙ ap g β))
+        ( λ p' β → p' ＝ p ∙ ap g β)
         ( refl)
         ( inv right-unit)
         ( λ y → id-equiv)
         ( λ p' → equiv-concat' p' (inv right-unit) ∘e equiv-inv p p'))
 
-  map-extensionality-canonical-pullback :
-    { s t : canonical-pullback f g} ( α : π₁ s ＝ π₁ t) (β : π₂ s ＝ π₂ t) →
-    ( ((ap f α) ∙ π₃ t) ＝ (π₃ s ∙ (ap g β))) → s ＝ t
-  map-extensionality-canonical-pullback {s} {t} α β γ =
+  map-extensionality-standard-pullback :
+    { s t : standard-pullback f g}
+    ( α : vertical-map-standard-pullback s ＝ vertical-map-standard-pullback t)
+    ( β :
+      horizontal-map-standard-pullback s ＝ horizontal-map-standard-pullback t) →
+    ( ( ap f α ∙ coherence-square-standard-pullback t) ＝
+      ( coherence-square-standard-pullback s ∙ ap g β)) →
+    s ＝ t
+  map-extensionality-standard-pullback {s} {t} α β γ =
     map-inv-equiv
-      ( extensionality-canonical-pullback s t)
-      ( triple α β γ)
+      ( extensionality-standard-pullback s t)
+      ( α , β , γ)
 ```
 
-### The canonical pullback satisfies the universal property of pullbacks
+### The standard pullback satisfies the universal property of pullbacks
 
 ```agda
 module _
@@ -192,10 +169,10 @@ module _
   where
 
   abstract
-    universal-property-pullback-canonical-pullback :
+    universal-property-pullback-standard-pullback :
       {l : Level} →
-      universal-property-pullback l f g (cone-canonical-pullback f g)
-    universal-property-pullback-canonical-pullback C =
+      universal-property-pullback l f g (cone-standard-pullback f g)
+    universal-property-pullback-standard-pullback C =
       is-equiv-comp
         ( tot (λ p → map-distributive-Π-Σ))
         ( mapping-into-Σ)
@@ -212,12 +189,12 @@ module _
   (f : A → X) (g : B → X)
   where
 
-  htpy-cone-up-pullback-canonical-pullback :
+  htpy-cone-up-pullback-standard-pullback :
     (c : cone f g C) →
-    htpy-cone f g (cone-map f g (cone-canonical-pullback f g) (gap f g c)) c
-  pr1 (htpy-cone-up-pullback-canonical-pullback c) = refl-htpy
-  pr1 (pr2 (htpy-cone-up-pullback-canonical-pullback c)) = refl-htpy
-  pr2 (pr2 (htpy-cone-up-pullback-canonical-pullback c)) = right-unit-htpy
+    htpy-cone f g (cone-map f g (cone-standard-pullback f g) (gap f g c)) c
+  pr1 (htpy-cone-up-pullback-standard-pullback c) = refl-htpy
+  pr1 (pr2 (htpy-cone-up-pullback-standard-pullback c)) = refl-htpy
+  pr2 (pr2 (htpy-cone-up-pullback-standard-pullback c)) = right-unit-htpy
 ```
 
 ### A cone satisfies the universal property of the pullback if and only if the gap map is an equivalence
@@ -232,14 +209,13 @@ module _
     is-pullback-universal-property-pullback :
       (c : cone f g C) →
       ({l : Level} → universal-property-pullback l f g c) → is-pullback f g c
-    is-pullback-universal-property-pullback c up =
+    is-pullback-universal-property-pullback c =
       is-equiv-up-pullback-up-pullback
-        ( cone-canonical-pullback f g)
+        ( cone-standard-pullback f g)
         ( c)
         ( gap f g c)
-        ( htpy-cone-up-pullback-canonical-pullback f g c)
-        ( universal-property-pullback-canonical-pullback f g)
-        ( up)
+        ( htpy-cone-up-pullback-standard-pullback f g c)
+        ( universal-property-pullback-standard-pullback f g)
 
   abstract
     universal-property-pullback-is-pullback :
@@ -247,12 +223,12 @@ module _
       {l : Level} → universal-property-pullback l f g c
     universal-property-pullback-is-pullback c is-pullback-c =
       up-pullback-up-pullback-is-equiv
-        ( cone-canonical-pullback f g)
+        ( cone-standard-pullback f g)
         ( c)
         ( gap f g c)
-        ( htpy-cone-up-pullback-canonical-pullback f g c)
+        ( htpy-cone-up-pullback-standard-pullback f g c)
         ( is-pullback-c)
-        ( universal-property-pullback-canonical-pullback f g)
+        ( universal-property-pullback-standard-pullback f g)
 ```
 
 ### The pullback of a Σ-type
@@ -262,90 +238,95 @@ module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (Q : B → UU l3)
   where
 
-  canonical-pullback-Σ : UU (l1 ⊔ l3)
-  canonical-pullback-Σ = Σ A (λ x → Q (f x))
+  standard-pullback-Σ : UU (l1 ⊔ l3)
+  standard-pullback-Σ = Σ A (λ x → Q (f x))
 
-  cone-canonical-pullback-Σ : cone f (pr1 {B = Q}) canonical-pullback-Σ
-  pr1 cone-canonical-pullback-Σ = pr1
-  pr1 (pr2 cone-canonical-pullback-Σ) = map-Σ-map-base f Q
-  pr2 (pr2 cone-canonical-pullback-Σ) = refl-htpy
+  cone-standard-pullback-Σ : cone f pr1 standard-pullback-Σ
+  pr1 cone-standard-pullback-Σ = pr1
+  pr1 (pr2 cone-standard-pullback-Σ) = map-Σ-map-base f Q
+  pr2 (pr2 cone-standard-pullback-Σ) = refl-htpy
 
-  inv-gap-cone-canonical-pullback-Σ :
-    canonical-pullback f (pr1 {B = Q}) → canonical-pullback-Σ
-  pr1 (inv-gap-cone-canonical-pullback-Σ (x , (.(f x) , q) , refl)) = x
-  pr2 (inv-gap-cone-canonical-pullback-Σ (x , (.(f x) , q) , refl)) = q
+  inv-gap-cone-standard-pullback-Σ :
+    standard-pullback f (pr1 {B = Q}) → standard-pullback-Σ
+  pr1 (inv-gap-cone-standard-pullback-Σ (x , (.(f x) , q) , refl)) = x
+  pr2 (inv-gap-cone-standard-pullback-Σ (x , (.(f x) , q) , refl)) = q
 
   abstract
-    is-section-inv-gap-cone-canonical-pullback-Σ :
-      ( ( gap f (pr1 {B = Q}) cone-canonical-pullback-Σ) ∘
-        ( inv-gap-cone-canonical-pullback-Σ)) ~ id
-    is-section-inv-gap-cone-canonical-pullback-Σ (x , (.(f x) , q) , refl) =
+    is-section-inv-gap-cone-standard-pullback-Σ :
+      ( gap f pr1 cone-standard-pullback-Σ ∘ inv-gap-cone-standard-pullback-Σ) ~
+      ( id)
+    is-section-inv-gap-cone-standard-pullback-Σ (x , (.(f x) , q) , refl) =
       refl
 
   abstract
-    is-retraction-inv-gap-cone-canonical-pullback-Σ :
-      ( ( inv-gap-cone-canonical-pullback-Σ) ∘
-        ( gap f (pr1 {B = Q}) cone-canonical-pullback-Σ)) ~ id
-    is-retraction-inv-gap-cone-canonical-pullback-Σ (x , q) = refl
+    is-retraction-inv-gap-cone-standard-pullback-Σ :
+      ( inv-gap-cone-standard-pullback-Σ ∘
+        gap f pr1 cone-standard-pullback-Σ) ~ id
+    is-retraction-inv-gap-cone-standard-pullback-Σ (x , q) = refl
 
   abstract
-    is-pullback-cone-canonical-pullback-Σ :
-      is-pullback f (pr1 {B = Q}) cone-canonical-pullback-Σ
-    is-pullback-cone-canonical-pullback-Σ =
+    is-pullback-cone-standard-pullback-Σ :
+      is-pullback f pr1 cone-standard-pullback-Σ
+    is-pullback-cone-standard-pullback-Σ =
       is-equiv-is-invertible
-        inv-gap-cone-canonical-pullback-Σ
-        is-section-inv-gap-cone-canonical-pullback-Σ
-        is-retraction-inv-gap-cone-canonical-pullback-Σ
-
-  compute-canonical-pullback-Σ :
-    canonical-pullback-Σ ≃ canonical-pullback f (pr1 {B = Q})
-  pr1 compute-canonical-pullback-Σ = gap f pr1 cone-canonical-pullback-Σ
-  pr2 compute-canonical-pullback-Σ = is-pullback-cone-canonical-pullback-Σ
+        inv-gap-cone-standard-pullback-Σ
+        is-section-inv-gap-cone-standard-pullback-Σ
+        is-retraction-inv-gap-cone-standard-pullback-Σ
+
+  compute-standard-pullback-Σ :
+    standard-pullback-Σ ≃ standard-pullback f pr1
+  pr1 compute-standard-pullback-Σ = gap f pr1 cone-standard-pullback-Σ
+  pr2 compute-standard-pullback-Σ = is-pullback-cone-standard-pullback-Σ
 ```
 
 ### Pullbacks are symmetric
 
 ```agda
-map-commutative-canonical-pullback :
+map-commutative-standard-pullback :
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X) → canonical-pullback f g → canonical-pullback g f
-pr1 (map-commutative-canonical-pullback f g x) = π₂ x
-pr1 (pr2 (map-commutative-canonical-pullback f g x)) = π₁ x
-pr2 (pr2 (map-commutative-canonical-pullback f g x)) = inv (π₃ x)
-
-inv-inv-map-commutative-canonical-pullback :
+  (f : A → X) (g : B → X) → standard-pullback f g → standard-pullback g f
+pr1 (map-commutative-standard-pullback f g x) =
+  horizontal-map-standard-pullback x
+pr1 (pr2 (map-commutative-standard-pullback f g x)) =
+  vertical-map-standard-pullback x
+pr2 (pr2 (map-commutative-standard-pullback f g x)) =
+  inv (coherence-square-standard-pullback x)
+
+inv-inv-map-commutative-standard-pullback :
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
   (f : A → X) (g : B → X) →
-  ( map-commutative-canonical-pullback f g ∘
-    map-commutative-canonical-pullback g f) ~ id
-inv-inv-map-commutative-canonical-pullback f g x =
-  eq-pair-Σ refl (eq-pair-Σ refl (inv-inv (π₃ x)))
+  ( map-commutative-standard-pullback f g ∘
+    map-commutative-standard-pullback g f) ~ id
+inv-inv-map-commutative-standard-pullback f g x =
+  eq-pair-Σ-eq-pr2
+    ( eq-pair-Σ-eq-pr2
+      ( inv-inv (coherence-square-standard-pullback x)))
 
 abstract
-  is-equiv-map-commutative-canonical-pullback :
+  is-equiv-map-commutative-standard-pullback :
     {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-    (f : A → X) (g : B → X) → is-equiv (map-commutative-canonical-pullback f g)
-  is-equiv-map-commutative-canonical-pullback f g =
+    (f : A → X) (g : B → X) → is-equiv (map-commutative-standard-pullback f g)
+  is-equiv-map-commutative-standard-pullback f g =
     is-equiv-is-invertible
-      ( map-commutative-canonical-pullback g f)
-      ( inv-inv-map-commutative-canonical-pullback f g)
-      ( inv-inv-map-commutative-canonical-pullback g f)
+      ( map-commutative-standard-pullback g f)
+      ( inv-inv-map-commutative-standard-pullback f g)
+      ( inv-inv-map-commutative-standard-pullback g f)
 
-commutative-canonical-pullback :
+commutative-standard-pullback :
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
   (f : A → X) (g : B → X) →
-  canonical-pullback f g ≃ canonical-pullback g f
-pr1 (commutative-canonical-pullback f g) =
-  map-commutative-canonical-pullback f g
-pr2 (commutative-canonical-pullback f g) =
-  is-equiv-map-commutative-canonical-pullback f g
+  standard-pullback f g ≃ standard-pullback g f
+pr1 (commutative-standard-pullback f g) =
+  map-commutative-standard-pullback f g
+pr2 (commutative-standard-pullback f g) =
+  is-equiv-map-commutative-standard-pullback f g
 
-triangle-map-commutative-canonical-pullback :
+triangle-map-commutative-standard-pullback :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   (f : A → X) (g : B → X) (c : cone f g C) →
   ( gap g f (swap-cone f g c)) ~
-  ( ( map-commutative-canonical-pullback f g) ∘ ( gap f g c))
-triangle-map-commutative-canonical-pullback f g (p , q , H) x = refl
+  ( map-commutative-standard-pullback f g ∘ gap f g c)
+triangle-map-commutative-standard-pullback f g (p , q , H) x = refl
 
 abstract
   is-pullback-swap-cone :
@@ -355,11 +336,11 @@ abstract
   is-pullback-swap-cone f g c is-pb-c =
     is-equiv-comp-htpy
       ( gap g f (swap-cone f g c))
-      ( map-commutative-canonical-pullback f g)
+      ( map-commutative-standard-pullback f g)
       ( gap f g c)
-      ( triangle-map-commutative-canonical-pullback f g c)
+      ( triangle-map-commutative-standard-pullback f g c)
       ( is-pb-c)
-      ( is-equiv-map-commutative-canonical-pullback f g)
+      ( is-equiv-map-commutative-standard-pullback f g)
 
 abstract
   is-pullback-swap-cone' :
@@ -369,10 +350,10 @@ abstract
   is-pullback-swap-cone' f g c is-pb-c' =
     is-equiv-right-factor-htpy
       ( gap g f (swap-cone f g c))
-      ( map-commutative-canonical-pullback f g)
+      ( map-commutative-standard-pullback f g)
       ( gap f g c)
-      ( triangle-map-commutative-canonical-pullback f g c)
-      ( is-equiv-map-commutative-canonical-pullback f g)
+      ( triangle-map-commutative-standard-pullback f g c)
+      ( is-equiv-map-commutative-standard-pullback f g)
       ( is-pb-c')
 ```
 
@@ -391,18 +372,20 @@ pr2 (pr2 (fold-cone f g c)) z = eq-pair (coherence-square-cone f g c z) refl
 map-fold-cone :
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
   (f : A → X) → (g : B → X) →
-  canonical-pullback f g → canonical-pullback (map-prod f g) (diagonal X)
-pr1 (pr1 (map-fold-cone f g x)) = π₁ x
-pr2 (pr1 (map-fold-cone f g x)) = π₂ x
-pr1 (pr2 (map-fold-cone f g x)) = g (π₂ x)
-pr2 (pr2 (map-fold-cone f g x)) = eq-pair (π₃ x) refl
+  standard-pullback f g → standard-pullback (map-prod f g) (diagonal X)
+pr1 (pr1 (map-fold-cone f g x)) = vertical-map-standard-pullback x
+pr2 (pr1 (map-fold-cone f g x)) = horizontal-map-standard-pullback x
+pr1 (pr2 (map-fold-cone f g x)) = g (horizontal-map-standard-pullback x)
+pr2 (pr2 (map-fold-cone f g x)) =
+  eq-pair (coherence-square-standard-pullback x) refl
 
 inv-map-fold-cone :
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
   (f : A → X) → (g : B → X) →
-  canonical-pullback (map-prod f g) (diagonal X) → canonical-pullback f g
-inv-map-fold-cone f g ((a , b) , (x , α)) =
-  triple a b ((ap pr1 α) ∙ (inv (ap pr2 α)))
+  standard-pullback (map-prod f g) (diagonal X) → standard-pullback f g
+pr1 (inv-map-fold-cone f g ((a , b) , x , α)) = a
+pr1 (pr2 (inv-map-fold-cone f g ((a , b) , x , α))) = b
+pr2 (pr2 (inv-map-fold-cone f g ((a , b) , x , α))) = ap pr1 α ∙ inv (ap pr2 α)
 
 abstract
   is-section-inv-map-fold-cone :
@@ -410,25 +393,25 @@ abstract
     (f : A → X) (g : B → X) →
     ((map-fold-cone f g) ∘ (inv-map-fold-cone f g)) ~ id
   is-section-inv-map-fold-cone {A = A} {B} {X} f g ((a , b) , (x , α)) =
-    map-extensionality-canonical-pullback
+    map-extensionality-standard-pullback
       ( map-prod f g)
       ( diagonal X)
       refl
       ( ap pr2 α)
-      ( ( ( ( inv (is-section-pair-eq α)) ∙
-            ( ap
-              ( λ t → (eq-pair t (ap pr2 α)))
-              ( ( ( inv right-unit) ∙
-                  ( inv (ap (concat (ap pr1 α) x) (left-inv (ap pr2 α))))) ∙
-                ( inv (assoc (ap pr1 α) (inv (ap pr2 α)) (ap pr2 α)))))) ∙
-          ( eq-pair-concat
-            ( (ap pr1 α) ∙ (inv (ap pr2 α)))
-            ( ap pr2 α)
-            ( refl)
-            ( ap pr2 α))) ∙
+      ( ( inv (is-section-pair-eq α)) ∙
+        ( ap
+          ( λ t → (eq-pair t (ap pr2 α)))
+          ( ( inv right-unit) ∙
+            ( inv (ap (concat (ap pr1 α) x) (left-inv (ap pr2 α)))) ∙
+            ( inv (assoc (ap pr1 α) (inv (ap pr2 α)) (ap pr2 α))))) ∙
+        ( eq-pair-concat
+          ( ap pr1 α ∙ inv (ap pr2 α))
+          ( ap pr2 α)
+          ( refl)
+          ( ap pr2 α)) ∙
         ( ap
           ( concat
-            ( eq-pair ((ap pr1 α) ∙ (inv (ap pr2 α))) refl)
+            ( eq-pair (ap pr1 α ∙ inv (ap pr2 α)) refl)
             ( x , x))
           ( inv (ap-diagonal (ap pr2 α)))))
 
@@ -436,24 +419,18 @@ abstract
   is-retraction-inv-map-fold-cone :
     {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
     (f : A → X) (g : B → X) →
-    ((inv-map-fold-cone f g) ∘ (map-fold-cone f g)) ~ id
-  is-retraction-inv-map-fold-cone { A = A} { B = B} { X = X} f g (a , b , p) =
-
-    map-extensionality-canonical-pullback {A = A} {B = B} {X = X} f g
-      refl
-      refl
+    inv-map-fold-cone f g ∘ map-fold-cone f g ~ id
+  is-retraction-inv-map-fold-cone f g (a , b , p) =
+    map-extensionality-standard-pullback f g
+      ( refl)
+      ( refl)
       ( inv
         ( ( ap
             ( concat' (f a) refl)
-            ( ( ( ap
-                  ( λ t → t ∙
-                    ( inv
-                      ( ap pr2 (eq-pair
-                      { s = (f a , g b)}
-                      { (g b , g b)}
-                      p refl))))
-                    ( ap-pr1-eq-pair p refl)) ∙
-                ( ap (λ t → p ∙ (inv t)) (ap-pr2-eq-pair p refl))) ∙
+            ( ( ap
+                ( λ t → t ∙ inv (ap pr2 (eq-pair p refl)))
+                ( ap-pr1-eq-pair p refl)) ∙
+              ( ap (λ t → p ∙ inv t) (ap-pr2-eq-pair p refl)) ∙
               ( right-unit))) ∙
           ( right-unit)))
 
@@ -471,8 +448,8 @@ triangle-map-fold-cone :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   (f : A → X) (g : B → X) (c : cone f g C) →
   ( gap (map-prod f g) (diagonal X) (fold-cone f g c)) ~
-  ( (map-fold-cone f g) ∘ (gap f g c))
-triangle-map-fold-cone f g (p , q , H) z = refl
+  ( map-fold-cone f g ∘ gap f g c)
+triangle-map-fold-cone f g c z = refl
 
 abstract
   is-pullback-fold-cone-is-pullback :
@@ -480,9 +457,9 @@ abstract
     (f : A → X) (g : B → X) (c : cone f g C) →
     is-pullback f g c →
     is-pullback (map-prod f g) (diagonal X) (fold-cone f g c)
-  is-pullback-fold-cone-is-pullback f g c is-pb-c =
+  is-pullback-fold-cone-is-pullback {X = X} f g c is-pb-c =
     is-equiv-comp-htpy
-      ( gap (map-prod f g) (diagonal _) (fold-cone f g c))
+      ( gap (map-prod f g) (diagonal X) (fold-cone f g c))
       ( map-fold-cone f g)
       ( gap f g c)
       ( triangle-map-fold-cone f g c)
@@ -495,9 +472,9 @@ abstract
     (f : A → X) (g : B → X) (c : cone f g C) →
     is-pullback (map-prod f g) (diagonal X) (fold-cone f g c) →
     is-pullback f g c
-  is-pullback-is-pullback-fold-cone f g c is-pb-fold =
+  is-pullback-is-pullback-fold-cone {X = X} f g c is-pb-fold =
     is-equiv-right-factor-htpy
-      ( gap (map-prod f g) (diagonal _) (fold-cone f g c))
+      ( gap (map-prod f g) (diagonal X) (fold-cone f g c))
       ( map-fold-cone f g)
       ( gap f g c)
       ( triangle-map-fold-cone f g c)
@@ -519,22 +496,22 @@ pr1 (prod-cone f g f' g' (p , q , H) (p' , q' , H')) = map-prod p p'
 pr1 (pr2 (prod-cone f g f' g' (p , q , H) (p' , q' , H'))) = map-prod q q'
 pr2 (pr2 (prod-cone f g f' g' (p , q , H) (p' , q' , H'))) =
   ( inv-htpy (map-prod-comp p p' f f')) ∙h
-  ( ( htpy-map-prod H H') ∙h
-    ( map-prod-comp q q' g g'))
+  ( htpy-map-prod H H') ∙h
+  ( map-prod-comp q q' g g')
 
 map-prod-cone :
   {l1 l2 l3 l1' l2' l3' : Level}
   {A : UU l1} {B : UU l2} {X : UU l3}
   {A' : UU l1'} {B' : UU l2'} {X' : UU l3'}
   (f : A → X) (g : B → X) (f' : A' → X') (g' : B' → X') →
-  (canonical-pullback f g) × (canonical-pullback f' g') →
-  canonical-pullback (map-prod f f') (map-prod g g')
+  (standard-pullback f g) × (standard-pullback f' g') →
+  standard-pullback (map-prod f f') (map-prod g g')
 map-prod-cone {A' = A'} {B'} f g f' g' =
   ( tot
     ( λ t →
       ( tot (λ s → eq-pair')) ∘
-      ( map-interchange-Σ-Σ (λ y p y' → Id (f' (pr2 t)) (g' y'))))) ∘
-  ( map-interchange-Σ-Σ (λ x t x' → Σ _ (λ y' → Id (f' x') (g' y'))))
+      ( map-interchange-Σ-Σ (λ y p y' → f' (pr2 t) ＝ g' y')))) ∘
+  ( map-interchange-Σ-Σ (λ x t x' → Σ B' (λ y' → f' x' ＝ g' y')))
 
 triangle-map-prod-cone :
   {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
@@ -542,10 +519,10 @@ triangle-map-prod-cone :
   {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {C' : UU l4'}
   (f : A → X) (g : B → X) (c : cone f g C)
   (f' : A' → X') (g' : B' → X') (c' : cone f' g' C') →
-  (gap (map-prod f f') (map-prod g g') (prod-cone f g f' g' c c')) ~
-  ((map-prod-cone f g f' g') ∘ (map-prod (gap f g c) (gap f' g' c')))
-triangle-map-prod-cone {B' = B'} f g (p , q , H) f' g' (p' , q' , H') (z , z') =
-  eq-pair-Σ refl (eq-pair-Σ refl right-unit)
+  ( gap (map-prod f f') (map-prod g g') (prod-cone f g f' g' c c')) ~
+  ( map-prod-cone f g f' g' ∘ map-prod (gap f g c) (gap f' g' c'))
+triangle-map-prod-cone f g c f' g' c' z =
+  eq-pair-Σ-eq-pr2 (eq-pair-Σ-eq-pr2 right-unit)
 
 abstract
   is-equiv-map-prod-cone :
@@ -556,25 +533,27 @@ abstract
     is-equiv (map-prod-cone f g f' g')
   is-equiv-map-prod-cone f g f' g' =
     is-equiv-comp
-      ( tot ( λ t →
-        ( tot (λ s → eq-pair')) ∘
-        ( map-interchange-Σ-Σ _)))
+      ( tot
+        ( λ t →
+          ( tot (λ s → eq-pair')) ∘
+          ( map-interchange-Σ-Σ _)))
       ( map-interchange-Σ-Σ _)
       ( is-equiv-map-interchange-Σ-Σ _)
       ( is-equiv-tot-is-fiberwise-equiv
-        ( λ t → is-equiv-comp
-          ( tot (λ s → eq-pair'))
-          ( map-interchange-Σ-Σ
-            ( λ y p y' → Id (f' (pr2 t)) (g' y')))
-          ( is-equiv-map-interchange-Σ-Σ _)
-          ( is-equiv-tot-is-fiberwise-equiv
-            ( λ s → is-equiv-comp
-              ( eq-pair')
-              ( id)
-              ( is-equiv-id)
-              ( is-equiv-eq-pair
-                ( map-prod f f' t)
-                ( map-prod g g' s))))))
+        ( λ t →
+          is-equiv-comp
+            ( tot (λ s → eq-pair'))
+            ( map-interchange-Σ-Σ
+              ( λ y p y' → f' (pr2 t) ＝ g' y'))
+            ( is-equiv-map-interchange-Σ-Σ _)
+            ( is-equiv-tot-is-fiberwise-equiv
+              ( λ s → is-equiv-comp
+                ( eq-pair')
+                ( id)
+                ( is-equiv-id)
+                ( is-equiv-eq-pair
+                  ( map-prod f f' t)
+                  ( map-prod g g' s))))))
 
 abstract
   is-pullback-prod-is-pullback-pair :
@@ -592,7 +571,7 @@ abstract
       ( map-prod-cone f g f' g')
       ( map-prod (gap f g c) (gap f' g' c'))
       ( triangle-map-prod-cone f g c f' g' c')
-      ( is-equiv-map-prod _ _ is-pb-c is-pb-c')
+      ( is-equiv-map-prod (gap f g c) (gap f' g' c') is-pb-c is-pb-c')
       ( is-equiv-map-prod-cone f g f' g')
 
 abstract
@@ -606,7 +585,7 @@ abstract
       ( map-prod f f')
       ( map-prod g g')
       ( prod-cone f g f' g' c c') →
-    canonical-pullback f' g' → is-pullback f g c
+    standard-pullback f' g' → is-pullback f g c
   is-pullback-left-factor-is-pullback-prod f g c f' g' c' is-pb-cc' t =
     is-equiv-left-factor-is-equiv-map-prod (gap f g c) (gap f' g' c') t
       ( is-equiv-right-factor-htpy
@@ -631,7 +610,7 @@ abstract
       ( map-prod f f')
       ( map-prod g g')
       ( prod-cone f g f' g' c c') →
-    canonical-pullback f g → is-pullback f' g' c'
+    standard-pullback f g → is-pullback f' g' c'
   is-pullback-right-factor-is-pullback-prod f g c f' g' c' is-pb-cc' t =
     is-equiv-right-factor-is-equiv-map-prod (gap f g c) (gap f' g' c') t
       ( is-equiv-right-factor-htpy
@@ -654,44 +633,43 @@ module _
   (Q : B → UU l4) (f : A → B) (g : (x : A) → (P x) → (Q (f x)))
   where
 
-  cone-map-Σ : cone f (pr1 {B = Q}) (Σ A P)
+  cone-map-Σ : cone f pr1 (Σ A P)
   pr1 cone-map-Σ = pr1
   pr1 (pr2 cone-map-Σ) = map-Σ Q f g
   pr2 (pr2 cone-map-Σ) = refl-htpy
 
   abstract
     is-pullback-is-fiberwise-equiv :
-      is-fiberwise-equiv g → is-pullback f (pr1 {B = Q}) cone-map-Σ
+      is-fiberwise-equiv g → is-pullback f pr1 cone-map-Σ
     is-pullback-is-fiberwise-equiv is-equiv-g =
       is-equiv-comp
-        ( gap f pr1 (cone-canonical-pullback-Σ f Q))
+        ( gap f pr1 (cone-standard-pullback-Σ f Q))
         ( tot g)
         ( is-equiv-tot-is-fiberwise-equiv is-equiv-g)
-        ( is-pullback-cone-canonical-pullback-Σ f Q)
+        ( is-pullback-cone-standard-pullback-Σ f Q)
 
   abstract
     universal-property-pullback-is-fiberwise-equiv :
       is-fiberwise-equiv g → {l : Level} →
-      universal-property-pullback l f (pr1 {B = Q}) cone-map-Σ
+      universal-property-pullback l f pr1 cone-map-Σ
     universal-property-pullback-is-fiberwise-equiv is-equiv-g =
       universal-property-pullback-is-pullback f pr1 cone-map-Σ
         ( is-pullback-is-fiberwise-equiv is-equiv-g)
 
   abstract
     is-fiberwise-equiv-is-pullback :
-      is-pullback f (pr1 {B = Q}) cone-map-Σ → is-fiberwise-equiv g
+      is-pullback f pr1 cone-map-Σ → is-fiberwise-equiv g
     is-fiberwise-equiv-is-pullback is-pullback-cone-map-Σ =
       is-fiberwise-equiv-is-equiv-tot
         ( is-equiv-right-factor
-          ( gap f pr1 (cone-canonical-pullback-Σ f Q))
+          ( gap f pr1 (cone-standard-pullback-Σ f Q))
           ( tot g)
-          ( is-pullback-cone-canonical-pullback-Σ f Q)
+          ( is-pullback-cone-standard-pullback-Σ f Q)
           ( is-pullback-cone-map-Σ))
 
   abstract
     is-fiberwise-equiv-universal-property-pullback :
-      ( {l : Level} →
-        universal-property-pullback l f (pr1 {B = Q}) cone-map-Σ) →
+      ( {l : Level} → universal-property-pullback l f pr1 cone-map-Σ) →
       is-fiberwise-equiv g
     is-fiberwise-equiv-universal-property-pullback up =
       is-fiberwise-equiv-is-pullback
@@ -707,14 +685,12 @@ module _
   where
 
   square-tot-map-fiber-cone :
-    ( (gap f g c) ∘ (map-equiv-total-fiber (pr1 c))) ~
-    ( (tot (λ a → tot (λ b → inv))) ∘ (tot (map-fiber-cone f g c)))
-  square-tot-map-fiber-cone (pair .((vertical-map-cone f g c) x) (x , refl)) =
-    eq-pair-Σ refl
-      ( eq-pair-Σ refl
-        ( inv
-          ( ( ap inv right-unit) ∙
-            ( inv-inv (coherence-square-cone f g c x)))))
+    ( gap f g c ∘ map-equiv-total-fiber (pr1 c)) ~
+    ( tot (λ a → tot (λ b → inv)) ∘ tot (map-fiber-cone f g c))
+  square-tot-map-fiber-cone (.(vertical-map-cone f g c x) , x , refl) =
+    eq-pair-Σ-eq-pr2
+      ( eq-pair-Σ-eq-pr2
+        ( inv (ap inv right-unit ∙ inv-inv (coherence-square-cone f g c x))))
 
   abstract
     is-fiberwise-equiv-map-fiber-cone-is-pullback :
@@ -889,3 +865,9 @@ module _
             ( λ t → is-fiberwise-equiv-map-fiber-cone-is-pullback
               (horizontal-map-cone f g c) h d is-pb-d (pr1 t))))
 ```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/foundation-core/universal-property-pullbacks.lagda.md b/src/foundation-core/universal-property-pullbacks.lagda.md
index d92c1a4a75..8e7a7c9f75 100644
--- a/src/foundation-core/universal-property-pullbacks.lagda.md
+++ b/src/foundation-core/universal-property-pullbacks.lagda.md
@@ -37,7 +37,25 @@ module _
   universal-property-pullback :
     (c : cone f g C) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
   universal-property-pullback c =
-    (C' : UU l) → is-equiv (cone-map f g {C' = C'} c)
+    (C' : UU l) → is-equiv (cone-map f g c {C'})
+
+module _
+  {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) {C : UU l4} (c : cone f g C)
+  where
+
+  map-universal-property-pullback :
+    ({l : Level} → universal-property-pullback l f g c) →
+    {C' : UU l5} (c' : cone f g C') → C' → C
+  map-universal-property-pullback up-c {C'} c' =
+    map-inv-is-equiv (up-c C') c'
+
+  compute-map-universal-property-pullback :
+    (up-c : {l : Level} → universal-property-pullback l f g c) →
+    {C' : UU l5} (c' : cone f g C') →
+    cone-map f g c (map-universal-property-pullback up-c c') ＝ c'
+  compute-map-universal-property-pullback up-c {C'} c' =
+    is-section-map-inv-is-equiv (up-c C') c'
 ```
 
 ## Properties
@@ -52,16 +70,18 @@ module _
   (h : C' → C) (KLM : htpy-cone f g (cone-map f g c h) c')
   where
 
+  inv-triangle-cone-cone :
+    {l6 : Level} (D : UU l6) →
+    cone-map f g c ∘ postcomp D h ~ cone-map f g c'
+  inv-triangle-cone-cone D k =
+    ap
+      ( λ t → cone-map f g t k)
+      ( eq-htpy-cone f g (cone-map f g c h) c' KLM)
+
   triangle-cone-cone :
     {l6 : Level} (D : UU l6) →
-    (cone-map f g {C' = D} c') ~ ((cone-map f g c) ∘ (λ (k : D → C') → h ∘ k))
-  triangle-cone-cone D k =
-    inv
-      ( ap
-        ( λ t → cone-map f g {C' = D} t k)
-        { x = (cone-map f g c h)}
-        { y = c'}
-        ( eq-htpy-cone f g (cone-map f g c h) c' KLM))
+    cone-map f g c' ~ cone-map f g c ∘ postcomp D h
+  triangle-cone-cone D k = inv (inv-triangle-cone-cone D k)
 
   abstract
     is-equiv-up-pullback-up-pullback :
@@ -70,13 +90,14 @@ module _
       is-equiv h
     is-equiv-up-pullback-up-pullback up up' =
       is-equiv-is-equiv-postcomp h
-        ( λ D → is-equiv-right-factor-htpy
-          ( cone-map f g {C' = D} c')
-          ( cone-map f g c)
-          ( λ (k : D → C') → h ∘ k)
-          ( triangle-cone-cone D)
-          ( up D)
-          ( up' D))
+        ( λ D →
+          is-equiv-right-factor-htpy
+            ( cone-map f g c')
+            ( cone-map f g c)
+            ( postcomp D h)
+            ( triangle-cone-cone D)
+            ( up D)
+            ( up' D))
 
   abstract
     up-pullback-up-pullback-is-equiv :
@@ -87,7 +108,7 @@ module _
       is-equiv-comp-htpy
         ( cone-map f g c')
         ( cone-map f g c)
-        ( λ k → h ∘ k)
+        ( postcomp D h)
         ( triangle-cone-cone D)
         ( is-equiv-postcomp-is-equiv h is-equiv-h D)
         ( up D)
@@ -101,7 +122,7 @@ module _
       is-equiv-left-factor-htpy
         ( cone-map f g c')
         ( cone-map f g c)
-        ( λ k → h ∘ k)
+        ( postcomp D h)
         ( triangle-cone-cone D)
         ( up' D)
         ( is-equiv-postcomp-is-equiv h is-equiv-h D)
@@ -123,7 +144,12 @@ module _
     uniqueness-universal-property-pullback up C' c' =
       is-contr-equiv'
         ( Σ (C' → C) (λ h → cone-map f g c h ＝ c'))
-        ( equiv-tot
-          ( λ h → extensionality-cone f g (cone-map f g c h) c'))
+        ( equiv-tot (λ h → extensionality-cone f g (cone-map f g c h) c'))
         ( is-contr-map-is-equiv (up C') c')
 ```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index d8ed51df47..c9860687d7 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -47,13 +47,16 @@ open import foundation.commuting-3-simplices-of-homotopies public
 open import foundation.commuting-3-simplices-of-maps public
 open import foundation.commuting-cubes-of-maps public
 open import foundation.commuting-hexagons-of-identifications public
+open import foundation.commuting-squares-of-homotopies public
 open import foundation.commuting-squares-of-identifications public
 open import foundation.commuting-squares-of-maps public
 open import foundation.commuting-triangles-of-homotopies public
 open import foundation.commuting-triangles-of-maps public
 open import foundation.complements public
 open import foundation.complements-subtypes public
+open import foundation.composite-maps-in-towers public
 open import foundation.cones-over-cospans public
+open import foundation.cones-over-towers public
 open import foundation.conjunction public
 open import foundation.connected-components public
 open import foundation.connected-components-universes public
@@ -84,6 +87,7 @@ open import foundation.dependent-epimorphisms public
 open import foundation.dependent-identifications public
 open import foundation.dependent-pair-types public
 open import foundation.dependent-sequences public
+open import foundation.dependent-towers public
 open import foundation.descent-coproduct-types public
 open import foundation.descent-dependent-pair-types public
 open import foundation.descent-empty-types public
@@ -117,6 +121,7 @@ open import foundation.equivalence-induction public
 open import foundation.equivalence-relations public
 open import foundation.equivalences public
 open import foundation.equivalences-maybe public
+open import foundation.equivalences-towers public
 open import foundation.exclusive-disjunction public
 open import foundation.existential-quantification public
 open import foundation.exponents-set-quotients public
@@ -137,6 +142,8 @@ open import foundation.functoriality-dependent-pair-types public
 open import foundation.functoriality-fibers-of-maps public
 open import foundation.functoriality-function-types public
 open import foundation.functoriality-propositional-truncation public
+open import foundation.functoriality-pullbacks public
+open import foundation.functoriality-sequential-limits public
 open import foundation.functoriality-set-quotients public
 open import foundation.functoriality-set-truncation public
 open import foundation.functoriality-truncation public
@@ -185,6 +192,7 @@ open import foundation.mere-equivalences public
 open import foundation.monomorphisms public
 open import foundation.morphisms-binary-relations public
 open import foundation.morphisms-cospans public
+open import foundation.morphisms-towers public
 open import foundation.multisubsets public
 open import foundation.multivariable-correspondences public
 open import foundation.multivariable-decidable-relations public
@@ -236,6 +244,7 @@ open import foundation.russells-paradox public
 open import foundation.sections public
 open import foundation.separated-types public
 open import foundation.sequences public
+open import foundation.sequential-limits public
 open import foundation.set-presented-types public
 open import foundation.set-quotients public
 open import foundation.set-truncations public
@@ -271,6 +280,8 @@ open import foundation.symmetric-identity-types public
 open import foundation.symmetric-operations public
 open import foundation.tight-apartness-relations public
 open import foundation.torsorial-type-families public
+open import foundation.towers public
+open import foundation.transfinite-cocomposition-of-maps public
 open import foundation.transport-along-equivalences public
 open import foundation.transport-along-higher-identifications public
 open import foundation.transport-along-identifications public
@@ -318,6 +329,7 @@ open import foundation.universal-property-maybe public
 open import foundation.universal-property-propositional-truncation public
 open import foundation.universal-property-propositional-truncation-into-sets public
 open import foundation.universal-property-pullbacks public
+open import foundation.universal-property-sequential-limits public
 open import foundation.universal-property-set-quotients public
 open import foundation.universal-property-set-truncation public
 open import foundation.universal-property-truncation public
diff --git a/src/foundation/commuting-squares-of-homotopies.lagda.md b/src/foundation/commuting-squares-of-homotopies.lagda.md
new file mode 100644
index 0000000000..c14f9bbf33
--- /dev/null
+++ b/src/foundation/commuting-squares-of-homotopies.lagda.md
@@ -0,0 +1,45 @@
+# Commuting squares of homotopies
+
+```agda
+module foundation.commuting-squares-of-homotopies where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import foundation-core.homotopies
+```
+
+</details>
+
+## Idea
+
+A square of [homotopies](foundation-core.homotopies.md)
+
+```text
+          top
+      f ------> g
+      |         |
+ left |         | right
+      v         v
+      z ------> i
+        bottom
+```
+
+is said to **commute** if there is a homotopy `left ∙h bottom ~ top ∙h right`.
+Such a homotopy is called a **coherence** of the square.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
+  where
+
+  coherence-square-homotopies :
+    (left : f ~ h) (bottom : h ~ i) (top : f ~ g) (right : g ~ i) → UU (l1 ⊔ l2)
+  coherence-square-homotopies left bottom top right =
+    left ∙h bottom ~ top ∙h right
+```
diff --git a/src/foundation/commuting-squares-of-identifications.lagda.md b/src/foundation/commuting-squares-of-identifications.lagda.md
index 471bbd126f..e84892d6ba 100644
--- a/src/foundation/commuting-squares-of-identifications.lagda.md
+++ b/src/foundation/commuting-squares-of-identifications.lagda.md
@@ -18,7 +18,7 @@ open import foundation-core.identity-types
 
 ## Idea
 
-A square of identifications
+A square of [identifications](foundation-core.identity-types.md)
 
 ```text
           top
diff --git a/src/foundation/commuting-triangles-of-maps.lagda.md b/src/foundation/commuting-triangles-of-maps.lagda.md
index 9ddf15431b..58649c5f12 100644
--- a/src/foundation/commuting-triangles-of-maps.lagda.md
+++ b/src/foundation/commuting-triangles-of-maps.lagda.md
@@ -33,16 +33,16 @@ A triangle of maps
      X
 ```
 
-is said to commute if there is a homotopy between the map on the left and the
-composite map.
+is said to **commute** if there is a [homotopy](foundation-core.homotopies.md)
+between the map on the left and the composite map.
 
 ## Properties
 
 ### Top map is an equivalence
 
-If the top map is an equivalence, then there is an equivalence between the
-coherence triangle with the map of the equivalence as with the inverse map of
-the equivalence.
+If the top map is an [equivalence](foundation-core.equivalences.md), then there
+is an equivalence between the coherence triangle with the map of the equivalence
+as with the inverse map of the equivalence.
 
 ```agda
 module _
diff --git a/src/foundation/composite-maps-in-towers.lagda.md b/src/foundation/composite-maps-in-towers.lagda.md
new file mode 100644
index 0000000000..63f2583cb4
--- /dev/null
+++ b/src/foundation/composite-maps-in-towers.lagda.md
@@ -0,0 +1,59 @@
+# Composite maps in towers
+
+```agda
+module foundation.composite-maps-in-towers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-towers
+open import foundation.towers
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Given a ([dependent](foundation.dependent-towers.md))
+[tower](foundation.towers.md) `A`, we can extract the **composite map from
+`Aₙ₊ᵣ` to `Aₙ`**.
+
+## Definitions
+
+### Composite maps in towers
+
+```agda
+comp-map-tower :
+  {l : Level} (A : tower l) (n r : ℕ) → type-tower A (n +ℕ r) → type-tower A n
+comp-map-tower A n zero-ℕ = id
+comp-map-tower A n (succ-ℕ r) = comp-map-tower A n r ∘ map-tower A (n +ℕ r)
+```
+
+### Composite maps in dependent towers
+
+```agda
+comp-map-dependent-tower :
+  {l1 l2 : Level} {A : tower l1} (B : dependent-tower l2 A)
+  (n r : ℕ) (x : type-tower A (n +ℕ r)) →
+  family-dependent-tower B (n +ℕ r) x →
+  family-dependent-tower B n (comp-map-tower A n r x)
+comp-map-dependent-tower B n zero-ℕ x y = y
+comp-map-dependent-tower {A = A} B n (succ-ℕ r) x y =
+  comp-map-dependent-tower B n r
+    ( map-tower A (n +ℕ r) x)
+    ( map-dependent-tower B (n +ℕ r) x y)
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
diff --git a/src/foundation/cones-over-cospans.lagda.md b/src/foundation/cones-over-cospans.lagda.md
index 8ba8badbec..65a6e5a8ed 100644
--- a/src/foundation/cones-over-cospans.lagda.md
+++ b/src/foundation/cones-over-cospans.lagda.md
@@ -27,9 +27,9 @@ open import foundation-core.whiskering-homotopies
 
 ## Idea
 
-A cone on a cospan `A --f--> X <--g-- B` with vertex `C` is a triple `(p,q,H)`
-consisting of a map `p : C → A`, a map `q : C → B`, and a homotopy `H`
-witnessing that the square
+A **cone over a [cospan](foundation.cospans.md)** `A -f-> X <-g- B` with domain
+`C` is a triple `(p, q, H)` consisting of a map `p : C → A`, a map `q : C → B`,
+and a homotopy `H` witnessing that the square
 
 ```text
       q
@@ -45,11 +45,7 @@ commutes.
 
 ## Definitions
 
-### Cones on cospans
-
-A cone on a cospan with a vertex C is a pair of functions from C into the
-domains of the maps in the cospan, equipped with a homotopy witnessing that the
-resulting square commutes.
+### Cones over cospans
 
 ```agda
 module _
@@ -76,7 +72,7 @@ module _
   coherence-square-cone = pr2 (pr2 c)
 ```
 
-### Dependent cones
+### Dependent cones over cospans
 
 ```agda
 cone-family :
@@ -95,13 +91,7 @@ cone-family {C = C} PX {f = f} {g} f' g' c PC =
     ( PC x)
 ```
 
-### Identifications of cones
-
-Next we characterize the identity type of the type of cones with a given vertex
-C. Note that in the definition of htpy-cone we do not use pattern matching on
-the cones c and c'. This is to ensure that the type htpy-cone f g c c' is a
-Σ-type for any c and c', not just for c and c' of the form (p , q , H) and (p' ,
-q' , H') respectively.
+### Identifications of cones over cospans
 
 ```agda
 module _
@@ -110,7 +100,8 @@ module _
   where
 
   coherence-htpy-cone :
-    (c c' : cone f g C) (K : vertical-map-cone f g c ~ vertical-map-cone f g c')
+    (c c' : cone f g C)
+    (K : vertical-map-cone f g c ~ vertical-map-cone f g c')
     (L : horizontal-map-cone f g c ~ horizontal-map-cone f g c') → UU (l4 ⊔ l3)
   coherence-htpy-cone c c' K L =
     ( coherence-square-cone f g c ∙h (g ·l L)) ~
@@ -157,21 +148,20 @@ module _
   pr1 (extensionality-cone c c') = htpy-eq-cone c c'
   pr2 (extensionality-cone c c') = is-equiv-htpy-eq-cone c c'
 
-  eq-htpy-cone : (c c' : cone f g C) → htpy-cone c c' → (c ＝ c')
+  eq-htpy-cone : (c c' : cone f g C) → htpy-cone c c' → c ＝ c'
   eq-htpy-cone c c' = map-inv-equiv (extensionality-cone c c')
 ```
 
-### Precomposing cones
+### Precomposing cones over cospans with a map
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
   (f : A → X) (g : B → X)
   where
 
   cone-map :
-    {l4 l5 : Level} {C : UU l4} {C' : UU l5} →
-    cone f g C → (C' → C) → cone f g C'
+    {C : UU l4} → cone f g C → {C' : UU l5} → (C' → C) → cone f g C'
   pr1 (cone-map c h) = vertical-map-cone f g c ∘ h
   pr1 (pr2 (cone-map c h)) = horizontal-map-cone f g c ∘ h
   pr2 (pr2 (cone-map c h)) = coherence-square-cone f g c ·r h
@@ -227,18 +217,19 @@ module _
       ( coherence-square-cone f g c)
 ```
 
-### The swapping function on cones
+### The swapping function on cones over cospans
 
 ```agda
 swap-cone :
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   (f : A → X) (g : B → X) → cone f g C → cone g f C
 pr1 (swap-cone f g c) = horizontal-map-cone f g c
 pr1 (pr2 (swap-cone f g c)) = vertical-map-cone f g c
 pr2 (pr2 (swap-cone f g c)) = inv-htpy (coherence-square-cone f g c)
 ```
 
-### Parallel cones
+### Parallel cones over cospans
 
 ```agda
 module _
@@ -271,3 +262,9 @@ module _
     Σ ( vertical-map-cone f g c ~ vertical-map-cone f' g' c')
       ( fam-htpy-parallel-cone c c')
 ```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/foundation/cones-over-towers.lagda.md b/src/foundation/cones-over-towers.lagda.md
new file mode 100644
index 0000000000..dcece81a4f
--- /dev/null
+++ b/src/foundation/cones-over-towers.lagda.md
@@ -0,0 +1,146 @@
+# Cones over towers
+
+```agda
+module foundation.cones-over-towers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-homotopies
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-function-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopy-induction
+open import foundation.structure-identity-principle
+open import foundation.towers
+open import foundation.universe-levels
+
+open import foundation-core.commuting-triangles-of-maps
+open import foundation-core.contractible-types
+open import foundation-core.equivalences
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.whiskering-homotopies
+```
+
+</details>
+
+## Idea
+
+A **cone over a [tower](foundation.towers.md) `A` with domain `X`** is a
+[sequence](foundation.dependent-sequences.md) of functions from `X` into the
+sequence of types of `A` such that the triangles
+
+```text
+     X
+    / \
+   /   \
+  v     v
+ Aₙ₊₁ -> Aₙ
+```
+
+[commute](foundation-core.commuting-triangles-of-maps.md) for all `n : ℕ`.
+
+## Definitions
+
+### Cones over towers
+
+```agda
+module _
+  {l1 : Level} (A : tower l1)
+  where
+
+  cone-tower : {l2 : Level} → UU l2 → UU (l1 ⊔ l2)
+  cone-tower X =
+    Σ ( (n : ℕ) → X → type-tower A n)
+      ( λ f →
+        (n : ℕ) → coherence-triangle-maps (f n) (map-tower A n) (f (succ-ℕ n)))
+
+  map-cone-tower :
+    {l2 : Level} {X : UU l2} → cone-tower X → (n : ℕ) → X → type-tower A n
+  map-cone-tower = pr1
+
+  coherence-cone-tower :
+    {l2 : Level} {X : UU l2} (c : cone-tower X) (n : ℕ) →
+    coherence-triangle-maps
+      ( map-cone-tower c n)
+      ( map-tower A n)
+      ( map-cone-tower c (succ-ℕ n))
+  coherence-cone-tower = pr2
+```
+
+### Identifications of cones over towers of types
+
+```agda
+module _
+  {l1 l2 : Level} (A : tower l1) {X : UU l2}
+  where
+
+  coherence-htpy-cone-tower :
+    (c c' : cone-tower A X) →
+    ((n : ℕ) → map-cone-tower A c n ~ map-cone-tower A c' n) → UU (l1 ⊔ l2)
+  coherence-htpy-cone-tower c c' H =
+    (n : ℕ) →
+    ( coherence-cone-tower A c n ∙h (map-tower A n ·l H (succ-ℕ n))) ~
+    ( H n ∙h coherence-cone-tower A c' n)
+
+  htpy-cone-tower : cone-tower A X → cone-tower A X → UU (l1 ⊔ l2)
+  htpy-cone-tower c c' =
+    Σ ( (n : ℕ) → map-cone-tower A c n ~ map-cone-tower A c' n)
+      ( coherence-htpy-cone-tower c c')
+
+  refl-htpy-cone-tower : (c : cone-tower A X) → htpy-cone-tower c c
+  pr1 (refl-htpy-cone-tower c) n = refl-htpy
+  pr2 (refl-htpy-cone-tower c) n = right-unit-htpy
+
+  htpy-eq-cone-tower : (c c' : cone-tower A X) → c ＝ c' → htpy-cone-tower c c'
+  htpy-eq-cone-tower c .c refl = refl-htpy-cone-tower c
+
+  is-contr-total-htpy-cone-tower :
+    (c : cone-tower A X) → is-contr (Σ (cone-tower A X) (htpy-cone-tower c))
+  is-contr-total-htpy-cone-tower c =
+    is-contr-total-Eq-structure
+      ( λ x z → coherence-htpy-cone-tower c (x , z))
+      ( is-contr-total-binary-htpy (map-cone-tower A c))
+      ( map-cone-tower A c , (λ n → refl-htpy))
+      ( is-contr-total-Eq-Π
+        ( λ n → (coherence-cone-tower A c n ∙h refl-htpy) ~_)
+        ( λ n → is-contr-total-htpy (coherence-cone-tower A c n ∙h refl-htpy)))
+
+  is-equiv-htpy-eq-cone-tower :
+    (c c' : cone-tower A X) → is-equiv (htpy-eq-cone-tower c c')
+  is-equiv-htpy-eq-cone-tower c =
+    fundamental-theorem-id
+      ( is-contr-total-htpy-cone-tower c)
+      ( htpy-eq-cone-tower c)
+
+  extensionality-cone-tower :
+    (c c' : cone-tower A X) → (c ＝ c') ≃ htpy-cone-tower c c'
+  pr1 (extensionality-cone-tower c c') = htpy-eq-cone-tower c c'
+  pr2 (extensionality-cone-tower c c') = is-equiv-htpy-eq-cone-tower c c'
+
+  eq-htpy-cone-tower : (c c' : cone-tower A X) → htpy-cone-tower c c' → c ＝ c'
+  eq-htpy-cone-tower c c' = map-inv-equiv (extensionality-cone-tower c c')
+```
+
+### Precomposing cones over towers with a map
+
+```agda
+module _
+  {l1 l2 l3 : Level} (A : tower l1) {X : UU l2} {Y : UU l3}
+  where
+
+  cone-map-tower : cone-tower A X → (Y → X) → cone-tower A Y
+  pr1 (cone-map-tower c f) n x = map-cone-tower A c n (f x)
+  pr2 (cone-map-tower c f) n x = coherence-cone-tower A c n (f x)
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
diff --git a/src/foundation/cospans.lagda.md b/src/foundation/cospans.lagda.md
index e64c00246e..f5065c82a8 100644
--- a/src/foundation/cospans.lagda.md
+++ b/src/foundation/cospans.lagda.md
@@ -139,3 +139,9 @@ module _
 ## See also
 
 - The formal dual of cospans is [spans](foundation.spans.md).
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/foundation/dependent-identifications.lagda.md b/src/foundation/dependent-identifications.lagda.md
index 47e0067e56..80539b1d9c 100644
--- a/src/foundation/dependent-identifications.lagda.md
+++ b/src/foundation/dependent-identifications.lagda.md
@@ -12,13 +12,13 @@ open import foundation-core.dependent-identifications public
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.transport-along-higher-identifications
-open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
+open import foundation-core.transport-along-identifications
 ```
 
 </details>
diff --git a/src/foundation/dependent-towers.lagda.md b/src/foundation/dependent-towers.lagda.md
new file mode 100644
index 0000000000..a76ae07a78
--- /dev/null
+++ b/src/foundation/dependent-towers.lagda.md
@@ -0,0 +1,157 @@
+# Dependent towers of types
+
+```agda
+module foundation.dependent-towers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.towers
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+open import foundation-core.homotopies
+```
+
+</details>
+
+## Idea
+
+A **dependent tower** `B` over a base [tower](foundation.towers.md) `A` is a
+[sequence](foundation.sequences.md) of families over each `Aₙ` together with
+maps of fibers
+
+```text
+  gₙ : (xₙ₊₁ : Aₙ₊₁) → Bₙ₊₁(xₙ₊₁) → Bₙ(fₙ(xₙ₊₁)),
+```
+
+where `f` is the sequence of maps of the base tower, giving a dependent
+sequential diagram of maps that extend infinitely to the left:
+
+```text
+     g₃      g₂      g₁      g₀
+  ⋯ ---> B₃ ---> B₂ ---> B₁ ---> B₀.
+```
+
+## Definitions
+
+### Dependent towers of types
+
+```agda
+sequence-map-dependent-tower :
+  {l1 l2 : Level} (A : tower l1) →
+  ((n : ℕ) → type-tower A n → UU l2) → UU (l1 ⊔ l2)
+sequence-map-dependent-tower A B =
+  (n : ℕ) (x : type-tower A (succ-ℕ n)) → B (succ-ℕ n) x → B n (map-tower A n x)
+
+dependent-tower : {l1 : Level} (l2 : Level) (A : tower l1) → UU (l1 ⊔ lsuc l2)
+dependent-tower l2 A =
+  Σ ((n : ℕ) → type-tower A n → UU l2) (sequence-map-dependent-tower A)
+
+family-dependent-tower :
+  {l1 l2 : Level} {A : tower l1} →
+  dependent-tower l2 A → ((n : ℕ) → type-tower A n → UU l2)
+family-dependent-tower = pr1
+
+map-dependent-tower :
+  {l1 l2 : Level} {A : tower l1} (B : dependent-tower l2 A) →
+  (n : ℕ) (x : type-tower A (succ-ℕ n)) →
+  family-dependent-tower B (succ-ℕ n) x →
+  family-dependent-tower B n (map-tower A n x)
+map-dependent-tower = pr2
+```
+
+### Constant dependent towers of types
+
+```agda
+const-dependent-tower :
+    {l1 l2 : Level} (A : tower l1) → tower l2 → dependent-tower l2 A
+pr1 (const-dependent-tower A B) n _ = type-tower B n
+pr2 (const-dependent-tower A B) n _ = map-tower B n
+```
+
+### Sections of a dependent tower
+
+A **section of a dependent tower `(B , g)` over `(A , f)`** is a choice of
+sections `hₙ` of each `Bₙ` that vary naturally over `A`, by which we mean that
+the diagrams
+
+```text
+          gₙ
+    Bₙ₊₁ ---> Bₙ
+    ^         ^
+hₙ₊₁|         | hₙ
+    |         |
+    Aₙ₊₁ ---> Aₙ
+          fₙ
+```
+
+commute for each `n : ℕ`.
+
+```agda
+module _
+  {l1 l2 : Level} (A : tower l1) (B : dependent-tower l2 A)
+  where
+
+  naturality-section-dependent-tower :
+    (h : (n : ℕ) (x : type-tower A n) → family-dependent-tower B n x)
+    (n : ℕ) → UU (l1 ⊔ l2)
+  naturality-section-dependent-tower h n =
+    h n ∘ map-tower A n ~ map-dependent-tower B n _ ∘ h (succ-ℕ n)
+
+  section-dependent-tower : UU (l1 ⊔ l2)
+  section-dependent-tower =
+    Σ ( (n : ℕ) (x : type-tower A n) → family-dependent-tower B n x)
+      ( λ h → (n : ℕ) → naturality-section-dependent-tower h n)
+
+  map-section-dependent-tower :
+    section-dependent-tower →
+    (n : ℕ) (x : type-tower A n) → family-dependent-tower B n x
+  map-section-dependent-tower = pr1
+
+  naturality-map-section-dependent-tower :
+    (f : section-dependent-tower) (n : ℕ) →
+    naturality-section-dependent-tower (map-section-dependent-tower f) n
+  naturality-map-section-dependent-tower = pr2
+```
+
+## Operations
+
+### Right shifting a dependent tower
+
+We can **right shift** a dependent tower of types by forgetting the first terms.
+
+```agda
+right-shift-dependent-tower :
+  {l1 l2 : Level} {A : tower l1} →
+  dependent-tower l2 A → dependent-tower l2 (right-shift-tower A)
+pr1 (right-shift-dependent-tower B) n = family-dependent-tower B (succ-ℕ n)
+pr2 (right-shift-dependent-tower B) n = map-dependent-tower B (succ-ℕ n)
+```
+
+### Left shifting a dependent tower
+
+We can **left shift** a dependent tower of types by padding it with the
+[terminal type](foundation.unit-type.md) `unit`.
+
+```agda
+left-shift-dependent-tower :
+    {l1 l2 : Level} {A : tower l1} →
+  dependent-tower l2 A → dependent-tower l2 (left-shift-tower A)
+pr1 (left-shift-dependent-tower {l2 = l2} B) zero-ℕ x = raise-unit l2
+pr1 (left-shift-dependent-tower B) (succ-ℕ n) = family-dependent-tower B n
+pr2 (left-shift-dependent-tower B) zero-ℕ _ = raise-terminal-map
+pr2 (left-shift-dependent-tower B) (succ-ℕ n) = map-dependent-tower B n
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
diff --git a/src/foundation/diagonals-of-maps.lagda.md b/src/foundation/diagonals-of-maps.lagda.md
index 258021640b..48305185ff 100644
--- a/src/foundation/diagonals-of-maps.lagda.md
+++ b/src/foundation/diagonals-of-maps.lagda.md
@@ -33,7 +33,7 @@ open import foundation-core.truncation-levels
 ```agda
 diagonal-map :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
-  A → canonical-pullback f f
+  A → standard-pullback f f
 pr1 (diagonal-map f x) = x
 pr1 (pr2 (diagonal-map f x)) = x
 pr2 (pr2 (diagonal-map f x)) = refl
@@ -46,14 +46,14 @@ pr2 (pr2 (diagonal-map f x)) = refl
 ```agda
 fiber-ap-fiber-diagonal-map :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
-  (t : canonical-pullback f f) →
+  (t : standard-pullback f f) →
   (fiber (diagonal-map f) t) → (fiber (ap f) (pr2 (pr2 t)))
 pr1 (fiber-ap-fiber-diagonal-map f .(diagonal-map f z) (z , refl)) = refl
 pr2 (fiber-ap-fiber-diagonal-map f .(diagonal-map f z) (z , refl)) = refl
 
 fiber-diagonal-map-fiber-ap :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
-  (t : canonical-pullback f f) →
+  (t : standard-pullback f f) →
   (fiber (ap f) (pr2 (pr2 t))) → (fiber (diagonal-map f) t)
 pr1 (fiber-diagonal-map-fiber-ap f (x , .x , .(ap f refl)) (refl , refl)) = x
 pr2 (fiber-diagonal-map-fiber-ap f (x , .x , .(ap f refl)) (refl , refl)) = refl
@@ -61,7 +61,7 @@ pr2 (fiber-diagonal-map-fiber-ap f (x , .x , .(ap f refl)) (refl , refl)) = refl
 abstract
   is-section-fiber-diagonal-map-fiber-ap :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
-    (t : canonical-pullback f f) →
+    (t : standard-pullback f f) →
     ((fiber-ap-fiber-diagonal-map f t) ∘ (fiber-diagonal-map-fiber-ap f t)) ~ id
   is-section-fiber-diagonal-map-fiber-ap f (x , .x , .refl) (refl , refl) =
     refl
@@ -69,7 +69,7 @@ abstract
 abstract
   is-retraction-fiber-diagonal-map-fiber-ap :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
-    (t : canonical-pullback f f) →
+    (t : standard-pullback f f) →
     ((fiber-diagonal-map-fiber-ap f t) ∘ (fiber-ap-fiber-diagonal-map f t)) ~ id
   is-retraction-fiber-diagonal-map-fiber-ap f .(x , x , refl) (x , refl) =
     refl
@@ -77,7 +77,7 @@ abstract
 abstract
   is-equiv-fiber-ap-fiber-diagonal-map :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
-    (t : canonical-pullback f f) →
+    (t : standard-pullback f f) →
     is-equiv (fiber-ap-fiber-diagonal-map f t)
   is-equiv-fiber-ap-fiber-diagonal-map f t =
     is-equiv-is-invertible
diff --git a/src/foundation/equality-fibers-of-maps.lagda.md b/src/foundation/equality-fibers-of-maps.lagda.md
index 95464bc6a0..c4ccf1aa1a 100644
--- a/src/foundation/equality-fibers-of-maps.lagda.md
+++ b/src/foundation/equality-fibers-of-maps.lagda.md
@@ -119,6 +119,13 @@ module _
         ( is-equiv-tr (fiber (ap f)) right-unit)
 ```
 
+## 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}}
+
 ## See also
 
 - Equality proofs in dependent pair types are characterized in
diff --git a/src/foundation/equivalence-relations.lagda.md b/src/foundation/equivalence-relations.lagda.md
index 63a75e84f5..29d4a3c6a3 100644
--- a/src/foundation/equivalence-relations.lagda.md
+++ b/src/foundation/equivalence-relations.lagda.md
@@ -290,7 +290,6 @@ module _
     ( pr2
       ( pr2
         ( relate-same-elements-eq-rel-partition-Equivalence-Relation x y) r)) =
-
     make-is-in-block-partition
       ( partition-Equivalence-Relation R)
       ( inhabited-subtype-equivalence-class R (class R x))
@@ -301,7 +300,6 @@ module _
     ( pr2
       ( pr2
         ( relate-same-elements-eq-rel-partition-Equivalence-Relation x y) r)) =
-
     make-is-in-block-partition
       ( partition-Equivalence-Relation R)
       ( inhabited-subtype-equivalence-class R (class R x))
diff --git a/src/foundation/equivalences-towers.lagda.md b/src/foundation/equivalences-towers.lagda.md
new file mode 100644
index 0000000000..081ff2cb1a
--- /dev/null
+++ b/src/foundation/equivalences-towers.lagda.md
@@ -0,0 +1,104 @@
+# Equivalences of towers of types
+
+```agda
+module foundation.equivalences-towers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-function-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopy-induction
+open import foundation.morphisms-towers
+open import foundation.structure-identity-principle
+open import foundation.towers
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import foundation-core.contractible-types
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+An **equivalence of towers** `A ≃ B` is a commuting diagram of the form
+
+```text
+  ⋯ ----> Aₙ₊₁ ----> Aₙ ----> ⋯ ----> A₁ ----> A₀
+           |         |       |       |        |
+  ⋯        |         |       ⋯       |        |
+           v         v       v       v        v
+  ⋯ ----> Bₙ₊₁ ----> Bₙ ----> ⋯ ----> B₁ ----> B₀.
+```
+
+where every vertical map is an [equivalence](foundation-core.equivalences.md).
+
+## Definitions
+
+```agda
+equiv-tower :
+  {l1 l2 : Level} (A : tower l1) (B : tower l2) → UU (l1 ⊔ l2)
+equiv-tower A B =
+  Σ ( (n : ℕ) → type-tower A n ≃ type-tower B n)
+    ( λ e → (n : ℕ) → naturality-hom-tower A B (map-equiv ∘ e) n)
+
+hom-equiv-tower :
+  {l1 l2 : Level} (A : tower l1) (B : tower l2) →
+  equiv-tower A B → hom-tower A B
+pr1 (hom-equiv-tower A B e) n = pr1 (pr1 e n)
+pr2 (hom-equiv-tower A B e) = pr2 e
+```
+
+## Properties
+
+### Characterizing equality of towers
+
+```agda
+id-equiv-tower :
+  {l : Level} (A : tower l) → equiv-tower A A
+pr1 (id-equiv-tower A) n = id-equiv
+pr2 (id-equiv-tower A) n = refl-htpy
+
+equiv-eq-tower :
+  {l : Level} (A B : tower l) → A ＝ B → equiv-tower A B
+equiv-eq-tower A .A refl = id-equiv-tower A
+
+is-contr-total-equiv-tower :
+  {l : Level} (A : tower l) →
+  is-contr (Σ (tower l) (equiv-tower A))
+is-contr-total-equiv-tower A =
+  is-contr-total-Eq-structure _
+    ( is-contr-total-Eq-Π
+      ( λ n → type-tower A n ≃_)
+      ( λ n → is-contr-total-equiv (type-tower A n)))
+    ( type-tower A , λ n → id-equiv)
+    ( is-contr-total-Eq-Π _
+      ( λ n → is-contr-total-htpy (map-tower A n)))
+
+is-equiv-equiv-eq-tower :
+  {l : Level} (A B : tower l) → is-equiv (equiv-eq-tower A B)
+is-equiv-equiv-eq-tower A =
+  fundamental-theorem-id
+    ( is-contr-total-equiv-tower A)
+    ( equiv-eq-tower A)
+
+eq-equiv-tower :
+  {l : Level} {A B : tower l} → equiv-tower A B → A ＝ B
+eq-equiv-tower {A = A} {B} = map-inv-is-equiv (is-equiv-equiv-eq-tower A B)
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
diff --git a/src/foundation/fiber-inclusions.lagda.md b/src/foundation/fiber-inclusions.lagda.md
index 391888d979..c424825e33 100644
--- a/src/foundation/fiber-inclusions.lagda.md
+++ b/src/foundation/fiber-inclusions.lagda.md
@@ -38,8 +38,8 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-Given a family `B` of types over `A` and an element `a : A`, then the fiber
-inclusion of `B` at a is a map `B a → Σ A B`.
+Given a family `B` of types over `A` and an element `a : A`, then **the fiber
+inclusion** of `B` at `a` is a map `B a → Σ A B`.
 
 ## Definition
 
diff --git a/src/foundation/fibers-of-maps.lagda.md b/src/foundation/fibers-of-maps.lagda.md
index 7dcbc1e59f..94b6f353dc 100644
--- a/src/foundation/fibers-of-maps.lagda.md
+++ b/src/foundation/fibers-of-maps.lagda.md
@@ -58,3 +58,10 @@ module _
         ( cone-fiber)
         ( is-pullback-cone-fiber)
 ```
+
+## 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}}
diff --git a/src/foundation/functoriality-dependent-pair-types.lagda.md b/src/foundation/functoriality-dependent-pair-types.lagda.md
index 4c68002608..d43334be2d 100644
--- a/src/foundation/functoriality-dependent-pair-types.lagda.md
+++ b/src/foundation/functoriality-dependent-pair-types.lagda.md
@@ -65,21 +65,25 @@ module _
           ( g' (horizontal-map-cone f g c z))
           ( c' z))
 
-  map-canonical-pullback-tot-cone-cone-fam-right-factor :
-    Σ ( canonical-pullback f g)
-      ( λ t → canonical-pullback ((tr PX (π₃ t)) ∘ (f' (π₁ t))) (g' (π₂ t))) →
+  map-standard-pullback-tot-cone-cone-fam-right-factor :
+    Σ ( standard-pullback f g)
+      ( λ t →
+        standard-pullback
+          ( tr PX (coherence-square-standard-pullback t) ∘
+            f' (vertical-map-standard-pullback t))
+          ( g' (horizontal-map-standard-pullback t))) →
     Σ ( Σ A PA)
       ( λ aa' → Σ (Σ B (λ b → Id (f (pr1 aa')) (g b)))
         ( λ bα → Σ (PB (pr1 bα))
           ( λ b' → Id
             ( tr PX (pr2 bα) (f' (pr1 aa') (pr2 aa')))
             ( g' (pr1 bα) b'))))
-  map-canonical-pullback-tot-cone-cone-fam-right-factor =
+  map-standard-pullback-tot-cone-cone-fam-right-factor =
     map-interchange-Σ-Σ
       ( λ a bα a' → Σ (PB (pr1 bα))
         ( λ b' → Id (tr PX (pr2 bα) (f' a a')) (g' (pr1 bα) b')))
 
-  map-canonical-pullback-tot-cone-cone-fam-left-factor :
+  map-standard-pullback-tot-cone-cone-fam-left-factor :
     (aa' : Σ A PA) →
     Σ (Σ B (λ b → Id (f (pr1 aa')) (g b)))
       ( λ bα → Σ (PB (pr1 bα))
@@ -89,49 +93,54 @@ module _
     Σ ( Σ B PB)
       ( λ bb' → Σ (Id (f (pr1 aa')) (g (pr1 bb')))
         ( λ α → Id (tr PX α (f' (pr1 aa') (pr2 aa'))) (g' (pr1 bb') (pr2 bb'))))
-  map-canonical-pullback-tot-cone-cone-fam-left-factor aa' =
+  map-standard-pullback-tot-cone-cone-fam-left-factor aa' =
     ( map-interchange-Σ-Σ
       ( λ b α b' → Id (tr PX α (f' (pr1 aa') (pr2 aa'))) (g' b b')))
 
-  map-canonical-pullback-tot-cone-cone-family :
-    Σ ( canonical-pullback f g)
-      ( λ t → canonical-pullback ((tr PX (π₃ t)) ∘ (f' (π₁ t))) (g' (π₂ t))) →
-    canonical-pullback (map-Σ PX f f') (map-Σ PX g g')
-  map-canonical-pullback-tot-cone-cone-family =
-    ( tot (λ aa' →
-      ( tot (λ bb' → eq-pair-Σ')) ∘
-      ( map-canonical-pullback-tot-cone-cone-fam-left-factor aa'))) ∘
-    ( map-canonical-pullback-tot-cone-cone-fam-right-factor)
-
-  is-equiv-map-canonical-pullback-tot-cone-cone-family :
-    is-equiv map-canonical-pullback-tot-cone-cone-family
-  is-equiv-map-canonical-pullback-tot-cone-cone-family =
+  map-standard-pullback-tot-cone-cone-family :
+    Σ ( standard-pullback f g)
+      ( λ t →
+        standard-pullback
+          ( tr PX (coherence-square-standard-pullback t) ∘
+            f' (vertical-map-standard-pullback t))
+          ( g' (horizontal-map-standard-pullback t))) →
+    standard-pullback (map-Σ PX f f') (map-Σ PX g g')
+  map-standard-pullback-tot-cone-cone-family =
+    ( tot
+      (λ aa' →
+        ( tot (λ bb' → eq-pair-Σ')) ∘
+        ( map-standard-pullback-tot-cone-cone-fam-left-factor aa'))) ∘
+    ( map-standard-pullback-tot-cone-cone-fam-right-factor)
+
+  is-equiv-map-standard-pullback-tot-cone-cone-family :
+    is-equiv map-standard-pullback-tot-cone-cone-family
+  is-equiv-map-standard-pullback-tot-cone-cone-family =
     is-equiv-comp
       ( tot (λ aa' →
         ( tot (λ bb' → eq-pair-Σ')) ∘
-        ( map-canonical-pullback-tot-cone-cone-fam-left-factor aa')))
-      ( map-canonical-pullback-tot-cone-cone-fam-right-factor)
+        ( map-standard-pullback-tot-cone-cone-fam-left-factor aa')))
+      ( map-standard-pullback-tot-cone-cone-fam-right-factor)
       ( is-equiv-map-interchange-Σ-Σ
         ( λ a bα a' → Σ (PB (pr1 bα))
           ( λ b' → Id (tr PX (pr2 bα) (f' a a')) (g' (pr1 bα) b'))))
       ( is-equiv-tot-is-fiberwise-equiv (λ aa' → is-equiv-comp
         ( tot (λ bb' → eq-pair-Σ'))
-        ( map-canonical-pullback-tot-cone-cone-fam-left-factor aa')
+        ( map-standard-pullback-tot-cone-cone-fam-left-factor aa')
         ( is-equiv-map-interchange-Σ-Σ _)
         ( is-equiv-tot-is-fiberwise-equiv (λ bb' → is-equiv-eq-pair-Σ
           ( pair (f (pr1 aa')) (f' (pr1 aa') (pr2 aa')))
           ( pair (g (pr1 bb')) (g' (pr1 bb') (pr2 bb')))))))
 
-  triangle-canonical-pullback-tot-cone-cone-family :
+  triangle-standard-pullback-tot-cone-cone-family :
     ( gap (map-Σ PX f f') (map-Σ PX g g') tot-cone-cone-family) ~
-    ( ( map-canonical-pullback-tot-cone-cone-family) ∘
+    ( ( map-standard-pullback-tot-cone-cone-family) ∘
       ( map-Σ _
         ( gap f g c)
         ( λ x → gap
           ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
           ( g' (pr1 (pr2 c) x))
           ( c' x))))
-  triangle-canonical-pullback-tot-cone-cone-family x =
+  triangle-standard-pullback-tot-cone-cone-family x =
     refl
 
   is-pullback-family-is-pullback-tot :
@@ -153,15 +162,15 @@ module _
       ( is-pb-c)
       ( is-equiv-right-factor-htpy
         ( gap (map-Σ PX f f') (map-Σ PX g g') tot-cone-cone-family)
-        ( map-canonical-pullback-tot-cone-cone-family)
+        ( map-standard-pullback-tot-cone-cone-family)
         ( map-Σ _
           ( gap f g c)
           ( λ x → gap
             ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
             ( g' (pr1 (pr2 c) x))
             ( c' x)))
-        ( triangle-canonical-pullback-tot-cone-cone-family)
-        ( is-equiv-map-canonical-pullback-tot-cone-cone-family)
+        ( triangle-standard-pullback-tot-cone-cone-family)
+        ( is-equiv-map-standard-pullback-tot-cone-cone-family)
         ( is-pb-tot))
 
   is-pullback-tot-is-pullback-family :
@@ -176,14 +185,14 @@ module _
   is-pullback-tot-is-pullback-family is-pb-c is-pb-c' =
     is-equiv-comp-htpy
       ( gap (map-Σ PX f f') (map-Σ PX g g') tot-cone-cone-family)
-      ( map-canonical-pullback-tot-cone-cone-family)
+      ( map-standard-pullback-tot-cone-cone-family)
       ( map-Σ _
         ( gap f g c)
         ( λ x → gap
           ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
           ( g' (pr1 (pr2 c) x))
           ( c' x)))
-      ( triangle-canonical-pullback-tot-cone-cone-family)
+      ( triangle-standard-pullback-tot-cone-cone-family)
       ( is-equiv-map-Σ _
         ( gap f g c)
         ( λ x → gap
@@ -192,7 +201,7 @@ module _
           ( c' x))
           ( is-pb-c)
           ( is-pb-c'))
-      ( is-equiv-map-canonical-pullback-tot-cone-cone-family)
+      ( is-equiv-map-standard-pullback-tot-cone-cone-family)
 ```
 
 ### Commuting squares of maps on total spaces
diff --git a/src/foundation/functoriality-fibers-of-maps.lagda.md b/src/foundation/functoriality-fibers-of-maps.lagda.md
index 83691df19a..96c0770060 100644
--- a/src/foundation/functoriality-fibers-of-maps.lagda.md
+++ b/src/foundation/functoriality-fibers-of-maps.lagda.md
@@ -1,4 +1,4 @@
-# The functoriality of `fiber`
+# Functoriality of fibers of maps
 
 ```agda
 module foundation.functoriality-fibers-of-maps where
@@ -24,9 +24,8 @@ open import foundation-core.identity-types
 
 ## Idea
 
-Any commuting square
-
-induces a map between the fibers of the vertical maps
+Any [commuting square](foundation-core.commuting-squares-of-maps.md) induces a
+map between the fibers of the vertical maps.
 
 ## Definitions
 
@@ -44,8 +43,8 @@ module _
 
 map-fiber-cone-id :
   {l1 l2 : Level} {B : UU l1} {X : UU l2} (g : B → X) (x : X) →
-  map-fiber-cone id g (triple g id refl-htpy) x ~ id
-map-fiber-cone-id g .(g b) (pair b refl) =
+  map-fiber-cone id g (g , id , refl-htpy) x ~ id
+map-fiber-cone-id g .(g b) (b , refl) =
   refl
 ```
 
@@ -63,19 +62,18 @@ module _
   map-fiber-pasting-horizontal-cone :
     (c : cone j h B) (d : cone i (pr1 c) A) → (x : X) →
     ( map-fiber-cone (j ∘ i) h (pasting-horizontal-cone i j h c d) x) ~
-    ( (map-fiber-cone j h c (i x)) ∘ (map-fiber-cone i (pr1 c) d x))
+    ( map-fiber-cone j h c (i x) ∘ map-fiber-cone i (pr1 c) d x)
   map-fiber-pasting-horizontal-cone
-    (pair g (pair q K)) (pair f (pair p H)) .(f a) (pair a refl) =
-    eq-pair-Σ
-      ( refl)
+    (g , q , K) (f , p , H) .(f a) (a , refl) =
+    eq-pair-Σ-eq-pr2
       ( ( ap
           ( concat' (h (q (p a))) refl)
           ( distributive-inv-concat (ap j (H a)) (K (p a)))) ∙
-        ( ( assoc (inv (K (p a))) (inv (ap j (H a))) refl) ∙
-          ( ap
-            ( concat (inv (K (p a))) (j (i (f a))))
-            ( ( ap (concat' (j (g (p a))) refl) (inv (ap-inv j (H a)))) ∙
-              ( inv (ap-concat j (inv (H a)) refl))))))
+        ( assoc (inv (K (p a))) (inv (ap j (H a))) refl) ∙
+        ( ap
+          ( concat (inv (K (p a))) (j (i (f a))))
+          ( ( ap (concat' (j (g (p a))) refl) (inv (ap-inv j (H a)))) ∙
+            ( inv (ap-concat j (inv (H a)) refl)))))
 ```
 
 ### Computing `map-fiber-cone` of a horizontal pasting of cones
@@ -97,26 +95,28 @@ module _
         ( map-fiber-cone f g c x)
         ( λ t → map-fiber-cone (pr1 (pr2 c)) h d (pr1 t))))
   map-fiber-pasting-vertical-cone
-    (pair p (pair q H)) (pair p' (pair q' H')) .(p (p' a))
-    (pair (pair .(p' a) refl) (pair a refl)) =
-    eq-pair-Σ refl
+    (p , q , H) (p' , q' , H') .(p (p' a))
+    ((.(p' a) , refl) , (a , refl)) =
+    eq-pair-Σ-eq-pr2
       ( ( right-unit) ∙
-        ( ( distributive-inv-concat (H (p' a)) (ap g (H' a))) ∙
-          ( ( ap
-              ( concat (inv (ap g (H' a))) (f (p (p' a))))
-              ( inv right-unit)) ∙
-            ( ap
-              ( concat' (g (h (q' a)))
-                ( pr2
-                  ( map-fiber-cone f g
-                    ( triple p q H)
-                    ( p (p' a))
-                    ( pair (p' a) refl))))
-              ( ( inv (ap-inv g (H' a))) ∙
-                ( ap (ap g) (inv right-unit)))))))
+        ( distributive-inv-concat (H (p' a)) (ap g (H' a))) ∙
+        ( ap
+          ( concat (inv (ap g (H' a))) (f (p (p' a))))
+          ( inv right-unit)) ∙
+        ( ap
+          ( concat' (g (h (q' a)))
+            ( pr2
+              ( map-fiber-cone f g
+                ( p , q , H)
+                ( p (p' a))
+                ( p' a , refl))))
+          ( ( inv (ap-inv g (H' a))) ∙
+            ( ap (ap g) (inv right-unit)))))
 ```
 
-## See also
+## Table of files about fibers of maps
+
+The following table lists files that are about fibers of maps as a general
+concept.
 
-- Equality proofs in the fiber of a map are characterized in
-  [`foundation.equality-fibers-of-maps`](foundation.equality-fibers-of-maps.md).
+{{#include tables/fibers-of-maps.md}}
diff --git a/src/foundation/functoriality-pullbacks.lagda.md b/src/foundation/functoriality-pullbacks.lagda.md
new file mode 100644
index 0000000000..737434ef51
--- /dev/null
+++ b/src/foundation/functoriality-pullbacks.lagda.md
@@ -0,0 +1,59 @@
+# Functorialty of pullbacks
+
+```agda
+module foundation.functoriality-pullbacks where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cones-over-cospans
+open import foundation.dependent-pair-types
+open import foundation.morphisms-cospans
+open import foundation.universe-levels
+
+open import foundation-core.equivalences
+open import foundation-core.identity-types
+open import foundation-core.pullbacks
+```
+
+</details>
+
+## Idea
+
+The construction of the [standard pullback](foundation-core.pullbacks.md) is
+functorial.
+
+## Definitions
+
+### The functorial action on maps of pullbacks
+
+```agda
+module _
+  {l1 l2 l3 l1' l2' l3' : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
+  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X')
+  where
+
+  map-standard-pullback :
+    hom-cospan f' g' f g → standard-pullback f' g' → standard-pullback f g
+  pr1 (map-standard-pullback (hA , _) (a' , _)) = hA a'
+  pr1 (pr2 (map-standard-pullback (hA , hB , _) (a' , b' , _))) = hB b'
+  pr2 (pr2 (map-standard-pullback (hA , hB , hX , HA , HB) (a' , b' , p'))) =
+    HA a' ∙ ap hX p' ∙ inv (HB b')
+
+  map-is-pullback :
+    {l4 l4' : Level} {C : UU l4} {C' : UU l4'} →
+    (c : cone f g C) (c' : cone f' g' C') →
+    is-pullback f g c → is-pullback f' g' c' →
+    hom-cospan f' g' f g → C' → C
+  map-is-pullback c c' is-pb-c is-pb-c' h x =
+    map-inv-is-equiv is-pb-c (map-standard-pullback h (gap f' g' c' x))
+```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/foundation/functoriality-sequential-limits.lagda.md b/src/foundation/functoriality-sequential-limits.lagda.md
new file mode 100644
index 0000000000..086db18443
--- /dev/null
+++ b/src/foundation/functoriality-sequential-limits.lagda.md
@@ -0,0 +1,62 @@
+# Functoriality of sequential limits
+
+```agda
+module foundation.functoriality-sequential-limits where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.cones-over-towers
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.morphisms-towers
+open import foundation.sequential-limits
+open import foundation.towers
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+The construction of the [sequential limit](foundation.sequential-limits.md) is
+functorial.
+
+## Definitions
+
+### The functorial action on maps of standard sequential limits
+
+```agda
+module _
+  {l1 l2 : Level} {A : tower l1} {A' : tower l2}
+  where
+
+  map-hom-standard-sequential-limit :
+    hom-tower A' A → standard-sequential-limit A' → standard-sequential-limit A
+  pr1 (map-hom-standard-sequential-limit (f , F) (x , H)) n = f n (x n)
+  pr2 (map-hom-standard-sequential-limit (f , F) (x , H)) n =
+    ap (f n) (H n) ∙ F n (x (succ-ℕ n))
+
+  map-hom-is-sequential-limit :
+    {l4 l4' : Level} {C : UU l4} {C' : UU l4'} →
+    (c : cone-tower A C) (c' : cone-tower A' C') →
+    is-sequential-limit A c → is-sequential-limit A' c' →
+    hom-tower A' A → C' → C
+  map-hom-is-sequential-limit c c' is-lim-c is-lim-c' h x =
+    map-inv-is-equiv
+      ( is-lim-c)
+      ( map-hom-standard-sequential-limit h (gap-tower A' c' x))
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
diff --git a/src/foundation/morphisms-cospans.lagda.md b/src/foundation/morphisms-cospans.lagda.md
index c63c822306..d8f07831fe 100644
--- a/src/foundation/morphisms-cospans.lagda.md
+++ b/src/foundation/morphisms-cospans.lagda.md
@@ -19,14 +19,14 @@ open import foundation-core.homotopies
 
 ## Idea
 
-A morphism of cospans is a commuting diagram of the form
+A **morphism of cospans** is a commuting diagram of the form
 
 ```text
   A -----> X <----- B
   |        |        |
   |        |        |
   V        V        V
-  A' ----> X' <---- B'
+  A' ----> X' <---- B'.
 ```
 
 ## Definitions
@@ -40,10 +40,12 @@ hom-cospan :
   {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X') →
   UU (l1 ⊔ l2 ⊔ l3 ⊔ l1' ⊔ l2' ⊔ l3')
 hom-cospan {A = A} {B} {X} f g {A'} {B'} {X'} f' g' =
-  Σ (A → A') (λ hA →
-    Σ (B → B') (λ hB →
-      Σ (X → X') (λ hX →
-        ((f' ∘ hA) ~ (hX ∘ f)) × ((g' ∘ hB) ~ (hX ∘ g)))))
+  Σ ( A → A')
+    ( λ hA →
+      Σ ( B → B')
+        ( λ hB →
+          Σ ( X → X')
+            ( λ hX → (f' ∘ hA ~ hX ∘ f) × (g' ∘ hB ~ hX ∘ g))))
 ```
 
 ### Identity morphisms of cospans
@@ -73,33 +75,33 @@ cospan-hom-cospan-rotate :
   hom-cospan (pr1 h) (pr1 h') (pr1 (pr2 (pr2 h))) (pr1 (pr2 (pr2 h')))
 pr1
   ( cospan-hom-cospan-rotate f g f' g' f'' g''
-    ( pair hA (pair hB (pair hX (pair HA HB))))
-    ( pair hA' (pair hB' (pair hX' (pair HA' HB'))))) = f'
+    ( hA , hB , hX , HA , HB)
+    ( hA' , hB' , hX' , HA' , HB')) = f'
 pr1
   ( pr2
     ( cospan-hom-cospan-rotate f g f' g' f'' g''
-      ( pair hA (pair hB (pair hX (pair HA HB))))
-      ( pair hA' (pair hB' (pair hX' (pair HA' HB')))))) = f''
+      ( hA , hB , hX , HA , HB)
+      ( hA' , hB' , hX' , HA' , HB'))) = f''
 pr1
   ( pr2
     ( pr2
       ( cospan-hom-cospan-rotate f g f' g' f'' g''
-        ( pair hA (pair hB (pair hX (pair HA HB))))
-        ( pair hA' (pair hB' (pair hX' (pair HA' HB'))))))) = f
+        ( hA , hB , hX , HA , HB)
+        ( hA' , hB' , hX' , HA' , HB')))) = f
 pr1
   ( pr2
     ( pr2
       ( pr2
         ( cospan-hom-cospan-rotate f g f' g' f'' g''
-          ( pair hA (pair hB (pair hX (pair HA HB))))
-          ( pair hA' (pair hB' (pair hX' (pair HA' HB')))))))) = inv-htpy HA
+          ( hA , hB , hX , HA , HB)
+          ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HA
 pr2
   ( pr2
     ( pr2
       ( pr2
         ( cospan-hom-cospan-rotate f g f' g' f'' g''
-          ( pair hA (pair hB (pair hX (pair HA HB))))
-          ( pair hA' (pair hB' (pair hX' (pair HA' HB')))))))) = inv-htpy HA'
+          ( hA , hB , hX , HA , HB)
+          ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HA'
 
 cospan-hom-cospan-rotate' :
   {l1 l2 l3 l1' l2' l3' l1'' l2'' l3'' : Level}
@@ -112,31 +114,31 @@ cospan-hom-cospan-rotate' :
     (pr1 (pr2 h)) (pr1 (pr2 h')) (pr1 (pr2 (pr2 h))) (pr1 (pr2 (pr2 h')))
 pr1
   ( cospan-hom-cospan-rotate' f g f' g' f'' g''
-    ( pair hA (pair hB (pair hX (pair HA HB))))
-    ( pair hA' (pair hB' (pair hX' (pair HA' HB'))))) = g'
+    ( hA , hB , hX , HA , HB)
+    ( hA' , hB' , hX' , HA' , HB')) = g'
 pr1
   ( pr2
     ( cospan-hom-cospan-rotate' f g f' g' f'' g''
-      ( pair hA (pair hB (pair hX (pair HA HB))))
-      ( pair hA' (pair hB' (pair hX' (pair HA' HB')))))) = g''
+      ( hA , hB , hX , HA , HB)
+      ( hA' , hB' , hX' , HA' , HB'))) = g''
 pr1
   ( pr2
     ( pr2
       ( cospan-hom-cospan-rotate' f g f' g' f'' g''
-        ( pair hA (pair hB (pair hX (pair HA HB))))
-        ( pair hA' (pair hB' (pair hX' (pair HA' HB'))))))) = g
+        ( hA , hB , hX , HA , HB)
+        ( hA' , hB' , hX' , HA' , HB')))) = g
 pr1
   ( pr2
     ( pr2
       ( pr2
         ( cospan-hom-cospan-rotate' f g f' g' f'' g''
-          ( pair hA (pair hB (pair hX (pair HA HB))))
-          ( pair hA' (pair hB' (pair hX' (pair HA' HB')))))))) = inv-htpy HB
+          ( hA , hB , hX , HA , HB)
+          ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HB
 pr2
   ( pr2
     ( pr2
       ( pr2
         ( cospan-hom-cospan-rotate' f g f' g' f'' g''
-          ( pair hA (pair hB (pair hX (pair HA HB))))
-          ( pair hA' (pair hB' (pair hX' (pair HA' HB')))))))) = inv-htpy HB'
+          ( hA , hB , hX , HA , HB)
+          ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HB'
 ```
diff --git a/src/foundation/morphisms-towers.lagda.md b/src/foundation/morphisms-towers.lagda.md
new file mode 100644
index 0000000000..0f2335f051
--- /dev/null
+++ b/src/foundation/morphisms-towers.lagda.md
@@ -0,0 +1,163 @@
+# Morphisms of towers of types
+
+```agda
+module foundation.morphisms-towers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
+open import foundation.dependent-pair-types
+open import foundation.dependent-towers
+open import foundation.equality-dependent-function-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopy-induction
+open import foundation.structure-identity-principle
+open import foundation.towers
+open import foundation.universe-levels
+
+open import foundation-core.contractible-types
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.whiskering-homotopies
+```
+
+</details>
+
+## Idea
+
+A **morphism of towers** `A → B` is a commuting diagram of the form
+
+```text
+  ⋯ ----> Aₙ₊₁ ----> Aₙ ----> ⋯ ----> A₁ ----> A₀
+           |         |       |       |        |
+  ⋯        |         |       ⋯       |        |
+           v         v       v       v        v
+  ⋯ ----> Bₙ₊₁ ----> Bₙ ----> ⋯ ----> B₁ ----> B₀.
+```
+
+## Definitions
+
+### Morphisms of towers
+
+```agda
+naturality-hom-tower :
+  {l1 l2 : Level} (A : tower l1) (B : tower l2)
+  (h : (n : ℕ) → type-tower A n → type-tower B n) (n : ℕ) → UU (l1 ⊔ l2)
+naturality-hom-tower A B =
+  naturality-section-dependent-tower A (const-dependent-tower A B)
+
+hom-tower : {l1 l2 : Level} (A : tower l1) (B : tower l2) → UU (l1 ⊔ l2)
+hom-tower A B = section-dependent-tower A (const-dependent-tower A B)
+
+module _
+  {l1 l2 : Level} (A : tower l1) (B : tower l2)
+  where
+
+  map-hom-tower : hom-tower A B → (n : ℕ) → type-tower A n → type-tower B n
+  map-hom-tower = map-section-dependent-tower A (const-dependent-tower A B)
+
+  naturality-map-hom-tower :
+    (f : hom-tower A B) (n : ℕ) → naturality-hom-tower A B (map-hom-tower f) n
+  naturality-map-hom-tower =
+    naturality-map-section-dependent-tower A (const-dependent-tower A B)
+```
+
+### Identity map on towers
+
+```agda
+id-hom-tower :
+  {l : Level} (A : tower l) → hom-tower A A
+pr1 (id-hom-tower A) n = id
+pr2 (id-hom-tower A) n = refl-htpy
+```
+
+### Composition of map of towers
+
+```agda
+map-comp-hom-tower :
+  {l : Level} (A B C : tower l) → hom-tower B C → hom-tower A B →
+  (n : ℕ) → type-tower A n → type-tower C n
+map-comp-hom-tower A B C g f n = map-hom-tower B C g n ∘ map-hom-tower A B f n
+
+naturality-comp-hom-tower :
+  {l : Level} (A B C : tower l) (g : hom-tower B C) (f : hom-tower A B)
+  (n : ℕ) → naturality-hom-tower A C (map-comp-hom-tower A B C g f) n
+naturality-comp-hom-tower A B C g f n x =
+  ( ap (map-hom-tower B C g n) (naturality-map-hom-tower A B f n x)) ∙
+  ( naturality-map-hom-tower B C g n (map-hom-tower A B f (succ-ℕ n) x))
+
+comp-hom-tower :
+  {l : Level} (A B C : tower l) → hom-tower B C → hom-tower A B → hom-tower A C
+pr1 (comp-hom-tower A B C g f) = map-comp-hom-tower A B C g f
+pr2 (comp-hom-tower A B C g f) = naturality-comp-hom-tower A B C g f
+```
+
+## Properties
+
+### Characterization of equality of maps of towers
+
+```agda
+module _
+  {l1 l2 : Level} (A : tower l1) (B : tower l2)
+  where
+
+  coherence-htpy-hom-tower :
+    (f g : hom-tower A B) →
+    ((n : ℕ) → map-hom-tower A B f n ~ map-hom-tower A B g n) →
+    (n : ℕ) → UU (l1 ⊔ l2)
+  coherence-htpy-hom-tower f g H n =
+    ( naturality-map-hom-tower A B f n ∙h (map-tower B n ·l H (succ-ℕ n))) ~
+    ( (H n ·r map-tower A n) ∙h naturality-map-hom-tower A B g n)
+
+  htpy-hom-tower :
+    (f g : hom-tower A B) → UU (l1 ⊔ l2)
+  htpy-hom-tower f g =
+    Σ ( (n : ℕ) → map-hom-tower A B f n ~ map-hom-tower A B g n)
+      ( λ H → (n : ℕ) → coherence-htpy-hom-tower f g H n)
+
+  refl-htpy-hom-tower : (f : hom-tower A B) → htpy-hom-tower f f
+  pr1 (refl-htpy-hom-tower f) n = refl-htpy
+  pr2 (refl-htpy-hom-tower f) n = right-unit-htpy
+
+  htpy-eq-hom-tower : (f g : hom-tower A B) → f ＝ g → htpy-hom-tower f g
+  htpy-eq-hom-tower f .f refl = refl-htpy-hom-tower f
+
+  is-contr-total-htpy-hom-tower :
+    (f : hom-tower A B) → is-contr (Σ (hom-tower A B) (htpy-hom-tower f))
+  is-contr-total-htpy-hom-tower f =
+    is-contr-total-Eq-structure _
+      ( is-contr-total-binary-htpy (map-hom-tower A B f))
+      ( map-hom-tower A B f , refl-binary-htpy (map-hom-tower A B f))
+      ( is-contr-total-Eq-Π _
+        ( λ n →
+          is-contr-total-htpy (naturality-map-hom-tower A B f n ∙h refl-htpy)))
+
+  is-equiv-htpy-eq-hom-tower :
+    (f g : hom-tower A B) → is-equiv (htpy-eq-hom-tower f g)
+  is-equiv-htpy-eq-hom-tower f =
+    fundamental-theorem-id
+      ( is-contr-total-htpy-hom-tower f)
+      ( htpy-eq-hom-tower f)
+
+  extensionality-hom-tower :
+    (f g : hom-tower A B) → (f ＝ g) ≃ htpy-hom-tower f g
+  pr1 (extensionality-hom-tower f g) = htpy-eq-hom-tower f g
+  pr2 (extensionality-hom-tower f g) = is-equiv-htpy-eq-hom-tower f g
+
+  eq-htpy-hom-tower : (f g : hom-tower A B) → htpy-hom-tower f g → f ＝ g
+  eq-htpy-hom-tower f g = map-inv-equiv (extensionality-hom-tower f g)
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
diff --git a/src/foundation/pullback-squares.lagda.md b/src/foundation/pullback-squares.lagda.md
index 59c26f5ae6..25938b8b89 100644
--- a/src/foundation/pullback-squares.lagda.md
+++ b/src/foundation/pullback-squares.lagda.md
@@ -83,3 +83,9 @@ module _
   universal-property-pullback-cone : universal-property-pullback l f g (pr1 c)
   universal-property-pullback-cone = pr2 c
 ```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md
index d85301db73..839966403b 100644
--- a/src/foundation/pullbacks.lagda.md
+++ b/src/foundation/pullbacks.lagda.md
@@ -52,7 +52,8 @@ module _
   is-property-is-pullback c = is-property-is-equiv (gap f g c)
 
   is-pullback-Prop : (c : cone f g C) → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  is-pullback-Prop c = pair (is-pullback f g c) (is-property-is-pullback c)
+  pr1 (is-pullback-Prop c) = is-pullback f g c
+  pr2 (is-pullback-Prop c) = is-property-is-pullback c
 ```
 
 ### Exponents of pullbacks are pullbacks
@@ -62,43 +63,43 @@ exponent-cone :
   {l1 l2 l3 l4 l5 : Level}
   {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} (T : UU l5)
   (f : A → X) (g : B → X) (c : cone f g C) →
-  cone (λ (h : T → A) → f ∘ h) (λ (h : T → B) → g ∘ h) (T → C)
+  cone (postcomp T f) (postcomp T g) (T → C)
 pr1 (exponent-cone T f g c) h = vertical-map-cone f g c ∘ h
 pr1 (pr2 (exponent-cone T f g c)) h = horizontal-map-cone f g c ∘ h
 pr2 (pr2 (exponent-cone T f g c)) h = eq-htpy (coherence-square-cone f g c ·r h)
 
-map-canonical-pullback-exponent :
+map-standard-pullback-exponent :
   {l1 l2 l3 l4 : Level}
   {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
   (T : UU l4) →
-  canonical-pullback (λ (h : T → A) → f ∘ h) (λ (h : T → B) → g ∘ h) →
+  standard-pullback (postcomp T f) (postcomp T g) →
   cone f g T
-map-canonical-pullback-exponent f g T =
+map-standard-pullback-exponent f g T =
   tot (λ p → tot (λ q → htpy-eq))
 
 abstract
-  is-equiv-map-canonical-pullback-exponent :
+  is-equiv-map-standard-pullback-exponent :
     {l1 l2 l3 l4 : Level}
     {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
-    (T : UU l4) → is-equiv (map-canonical-pullback-exponent f g T)
-  is-equiv-map-canonical-pullback-exponent f g T =
+    (T : UU l4) → is-equiv (map-standard-pullback-exponent f g T)
+  is-equiv-map-standard-pullback-exponent f g T =
     is-equiv-tot-is-fiberwise-equiv
       ( λ p → is-equiv-tot-is-fiberwise-equiv
         ( λ q → funext (f ∘ p) (g ∘ q)))
 
-triangle-map-canonical-pullback-exponent :
+triangle-map-standard-pullback-exponent :
   {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   (T : UU l5) (f : A → X) (g : B → X) (c : cone f g C) →
-  ( cone-map f g {C' = T} c) ~
-  ( ( map-canonical-pullback-exponent f g T) ∘
+  ( cone-map f g c {T}) ~
+  ( ( map-standard-pullback-exponent f g T) ∘
     ( gap
-      ( λ (h : T → A) → f ∘ h)
-      ( λ (h : T → B) → g ∘ h)
+      ( postcomp T f)
+      ( postcomp T g)
       ( exponent-cone T f g c)))
-triangle-map-canonical-pullback-exponent
+triangle-map-standard-pullback-exponent
   {A = A} {B} T f g c h =
-  eq-pair-Σ refl
-    ( eq-pair-Σ refl
+  eq-pair-Σ-eq-pr2
+    ( eq-pair-Σ-eq-pr2
       ( inv (is-section-eq-htpy (coherence-square-cone f g c ·r h))))
 
 abstract
@@ -107,16 +108,16 @@ abstract
     (f : A → X) (g : B → X) (c : cone f g C) → is-pullback f g c →
     (T : UU l5) →
     is-pullback
-      ( λ (h : T → A) → f ∘ h)
-      ( λ (h : T → B) → g ∘ h)
+      ( postcomp T f)
+      ( postcomp T g)
       ( exponent-cone T f g c)
   is-pullback-exponent-is-pullback f g c is-pb-c T =
     is-equiv-right-factor-htpy
       ( cone-map f g c)
-      ( map-canonical-pullback-exponent f g T)
+      ( map-standard-pullback-exponent f g T)
       ( gap (f ∘_) (g ∘_) (exponent-cone T f g c))
-      ( triangle-map-canonical-pullback-exponent T f g c)
-      ( is-equiv-map-canonical-pullback-exponent f g T)
+      ( triangle-map-standard-pullback-exponent T f g c)
+      ( is-equiv-map-standard-pullback-exponent f g T)
       ( universal-property-pullback-is-pullback f g c is-pb-c T)
 
 abstract
@@ -124,19 +125,19 @@ abstract
     {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
     (f : A → X) (g : B → X) (c : cone f g C) →
     ((l5 : Level) (T : UU l5) → is-pullback
-      ( λ (h : T → A) → f ∘ h)
-      ( λ (h : T → B) → g ∘ h)
+      ( postcomp T f)
+      ( postcomp T g)
       ( exponent-cone T f g c)) →
     is-pullback f g c
   is-pullback-is-pullback-exponent f g c is-pb-exp =
     is-pullback-universal-property-pullback f g c
       ( λ T → is-equiv-comp-htpy
         ( cone-map f g c)
-        ( map-canonical-pullback-exponent f g T)
-        ( gap (_∘_ f) (_∘_ g) (exponent-cone T f g c))
-        ( triangle-map-canonical-pullback-exponent T f g c)
+        ( map-standard-pullback-exponent f g T)
+        ( gap (f ∘_) (g ∘_) (exponent-cone T f g c))
+        ( triangle-map-standard-pullback-exponent T f g c)
         ( is-pb-exp _ T)
-        ( is-equiv-map-canonical-pullback-exponent f g T))
+        ( is-equiv-map-standard-pullback-exponent f g T))
 ```
 
 ### Identity types can be presented as pullbacks
@@ -145,20 +146,22 @@ abstract
 cone-Id :
   {l : Level} {A : UU l} (x y : A) →
   cone (const unit A x) (const unit A y) (x ＝ y)
-cone-Id x y =
-  triple (const (x ＝ y) unit star) (const (x ＝ y) unit star) id
+pr1 (cone-Id x y) = const (x ＝ y) unit star
+pr1 (pr2 (cone-Id x y)) = const (x ＝ y) unit star
+pr2 (pr2 (cone-Id x y)) = id
 
 inv-gap-cone-Id :
   {l : Level} {A : UU l} (x y : A) →
-  canonical-pullback (const unit A x) (const unit A y) → x ＝ y
-inv-gap-cone-Id x y (pair star (pair star p)) = p
+  standard-pullback (const unit A x) (const unit A y) → x ＝ y
+inv-gap-cone-Id x y (star , star , p) = p
 
 abstract
   is-section-inv-gap-cone-Id :
     {l : Level} {A : UU l} (x y : A) →
-    ( ( gap (const unit A x) (const unit A y) (cone-Id x y)) ∘
-      ( inv-gap-cone-Id x y)) ~ id
-  is-section-inv-gap-cone-Id x y (pair star (pair star p)) = refl
+    ( gap (const unit A x) (const unit A y) (cone-Id x y) ∘
+      inv-gap-cone-Id x y) ~
+    id
+  is-section-inv-gap-cone-Id x y (star , star , p) = refl
 
 abstract
   is-retraction-inv-gap-cone-Id :
@@ -180,31 +183,28 @@ abstract
 cone-Id' :
   {l : Level} {A : UU l} (t : A × A) →
   cone (const unit (A × A) t) (diagonal A) (pr1 t ＝ pr2 t)
-cone-Id' {A = A} (pair x y) =
-  triple
-    ( const (x ＝ y) unit star)
-    ( const (x ＝ y) A x)
-    ( λ p → eq-pair-Σ refl (inv p))
+pr1 (cone-Id' {A = A} (x , y)) = const (x ＝ y) unit star
+pr1 (pr2 (cone-Id' {A = A} (x , y))) = const (x ＝ y) A x
+pr2 (pr2 (cone-Id' {A = A} (x , y))) p = eq-pair-Σ-eq-pr2 (inv p)
 
 inv-gap-cone-Id' :
   {l : Level} {A : UU l} (t : A × A) →
-  canonical-pullback (const unit (A × A) t) (diagonal A) → (pr1 t ＝ pr2 t)
-inv-gap-cone-Id' t (pair star (pair z p)) =
-  (ap pr1 p) ∙ (inv (ap pr2 p))
+  standard-pullback (const unit (A × A) t) (diagonal A) → (pr1 t ＝ pr2 t)
+inv-gap-cone-Id' t (star , z , p) = ap pr1 p ∙ inv (ap pr2 p)
 
 abstract
   is-section-inv-gap-cone-Id' :
     {l : Level} {A : UU l} (t : A × A) →
     ( ( gap (const unit (A × A) t) (diagonal A) (cone-Id' t)) ∘
       ( inv-gap-cone-Id' t)) ~ id
-  is-section-inv-gap-cone-Id' .(pair z z) (pair star (pair z refl)) = refl
+  is-section-inv-gap-cone-Id' .(z , z) (star , z , refl) = refl
 
 abstract
   is-retraction-inv-gap-cone-Id' :
     {l : Level} {A : UU l} (t : A × A) →
     ( ( inv-gap-cone-Id' t) ∘
       ( gap (const unit (A × A) t) (diagonal A) (cone-Id' t))) ~ id
-  is-retraction-inv-gap-cone-Id' (pair x .x) refl = refl
+  is-retraction-inv-gap-cone-Id' (x , .x) refl = refl
 
 abstract
   is-pullback-cone-Id' :
@@ -225,16 +225,16 @@ module _
   {f f' : A → X} (Hf : f ~ f') {g g' : B → X} (Hg : g ~ g')
   where
 
-  map-equiv-canonical-pullback-htpy :
-    canonical-pullback f' g' → canonical-pullback f g
-  map-equiv-canonical-pullback-htpy =
+  map-equiv-standard-pullback-htpy :
+    standard-pullback f' g' → standard-pullback f g
+  map-equiv-standard-pullback-htpy =
     tot (λ a → tot (λ b →
       ( concat' (f a) (inv (Hg b))) ∘ (concat (Hf a) (g' b))))
 
   abstract
-    is-equiv-map-equiv-canonical-pullback-htpy :
-      is-equiv map-equiv-canonical-pullback-htpy
-    is-equiv-map-equiv-canonical-pullback-htpy =
+    is-equiv-map-equiv-standard-pullback-htpy :
+      is-equiv map-equiv-standard-pullback-htpy
+    is-equiv-map-equiv-standard-pullback-htpy =
       is-equiv-tot-is-fiberwise-equiv (λ a →
         is-equiv-tot-is-fiberwise-equiv (λ b →
           is-equiv-comp
@@ -243,10 +243,10 @@ module _
             ( is-equiv-concat (Hf a) (g' b))
             ( is-equiv-concat' (f a) (inv (Hg b)))))
 
-  equiv-canonical-pullback-htpy :
-    canonical-pullback f' g' ≃ canonical-pullback f g
-  pr1 equiv-canonical-pullback-htpy = map-equiv-canonical-pullback-htpy
-  pr2 equiv-canonical-pullback-htpy = is-equiv-map-equiv-canonical-pullback-htpy
+  equiv-standard-pullback-htpy :
+    standard-pullback f' g' ≃ standard-pullback f g
+  pr1 equiv-standard-pullback-htpy = map-equiv-standard-pullback-htpy
+  pr2 equiv-standard-pullback-htpy = is-equiv-map-equiv-standard-pullback-htpy
 ```
 
 ### Parallel pullback squares
@@ -260,10 +260,9 @@ module _
   triangle-is-pullback-htpy :
     {l4 : Level} {C : UU l4}
     {c : cone f g C} {c' : cone f' g' C} (Hc : htpy-parallel-cone Hf Hg c c') →
-    (gap f g c) ~ (map-equiv-canonical-pullback-htpy Hf Hg ∘ (gap f' g' c'))
-  triangle-is-pullback-htpy
-    {c = pair p (pair q H)} {pair p' (pair q' H')} (pair Hp (pair Hq HH)) z =
-    map-extensionality-canonical-pullback f g
+    (gap f g c) ~ (map-equiv-standard-pullback-htpy Hf Hg ∘ (gap f' g' c'))
+  triangle-is-pullback-htpy {c = p , q , H} {p' , q' , H'} (Hp , Hq , HH) z =
+    map-extensionality-standard-pullback f g
       ( Hp z)
       ( Hq z)
       ( ( inv
@@ -285,33 +284,29 @@ module _
       {l4 : Level} {C : UU l4} {c : cone f g C} (c' : cone f' g' C)
       (Hc : htpy-parallel-cone Hf Hg c c') →
       is-pullback f' g' c' → is-pullback f g c
-    is-pullback-htpy
-      {c = pair p (pair q H)} (pair p' (pair q' H'))
-      (pair Hp (pair Hq HH)) is-pb-c' =
+    is-pullback-htpy {c = p , q , H} (p' , q' , H') (Hp , Hq , HH) is-pb-c' =
       is-equiv-comp-htpy
-        ( gap f g (triple p q H))
-        ( map-equiv-canonical-pullback-htpy Hf Hg)
-        ( gap f' g' (triple p' q' H'))
+        ( gap f g (p , q , H))
+        ( map-equiv-standard-pullback-htpy Hf Hg)
+        ( gap f' g' (p' , q' , H'))
         ( triangle-is-pullback-htpy
-          {c = triple p q H} {triple p' q' H'} (triple Hp Hq HH))
+          {c = p , q , H} {p' , q' , H'} (Hp , Hq , HH))
         ( is-pb-c')
-        ( is-equiv-map-equiv-canonical-pullback-htpy Hf Hg)
+        ( is-equiv-map-equiv-standard-pullback-htpy Hf Hg)
 
   abstract
     is-pullback-htpy' :
       {l4 : Level} {C : UU l4} (c : cone f g C) {c' : cone f' g' C}
       (Hc : htpy-parallel-cone Hf Hg c c') →
       is-pullback f g c → is-pullback f' g' c'
-    is-pullback-htpy'
-      (pair p (pair q H)) {pair p' (pair q' H')}
-      (pair Hp (pair Hq HH)) is-pb-c =
+    is-pullback-htpy' (p , q , H) {p' , q' , H'} (Hp , Hq , HH) is-pb-c =
       is-equiv-right-factor-htpy
-        ( gap f g (triple p q H))
-        ( map-equiv-canonical-pullback-htpy Hf Hg)
-        ( gap f' g' (triple p' q' H'))
+        ( gap f g (p , q , H))
+        ( map-equiv-standard-pullback-htpy Hf Hg)
+        ( gap f' g' (p' , q' , H'))
         ( triangle-is-pullback-htpy
-          {c = triple p q H} {triple p' q' H'} (triple Hp Hq HH))
-        ( is-equiv-map-equiv-canonical-pullback-htpy Hf Hg)
+          {c = p , q , H} {p' , q' , H'} (Hp , Hq , HH))
+        ( is-equiv-map-equiv-standard-pullback-htpy Hf Hg)
         ( is-pb-c)
 ```
 
@@ -323,15 +318,15 @@ refl-htpy-parallel-cone :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   (f : A → X) (g : B → X) (c : cone f g C) →
   htpy-parallel-cone (refl-htpy {f = f}) (refl-htpy {f = g}) c c
-refl-htpy-parallel-cone f g c =
-  triple refl-htpy refl-htpy right-unit-htpy
+pr1 (refl-htpy-parallel-cone f g c) = refl-htpy
+pr1 (pr2 (refl-htpy-parallel-cone f g c)) = refl-htpy
+pr2 (pr2 (refl-htpy-parallel-cone f g c)) = right-unit-htpy
 
 htpy-eq-square :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   (f : A → X) (g : B → X) (c c' : cone f g C) →
   c ＝ c' → htpy-parallel-cone (refl-htpy {f = f}) (refl-htpy {f = g}) c c'
-htpy-eq-square f g c .c refl =
-  triple refl-htpy refl-htpy right-unit-htpy
+htpy-eq-square f g c .c refl = refl-htpy-parallel-cone f g c
 
 htpy-parallel-cone-refl-htpy-htpy-cone :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
@@ -339,11 +334,11 @@ htpy-parallel-cone-refl-htpy-htpy-cone :
   (c c' : cone f g C) →
   htpy-cone f g c c' →
   htpy-parallel-cone (refl-htpy {f = f}) (refl-htpy {f = g}) c c'
-htpy-parallel-cone-refl-htpy-htpy-cone f g
-  (pair p (pair q H)) (pair p' (pair q' H')) =
+htpy-parallel-cone-refl-htpy-htpy-cone f g (p , q , H) (p' , q' , H') =
   tot
     ( λ K → tot
-      ( λ L M → ( ap-concat-htpy H _ _ right-unit-htpy) ∙h
+      ( λ L M →
+        ( ap-concat-htpy H _ _ right-unit-htpy) ∙h
         ( M ∙h ap-concat-htpy' _ _ H' inv-htpy-right-unit-htpy)))
 
 abstract
@@ -353,13 +348,13 @@ abstract
     (c c' : cone f g C) →
     is-equiv (htpy-parallel-cone-refl-htpy-htpy-cone f g c c')
   is-equiv-htpy-parallel-cone-refl-htpy-htpy-cone f g
-    (pair p (pair q H)) (pair p' (pair q' H')) =
+    (p , q , H) (p' , q' , H') =
     is-equiv-tot-is-fiberwise-equiv
       ( λ K → is-equiv-tot-is-fiberwise-equiv
         ( λ L → is-equiv-comp
           ( concat-htpy
             ( ap-concat-htpy H _ _ right-unit-htpy)
-            ( ((f ·l K) ∙h refl-htpy) ∙h H'))
+            ( (f ·l K) ∙h refl-htpy ∙h H'))
           ( concat-htpy'
             ( H ∙h (g ·l L))
             ( ap-concat-htpy' _ _ H' inv-htpy-right-unit-htpy))
@@ -367,8 +362,8 @@ abstract
             ( H ∙h (g ·l L))
             ( λ x → ap (λ z → z ∙ H' x) (inv right-unit)))
           ( is-equiv-concat-htpy
-            ( λ x → ap (_∙_ (H x)) right-unit)
-            ( ((f ·l K) ∙h refl-htpy) ∙h H'))))
+            ( λ x → ap (H x ∙_) right-unit)
+            ( (f ·l K) ∙h refl-htpy ∙h H'))))
 
 abstract
   is-contr-total-htpy-parallel-cone-refl-htpy-refl-htpy :
@@ -377,9 +372,7 @@ abstract
     (c : cone f g C) →
     is-contr
       ( Σ (cone f g C) (htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c))
-  is-contr-total-htpy-parallel-cone-refl-htpy-refl-htpy {A = A} {B} {X} {C}
-    f g (pair p (pair q H)) =
-    let c = triple p q H in
+  is-contr-total-htpy-parallel-cone-refl-htpy-refl-htpy {C = C} f g c =
     is-contr-is-equiv'
       ( Σ (cone f g C) (htpy-cone f g c))
       ( tot (htpy-parallel-cone-refl-htpy-htpy-cone f g c))
@@ -395,7 +388,8 @@ abstract
     is-contr (Σ (cone f g' C) (htpy-parallel-cone (refl-htpy' f) Hg c))
   is-contr-total-htpy-parallel-cone-refl-htpy {C = C} f {g} =
     ind-htpy g
-      ( λ g'' Hg' → ( c : cone f g C) →
+      ( λ g'' Hg' →
+        ( c : cone f g C) →
         is-contr (Σ (cone f g'' C) (htpy-parallel-cone (refl-htpy' f) Hg' c)))
       ( is-contr-total-htpy-parallel-cone-refl-htpy-refl-htpy f g)
 
@@ -419,17 +413,19 @@ abstract
 tr-tr-refl-htpy-cone :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   (f : A → X) (g : B → X) (c : cone f g C) →
-  let tr-c = tr (λ x → cone x g C) (eq-htpy (refl-htpy {f = f})) c
-      tr-tr-c = tr (λ y → cone f y C) (eq-htpy (refl-htpy {f = g})) tr-c
+  let
+    tr-c = tr (λ x → cone x g C) (eq-htpy (refl-htpy {f = f})) c
+    tr-tr-c = tr (λ y → cone f y C) (eq-htpy (refl-htpy {f = g})) tr-c
   in
   tr-tr-c ＝ c
 tr-tr-refl-htpy-cone {C = C} f g c =
-  let tr-c = tr (λ f''' → cone f''' g C) (eq-htpy refl-htpy) c
-      tr-tr-c = tr (λ g'' → cone f g'' C) (eq-htpy refl-htpy) tr-c
-      α : tr-tr-c ＝ tr-c
-      α = ap (λ t → tr (λ g'' → cone f g'' C) t tr-c) (eq-htpy-refl-htpy g)
-      β : tr-c ＝ c
-      β = ap (λ t → tr (λ f''' → cone f''' g C) t c) (eq-htpy-refl-htpy f)
+  let
+    tr-c = tr (λ f''' → cone f''' g C) (eq-htpy refl-htpy) c
+    tr-tr-c = tr (λ g'' → cone f g'' C) (eq-htpy refl-htpy) tr-c
+    α : tr-tr-c ＝ tr-c
+    α = ap (λ t → tr (λ g'' → cone f g'' C) t tr-c) (eq-htpy-refl-htpy g)
+    β : tr-c ＝ c
+    β = ap (λ t → tr (λ f''' → cone f''' g C) t c) (eq-htpy-refl-htpy f)
   in
   α ∙ β
 
@@ -449,8 +445,8 @@ htpy-eq-square-refl-htpy f g c c' =
 comp-htpy-eq-square-refl-htpy :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   (f : A → X) (g : B → X) (c c' : cone f g C) →
-  ( (htpy-eq-square-refl-htpy f g c c') ∘
-    (concat (tr-tr-refl-htpy-cone f g c) c')) ~
+  ( htpy-eq-square-refl-htpy f g c c' ∘
+    concat (tr-tr-refl-htpy-cone f g c) c') ~
   ( htpy-eq-square f g c c')
 comp-htpy-eq-square-refl-htpy f g c c' =
   is-section-map-inv-is-equiv-precomp-Π-is-equiv
@@ -463,8 +459,9 @@ abstract
     {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
     (f : A → X) {g g' : B → X} (Hg : g ~ g') →
     (c : cone f g C) (c' : cone f g' C) →
-    let tr-c = tr (λ x → cone x g C) (eq-htpy (refl-htpy {f = f})) c
-        tr-tr-c = tr (λ y → cone f y C) (eq-htpy Hg) tr-c
+    let
+      tr-c = tr (λ x → cone x g C) (eq-htpy (refl-htpy {f = f})) c
+      tr-tr-c = tr (λ y → cone f y C) (eq-htpy Hg) tr-c
     in
     tr-tr-c ＝ c' → htpy-parallel-cone (refl-htpy' f) Hg c c'
   htpy-parallel-cone-eq' {C = C} f {g} =
@@ -491,8 +488,9 @@ abstract
       ( htpy-eq (htpy-eq (htpy-eq (compute-ind-htpy g
         ( λ g'' Hg' →
           ( c : cone f g C) (c' : cone f g'' C) →
-            Id (tr (λ g'' → cone f g'' C) (eq-htpy Hg')
-              ( tr (λ f''' → cone f''' g C) (eq-htpy (refl-htpy' f)) c)) c' →
+            Id
+              ( tr (λ g'' → cone f g'' C) (eq-htpy Hg')
+                ( tr (λ f''' → cone f''' g C) (eq-htpy (refl-htpy' f)) c)) c' →
           htpy-parallel-cone refl-htpy Hg' c c')
       ( htpy-eq-square-refl-htpy f g)) c) c'))
       ( concat (tr-tr-refl-htpy-cone f g c) c') ∙h
@@ -506,13 +504,15 @@ abstract
     let tr-c = tr (λ x → cone x g C) (eq-htpy Hf) c
         tr-tr-c = tr (λ y → cone f' y C) (eq-htpy Hg) tr-c
     in
-    Id tr-tr-c c' → htpy-parallel-cone Hf Hg c c'
+    tr-tr-c ＝ c' → htpy-parallel-cone Hf Hg c c'
   htpy-parallel-cone-eq {A = A} {B} {X} {C} {f} {f'} Hf {g} {g'} Hg c c' p =
     ind-htpy f
     ( λ f'' Hf' →
       ( g g' : B → X) (Hg : g ~ g') (c : cone f g C) (c' : cone f'' g' C) →
-      ( Id (tr (λ g'' → cone f'' g'' C) (eq-htpy Hg)
-        ( tr (λ f''' → cone f''' g C) (eq-htpy Hf') c)) c') →
+      ( Id
+        ( tr (λ g'' → cone f'' g'' C) (eq-htpy Hg)
+          ( tr (λ f''' → cone f''' g C) (eq-htpy Hf') c))
+        ( c')) →
       htpy-parallel-cone Hf' Hg c c')
     ( λ g g' → htpy-parallel-cone-eq' f {g = g} {g' = g'})
     Hf g g' Hg c c' p
@@ -532,7 +532,8 @@ abstract
               ( tr
                 ( λ g'' → cone f'' g'' C)
                 ( eq-htpy Hg)
-                ( tr (λ f''' → cone f''' g C) (eq-htpy Hf') c)) c') →
+                ( tr (λ f''' → cone f''' g C) (eq-htpy Hf') c))
+              ( c')) →
             htpy-parallel-cone Hf' Hg c c')
         ( λ g g' → htpy-parallel-cone-eq' f {g = g} {g' = g'})) g) g)
         refl-htpy) c) c'))
@@ -576,14 +577,13 @@ eq-htpy-parallel-cone :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   {f f' : A → X} (Hf : f ~ f') {g g' : B → X} (Hg : g ~ g') →
   (c : cone f g C) (c' : cone f' g' C) →
-  let tr-c = tr (λ x → cone x g C) (eq-htpy Hf) c
-      tr-tr-c = tr (λ y → cone f' y C) (eq-htpy Hg) tr-c
+  let
+    tr-c = tr (λ x → cone x g C) (eq-htpy Hf) c
+    tr-tr-c = tr (λ y → cone f' y C) (eq-htpy Hg) tr-c
   in
-  htpy-parallel-cone Hf Hg c c' → Id tr-tr-c c'
+  htpy-parallel-cone Hf Hg c c' → tr-tr-c ＝ c'
 eq-htpy-parallel-cone Hf Hg c c' =
-  map-inv-is-equiv
-    { f = htpy-parallel-cone-eq Hf Hg c c'}
-    ( is-fiberwise-equiv-htpy-parallel-cone-eq Hf Hg c c')
+  map-inv-is-equiv (is-fiberwise-equiv-htpy-parallel-cone-eq Hf Hg c c')
 ```
 
 ### Dependent products of pullbacks are pullbacks
@@ -595,54 +595,53 @@ cone-Π :
   (f : (i : I) → A i → X i) (g : (i : I) → B i → X i)
   (c : (i : I) → cone (f i) (g i) (C i)) →
   cone (map-Π f) (map-Π g) ((i : I) → C i)
-cone-Π f g c =
-  triple
-    ( map-Π (λ i → pr1 (c i)))
-    ( map-Π (λ i → pr1 (pr2 (c i))))
-    ( htpy-map-Π (λ i → pr2 (pr2 (c i))))
+pr1 (cone-Π f g c) = map-Π (λ i → pr1 (c i))
+pr1 (pr2 (cone-Π f g c)) = map-Π (λ i → pr1 (pr2 (c i)))
+pr2 (pr2 (cone-Π f g c)) = htpy-map-Π (λ i → pr2 (pr2 (c i)))
 
-map-canonical-pullback-Π :
+map-standard-pullback-Π :
   {l1 l2 l3 l4 : Level} {I : UU l1}
   {A : I → UU l2} {B : I → UU l3} {X : I → UU l4}
   (f : (i : I) → A i → X i) (g : (i : I) → B i → X i) →
-  canonical-pullback (map-Π f) (map-Π g) →
-  (i : I) → canonical-pullback (f i) (g i)
-map-canonical-pullback-Π f g (pair α (pair β γ)) i =
-  triple (α i) (β i) (htpy-eq γ i)
+  standard-pullback (map-Π f) (map-Π g) →
+  (i : I) → standard-pullback (f i) (g i)
+pr1 (map-standard-pullback-Π f g (α , β , γ) i) = α i
+pr1 (pr2 (map-standard-pullback-Π f g (α , β , γ) i)) = β i
+pr2 (pr2 (map-standard-pullback-Π f g (α , β , γ) i)) = htpy-eq γ i
 
-inv-map-canonical-pullback-Π :
+inv-map-standard-pullback-Π :
   {l1 l2 l3 l4 : Level} {I : UU l1}
   {A : I → UU l2} {B : I → UU l3} {X : I → UU l4}
   (f : (i : I) → A i → X i) (g : (i : I) → B i → X i) →
-  ((i : I) → canonical-pullback (f i) (g i)) →
-  canonical-pullback (map-Π f) (map-Π g)
-inv-map-canonical-pullback-Π f g h =
-  triple
-    ( λ i → (pr1 (h i)))
-    ( λ i → (pr1 (pr2 (h i))))
-    ( eq-htpy (λ i → (pr2 (pr2 (h i)))))
+  ((i : I) → standard-pullback (f i) (g i)) →
+  standard-pullback (map-Π f) (map-Π g)
+pr1 (inv-map-standard-pullback-Π f g h) i = pr1 (h i)
+pr1 (pr2 (inv-map-standard-pullback-Π f g h)) i = pr1 (pr2 (h i))
+pr2 (pr2 (inv-map-standard-pullback-Π f g h)) =
+  eq-htpy (λ i → (pr2 (pr2 (h i))))
 
 abstract
-  is-section-inv-map-canonical-pullback-Π :
+  is-section-inv-map-standard-pullback-Π :
     {l1 l2 l3 l4 : Level} {I : UU l1}
     {A : I → UU l2} {B : I → UU l3} {X : I → UU l4}
     (f : (i : I) → A i → X i) (g : (i : I) → B i → X i) →
-    ((map-canonical-pullback-Π f g) ∘ (inv-map-canonical-pullback-Π f g)) ~ id
-  is-section-inv-map-canonical-pullback-Π f g h =
+    map-standard-pullback-Π f g ∘ inv-map-standard-pullback-Π f g ~ id
+  is-section-inv-map-standard-pullback-Π f g h =
     eq-htpy
-      ( λ i → map-extensionality-canonical-pullback (f i) (g i) refl refl
-        ( inv
-          ( ( right-unit) ∙
-            ( htpy-eq (is-section-eq-htpy (λ i → (pr2 (pr2 (h i))))) i))))
+      ( λ i →
+        map-extensionality-standard-pullback (f i) (g i) refl refl
+          ( inv
+            ( ( right-unit) ∙
+              ( htpy-eq (is-section-eq-htpy (λ i → pr2 (pr2 (h i)))) i))))
 
 abstract
-  is-retraction-inv-map-canonical-pullback-Π :
+  is-retraction-inv-map-standard-pullback-Π :
     {l1 l2 l3 l4 : Level} {I : UU l1}
     {A : I → UU l2} {B : I → UU l3} {X : I → UU l4}
     (f : (i : I) → A i → X i) (g : (i : I) → B i → X i) →
-    ((inv-map-canonical-pullback-Π f g) ∘ (map-canonical-pullback-Π f g)) ~ id
-  is-retraction-inv-map-canonical-pullback-Π f g (pair α (pair β γ)) =
-    map-extensionality-canonical-pullback
+    inv-map-standard-pullback-Π f g ∘ map-standard-pullback-Π f g ~ id
+  is-retraction-inv-map-standard-pullback-Π f g (α , β , γ) =
+    map-extensionality-standard-pullback
       ( map-Π f)
       ( map-Π g)
       refl
@@ -650,32 +649,31 @@ abstract
       ( inv (right-unit ∙ (is-retraction-eq-htpy γ)))
 
 abstract
-  is-equiv-map-canonical-pullback-Π :
+  is-equiv-map-standard-pullback-Π :
     {l1 l2 l3 l4 : Level} {I : UU l1}
     {A : I → UU l2} {B : I → UU l3} {X : I → UU l4}
     (f : (i : I) → A i → X i) (g : (i : I) → B i → X i) →
-    is-equiv (map-canonical-pullback-Π f g)
-  is-equiv-map-canonical-pullback-Π f g =
+    is-equiv (map-standard-pullback-Π f g)
+  is-equiv-map-standard-pullback-Π f g =
     is-equiv-is-invertible
-      ( inv-map-canonical-pullback-Π f g)
-      ( is-section-inv-map-canonical-pullback-Π f g)
-      ( is-retraction-inv-map-canonical-pullback-Π f g)
+      ( inv-map-standard-pullback-Π f g)
+      ( is-section-inv-map-standard-pullback-Π f g)
+      ( is-retraction-inv-map-standard-pullback-Π f g)
 
-triangle-map-canonical-pullback-Π :
+triangle-map-standard-pullback-Π :
   {l1 l2 l3 l4 l5 : Level} {I : UU l1}
   {A : I → UU l2} {B : I → UU l3} {X : I → UU l4} {C : I → UU l5}
   (f : (i : I) → A i → X i) (g : (i : I) → B i → X i)
   (c : (i : I) → cone (f i) (g i) (C i)) →
   ( map-Π (λ i → gap (f i) (g i) (c i))) ~
-  ( ( map-canonical-pullback-Π f g) ∘
-    ( gap (map-Π f) (map-Π g) (cone-Π f g c)))
-triangle-map-canonical-pullback-Π f g c h =
+  ( map-standard-pullback-Π f g ∘ gap (map-Π f) (map-Π g) (cone-Π f g c))
+triangle-map-standard-pullback-Π f g c h =
   eq-htpy (λ i →
-    map-extensionality-canonical-pullback
+    map-extensionality-standard-pullback
       (f i)
       (g i)
       refl refl
-      ( (htpy-eq (is-section-eq-htpy _) i) ∙ (inv right-unit)))
+      ( htpy-eq (is-section-eq-htpy _) i ∙ inv right-unit))
 
 abstract
   is-pullback-cone-Π :
@@ -688,10 +686,10 @@ abstract
   is-pullback-cone-Π f g c is-pb-c =
     is-equiv-right-factor-htpy
       ( map-Π (λ i → gap (f i) (g i) (c i)))
-      ( map-canonical-pullback-Π f g)
+      ( map-standard-pullback-Π f g)
       ( gap (map-Π f) (map-Π g) (cone-Π f g c))
-      ( triangle-map-canonical-pullback-Π f g c)
-      ( is-equiv-map-canonical-pullback-Π f g)
+      ( triangle-map-standard-pullback-Π f g c)
+      ( is-equiv-map-standard-pullback-Π f g)
       ( is-equiv-map-Π-is-fiberwise-equiv is-pb-c)
 ```
 
@@ -703,50 +701,46 @@ is-pullback-back-left-is-pullback-back-right-cube :
   {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
   {f' : A' → B'} {g' : A' → C'} {h' : B' → D'} {k' : C' → D'}
   {hA : A' → A} {hB : B' → B} {hC : C' → C} {hD : D' → D}
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
-  (c : coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
-    top back-left back-right front-left front-right bottom) →
-  is-pullback h hD (pair hB (pair h' front-left)) →
-  is-pullback k hD (pair hC (pair k' front-right)) →
-  is-pullback g hC (pair hA (pair g' back-right)) →
-  is-pullback f hB (pair hA (pair f' back-left))
+  (top : h' ∘ f' ~ k' ∘ g')
+  (back-left : f ∘ hA ~ hB ∘ f')
+  (back-right : g ∘ hA ~ hC ∘ g')
+  (front-left : h ∘ hB ~ hD ∘ h')
+  (front-right : k ∘ hC ~ hD ∘ k')
+  (bottom : h ∘ f ~ k ∘ g) →
+  (c :
+    coherence-cube-maps
+      f g h k f' g' h' k' hA hB hC hD
+      top back-left back-right front-left front-right bottom) →
+  is-pullback h hD (hB , h' , front-left) →
+  is-pullback k hD (hC , k' , front-right) →
+  is-pullback g hC (hA , g' , back-right) →
+  is-pullback f hB (hA , f' , back-left)
 is-pullback-back-left-is-pullback-back-right-cube
   {f = f} {g} {h} {k} {f' = f'} {g'} {h'} {k'} {hA = hA} {hB} {hC} {hD}
   top back-left back-right front-left front-right bottom c
   is-pb-front-left is-pb-front-right is-pb-back-right =
   is-pullback-left-square-is-pullback-rectangle f h hD
-    ( pair hB (pair h' front-left))
-    ( pair hA (pair f' back-left))
+    ( hB , h' , front-left)
+    ( hA , f' , back-left)
     ( is-pb-front-left)
     ( is-pullback-htpy
-      { f = h ∘ f}
-      -- ( k ∘ g)
       ( bottom)
-      { g = hD}
-      -- ( hD)
       ( refl-htpy)
-      { c = pair hA (pair (h' ∘ f')
-        ( rectangle-left-cube
-          f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom))}
-      ( pair hA (pair (k' ∘ g')
+      ( triple
+        ( hA)
+        ( k' ∘ g')
         ( rectangle-right-cube
           f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom)))
-      ( pair
+          top back-left back-right front-left front-right bottom))
+      ( triple
         ( refl-htpy)
-        ( pair top
-          ( coherence-htpy-parallel-cone-rectangle-left-rectangle-right-cube
-            f g h k f' g' h' k' hA hB hC hD
-            top back-left back-right front-left front-right bottom c)))
+        ( top)
+        ( coherence-htpy-parallel-cone-rectangle-left-rectangle-right-cube
+          f g h k f' g' h' k' hA hB hC hD
+          top back-left back-right front-left front-right bottom c))
       ( is-pullback-rectangle-is-pullback-left-square g k hD
-        ( pair hC (pair k' front-right))
-        ( pair hA (pair g' back-right))
+        ( hC , k' , front-right)
+        ( hA , g' , back-right)
         ( is-pb-front-right)
         ( is-pb-back-right)))
 
@@ -757,48 +751,46 @@ is-pullback-back-right-is-pullback-back-left-cube :
   {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
   {f' : A' → B'} {g' : A' → C'} {h' : B' → D'} {k' : C' → D'}
   {hA : A' → A} {hB : B' → B} {hC : C' → C} {hD : D' → D}
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
-  (c : coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
-    top back-left back-right front-left front-right bottom) →
-  is-pullback h hD (pair hB (pair h' front-left)) →
-  is-pullback k hD (pair hC (pair k' front-right)) →
-  is-pullback f hB (pair hA (pair f' back-left)) →
-  is-pullback g hC (pair hA (pair g' back-right))
+  (top : h' ∘ f' ~ k' ∘ g')
+  (back-left : f ∘ hA ~ hB ∘ f')
+  (back-right : g ∘ hA ~ hC ∘ g')
+  (front-left : h ∘ hB ~ hD ∘ h')
+  (front-right : k ∘ hC ~ hD ∘ k')
+  (bottom : h ∘ f ~ k ∘ g) →
+  (c :
+    coherence-cube-maps
+      f g h k f' g' h' k' hA hB hC hD
+      top back-left back-right front-left front-right bottom) →
+  is-pullback h hD (hB , h' , front-left) →
+  is-pullback k hD (hC , k' , front-right) →
+  is-pullback f hB (hA , f' , back-left) →
+  is-pullback g hC (hA , g' , back-right)
 is-pullback-back-right-is-pullback-back-left-cube
   {f = f} {g} {h} {k} {f' = f'} {g'} {h'} {k'} {hA = hA} {hB} {hC} {hD}
   top back-left back-right front-left front-right bottom c
   is-pb-front-left is-pb-front-right is-pb-back-left =
   is-pullback-left-square-is-pullback-rectangle g k hD
-    ( pair hC (pair k' front-right))
-    ( pair hA (pair g' back-right))
+    ( hC , k' , front-right)
+    ( hA , g' , back-right)
     ( is-pb-front-right)
     ( is-pullback-htpy'
-      { f' = k ∘ g}
       ( bottom)
-      { g' = hD}
       ( refl-htpy)
-      ( pair hA (pair (h' ∘ f')
+      ( triple
+        ( hA)
+        ( h' ∘ f')
         ( rectangle-left-cube
           f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom)))
-      { c' = pair hA (pair (k' ∘ g')
-        ( rectangle-right-cube
-          f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom))}
-      ( pair
+          top back-left back-right front-left front-right bottom))
+      ( triple
         ( refl-htpy)
-        ( pair top
-          ( coherence-htpy-parallel-cone-rectangle-left-rectangle-right-cube
-            f g h k f' g' h' k' hA hB hC hD
-            top back-left back-right front-left front-right bottom c)))
+        ( top)
+        ( coherence-htpy-parallel-cone-rectangle-left-rectangle-right-cube
+          f g h k f' g' h' k' hA hB hC hD
+          top back-left back-right front-left front-right bottom c))
       ( is-pullback-rectangle-is-pullback-left-square f h hD
-        ( pair hB (pair h' front-left))
-        ( pair hA (pair f' back-left))
+        ( hB , h' , front-left)
+        ( hA , f' , back-left)
         ( is-pb-front-left)
         ( is-pb-back-left)))
 ```
@@ -813,62 +805,51 @@ is-pullback-bottom-is-pullback-top-cube-is-equiv :
   {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
   (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
   (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
+  (top : h' ∘ f' ~ k' ∘ g')
+  (back-left : f ∘ hA ~ hB ∘ f')
+  (back-right : g ∘ hA ~ hC ∘ g')
+  (front-left : h ∘ hB ~ hD ∘ h')
+  (front-right : k ∘ hC ~ hD ∘ k')
+  (bottom : h ∘ f ~ k ∘ g) →
   (c :
-    coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
+    coherence-cube-maps
+      f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
   is-equiv hA → is-equiv hB → is-equiv hC → is-equiv hD →
-  is-pullback h' k' (pair f' (pair g' top)) →
-  is-pullback h k (pair f (pair g bottom))
+  is-pullback h' k' (f' , g' , top) →
+  is-pullback h k (f , g , bottom)
 is-pullback-bottom-is-pullback-top-cube-is-equiv
   f g h k f' g' h' k' hA hB hC hD
   top back-left back-right front-left front-right bottom c
   is-equiv-hA is-equiv-hB is-equiv-hC is-equiv-hD is-pb-top =
   descent-is-equiv hB h k
-    ( pair f (pair g bottom))
-    ( pair f' (pair hA (inv-htpy (back-left))))
+    ( f , g , bottom)
+    ( f' , hA , inv-htpy (back-left))
     ( is-equiv-hB)
     ( is-equiv-hA)
     ( is-pullback-htpy
-      {f = h ∘ hB}
-      -- ( hD ∘ h')
       ( front-left)
-      {g = k}
-      -- ( k)
       ( refl-htpy' k)
-      { c = pair f'
-        ( pair
-          ( g ∘ hA)
-          ( rectangle-back-left-bottom-cube
-            f g h k f' g' h' k' hA hB hC hD
-            top back-left back-right front-left front-right bottom))}
-      ( pair
+      ( triple
         ( f')
-        ( pair
-          ( hC ∘ g')
-          ( rectangle-top-front-right-cube
-            f g h k f' g' h' k' hA hB hC hD
-            top back-left back-right front-left front-right bottom)))
-      ( pair
+        ( hC ∘ g')
+        ( rectangle-top-front-right-cube
+          f g h k f' g' h' k' hA hB hC hD
+          top back-left back-right front-left front-right bottom))
+      ( triple
         ( refl-htpy' f')
-        ( pair
-          ( back-right)
-          ( coherence-htpy-parallel-cone-coherence-cube-maps
-            f g h k f' g' h' k' hA hB hC hD
-            top back-left back-right front-left front-right bottom c)))
+        ( back-right)
+        ( coherence-htpy-parallel-cone-coherence-cube-maps
+          f g h k f' g' h' k' hA hB hC hD
+          top back-left back-right front-left front-right bottom c))
       ( is-pullback-rectangle-is-pullback-left-square
         ( h')
         ( hD)
         ( k)
-        ( pair k' (pair hC (inv-htpy front-right)))
-        ( pair f' (pair g' top))
+        ( k' , hC , inv-htpy front-right)
+        ( f' , g' , top)
         ( is-pullback-is-equiv' hD k
-          ( pair k' (pair hC (inv-htpy front-right)))
+          ( k' , hC , inv-htpy front-right)
           ( is-equiv-hD)
           ( is-equiv-hC))
         ( is-pb-top)))
@@ -880,54 +861,50 @@ is-pullback-top-is-pullback-bottom-cube-is-equiv :
   {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
   (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
   (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
+  (top : h' ∘ f' ~ k' ∘ g')
+  (back-left : f ∘ hA ~ hB ∘ f')
+  (back-right : g ∘ hA ~ hC ∘ g')
+  (front-left : h ∘ hB ~ hD ∘ h')
+  (front-right : k ∘ hC ~ hD ∘ k')
+  (bottom : h ∘ f ~ k ∘ g) →
   (c :
-    coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
+    coherence-cube-maps
+      f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
   is-equiv hA → is-equiv hB → is-equiv hC → is-equiv hD →
-  is-pullback h k (pair f (pair g bottom)) →
-  is-pullback h' k' (pair f' (pair g' top))
+  is-pullback h k (f , g , bottom) →
+  is-pullback h' k' (f' , g' , top)
 is-pullback-top-is-pullback-bottom-cube-is-equiv
   f g h k f' g' h' k' hA hB hC hD
   top back-left back-right front-left front-right bottom c
   is-equiv-hA is-equiv-hB is-equiv-hC is-equiv-hD is-pb-bottom =
   is-pullback-top-is-pullback-rectangle h hD k'
-    ( pair hB (pair h' front-left))
-    ( pair f' (pair g' top))
+    ( hB , h' , front-left)
+    ( f' , g' , top)
     ( is-pullback-is-equiv h hD
-      ( pair hB (pair h' front-left))
+      ( hB , h' , front-left)
       is-equiv-hD is-equiv-hB)
     ( is-pullback-htpy' refl-htpy front-right
       ( pasting-vertical-cone h k hC
-        ( pair f (pair g bottom))
-        ( pair hA (pair g' back-right)))
-      { c' = pasting-vertical-cone h hD k'
-        ( pair hB (pair h' front-left))
-        ( pair f' (pair g' top))}
-      ( pair back-left
-        ( pair
-          ( refl-htpy)
-          ( ( ( ( assoc-htpy
-                    ( bottom ·r hA) (k ·l back-right) (front-right ·r g')) ∙h
-                ( inv-htpy c)) ∙h
-              ( assoc-htpy
-                  ( h ·l back-left) (front-left ·r f') (hD ·l top))) ∙h
-            ( ap-concat-htpy'
-              ( h ·l back-left)
-              ( (h ·l back-left) ∙h refl-htpy)
-              ( (front-left ·r f') ∙h (hD ·l top))
-              ( inv-htpy-right-unit-htpy)))))
+        ( f , g , bottom)
+        ( hA , g' , back-right))
+      ( triple
+        ( back-left)
+        ( refl-htpy)
+        ( ( assoc-htpy (bottom ·r hA) (k ·l back-right) (front-right ·r g')) ∙h
+          ( inv-htpy c) ∙h
+          ( assoc-htpy (h ·l back-left) (front-left ·r f') (hD ·l top)) ∙h
+          ( ap-concat-htpy'
+            ( h ·l back-left)
+            ( (h ·l back-left) ∙h refl-htpy)
+            ( (front-left ·r f') ∙h (hD ·l top))
+            ( inv-htpy-right-unit-htpy))))
       ( is-pullback-rectangle-is-pullback-top h k hC
-        ( pair f (pair g bottom))
-        ( pair hA (pair g' back-right))
+        ( f , g , bottom)
+        ( hA , g' , back-right)
         ( is-pb-bottom)
         ( is-pullback-is-equiv g hC
-          ( pair hA (pair g' back-right))
+          ( hA , g' , back-right)
           is-equiv-hC is-equiv-hA)))
 ```
 
@@ -941,18 +918,19 @@ is-pullback-front-left-is-pullback-back-right-cube-is-equiv :
   {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
   (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
   (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
+  (top : h' ∘ f' ~ k' ∘ g')
+  (back-left : f ∘ hA ~ hB ∘ f')
+  (back-right : g ∘ hA ~ hC ∘ g')
+  (front-left : h ∘ hB ~ hD ∘ h')
+  (front-right : k ∘ hC ~ hD ∘ k')
+  (bottom : h ∘ f ~ k ∘ g) →
   (c :
-    coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
+    coherence-cube-maps
+      f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
   is-equiv f' → is-equiv f → is-equiv k' → is-equiv k →
-  is-pullback g hC (pair hA (pair g' back-right)) →
-  is-pullback h hD (pair hB (pair h' front-left))
+  is-pullback g hC (hA , g' , back-right) →
+  is-pullback h hD (hB , h' , front-left)
 is-pullback-front-left-is-pullback-back-right-cube-is-equiv
   f g h k f' g' h' k' hA hB hC hD
   top back-left back-right front-left front-right bottom c
@@ -971,18 +949,19 @@ is-pullback-front-right-is-pullback-back-left-cube-is-equiv :
   {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
   (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
   (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
+  (top : h' ∘ f' ~ k' ∘ g')
+  (back-left : f ∘ hA ~ hB ∘ f')
+  (back-right : g ∘ hA ~ hC ∘ g')
+  (front-left : h ∘ hB ~ hD ∘ h')
+  (front-right : k ∘ hC ~ hD ∘ k')
+  (bottom : h ∘ f ~ k ∘ g) →
   (c :
-    coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
+    coherence-cube-maps
+      f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
   is-equiv g' → is-equiv h' → is-equiv g → is-equiv h →
-  is-pullback f hB (pair hA (pair f' back-left)) →
-  is-pullback k hD (pair hC (pair k' front-right))
+  is-pullback f hB (hA , f' , back-left) →
+  is-pullback k hD (hC , k' , front-right)
 is-pullback-front-right-is-pullback-back-left-cube-is-equiv
   f g h k f' g' h' k' hA hB hC hD
   top back-left back-right front-left front-right bottom c
@@ -1007,12 +986,12 @@ cone-ap :
       H = pr2 (pr2 c)
   in
   cone
-    ( λ (α : Id (p c1) (p c2)) → (ap f α) ∙ (H c2))
-    ( λ (β : Id (q c1) (q c2)) → (H c1) ∙ (ap g β))
-    ( Id c1 c2)
-pr1 (cone-ap f g (pair p (pair q H)) c1 c2) = ap p
-pr1 (pr2 (cone-ap f g (pair p (pair q H)) c1 c2)) = ap q
-pr2 (pr2 (cone-ap f g (pair p (pair q H)) c1 c2)) γ =
+    ( λ (α : p c1 ＝ p c2) → ap f α ∙ H c2)
+    ( λ (β : q c1 ＝ q c2) → H c1 ∙ ap g β)
+    ( c1 ＝ c2)
+pr1 (cone-ap f g (p , q , H) c1 c2) = ap p
+pr1 (pr2 (cone-ap f g (p , q , H) c1 c2)) = ap q
+pr2 (pr2 (cone-ap f g (p , q , H) c1 c2)) γ =
   ( ap (λ t → t ∙ (H c2)) (inv (ap-comp f p γ))) ∙
   ( ( inv-nat-htpy H γ) ∙
     ( ap (λ t → (H c1) ∙ t) (ap-comp g q γ)))
@@ -1025,16 +1004,16 @@ cone-ap' :
       H = pr2 (pr2 c)
   in
   cone
-    ( λ (α : Id (p c1) (p c2)) → tr (λ t → Id (f (p c1)) t) (H c2) (ap f α))
-    ( λ (β : Id (q c1) (q c2)) → (H c1) ∙ (ap g β))
-    ( Id c1 c2)
-pr1 (cone-ap' f g (pair p (pair q H)) c1 c2) = ap p
-pr1 (pr2 (cone-ap' f g (pair p (pair q H)) c1 c2)) = ap q
-pr2 (pr2 (cone-ap' f g (pair p (pair q H)) c1 c2)) γ =
+    ( λ (α : p c1 ＝ p c2) → tr (f (p c1) ＝_) (H c2) (ap f α))
+    ( λ (β : q c1 ＝ q c2) → H c1 ∙ ap g β)
+    ( c1 ＝ c2)
+pr1 (cone-ap' f g (p , q , H) c1 c2) = ap p
+pr1 (pr2 (cone-ap' f g (p , q , H) c1 c2)) = ap q
+pr2 (pr2 (cone-ap' f g (p , q , H) c1 c2)) γ =
   ( tr-Id-right (H c2) (ap f (ap p γ))) ∙
-  ( ( ap (λ t → t ∙ (H c2)) (inv (ap-comp f p γ))) ∙
+  ( ( ap (_∙ H c2) (inv (ap-comp f p γ))) ∙
     ( ( inv-nat-htpy H γ) ∙
-      ( ap (λ t → (H c1) ∙ t) (ap-comp g q γ))))
+      ( ap (H c1 ∙_) (ap-comp g q γ))))
 
 is-pullback-cone-ap :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
@@ -1045,34 +1024,33 @@ is-pullback-cone-ap :
       H = pr2 (pr2 c)
   in
   is-pullback
-    ( λ (α : Id (vertical-map-cone f g c c1) (vertical-map-cone f g c c2)) →
-      (ap f α) ∙ (coherence-square-cone f g c c2))
-    ( λ (β : Id (horizontal-map-cone f g c c1) (horizontal-map-cone f g c c2)) →
-      (H c1) ∙ (ap g β))
+    ( λ (α : vertical-map-cone f g c c1 ＝ vertical-map-cone f g c c2) →
+      ap f α ∙ coherence-square-cone f g c c2)
+    ( λ (β : horizontal-map-cone f g c c1 ＝ horizontal-map-cone f g c c2) →
+      H c1 ∙ ap g β)
     ( cone-ap f g c c1 c2)
-is-pullback-cone-ap f g (pair p (pair q H)) is-pb-c c1 c2 =
+is-pullback-cone-ap f g (p , q , H) is-pb-c c1 c2 =
   is-pullback-htpy'
     ( λ α → tr-Id-right (H c2) (ap f α))
     ( refl-htpy)
-    ( cone-ap' f g (pair p (pair q H)) c1 c2)
-    { c' = cone-ap f g (pair p (pair q H)) c1 c2}
-    ( pair refl-htpy (pair refl-htpy right-unit-htpy))
+    ( cone-ap' f g (p , q , H) c1 c2)
+    ( refl-htpy , refl-htpy , right-unit-htpy)
     ( is-pullback-family-is-pullback-tot
-      ( λ x → Id (f (p c1)) x)
+      ( f (p c1) ＝_)
       ( λ a → ap f {x = p c1} {y = a})
-      ( λ b β → (H c1) ∙ (ap g β))
-      ( pair p (pair q H))
-      ( cone-ap' f g (pair p (pair q H)) c1)
+      ( λ b β → H c1 ∙ ap g β)
+      ( p , q , H)
+      ( cone-ap' f g (p , q , H) c1)
       ( is-pb-c)
       ( is-pullback-is-equiv
         ( map-Σ _ f (λ a α → ap f α))
-        ( map-Σ _ g (λ b β → (H c1) ∙ (ap g β)))
+        ( map-Σ _ g (λ b β → H c1 ∙ ap g β))
         ( tot-cone-cone-family
-          ( Id (f (p c1)))
+          ( f (p c1) ＝_)
           ( λ a → ap f)
-          ( λ b β → (H c1) ∙ (ap g β))
-          ( pair p (pair q H))
-          ( cone-ap' f g (pair p (pair q H)) c1))
+          ( λ b β → H c1 ∙ ap g β)
+          ( p , q , H)
+          ( cone-ap' f g (p , q , H) c1))
         ( is-equiv-is-contr _
           ( is-contr-total-path (q c1))
           ( is-contr-total-path (f (p c1))))
@@ -1081,3 +1059,9 @@ is-pullback-cone-ap f g (pair p (pair q H)) is-pb-c c1 c2 =
           ( is-contr-total-path (p c1))))
       ( c2))
 ```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/foundation/sequences.lagda.md b/src/foundation/sequences.lagda.md
index 53f07d5c44..5a8b9fa482 100644
--- a/src/foundation/sequences.lagda.md
+++ b/src/foundation/sequences.lagda.md
@@ -7,8 +7,6 @@ module foundation.sequences where
 <details><summary>Imports</summary>
 
 ```agda
-open import elementary-number-theory.natural-numbers
-
 open import foundation.dependent-sequences
 open import foundation.universe-levels
 
diff --git a/src/foundation/sequential-limits.lagda.md b/src/foundation/sequential-limits.lagda.md
new file mode 100644
index 0000000000..216a24d8be
--- /dev/null
+++ b/src/foundation/sequential-limits.lagda.md
@@ -0,0 +1,294 @@
+# Sequential limits
+
+```agda
+module foundation.sequential-limits where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-homotopies
+open import foundation.cones-over-towers
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-function-types
+open import foundation.equivalences
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopy-induction
+open import foundation.structure-identity-principle
+open import foundation.towers
+open import foundation.universal-property-sequential-limits
+open import foundation.universe-levels
+
+open import foundation-core.contractible-types
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+Given a [tower of types](foundation.towers.md)
+
+```text
+               fₙ                     f₁      f₀
+  ⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₂ ---> A₁ ---> A₀
+```
+
+we can form the **standard sequential limit** `limₙ Aₙ` satisfying
+[the universal property of the sequential limit](foundation.universal-property-sequential-limits.md)
+of `Aₙ` thus completing the diagram
+
+```text
+                           fₙ                     f₁      f₀
+  limₙ Aₙ ---> ⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₂ ---> A₁ ---> A₀.
+```
+
+The standard sequential limit consists of "points at infinity", which can be
+recorded as [sequences](foundation.dependent-sequences.md) of terms whose images
+under `f` agree:
+
+```text
+  ⋯  ↦   xₙ₊₁  ↦   xₙ  ↦   ⋯  ↦   x₂  ↦   x₁  ↦   x₀
+          ⫙        ⫙              ⫙       ⫙       ⫙
+  ⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₂ ---> A₁ ---> A₀.
+```
+
+## Definitions
+
+### The standard sequential limit
+
+```agda
+module _
+  {l : Level} (A : tower l)
+  where
+
+  standard-sequential-limit : UU l
+  standard-sequential-limit =
+    Σ ( (n : ℕ) → type-tower A n)
+      ( λ a → (n : ℕ) → a n ＝ map-tower A n (a (succ-ℕ n)))
+
+module _
+  {l : Level} (A : tower l)
+  where
+
+  sequence-standard-sequential-limit :
+    standard-sequential-limit A → (n : ℕ) → type-tower A n
+  sequence-standard-sequential-limit = pr1
+
+  coherence-standard-sequential-limit :
+    (x : standard-sequential-limit A) (n : ℕ) →
+    sequence-standard-sequential-limit x n ＝
+    map-tower A n (sequence-standard-sequential-limit x (succ-ℕ n))
+  coherence-standard-sequential-limit = pr2
+```
+
+### The cone at the standard sequential limit
+
+```agda
+module _
+  {l : Level} (A : tower l)
+  where
+
+  cone-standard-sequential-limit : cone-tower A (standard-sequential-limit A)
+  pr1 cone-standard-sequential-limit n x =
+    sequence-standard-sequential-limit A x n
+  pr2 cone-standard-sequential-limit n x =
+    coherence-standard-sequential-limit A x n
+```
+
+### The gap map into the standard sequential limit
+
+The **gap map** of a [cone over a tower](foundation.cones-over-towers.md) is the
+map from the domain of the cone into the standard sequential limit.
+
+```agda
+module _
+  {l1 l2 : Level} (A : tower l1) {X : UU l2}
+  where
+
+  gap-tower : cone-tower A X → X → standard-sequential-limit A
+  pr1 (gap-tower c x) n = map-cone-tower A c n x
+  pr2 (gap-tower c x) n = coherence-cone-tower A c n x
+```
+
+### The property of being a sequential limit
+
+The [proposition](foundation-core.propositions.md) `is-sequential-limit` is the
+assertion that the gap map is an [equivalence](foundation-core.equivalences.md).
+Note that this proposition is [small](foundation-core.small-types.md), whereas
+[the universal property](foundation.universal-property-sequential-limits.md) is
+a large proposition.
+
+```agda
+module _
+  {l1 l2 : Level} (A : tower l1) {X : UU l2}
+  where
+
+  is-sequential-limit : cone-tower A X → UU (l1 ⊔ l2)
+  is-sequential-limit c = is-equiv (gap-tower A c)
+
+  is-property-is-sequential-limit :
+    (c : cone-tower A X) → is-prop (is-sequential-limit c)
+  is-property-is-sequential-limit c = is-property-is-equiv (gap-tower A c)
+
+  is-sequential-limit-Prop : (c : cone-tower A X) → Prop (l1 ⊔ l2)
+  pr1 (is-sequential-limit-Prop c) = is-sequential-limit c
+  pr2 (is-sequential-limit-Prop c) = is-property-is-sequential-limit c
+```
+
+## Properties
+
+### Characterization of equality in the standard sequential limit
+
+```agda
+module _
+  {l : Level} (A : tower l)
+  where
+
+  Eq-standard-sequential-limit : (s t : standard-sequential-limit A) → UU l
+  Eq-standard-sequential-limit s t =
+    Σ ( sequence-standard-sequential-limit A s ~
+        sequence-standard-sequential-limit A t)
+      ( λ H →
+        coherence-square-homotopies
+          ( coherence-standard-sequential-limit A s)
+          ( λ n → ap (map-tower A n) (H (succ-ℕ n)))
+          ( H)
+          ( coherence-standard-sequential-limit A t))
+
+  refl-Eq-standard-sequential-limit :
+    (s : standard-sequential-limit A) → Eq-standard-sequential-limit s s
+  pr1 (refl-Eq-standard-sequential-limit s) = refl-htpy
+  pr2 (refl-Eq-standard-sequential-limit s) = right-unit-htpy
+
+  Eq-eq-standard-sequential-limit :
+    (s t : standard-sequential-limit A) →
+    s ＝ t → Eq-standard-sequential-limit s t
+  Eq-eq-standard-sequential-limit s .s refl =
+    refl-Eq-standard-sequential-limit s
+
+  is-contr-total-Eq-standard-sequential-limit :
+    (s : standard-sequential-limit A) →
+    is-contr (Σ (standard-sequential-limit A) (Eq-standard-sequential-limit s))
+  is-contr-total-Eq-standard-sequential-limit s =
+    is-contr-total-Eq-structure _
+      ( is-contr-total-htpy (pr1 s))
+      ( pr1 s , refl-htpy)
+      ( is-contr-total-Eq-Π _ (λ n → is-contr-total-path (pr2 s n ∙ refl)))
+
+  is-equiv-Eq-eq-standard-sequential-limit :
+    (s t : standard-sequential-limit A) →
+    is-equiv (Eq-eq-standard-sequential-limit s t)
+  is-equiv-Eq-eq-standard-sequential-limit s =
+    fundamental-theorem-id
+      ( is-contr-total-Eq-standard-sequential-limit s)
+      ( Eq-eq-standard-sequential-limit s)
+
+  extensionality-standard-sequential-limit :
+    (s t : standard-sequential-limit A) →
+    (s ＝ t) ≃ Eq-standard-sequential-limit s t
+  pr1 (extensionality-standard-sequential-limit s t) =
+    Eq-eq-standard-sequential-limit s t
+  pr2 (extensionality-standard-sequential-limit s t) =
+    is-equiv-Eq-eq-standard-sequential-limit s t
+
+  eq-Eq-standard-sequential-limit :
+    (s t : standard-sequential-limit A) →
+    Eq-standard-sequential-limit s t → s ＝ t
+  eq-Eq-standard-sequential-limit s t =
+    map-inv-equiv (extensionality-standard-sequential-limit s t)
+```
+
+### The standard sequential limit satisfies the universal property of a sequential limit
+
+```agda
+module _
+  {l1 : Level} (A : tower l1)
+  where
+
+  cone-map-standard-sequential-limit :
+    {l : Level} {Y : UU l} → (Y → standard-sequential-limit A) → cone-tower A Y
+  cone-map-standard-sequential-limit {Y = Y} =
+    cone-map-tower A {Y = Y} (cone-standard-sequential-limit A)
+
+  is-retraction-gap-tower :
+    {l : Level} {Y : UU l} →
+    gap-tower A ∘ cone-map-standard-sequential-limit {Y = Y} ~ id
+  is-retraction-gap-tower x = refl
+
+  is-section-gap-tower :
+    {l : Level} {Y : UU l} →
+    cone-map-standard-sequential-limit {Y = Y} ∘ gap-tower A ~ id
+  is-section-gap-tower x = refl
+
+  universal-property-standard-sequential-limit :
+    {l : Level} →
+    universal-property-sequential-limit l A (cone-standard-sequential-limit A)
+  pr1 (pr1 (universal-property-standard-sequential-limit X)) = gap-tower A
+  pr2 (pr1 (universal-property-standard-sequential-limit X)) =
+    is-section-gap-tower
+  pr1 (pr2 (universal-property-standard-sequential-limit X)) = gap-tower A
+  pr2 (pr2 (universal-property-standard-sequential-limit X)) =
+    is-retraction-gap-tower
+```
+
+### A cone over a tower is equal to the value of `cone-map-tower` at its own gap map
+
+```agda
+module _
+  {l1 l2 : Level} (A : tower l1) {X : UU l2}
+  where
+
+  htpy-cone-up-pullback-standard-sequential-limit :
+    (c : cone-tower A X) →
+    htpy-cone-tower A
+      ( cone-map-tower A (cone-standard-sequential-limit A) (gap-tower A c))
+      ( c)
+  pr1 (htpy-cone-up-pullback-standard-sequential-limit c) n = refl-htpy
+  pr2 (htpy-cone-up-pullback-standard-sequential-limit c) n = right-unit-htpy
+```
+
+### A cone satisfies the universal property of the limit if and only if the gap map is an equivalence
+
+```agda
+module _
+  {l1 l2 : Level} (A : tower l1) {X : UU l2}
+  where
+
+  is-sequential-limit-universal-property-sequential-limit :
+    (c : cone-tower A X) →
+    ({l : Level} → universal-property-sequential-limit l A c) →
+    is-sequential-limit A c
+  is-sequential-limit-universal-property-sequential-limit c =
+    is-equiv-universal-property-sequential-limit-universal-property-sequential-limit
+      ( cone-standard-sequential-limit A)
+      ( c)
+      ( gap-tower A c)
+      ( htpy-cone-up-pullback-standard-sequential-limit A c)
+      ( universal-property-standard-sequential-limit A)
+
+  universal-property-is-sequential-limit :
+    (c : cone-tower A X) → is-sequential-limit A c →
+    {l : Level} → universal-property-sequential-limit l A c
+  universal-property-is-sequential-limit c is-lim-c =
+    universal-property-sequential-limit-universal-property-sequential-limit-is-equiv
+      ( cone-standard-sequential-limit A)
+      ( c)
+      ( gap-tower A c)
+      ( htpy-cone-up-pullback-standard-sequential-limit A c)
+      ( is-lim-c)
+      ( universal-property-standard-sequential-limit A)
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
diff --git a/src/foundation/subuniverses.lagda.md b/src/foundation/subuniverses.lagda.md
index f327d3afe6..2cfa64f9c4 100644
--- a/src/foundation/subuniverses.lagda.md
+++ b/src/foundation/subuniverses.lagda.md
@@ -10,7 +10,6 @@ module foundation.subuniverses where
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-function-types
 open import foundation.equivalences
-open import foundation.functoriality-dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.subtype-identity-principle
 open import foundation.type-arithmetic-dependent-pair-types
@@ -20,6 +19,7 @@ open import foundation.universe-levels
 open import foundation-core.contractible-types
 open import foundation-core.embeddings
 open import foundation-core.fibers-of-maps
+open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.identity-types
 open import foundation-core.propositions
 open import foundation-core.subtypes
diff --git a/src/foundation/symmetric-operations.lagda.md b/src/foundation/symmetric-operations.lagda.md
index 78211eaa74..d2a140ab19 100644
--- a/src/foundation/symmetric-operations.lagda.md
+++ b/src/foundation/symmetric-operations.lagda.md
@@ -143,7 +143,6 @@ module _
     symmetric-operation-is-commutative f H (standard-unordered-pair x y) ＝
     f x y
   compute-symmetric-operation-is-commutative f H x y =
-
     htpy-universal-property-set-quotient-trunc-Prop B
       ( λ e → f (p (map-equiv e (zero-Fin 1))) (p (map-equiv e (one-Fin 1))))
       ( λ e e' →
diff --git a/src/foundation/towers.lagda.md b/src/foundation/towers.lagda.md
new file mode 100644
index 0000000000..da4966c9b6
--- /dev/null
+++ b/src/foundation/towers.lagda.md
@@ -0,0 +1,91 @@
+# Towers of types
+
+```agda
+module foundation.towers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.iterating-functions
+open import foundation.unit-type
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A **tower of types** `A` is a [sequence](foundation.sequences.md) of types
+together with maps between every two consecutive types
+
+```text
+  fₙ : Aₙ₊₁ → Aₙ
+```
+
+giving a sequential diagram of maps that extend infinitely to the left:
+
+```text
+     f₃      f₂      f₁      f₀
+  ⋯ ---> A₃ ---> A₂ ---> A₁ ---> A₀.
+```
+
+## Definitions
+
+### Towers of types
+
+```agda
+sequence-map-tower : {l : Level} → (ℕ → UU l) → UU l
+sequence-map-tower A = (n : ℕ) → A (succ-ℕ n) → A n
+
+tower : (l : Level) → UU (lsuc l)
+tower l = Σ (ℕ → UU l) (sequence-map-tower)
+
+type-tower : {l : Level} → tower l → ℕ → UU l
+type-tower = pr1
+
+map-tower :
+  {l : Level} (A : tower l) (n : ℕ) → type-tower A (succ-ℕ n) → type-tower A n
+map-tower = pr2
+```
+
+## Operations
+
+### Right shifting a tower
+
+We can **right shift** a tower of types by forgetting the first terms.
+
+```agda
+right-shift-tower : {l : Level} → tower l → tower l
+pr1 (right-shift-tower A) n = type-tower A (succ-ℕ n)
+pr2 (right-shift-tower A) n = map-tower A (succ-ℕ n)
+
+iterated-right-shift-tower : {l : Level} (n : ℕ) → tower l → tower l
+iterated-right-shift-tower n = iterate n right-shift-tower
+```
+
+### Left shifting a tower
+
+We can **left shift** a tower of types by padding it with the
+[terminal type](foundation.unit-type.md) `unit`.
+
+```agda
+left-shift-tower : {l : Level} → tower l → tower l
+pr1 (left-shift-tower {l} A) zero-ℕ = raise-unit l
+pr1 (left-shift-tower A) (succ-ℕ n) = type-tower A n
+pr2 (left-shift-tower A) zero-ℕ = raise-terminal-map
+pr2 (left-shift-tower A) (succ-ℕ n) = map-tower A n
+
+iterated-left-shift-tower : {l : Level} (n : ℕ) → tower l → tower l
+iterated-left-shift-tower n = iterate n left-shift-tower
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
diff --git a/src/foundation/transfinite-cocomposition-of-maps.lagda.md b/src/foundation/transfinite-cocomposition-of-maps.lagda.md
new file mode 100644
index 0000000000..2e7981028a
--- /dev/null
+++ b/src/foundation/transfinite-cocomposition-of-maps.lagda.md
@@ -0,0 +1,49 @@
+# Transfinite cocomposition of maps
+
+```agda
+module foundation.transfinite-cocomposition-of-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.sequential-limits
+open import foundation.towers
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given a [tower](foundation.towers.md) of maps, i.e. a certain infinite
+[sequence](foundation.dependent-sequences.md) of maps `fₙ`:
+
+```text
+      ⋯        fₙ      ⋯      f₁      f₀
+  ⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₁ ---> A₀,
+```
+
+we can form the **transfinite cocomposition** of `f` by taking the canonical map
+from the [standard sequential limit](foundation.sequential-limits.md) `limₙ Aₙ`
+into `A₀`.
+
+## Definitions
+
+### The transfinite cocomposition of a tower of maps
+
+```agda
+module _
+  {l : Level} (f : tower l)
+  where
+
+  transfinite-cocomp : standard-sequential-limit f → type-tower f 0
+  transfinite-cocomp x = sequence-standard-sequential-limit f x 0
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
diff --git a/src/foundation/unions-subtypes.lagda.md b/src/foundation/unions-subtypes.lagda.md
index bc93e5ed64..35bcadff24 100644
--- a/src/foundation/unions-subtypes.lagda.md
+++ b/src/foundation/unions-subtypes.lagda.md
@@ -24,8 +24,8 @@ open import order-theory.least-upper-bounds-large-posets
 
 ## Idea
 
-The union of two subtypes `A` and `B` is the subtype that contains the elements
-that are in `A` or in `B`.
+The **union** of two [subtypes](foundation-core.subtypes.md) `A` and `B` is the
+subtype that contains the elements that are in `A` or in `B`.
 
 ## Definition
 
diff --git a/src/foundation/unit-type.lagda.md b/src/foundation/unit-type.lagda.md
index af08b70308..da71da93d1 100644
--- a/src/foundation/unit-type.lagda.md
+++ b/src/foundation/unit-type.lagda.md
@@ -68,6 +68,9 @@ raise-unit l = raise l unit
 raise-star : {l : Level} → raise l unit
 raise-star = map-raise star
 
+raise-terminal-map : {l1 l2 : Level} {A : UU l1} → A → raise-unit l2
+raise-terminal-map {l2 = l2} = const _ (raise-unit l2) raise-star
+
 compute-raise-unit : (l : Level) → unit ≃ raise-unit l
 compute-raise-unit l = compute-raise l unit
 ```
diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md
index 3409e6f96d..4cba37f1d2 100644
--- a/src/foundation/universal-property-cartesian-product-types.lagda.md
+++ b/src/foundation/universal-property-cartesian-product-types.lagda.md
@@ -63,18 +63,18 @@ We construct the cone for two maps into the unit type.
 Cartesian products are a special case of pullbacks.
 
 ```agda
-  gap-prod : A × B → canonical-pullback (const A unit star) (const B unit star)
+  gap-prod : A × B → standard-pullback (const A unit star) (const B unit star)
   gap-prod = gap (const A unit star) (const B unit star) cone-prod
 
   inv-gap-prod :
-    canonical-pullback (const A unit star) (const B unit star) → A × B
+    standard-pullback (const A unit star) (const B unit star) → A × B
   pr1 (inv-gap-prod (pair a (pair b p))) = a
   pr2 (inv-gap-prod (pair a (pair b p))) = b
 
   abstract
     is-section-inv-gap-prod : (gap-prod ∘ inv-gap-prod) ~ id
     is-section-inv-gap-prod (pair a (pair b p)) =
-      map-extensionality-canonical-pullback
+      map-extensionality-standard-pullback
         ( const A unit star)
         ( const B unit star)
         ( refl)
diff --git a/src/foundation/universal-property-fiber-products.lagda.md b/src/foundation/universal-property-fiber-products.lagda.md
index a3c3571684..ca15f68dab 100644
--- a/src/foundation/universal-property-fiber-products.lagda.md
+++ b/src/foundation/universal-property-fiber-products.lagda.md
@@ -51,11 +51,11 @@ map.
 
 ```agda
   gap-fiberwise-prod :
-    Σ X (λ x → (P x) × (Q x)) → canonical-pullback (pr1 {B = P}) (pr1 {B = Q})
+    Σ X (λ x → (P x) × (Q x)) → standard-pullback (pr1 {B = P}) (pr1 {B = Q})
   gap-fiberwise-prod = gap pr1 pr1 cone-fiberwise-prod
 
   inv-gap-fiberwise-prod :
-    canonical-pullback (pr1 {B = P}) (pr1 {B = Q}) → Σ X (λ x → (P x) × (Q x))
+    standard-pullback (pr1 {B = P}) (pr1 {B = Q}) → Σ X (λ x → (P x) × (Q x))
   pr1 (inv-gap-fiberwise-prod ((x , p) , ((.x , q) , refl))) = x
   pr1 (pr2 (inv-gap-fiberwise-prod ((x , p) , ((.x , q) , refl)))) = p
   pr2 (pr2 (inv-gap-fiberwise-prod ((x , p) , ((.x , q) , refl)))) = q
@@ -103,11 +103,11 @@ module _
   pr2 (pr2 cone-total-prod-fibers) (x , (a , p) , (b , q)) = p ∙ inv q
 
   gap-total-prod-fibers :
-    Σ X (λ x → (fiber f x) × (fiber g x)) → canonical-pullback f g
+    Σ X (λ x → (fiber f x) × (fiber g x)) → standard-pullback f g
   gap-total-prod-fibers = gap f g cone-total-prod-fibers
 
   inv-gap-total-prod-fibers :
-    canonical-pullback f g → Σ X (λ x → (fiber f x) × (fiber g x))
+    standard-pullback f g → Σ X (λ x → (fiber f x) × (fiber g x))
   pr1 (inv-gap-total-prod-fibers (a , b , p)) = g b
   pr1 (pr1 (pr2 (inv-gap-total-prod-fibers (a , b , p)))) = a
   pr2 (pr1 (pr2 (inv-gap-total-prod-fibers (a , b , p)))) = p
@@ -118,7 +118,7 @@ module _
     is-section-inv-gap-total-prod-fibers :
       (gap-total-prod-fibers ∘ inv-gap-total-prod-fibers) ~ id
     is-section-inv-gap-total-prod-fibers (a , b , p) =
-      map-extensionality-canonical-pullback f g refl refl
+      map-extensionality-standard-pullback f g refl refl
         ( inv right-unit ∙ inv right-unit)
 
   abstract
diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md
index fe171fbc6e..73c8bfbbf0 100644
--- a/src/foundation/universal-property-pullbacks.lagda.md
+++ b/src/foundation/universal-property-pullbacks.lagda.md
@@ -47,7 +47,7 @@ A -----> X
 
 ## Properties
 
-### The universal property is a property
+### The universal property of pullbacks at a universe level is a property
 
 ```agda
 module _
@@ -60,19 +60,6 @@ module _
       is-prop (universal-property-pullback l5 f g c)
     is-prop-universal-property-pullback =
       is-prop-Π (λ C' → is-property-is-equiv (cone-map f g c))
-
-  map-universal-property-pullback :
-    ({l : Level} → universal-property-pullback l f g c) →
-    {C' : UU l5} (c' : cone f g C') → C' → C
-  map-universal-property-pullback up-c {C'} c' =
-    map-inv-is-equiv (up-c C') c'
-
-  eq-map-universal-property-pullback :
-    (up-c : {l : Level} → universal-property-pullback l f g c) →
-    {C' : UU l5} (c' : cone f g C') →
-    cone-map f g c (map-universal-property-pullback up-c c') ＝ c'
-  eq-map-universal-property-pullback up-c {C'} c' =
-    is-section-map-inv-is-equiv (up-c C') c'
 ```
 
 ### The homotopy of cones obtained from the universal property of pullbacks
@@ -93,7 +80,7 @@ module _
     htpy-eq-cone f g
       ( cone-map f g c (map-universal-property-pullback f g c up c'))
       ( c')
-      ( eq-map-universal-property-pullback f g c up c')
+      ( compute-map-universal-property-pullback f g c up c')
 ```
 
 ### Uniquely uniqueness of pullbacks
@@ -122,3 +109,9 @@ module _
           ( htpy-cone-map-universal-property-pullback f g c up-c c')
           up-c up-c')
 ```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/foundation/universal-property-sequential-limits.lagda.md b/src/foundation/universal-property-sequential-limits.lagda.md
new file mode 100644
index 0000000000..e9eac427f1
--- /dev/null
+++ b/src/foundation/universal-property-sequential-limits.lagda.md
@@ -0,0 +1,252 @@
+# The universal property of sequential limits
+
+```agda
+module foundation.universal-property-sequential-limits where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cones-over-towers
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.subtype-identity-principle
+open import foundation.towers
+open import foundation.universe-levels
+
+open import foundation-core.contractible-maps
+open import foundation-core.contractible-types
+open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-pair-types
+open import foundation-core.functoriality-function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+Given a [tower of types](foundation.towers.md)
+
+```text
+               fₙ                     f₁      f₀
+  ⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₂ ---> A₁ ---> A₀
+```
+
+the **sequential limit** `limₙ Aₙ` is a universal type completing the diagram
+
+```text
+                           fₙ                     f₁      f₀
+  limₙ Aₙ ---> ⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₂ ---> A₁ ---> A₀.
+```
+
+The **universal property of the sequential limit** states that `limₙ Aₙ` is the
+terminal such type, by which we mean that given any
+[cone](foundation.cones-over-towers.md) over `A` with domain `X`, there is a
+[unique](foundation-core.contractible-types.md) map `g : X → limₙ Aₙ` exhibiting
+that cone as a composite of `g` with the cone of `limₙ Aₙ` over `A`.
+
+## Definition
+
+### The universal property of sequential limits
+
+```agda
+module _
+  {l1 l2 : Level} (l : Level) (A : tower l1) {X : UU l2}
+  where
+
+  universal-property-sequential-limit :
+    (c : cone-tower A X) → UU (l1 ⊔ l2 ⊔ lsuc l)
+  universal-property-sequential-limit c =
+    (Y : UU l) → is-equiv (cone-map-tower A {Y = Y} c)
+
+module _
+  {l1 l2 l3 : Level} (A : tower l1) {X : UU l2} (c : cone-tower A X)
+  where
+
+  map-universal-property-sequential-limit :
+    ({l : Level} → universal-property-sequential-limit l A c) →
+    {Y : UU l3} (c' : cone-tower A Y) → Y → X
+  map-universal-property-sequential-limit up-c {Y} c' =
+    map-inv-is-equiv (up-c Y) c'
+
+  compute-map-universal-property-sequential-limit :
+    (up-c : {l : Level} → universal-property-sequential-limit l A c) →
+    {Y : UU l3} (c' : cone-tower A Y) →
+    cone-map-tower A c (map-universal-property-sequential-limit up-c c') ＝ c'
+  compute-map-universal-property-sequential-limit up-c {Y} c' =
+    is-section-map-inv-is-equiv (up-c Y) c'
+```
+
+## Properties
+
+### 3-for-2 property of sequential limits
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  {A : tower l1} {X : UU l2} {Y : UU l3}
+  (c : cone-tower A X) (c' : cone-tower A Y)
+  (h : Y → X) (KLM : htpy-cone-tower A (cone-map-tower A c h) c')
+  where
+
+  inv-triangle-cone-cone-tower :
+    {l6 : Level} (D : UU l6) →
+    cone-map-tower A c ∘ postcomp D h ~ cone-map-tower A c'
+  inv-triangle-cone-cone-tower D k =
+    ap
+      ( λ t → cone-map-tower A t k)
+      ( eq-htpy-cone-tower A (cone-map-tower A c h) c' KLM)
+
+  triangle-cone-cone-tower :
+    {l6 : Level} (D : UU l6) →
+    cone-map-tower A c' ~ cone-map-tower A c ∘ postcomp D h
+  triangle-cone-cone-tower D k = inv (inv-triangle-cone-cone-tower D k)
+
+  abstract
+    is-equiv-universal-property-sequential-limit-universal-property-sequential-limit :
+      ({l : Level} → universal-property-sequential-limit l A c) →
+      ({l : Level} → universal-property-sequential-limit l A c') →
+      is-equiv h
+    is-equiv-universal-property-sequential-limit-universal-property-sequential-limit
+      up up' =
+      is-equiv-is-equiv-postcomp h
+        ( λ D →
+          is-equiv-right-factor-htpy
+            ( cone-map-tower A c')
+            ( cone-map-tower A c)
+            ( postcomp D h)
+            ( triangle-cone-cone-tower D)
+            ( up D)
+            ( up' D))
+
+  abstract
+    universal-property-sequential-limit-universal-property-sequential-limit-is-equiv :
+      is-equiv h →
+      ({l : Level} → universal-property-sequential-limit l A c) →
+      ({l : Level} → universal-property-sequential-limit l A c')
+    universal-property-sequential-limit-universal-property-sequential-limit-is-equiv
+      is-equiv-h up D =
+      is-equiv-comp-htpy
+        ( cone-map-tower A c')
+        ( cone-map-tower A c)
+        ( postcomp D h)
+        ( triangle-cone-cone-tower D)
+        ( is-equiv-postcomp-is-equiv h is-equiv-h D)
+        ( up D)
+
+  abstract
+    universal-property-sequential-limit-is-equiv-universal-property-sequential-limit :
+      ({l : Level} → universal-property-sequential-limit l A c') →
+      is-equiv h →
+      ({l : Level} → universal-property-sequential-limit l A c)
+    universal-property-sequential-limit-is-equiv-universal-property-sequential-limit
+      up' is-equiv-h D =
+      is-equiv-left-factor-htpy
+        ( cone-map-tower A c')
+        ( cone-map-tower A c)
+        ( postcomp D h)
+        ( triangle-cone-cone-tower D)
+        ( up' D)
+        ( is-equiv-postcomp-is-equiv h is-equiv-h D)
+```
+
+### Uniqueness of maps obtained via the universal property of sequential limits
+
+```agda
+module _
+  {l1 l2 : Level} (A : tower l1) {X : UU l2} (c : cone-tower A X)
+  where
+
+  abstract
+    uniqueness-universal-property-sequential-limit :
+      ({l : Level} → universal-property-sequential-limit l A c) →
+      {l3 : Level} (Y : UU l3) (c' : cone-tower A Y) →
+      is-contr (Σ (Y → X) (λ h → htpy-cone-tower A (cone-map-tower A c h) c'))
+    uniqueness-universal-property-sequential-limit up Y c' =
+      is-contr-equiv'
+        ( Σ (Y → X) (λ h → cone-map-tower A c h ＝ c'))
+        ( equiv-tot
+          ( λ h → extensionality-cone-tower A (cone-map-tower A c h) c'))
+        ( is-contr-map-is-equiv (up Y) c')
+```
+
+### The universal property of sequential limits at a universe level is a property
+
+```agda
+module _
+  {l1 l2 l3 : Level} (A : tower l1) {X : UU l2} (c : cone-tower A X)
+  where
+
+  abstract
+    is-prop-universal-property-sequential-limit :
+      is-prop (universal-property-sequential-limit l3 A c)
+    is-prop-universal-property-sequential-limit =
+      is-prop-Π (λ Y → is-property-is-equiv (cone-map-tower A c))
+```
+
+### The homotopy of cones obtained from the universal property of sequential limits
+
+```agda
+module _
+  {l1 l2 : Level} (A : tower l1) {X : UU l2}
+  where
+
+  htpy-cone-map-universal-property-sequential-limit :
+    (c : cone-tower A X)
+    (up : {l : Level} → universal-property-sequential-limit l A c) →
+    {l3 : Level} {Y : UU l3} (c' : cone-tower A Y) →
+    htpy-cone-tower A
+      ( cone-map-tower A c (map-universal-property-sequential-limit A c up c'))
+      ( c')
+  htpy-cone-map-universal-property-sequential-limit c up c' =
+    htpy-eq-cone-tower A
+      ( cone-map-tower A c (map-universal-property-sequential-limit A c up c'))
+      ( c')
+      ( compute-map-universal-property-sequential-limit A c up c')
+```
+
+### Unique uniqueness of sequential limits
+
+```agda
+module _
+  {l1 l2 l3 : Level} (A : tower l1) {X : UU l2} {Y : UU l3}
+  where
+
+  abstract
+    uniquely-unique-sequential-limit :
+      ( c' : cone-tower A Y) (c : cone-tower A X) →
+      ( up-c' : {l : Level} → universal-property-sequential-limit l A c') →
+      ( up-c : {l : Level} → universal-property-sequential-limit l A c) →
+      is-contr
+        ( Σ (Y ≃ X)
+            ( λ e → htpy-cone-tower A (cone-map-tower A c (map-equiv e)) c'))
+    uniquely-unique-sequential-limit c' c up-c' up-c =
+      is-contr-total-Eq-subtype
+        ( uniqueness-universal-property-sequential-limit A c up-c Y c')
+        ( is-property-is-equiv)
+        ( map-universal-property-sequential-limit A c up-c c')
+        ( htpy-cone-map-universal-property-sequential-limit A c up-c c')
+        ( is-equiv-universal-property-sequential-limit-universal-property-sequential-limit
+          ( c)
+          ( c')
+          ( map-universal-property-sequential-limit A c up-c c')
+          ( htpy-cone-map-universal-property-sequential-limit A c up-c c')
+          ( up-c)
+          ( up-c'))
+```
+
+## Table of files about sequential limits
+
+The following table lists files that are about sequential limits as a general
+concept.
+
+{{#include tables/sequential-limits.md}}
+
+## See also
+
+- For sequential colimits, see
+  [`synthetic-homotopy-theory.27-sequences`](synthetic-homotopy-theory.27-sequences.md)
diff --git a/src/group-theory/torsion-free-groups.lagda.md b/src/group-theory/torsion-free-groups.lagda.md
index deed7a3d08..edbbf39e7d 100644
--- a/src/group-theory/torsion-free-groups.lagda.md
+++ b/src/group-theory/torsion-free-groups.lagda.md
@@ -27,7 +27,6 @@ open import group-theory.groups
 open import group-theory.integer-powers-of-elements-groups
 open import group-theory.orders-of-elements-groups
 open import group-theory.subgroups
-open import group-theory.subgroups-generated-by-elements-groups
 open import group-theory.torsion-elements-groups
 ```
 
@@ -119,22 +118,23 @@ module _
   {l1 : Level} (G : Group l1)
   where
 
-  is-equiv-first-projection-pullback-subgroup-prop-prop-Group :
+  is-equiv-vertical-map-standard-pullback-subgroup-prop-prop-Group :
     Prop (lsuc l1)
-  is-equiv-first-projection-pullback-subgroup-prop-prop-Group =
+  is-equiv-vertical-map-standard-pullback-subgroup-prop-prop-Group =
     is-equiv-Prop
-      ( π₁ {f = subgroup-order-element-Group G} {g = subgroup-Prop ℤ-Group})
+      ( vertical-map-standard-pullback
+        { f = subgroup-order-element-Group G}
+        { g = subgroup-Prop ℤ-Group})
 
-  is-equiv-first-projection-pullback-subgroup-prop-Group :
-    UU (lsuc l1)
+  is-equiv-first-projection-pullback-subgroup-prop-Group : UU (lsuc l1)
   is-equiv-first-projection-pullback-subgroup-prop-Group =
-    type-Prop is-equiv-first-projection-pullback-subgroup-prop-prop-Group
+    type-Prop is-equiv-vertical-map-standard-pullback-subgroup-prop-prop-Group
 
   is-prop-is-equiv-first-projection-pullback-subgroup-prop-Group :
     is-prop is-equiv-first-projection-pullback-subgroup-prop-Group
   is-prop-is-equiv-first-projection-pullback-subgroup-prop-Group =
     is-prop-type-Prop
-      ( is-equiv-first-projection-pullback-subgroup-prop-prop-Group)
+      ( is-equiv-vertical-map-standard-pullback-subgroup-prop-prop-Group)
 ```
 
 ## Properties
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index cdf35701ef..31bc562be6 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -15,6 +15,7 @@ open import orthogonal-factorization-systems.factorization-operations public
 open import orthogonal-factorization-systems.factorization-operations-function-classes public
 open import orthogonal-factorization-systems.factorizations-of-maps public
 open import orthogonal-factorization-systems.function-classes public
+open import orthogonal-factorization-systems.functoriality-pullback-hom public
 open import orthogonal-factorization-systems.higher-modalities public
 open import orthogonal-factorization-systems.identity-modality public
 open import orthogonal-factorization-systems.lifting-operations public
diff --git a/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md b/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md
new file mode 100644
index 0000000000..8758d07561
--- /dev/null
+++ b/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md
@@ -0,0 +1,73 @@
+# Functoriality of the pullback-hom
+
+```agda
+module orthogonal-factorization-systems.functoriality-pullback-hom where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cones-over-cospans
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.fibered-maps
+open import foundation.fibers-of-maps
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-pullbacks
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.morphisms-cospans
+open import foundation.pullbacks
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.universal-property-pullbacks
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies
+
+open import orthogonal-factorization-systems.lifting-squares
+open import orthogonal-factorization-systems.pullback-hom
+```
+
+</details>
+
+## Idea
+
+The construction of the
+[pullback-hom](orthogonal-factorization-systems.pullback-hom.md) is functorial.
+
+## Definition
+
+### Functorial action on maps of the pullback-hom
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y)
+  {l1' l2' l3' l4' : Level}
+  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {Y' : UU l4'}
+  (f' : A' → B') (g' : X' → Y')
+  where
+
+  map-pullback-hom :
+    hom-cospan (precomp f' Y') (postcomp A' g') (precomp f Y) (postcomp A g) →
+    fibered-map f' g' → fibered-map f g
+  map-pullback-hom =
+    map-is-pullback
+      ( precomp f Y)
+      ( postcomp A g)
+      ( precomp f' Y')
+      ( postcomp A' g')
+      ( cone-pullback-hom f g)
+      ( cone-pullback-hom f' g')
+      ( is-pullback-fibered-map f g)
+      ( is-pullback-fibered-map f' g')
+```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md
index 1daba5fb55..24b4ee3b68 100644
--- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md
@@ -100,7 +100,7 @@ module _
     is-modal-type-is-small (unit-○) (x ＝ y) (is-locally-small-○ X x y)
 ```
 
-### The `is-higher-modality` predicate
+### The predicate of being a higher modality
 
 ```agda
   is-higher-modality : UU (lsuc l1 ⊔ l2)
@@ -108,7 +108,7 @@ module _
     dependent-universal-property-modality (unit-○) × is-modal-identity-types
 ```
 
-### Components of a `is-higher-modality` proof
+### Components of a higher modality proof
 
 ```agda
   ind-modality-is-higher-modality : is-higher-modality → ind-modality unit-○
diff --git a/src/orthogonal-factorization-systems/pullback-hom.lagda.md b/src/orthogonal-factorization-systems/pullback-hom.lagda.md
index d2792ae611..8bb1bbb520 100644
--- a/src/orthogonal-factorization-systems/pullback-hom.lagda.md
+++ b/src/orthogonal-factorization-systems/pullback-hom.lagda.md
@@ -68,13 +68,13 @@ vertical maps are `f` and `g`.
 ### The codomain of the pullback-hom
 
 ```agda
-type-canonical-pullback-hom :
+type-standard-pullback-hom :
   {l1 l2 l3 l4 : Level}
   {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
   (f : A → B) (g : X → Y) →
   UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-type-canonical-pullback-hom {A = A} {Y = Y} f g =
-  canonical-pullback (precomp f Y) (postcomp A g)
+type-standard-pullback-hom {A = A} {Y = Y} f g =
+  standard-pullback (precomp f Y) (postcomp A g)
 ```
 
 #### The canonical pullback-hom type is equivalent to the type of fibered maps
@@ -86,35 +86,35 @@ module _
   (f : A → B) (g : X → Y)
   where
 
-  equiv-fibered-map-type-canonical-pullback-hom :
-    type-canonical-pullback-hom f g ≃ fibered-map f g
-  equiv-fibered-map-type-canonical-pullback-hom =
+  equiv-fibered-map-type-standard-pullback-hom :
+    type-standard-pullback-hom f g ≃ fibered-map f g
+  equiv-fibered-map-type-standard-pullback-hom =
     equiv-tot (λ _ → equiv-tot (λ _ → equiv-funext))
 
-  equiv-type-canonical-pullback-hom-fibered-map :
-    fibered-map f g ≃ type-canonical-pullback-hom f g
-  equiv-type-canonical-pullback-hom-fibered-map =
-    inv-equiv equiv-fibered-map-type-canonical-pullback-hom
+  equiv-type-standard-pullback-hom-fibered-map :
+    fibered-map f g ≃ type-standard-pullback-hom f g
+  equiv-type-standard-pullback-hom-fibered-map =
+    inv-equiv equiv-fibered-map-type-standard-pullback-hom
 
-  map-fibered-map-type-canonical-pullback-hom :
-    type-canonical-pullback-hom f g → fibered-map f g
-  map-fibered-map-type-canonical-pullback-hom =
-    map-equiv equiv-fibered-map-type-canonical-pullback-hom
+  map-fibered-map-type-standard-pullback-hom :
+    type-standard-pullback-hom f g → fibered-map f g
+  map-fibered-map-type-standard-pullback-hom =
+    map-equiv equiv-fibered-map-type-standard-pullback-hom
 
-  map-type-canonical-pullback-hom-fibered-map :
-    fibered-map f g → type-canonical-pullback-hom f g
-  map-type-canonical-pullback-hom-fibered-map =
-    map-equiv equiv-type-canonical-pullback-hom-fibered-map
+  map-type-standard-pullback-hom-fibered-map :
+    fibered-map f g → type-standard-pullback-hom f g
+  map-type-standard-pullback-hom-fibered-map =
+    map-equiv equiv-type-standard-pullback-hom-fibered-map
 ```
 
 Below are basic definitions related to the pullback property of the type of
 fibered maps.
 
 ```agda
-  cone-canonical-pullback-hom :
-    cone (precomp f Y) (postcomp A g) (type-canonical-pullback-hom f g)
-  cone-canonical-pullback-hom =
-    cone-canonical-pullback (precomp f Y) (postcomp A g)
+  cone-standard-pullback-hom :
+    cone (precomp f Y) (postcomp A g) (type-standard-pullback-hom f g)
+  cone-standard-pullback-hom =
+    cone-standard-pullback (precomp f Y) (postcomp A g)
 
   cone-pullback-hom :
     cone (precomp f Y) (postcomp A g) (fibered-map f g)
@@ -122,24 +122,24 @@ fibered maps.
     cone-map
       ( precomp f Y)
       ( postcomp A g)
-      ( cone-canonical-pullback (precomp f Y) (postcomp A g))
-      ( map-type-canonical-pullback-hom-fibered-map)
+      ( cone-standard-pullback (precomp f Y) (postcomp A g))
+      ( map-type-standard-pullback-hom-fibered-map)
 
-  gap-canonical-pullback-hom :
+  gap-standard-pullback-hom :
     {l : Level} {C : UU l} →
-    cone (precomp f Y) (postcomp A g) C → C → type-canonical-pullback-hom f g
-  gap-canonical-pullback-hom = gap (precomp f Y) (postcomp A g)
+    cone (precomp f Y) (postcomp A g) C → C → type-standard-pullback-hom f g
+  gap-standard-pullback-hom = gap (precomp f Y) (postcomp A g)
 
   gap-pullback-hom :
     {l : Level} {C : UU l} →
     cone (precomp f Y) (postcomp A g) C → C → fibered-map f g
   gap-pullback-hom c x =
-    map-fibered-map-type-canonical-pullback-hom (gap-canonical-pullback-hom c x)
+    map-fibered-map-type-standard-pullback-hom (gap-standard-pullback-hom c x)
 
   is-pullback-fibered-map :
     is-pullback (precomp f Y) (postcomp A g) (cone-pullback-hom)
   is-pullback-fibered-map =
-    is-equiv-map-equiv equiv-type-canonical-pullback-hom-fibered-map
+    is-equiv-map-equiv equiv-type-standard-pullback-hom-fibered-map
 
   universal-property-pullback-fibered-map :
     {l : Level} →
@@ -177,37 +177,6 @@ The symbol `⋔` is the [pitchfork](https://codepoints.net/U+22D4) (agda-input:
 
 ## Properties
 
-### Functoriality of the pullback-hom
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level}
-  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
-  (f : A → B) (g : X → Y)
-  {l1' l2' l3' l4' : Level}
-  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {Y' : UU l4'}
-  (f' : A' → B') (g' : X' → Y')
-  where
-
-  map-pullback-hom :
-    hom-cospan
-      ( precomp f' Y')
-      ( postcomp A' g')
-      ( precomp f Y)
-      ( postcomp A g) →
-    fibered-map f' g' → fibered-map f g
-  map-pullback-hom =
-    map-is-pullback
-      ( precomp f Y)
-      ( postcomp A g)
-      ( precomp f' Y')
-      ( postcomp A' g')
-      ( cone-pullback-hom f g)
-      ( cone-pullback-hom f' g')
-      ( is-pullback-fibered-map f g)
-      ( is-pullback-fibered-map f' g')
-```
-
 ### The fibers of the pullback-hom
 
 ```agda
@@ -217,7 +186,7 @@ module _
   where
 
   inv-compute-fiber-pullback-hom :
-    (fiber (pullback-hom f g) h) ≃ (lifting-square-fibered-map f g h)
+    fiber (pullback-hom f g) h ≃ lifting-square-fibered-map f g h
   inv-compute-fiber-pullback-hom =
     equiv-tot
       ( λ j →
@@ -245,6 +214,12 @@ module _
           ( extensionality-fibered-map f g (pullback-hom f g j) h)))
 
   compute-fiber-pullback-hom :
-    (lifting-square-fibered-map f g h) ≃ (fiber (pullback-hom f g) h)
+    lifting-square-fibered-map f g h ≃ fiber (pullback-hom f g) h
   compute-fiber-pullback-hom = inv-equiv inv-compute-fiber-pullback-hom
 ```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}
diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
index b7fb9d002b..49057ab99b 100644
--- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
@@ -32,7 +32,7 @@ precisely the types in the reflective subuniverse.
 
 ## Definitions
 
-### The `is-reflective-subuniverse` predicate on subuniverses
+### The predicate on subuniverses of being reflective
 
 ```agda
 is-reflective-subuniverse :
diff --git a/src/synthetic-homotopy-theory/27-sequences.lagda.md b/src/synthetic-homotopy-theory/27-sequences.lagda.md
index d9a83fcb4f..14e1931e28 100644
--- a/src/synthetic-homotopy-theory/27-sequences.lagda.md
+++ b/src/synthetic-homotopy-theory/27-sequences.lagda.md
@@ -60,16 +60,16 @@ equiv-Seq A B =
     ( λ e → (n : ℕ) →
       naturality-hom-Seq A B (λ n → map-equiv (e n)) n)
 
-reflexive-equiv-Seq :
+id-equiv-Seq :
   { l1 : Level} (A : Sequence l1) → equiv-Seq A A
-reflexive-equiv-Seq A =
+id-equiv-Seq A =
   pair
     ( λ n → id-equiv)
     ( λ n → refl-htpy)
 
 equiv-eq-Seq :
   { l1 : Level} (A B : Sequence l1) → Id A B → equiv-Seq A B
-equiv-eq-Seq A .A refl = reflexive-equiv-Seq A
+equiv-eq-Seq A .A refl = id-equiv-Seq A
 
 is-contr-total-equiv-Seq :
   { l1 : Level} (A : Sequence l1) →
diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-coequalizers.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-coequalizers.lagda.md
index dbf0179475..00583ad9ed 100644
--- a/src/synthetic-homotopy-theory/dependent-universal-property-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-universal-property-coequalizers.lagda.md
@@ -13,7 +13,6 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.fibers-of-maps
 open import foundation.functoriality-dependent-pair-types
-open import foundation.homotopies
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.coforks
diff --git a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
index d58d854463..e4c06b0003 100644
--- a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
@@ -7,21 +7,15 @@ module synthetic-homotopy-theory.maps-of-prespectra where
 <details><summary>Imports</summary>
 
 ```agda
-open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.natural-numbers
 
-open import foundation.commuting-squares-of-maps
 open import foundation.dependent-pair-types
-open import foundation.identity-types
-open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import structured-types.commuting-squares-of-pointed-maps
 open import structured-types.pointed-maps
-open import structured-types.pointed-types
 
 open import synthetic-homotopy-theory.functoriality-loop-spaces
-open import synthetic-homotopy-theory.loop-spaces
 open import synthetic-homotopy-theory.prespectra
 ```
 
diff --git a/src/synthetic-homotopy-theory/prespectra.lagda.md b/src/synthetic-homotopy-theory/prespectra.lagda.md
index 3d4733d122..419d94f51f 100644
--- a/src/synthetic-homotopy-theory/prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/prespectra.lagda.md
@@ -10,7 +10,6 @@ module synthetic-homotopy-theory.prespectra where
 open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
-open import foundation.function-types
 open import foundation.identity-types
 open import foundation.universe-levels
 
diff --git a/src/synthetic-homotopy-theory/spectra.lagda.md b/src/synthetic-homotopy-theory/spectra.lagda.md
index f719099060..6dfba54ea5 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -24,7 +24,6 @@ open import synthetic-homotopy-theory.loop-spaces
 open import synthetic-homotopy-theory.prespectra
 open import synthetic-homotopy-theory.suspensions-of-pointed-types
 open import synthetic-homotopy-theory.suspensions-of-types
-open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types
 ```
 
 </details>
diff --git a/src/univalent-combinatorics/fibers-of-maps.lagda.md b/src/univalent-combinatorics/fibers-of-maps.lagda.md
index 1779e20173..03b9c4c3cb 100644
--- a/src/univalent-combinatorics/fibers-of-maps.lagda.md
+++ b/src/univalent-combinatorics/fibers-of-maps.lagda.md
@@ -152,5 +152,5 @@ equiv-is-finite-domain-is-finite-fiber {A = A} B f =
       is-finite-equiv
         ( equiv-total-fiber f)
         ( is-finite-Σ (is-finite-type-𝔽 B) P))
-    ( λ P → is-finite-fiber f P ( is-finite-type-𝔽 B))
+    ( λ P → is-finite-fiber f P (is-finite-type-𝔽 B))
 ```
diff --git a/tables/fibers-of-maps.md b/tables/fibers-of-maps.md
new file mode 100644
index 0000000000..83de16f22c
--- /dev/null
+++ b/tables/fibers-of-maps.md
@@ -0,0 +1,8 @@
+| Concept                          | File                                                                                    |
+| -------------------------------- | --------------------------------------------------------------------------------------- |
+| Fibers of maps (foundation-core) | [`foundation-core.fibers-of-maps`](foundation-core.fibers-of-maps.md)                   |
+| Fibers of maps (foundation)      | [`foundation.fibers-of-maps`](foundation.fibers-of-maps.md)                             |
+| Equality in the fibers of a map  | [`foundation.equality-fibers-of-maps`](foundation.equality-fibers-of-maps.md)           |
+| Functoriality of fibers of maps  | [`foundation.functoriality-fibers-of-maps`](foundation.functoriality-fibers-of-maps.md) |
+| Fibers of pointed maps           | [`structured-types.fibers-of-pointed-maps`](structured-types.fibers-of-pointed-maps.md) |
+| Fibers of maps of finite types   | [`univalent-combinatorics.fibers-of-maps`](univalent-combinatorics.fibers-of-maps.md)   |
diff --git a/tables/pullbacks.md b/tables/pullbacks.md
new file mode 100644
index 0000000000..f93aa884ec
--- /dev/null
+++ b/tables/pullbacks.md
@@ -0,0 +1,14 @@
+| Concept                                               | File                                                                                                                            |
+| ----------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------- |
+| Cospans                                               | [`foundation.cospans`](foundation.cospans.md)                                                                                   |
+| Morphisms of cospans                                  | [`foundation.morphisms-cospans`](foundation.morphisms-cospans.md)                                                               |
+| Cones over cospans                                    | [`foundation.cones-over-cospans`](foundation.cones-over-cospans.md)                                                             |
+| The universal property of pullbacks (foundation-core) | [`foundation-core.universal-property-pullbacks`](foundation-core.universal-property-pullbacks.md)                               |
+| The universal property of pullbacks (foundation)      | [`foundation.universal-property-pullbacks`](foundation.universal-property-pullbacks.md)                                         |
+| Pullbacks (foundation-core)                           | [`foundation-core.pullbacks`](foundation-core.pullbacks.md)                                                                     |
+| Pullbacks (foundation)                                | [`foundation.pullbacks`](foundation.pullbacks.md)                                                                               |
+| Functoriality of pullbacks                            | [`foundation.functoriality-pullbacks`](foundation.functoriality-pullbacks.md)                                                   |
+| Pullback squares                                      | [`foundation.pullback-squares`](foundation.pullback-squares.md)                                                                 |
+| The pullback-hom                                      | [`orthogonal-factorization-systems.pullback-hom`](orthogonal-factorization-systems.pullback-hom.md)                             |
+| Functoriality of the pullback-hom                     | [`orthogonal-factorization-systems.functoriality-pullback-hom`](orthogonal-factorization-systems.functoriality-pullback-hom.md) |
+| Pullbacks in precategories                            | [`category-theory.pullbacks-in-precategories`](category-theory.pullbacks-in-precategories.md)                                   |
diff --git a/tables/sequential-limits.md b/tables/sequential-limits.md
new file mode 100644
index 0000000000..25c20ddcbb
--- /dev/null
+++ b/tables/sequential-limits.md
@@ -0,0 +1,12 @@
+| Concept                                     | File                                                                                                    |
+| ------------------------------------------- | ------------------------------------------------------------------------------------------------------- |
+| Towers of types                             | [`foundation.towers`](foundation.towers.md)                                                             |
+| Dependent towers of types                   | [`foundation.dependent-towers`](foundation.dependent-towers.md)                                         |
+| Composite maps in towers                    | [`foundation.composite-maps-in-towers`](foundation.composite-maps-in-towers.md)                         |
+| Morphisms of towers                         | [`foundation.morphisms-towers`](foundation.morphisms-towers.md)                                         |
+| Equivalences of towers                      | [`foundation.equivalences-towers`](foundation.equivalences-towers.md)                                   |
+| Cones over towers                           | [`foundation.cones-over-towers`](foundation.cones-over-towers.md)                                       |
+| The universal property of sequential limits | [`foundation.universal-property-sequential-limits`](foundation.universal-property-sequential-limits.md) |
+| Sequential limits                           | [`foundation.sequential-limits`](foundation.sequential-limits.md)                                       |
+| Functoriality of sequential limits          | [`foundation.functoriality-sequential-limits`](foundation.functoriality-sequential-limits.md)           |
+| Transfinite cocomposition of maps           | [`foundation.transfinite-cocomposition-of-maps`](foundation.transfinite-cocomposition-of-maps.md)       |