diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md
index f31ffa5491..7f25f3e438 100644
--- a/src/foundation-core.lagda.md
+++ b/src/foundation-core.lagda.md
@@ -50,7 +50,6 @@ open import foundation-core.retractions public
 open import foundation-core.sections public
 open import foundation-core.sets public
 open import foundation-core.small-types public
-open import foundation-core.standard-pullbacks public
 open import foundation-core.subtypes public
 open import foundation-core.torsorial-type-families public
 open import foundation-core.transport-along-identifications public
diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md
index 3218951ee7..369c89d4a5 100644
--- a/src/foundation-core/pullbacks.lagda.md
+++ b/src/foundation-core/pullbacks.lagda.md
@@ -13,6 +13,7 @@ open import foundation.dependent-pair-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-fibers-of-maps
 open import foundation.identity-types
+open import foundation.standard-pullbacks
 open import foundation.universe-levels
 
 open import foundation-core.diagonal-maps-of-types
@@ -23,7 +24,6 @@ open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
-open import foundation-core.standard-pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
 
@@ -50,7 +50,7 @@ this concept is captured by
 this is a large proposition, which is not suitable for all purposes. Therefore,
 as our main definition of a pullback cone we consider the
 {{#concept "small predicate of being a pullback" Agda=is-pullback}}: given the
-existence of the [standard pullback type](foundation-core.standard-pullbacks.md)
+existence of the [standard pullback type](foundation.standard-pullbacks.md)
 `A ×_X B`, a cone is a _pullback_ if the gap map into the standard pullback is
 an [equivalence](foundation-core.equivalences.md).
 
diff --git a/src/foundation-core/standard-pullbacks.lagda.md b/src/foundation-core/standard-pullbacks.lagda.md
deleted file mode 100644
index b3d447d6bb..0000000000
--- a/src/foundation-core/standard-pullbacks.lagda.md
+++ /dev/null
@@ -1,404 +0,0 @@
-# Standard pullbacks
-
-```agda
-module foundation-core.standard-pullbacks where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.action-on-identifications-functions
-open import foundation.cones-over-cospan-diagrams
-open import foundation.dependent-pair-types
-open import foundation.equality-cartesian-product-types
-open import foundation.functoriality-cartesian-product-types
-open import foundation.identity-types
-open import foundation.structure-identity-principle
-open import foundation.type-arithmetic-dependent-pair-types
-open import foundation.universe-levels
-
-open import foundation-core.cartesian-product-types
-open import foundation-core.commuting-squares-of-maps
-open import foundation-core.diagonal-maps-of-types
-open import foundation-core.equality-dependent-pair-types
-open import foundation-core.equivalences
-open import foundation-core.function-types
-open import foundation-core.functoriality-dependent-pair-types
-open import foundation-core.homotopies
-open import foundation-core.retractions
-open import foundation-core.sections
-open import foundation-core.type-theoretic-principle-of-choice
-open import foundation-core.universal-property-pullbacks
-open import foundation-core.whiskering-identifications-concatenation
-```
-
-</details>
-
-## Idea
-
-Given a [cospan of types](foundation.cospans.md)
-
-```text
-  f : A → X ← B : g,
-```
-
-we can form the
-{{#concept "standard pullback" Disambiguation="types" Agda=standard-pullback}}
-`A ×_X B` satisfying
-[the universal property of the pullback](foundation-core.universal-property-pullbacks.md)
-of the cospan, completing the diagram
-
-```text
-  A ×_X B ------> B
-     | ⌟          |
-     |            | g
-     |            |
-     v            v
-     A ---------> X.
-           f
-```
-
-The standard pullback consists of [pairs](foundation.dependent-pair-types.md)
-`a : A` and `b : B` such that `f a` and `g b` agree:
-
-```text
-  A ×_X B := Σ (a : A) (b : B), (f a ＝ g b).
-```
-
-Thus the standard [cone](foundation.cones-over-cospan-diagrams.md) consists of
-the canonical projections.
-
-## Definitions
-
-### 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
-
-  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
-
-  vertical-map-standard-pullback : standard-pullback f g → A
-  vertical-map-standard-pullback = pr1
-
-  horizontal-map-standard-pullback : standard-pullback f g → B
-  horizontal-map-standard-pullback t = pr1 (pr2 t)
-
-  coherence-square-standard-pullback :
-    coherence-square-maps
-      horizontal-map-standard-pullback
-      vertical-map-standard-pullback
-      g
-      f
-  coherence-square-standard-pullback t = pr2 (pr2 t)
-```
-
-### 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-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 standard pullback
-
-The {{#concept "standard gap map" Disambiguation="cone over a cospan" Agda=gap}}
-of a [commuting square](foundation-core.commuting-squares-of-maps.md) is the map
-from the domain of the cone into the standard pullback.
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
-  (f : A → X) (g : B → X)
-  where
-
-  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
-```
-
-## Properties
-
-### 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-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-Σ
-      ( λ bp' α → Σ (b ＝ pr1 bp') (λ β → ap f α ∙ pr2 bp' ＝ p ∙ ap g β))
-      ( refl)
-      ( refl , inv right-unit)
-      ( λ x → id-equiv)
-      ( extensionality-Σ
-        ( λ 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-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-standard-pullback s t) (α , β , γ)
-```
-
-### The standard pullback satisfies the universal property of pullbacks
-
-```agda
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
-  where
-
-  abstract
-    universal-property-standard-pullback :
-      universal-property-pullback f g (cone-standard-pullback f g)
-    universal-property-standard-pullback C =
-      is-equiv-comp
-        ( tot (λ _ → map-distributive-Π-Σ))
-        ( mapping-into-Σ)
-        ( is-equiv-mapping-into-Σ)
-        ( is-equiv-tot-is-fiberwise-equiv (λ _ → is-equiv-map-distributive-Π-Σ))
-```
-
-### A cone is equal to the value of `cone-map` at its own gap map
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
-  (f : A → X) (g : B → X)
-  where
-
-  htpy-cone-up-pullback-standard-pullback :
-    (c : cone f g C) →
-    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
-```
-
-### Standard pullbacks are symmetric
-
-The standard pullback of `f : A -> X <- B : g` is equivalent to the standard
-pullback of `g : B -> X <- A : f`.
-
-```agda
-map-commutative-standard-pullback :
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-  (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-standard-pullback f g ∘
-    map-commutative-standard-pullback g f) ~ id
-inv-inv-map-commutative-standard-pullback f g x =
-  eq-pair-eq-fiber
-    ( eq-pair-eq-fiber
-      ( inv-inv (coherence-square-standard-pullback x)))
-
-abstract
-  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-standard-pullback f g)
-  is-equiv-map-commutative-standard-pullback f g =
-    is-equiv-is-invertible
-      ( map-commutative-standard-pullback g f)
-      ( inv-inv-map-commutative-standard-pullback f g)
-      ( inv-inv-map-commutative-standard-pullback g f)
-
-commutative-standard-pullback :
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X) →
-  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
-```
-
-#### The gap map of the swapped cone computes as the underlying gap map followed by a swap
-
-```agda
-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-standard-pullback f g ∘ gap f g c
-triangle-map-commutative-standard-pullback f g c = refl-htpy
-```
-
-### Pullbacks can be "folded"
-
-Given a standard pullback square
-
-```text
-         f'
-    C -------> B
-    | ⌟        |
-  g'|          | g
-    v          v
-    A -------> X
-         f
-```
-
-we can "fold" the vertical edge onto the horizontal one and get a new pullback
-square
-
-```text
-            C ---------> X
-            | ⌟          |
-  (f' , g') |            |
-            v            v
-          A × B -----> X × X,
-                f × g
-```
-
-moreover, this folded square is a pullback if and only if the original one is.
-
-```agda
-module _
-  {l1 l2 l3 : Level}
-  {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X)
-  where
-
-  fold-cone :
-    {l4 : Level} {C : UU l4} →
-    cone f g C → cone (map-product f g) (diagonal X) C
-  pr1 (pr1 (fold-cone c) z) = vertical-map-cone f g c z
-  pr2 (pr1 (fold-cone c) z) = horizontal-map-cone f g c z
-  pr1 (pr2 (fold-cone c)) = g ∘ horizontal-map-cone f g c
-  pr2 (pr2 (fold-cone c)) z = eq-pair (coherence-square-cone f g c z) refl
-
-  map-fold-cone-standard-pullback :
-    standard-pullback f g → standard-pullback (map-product f g) (diagonal X)
-  pr1 (pr1 (map-fold-cone-standard-pullback x)) =
-    vertical-map-standard-pullback x
-  pr2 (pr1 (map-fold-cone-standard-pullback x)) =
-    horizontal-map-standard-pullback x
-  pr1 (pr2 (map-fold-cone-standard-pullback x)) =
-    g (horizontal-map-standard-pullback x)
-  pr2 (pr2 (map-fold-cone-standard-pullback x)) =
-    eq-pair (coherence-square-standard-pullback x) refl
-
-  map-inv-fold-cone-standard-pullback :
-    standard-pullback (map-product f g) (diagonal X) → standard-pullback f g
-  pr1 (map-inv-fold-cone-standard-pullback ((a , b) , x , α)) = a
-  pr1 (pr2 (map-inv-fold-cone-standard-pullback ((a , b) , x , α))) = b
-  pr2 (pr2 (map-inv-fold-cone-standard-pullback ((a , b) , x , α))) =
-    ap pr1 α ∙ inv (ap pr2 α)
-
-  abstract
-    is-section-map-inv-fold-cone-standard-pullback :
-      is-section
-        ( map-fold-cone-standard-pullback)
-        ( map-inv-fold-cone-standard-pullback)
-    is-section-map-inv-fold-cone-standard-pullback ((a , b) , (x , α)) =
-      map-extensionality-standard-pullback
-        ( map-product f g)
-        ( diagonal X)
-        ( refl)
-        ( ap pr2 α)
-        ( ( inv (is-section-pair-eq α)) ∙
-          ( ap
-            ( λ t → eq-pair t (ap pr2 α))
-            ( ( inv right-unit) ∙
-              ( inv
-                ( left-whisker-concat
-                  ( ap pr1 α)
-                  ( 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) (x , x))
-            ( inv (ap-diagonal (ap pr2 α)))))
-
-  abstract
-    is-retraction-map-inv-fold-cone-standard-pullback :
-      is-retraction
-        ( map-fold-cone-standard-pullback)
-        ( map-inv-fold-cone-standard-pullback)
-    is-retraction-map-inv-fold-cone-standard-pullback (a , b , p) =
-      map-extensionality-standard-pullback f g
-        ( refl)
-        ( refl)
-        ( inv
-          ( ( right-whisker-concat
-              ( ( right-whisker-concat
-                  ( ap-pr1-eq-pair p refl)
-                  ( inv (ap pr2 (eq-pair p refl)))) ∙
-                ( ap (λ t → p ∙ inv t) (ap-pr2-eq-pair p refl)) ∙
-                ( right-unit))
-              ( refl)) ∙
-            ( right-unit)))
-
-  abstract
-    is-equiv-map-fold-cone-standard-pullback :
-      is-equiv map-fold-cone-standard-pullback
-    is-equiv-map-fold-cone-standard-pullback =
-      is-equiv-is-invertible
-        ( map-inv-fold-cone-standard-pullback)
-        ( is-section-map-inv-fold-cone-standard-pullback)
-        ( is-retraction-map-inv-fold-cone-standard-pullback)
-
-  triangle-map-fold-cone-standard-pullback :
-    {l4 : Level} {C : UU l4} (c : cone f g C) →
-    gap (map-product f g) (diagonal X) (fold-cone c) ~
-    map-fold-cone-standard-pullback ∘ gap f g c
-  triangle-map-fold-cone-standard-pullback c = refl-htpy
-```
-
-## 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/coproducts-pullbacks.lagda.md b/src/foundation/coproducts-pullbacks.lagda.md
index 67e694bbc5..e61513962f 100644
--- a/src/foundation/coproducts-pullbacks.lagda.md
+++ b/src/foundation/coproducts-pullbacks.lagda.md
@@ -14,6 +14,7 @@ open import foundation.dependent-pair-types
 open import foundation.equality-coproduct-types
 open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
+open import foundation.standard-pullbacks
 open import foundation.universe-levels
 
 open import foundation-core.equality-dependent-pair-types
@@ -23,7 +24,6 @@ open import foundation-core.homotopies
 open import foundation-core.pullbacks
 open import foundation-core.retractions
 open import foundation-core.sections
-open import foundation-core.standard-pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
 
diff --git a/src/foundation/dependent-products-pullbacks.lagda.md b/src/foundation/dependent-products-pullbacks.lagda.md
index 9b34417078..157b8e5143 100644
--- a/src/foundation/dependent-products-pullbacks.lagda.md
+++ b/src/foundation/dependent-products-pullbacks.lagda.md
@@ -12,6 +12,7 @@ open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.functoriality-dependent-function-types
 open import foundation.identity-types
+open import foundation.standard-pullbacks
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
@@ -20,7 +21,6 @@ open import foundation-core.homotopies
 open import foundation-core.pullbacks
 open import foundation-core.retractions
 open import foundation-core.sections
-open import foundation-core.standard-pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
 
diff --git a/src/foundation/dependent-sums-pullbacks.lagda.md b/src/foundation/dependent-sums-pullbacks.lagda.md
index 852a428f9e..ae048f2205 100644
--- a/src/foundation/dependent-sums-pullbacks.lagda.md
+++ b/src/foundation/dependent-sums-pullbacks.lagda.md
@@ -11,6 +11,7 @@ open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
+open import foundation.standard-pullbacks
 open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
@@ -23,7 +24,6 @@ open import foundation-core.homotopies
 open import foundation-core.pullbacks
 open import foundation-core.retractions
 open import foundation-core.sections
-open import foundation-core.standard-pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
 
diff --git a/src/foundation/diagonals-of-maps.lagda.md b/src/foundation/diagonals-of-maps.lagda.md
index 0cbbaee888..fcf5a1366a 100644
--- a/src/foundation/diagonals-of-maps.lagda.md
+++ b/src/foundation/diagonals-of-maps.lagda.md
@@ -10,6 +10,7 @@ module foundation.diagonals-of-maps where
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-fibers-of-maps
+open import foundation.standard-pullbacks
 open import foundation.universe-levels
 
 open import foundation-core.contractible-maps
@@ -20,7 +21,6 @@ open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.propositional-maps
-open import foundation-core.standard-pullbacks
 open import foundation-core.truncated-maps
 open import foundation-core.truncated-types
 open import foundation-core.truncation-levels
diff --git a/src/foundation/fiber-inclusions.lagda.md b/src/foundation/fiber-inclusions.lagda.md
index ddd5de671f..fb33d403c9 100644
--- a/src/foundation/fiber-inclusions.lagda.md
+++ b/src/foundation/fiber-inclusions.lagda.md
@@ -12,6 +12,7 @@ open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.faithful-maps
 open import foundation.fibers-of-maps
+open import foundation.standard-pullbacks
 open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.unit-type
@@ -29,7 +30,6 @@ open import foundation-core.propositional-maps
 open import foundation-core.propositions
 open import foundation-core.pullbacks
 open import foundation-core.sets
-open import foundation-core.standard-pullbacks
 open import foundation-core.truncated-maps
 open import foundation-core.truncated-types
 open import foundation-core.truncation-levels
diff --git a/src/foundation/functoriality-pullbacks.lagda.md b/src/foundation/functoriality-pullbacks.lagda.md
index f09e4151a8..76eaf05019 100644
--- a/src/foundation/functoriality-pullbacks.lagda.md
+++ b/src/foundation/functoriality-pullbacks.lagda.md
@@ -11,12 +11,12 @@ open import foundation.action-on-identifications-functions
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.morphisms-cospan-diagrams
+open import foundation.standard-pullbacks
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
 open import foundation-core.identity-types
 open import foundation-core.pullbacks
-open import foundation-core.standard-pullbacks
 ```
 
 </details>
diff --git a/src/foundation/postcomposition-pullbacks.lagda.md b/src/foundation/postcomposition-pullbacks.lagda.md
index b075c5c722..725fae5fd9 100644
--- a/src/foundation/postcomposition-pullbacks.lagda.md
+++ b/src/foundation/postcomposition-pullbacks.lagda.md
@@ -11,6 +11,7 @@ open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-types
+open import foundation.standard-pullbacks
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
@@ -21,7 +22,6 @@ open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.postcomposition-functions
 open import foundation-core.pullbacks
-open import foundation-core.standard-pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
 
diff --git a/src/foundation/products-pullbacks.lagda.md b/src/foundation/products-pullbacks.lagda.md
index 8f6b311a98..6454d0137b 100644
--- a/src/foundation/products-pullbacks.lagda.md
+++ b/src/foundation/products-pullbacks.lagda.md
@@ -11,6 +11,7 @@ open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.functoriality-cartesian-product-types
+open import foundation.standard-pullbacks
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 
@@ -21,7 +22,6 @@ open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.pullbacks
-open import foundation-core.standard-pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
 
diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md
index 537e5052ec..652fa205db 100644
--- a/src/foundation/pullbacks.lagda.md
+++ b/src/foundation/pullbacks.lagda.md
@@ -65,7 +65,7 @@ this concept is captured by
 this is a large proposition, which is not suitable for all purposes. Therefore,
 as our main definition of a pullback cone we consider the
 {{#concept "small predicate of being a pullback" Agda=is-pullback}}: given the
-existence of the [standard pullback type](foundation-core.standard-pullbacks.md)
+existence of the [standard pullback type](foundation.standard-pullbacks.md)
 `A ×_X B`, a cone is a _pullback_ if the gap map into the standard pullback is
 an [equivalence](foundation-core.equivalences.md).
 
diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md
index 6ac58a978c..4d73beac89 100644
--- a/src/foundation/standard-pullbacks.lagda.md
+++ b/src/foundation/standard-pullbacks.lagda.md
@@ -2,8 +2,6 @@
 
 ```agda
 module foundation.standard-pullbacks where
-
-open import foundation-core.standard-pullbacks public
 ```
 
 <details><summary>Imports</summary>
@@ -11,24 +9,25 @@ open import foundation-core.standard-pullbacks public
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.cones-over-cospan-diagrams
-open import foundation.coproduct-types
 open import foundation.dependent-pair-types
-open import foundation.equality-coproduct-types
-open import foundation.function-extensionality
-open import foundation.functoriality-coproduct-types
-open import foundation.functoriality-function-types
+open import foundation.equality-cartesian-product-types
+open import foundation.functoriality-cartesian-product-types
 open import foundation.identity-types
+open import foundation.structure-identity-principle
 open import foundation.universe-levels
-open import foundation.whiskering-homotopies-composition
 
+open import foundation-core.commuting-squares-of-maps
+open import foundation-core.diagonal-maps-of-types
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
-open import foundation-core.postcomposition-functions
 open import foundation-core.retractions
 open import foundation-core.sections
+open import foundation-core.type-theoretic-principle-of-choice
+open import foundation-core.universal-property-pullbacks
+open import foundation-core.whiskering-identifications-concatenation
 ```
 
 </details>
@@ -67,6 +66,335 @@ The standard pullback consists of [pairs](foundation.dependent-pair-types.md)
 thus the standard [cone](foundation.cones-over-cospan-diagrams.md) consists of
 the canonical projections.
 
+## Definitions
+
+### 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
+
+  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
+
+  vertical-map-standard-pullback : standard-pullback f g → A
+  vertical-map-standard-pullback = pr1
+
+  horizontal-map-standard-pullback : standard-pullback f g → B
+  horizontal-map-standard-pullback t = pr1 (pr2 t)
+
+  coherence-square-standard-pullback :
+    coherence-square-maps
+      horizontal-map-standard-pullback
+      vertical-map-standard-pullback
+      g
+      f
+  coherence-square-standard-pullback t = pr2 (pr2 t)
+```
+
+### 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-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 standard pullback
+
+The {{#concept "standard gap map" Disambiguation="cone over a cospan" Agda=gap}}
+of a [commuting square](foundation-core.commuting-squares-of-maps.md) is the map
+from the domain of the cone into the standard pullback.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
+  (f : A → X) (g : B → X)
+  where
+
+  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
+```
+
+## Properties
+
+### 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-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-Σ
+      ( λ bp' α → Σ (b ＝ pr1 bp') (λ β → ap f α ∙ pr2 bp' ＝ p ∙ ap g β))
+      ( refl)
+      ( refl , inv right-unit)
+      ( λ x → id-equiv)
+      ( extensionality-Σ
+        ( λ 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-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-standard-pullback s t) (α , β , γ)
+```
+
+### The standard pullback satisfies the universal property of pullbacks
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
+  where
+
+  abstract
+    universal-property-standard-pullback :
+      universal-property-pullback f g (cone-standard-pullback f g)
+    universal-property-standard-pullback C =
+      is-equiv-comp
+        ( tot (λ _ → map-distributive-Π-Σ))
+        ( mapping-into-Σ)
+        ( is-equiv-mapping-into-Σ)
+        ( is-equiv-tot-is-fiberwise-equiv (λ _ → is-equiv-map-distributive-Π-Σ))
+```
+
+### A cone is equal to the value of `cone-map` at its own gap map
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
+  (f : A → X) (g : B → X)
+  where
+
+  htpy-cone-up-pullback-standard-pullback :
+    (c : cone f g C) →
+    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
+```
+
+### Standard pullbacks are symmetric
+
+The standard pullback of `f : A -> X <- B : g` is equivalent to the standard
+pullback of `g : B -> X <- A : f`.
+
+```agda
+map-commutative-standard-pullback :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (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-standard-pullback f g ∘
+    map-commutative-standard-pullback g f) ~ id
+inv-inv-map-commutative-standard-pullback f g x =
+  eq-pair-eq-fiber
+    ( eq-pair-eq-fiber
+      ( inv-inv (coherence-square-standard-pullback x)))
+
+abstract
+  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-standard-pullback f g)
+  is-equiv-map-commutative-standard-pullback f g =
+    is-equiv-is-invertible
+      ( map-commutative-standard-pullback g f)
+      ( inv-inv-map-commutative-standard-pullback f g)
+      ( inv-inv-map-commutative-standard-pullback g f)
+
+commutative-standard-pullback :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) →
+  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
+```
+
+#### The gap map of the swapped cone computes as the underlying gap map followed by a swap
+
+```agda
+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-standard-pullback f g ∘ gap f g c
+triangle-map-commutative-standard-pullback f g c = refl-htpy
+```
+
+### Pullbacks can be "folded"
+
+Given a standard pullback square
+
+```text
+         f'
+    C -------> B
+    | ⌟        |
+  g'|          | g
+    v          v
+    A -------> X
+         f
+```
+
+we can "fold" the vertical edge onto the horizontal one and get a new pullback
+square
+
+```text
+            C ---------> X
+            | ⌟          |
+  (f' , g') |            |
+            v            v
+          A × B -----> X × X,
+                f × g
+```
+
+moreover, this folded square is a pullback if and only if the original one is.
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X)
+  where
+
+  fold-cone :
+    {l4 : Level} {C : UU l4} →
+    cone f g C → cone (map-product f g) (diagonal X) C
+  pr1 (pr1 (fold-cone c) z) = vertical-map-cone f g c z
+  pr2 (pr1 (fold-cone c) z) = horizontal-map-cone f g c z
+  pr1 (pr2 (fold-cone c)) = g ∘ horizontal-map-cone f g c
+  pr2 (pr2 (fold-cone c)) z = eq-pair (coherence-square-cone f g c z) refl
+
+  map-fold-cone-standard-pullback :
+    standard-pullback f g → standard-pullback (map-product f g) (diagonal X)
+  pr1 (pr1 (map-fold-cone-standard-pullback x)) =
+    vertical-map-standard-pullback x
+  pr2 (pr1 (map-fold-cone-standard-pullback x)) =
+    horizontal-map-standard-pullback x
+  pr1 (pr2 (map-fold-cone-standard-pullback x)) =
+    g (horizontal-map-standard-pullback x)
+  pr2 (pr2 (map-fold-cone-standard-pullback x)) =
+    eq-pair (coherence-square-standard-pullback x) refl
+
+  map-inv-fold-cone-standard-pullback :
+    standard-pullback (map-product f g) (diagonal X) → standard-pullback f g
+  pr1 (map-inv-fold-cone-standard-pullback ((a , b) , x , α)) = a
+  pr1 (pr2 (map-inv-fold-cone-standard-pullback ((a , b) , x , α))) = b
+  pr2 (pr2 (map-inv-fold-cone-standard-pullback ((a , b) , x , α))) =
+    ap pr1 α ∙ inv (ap pr2 α)
+
+  abstract
+    is-section-map-inv-fold-cone-standard-pullback :
+      is-section
+        ( map-fold-cone-standard-pullback)
+        ( map-inv-fold-cone-standard-pullback)
+    is-section-map-inv-fold-cone-standard-pullback ((a , b) , (x , α)) =
+      map-extensionality-standard-pullback
+        ( map-product f g)
+        ( diagonal X)
+        ( refl)
+        ( ap pr2 α)
+        ( ( inv (is-section-pair-eq α)) ∙
+          ( ap
+            ( λ t → eq-pair t (ap pr2 α))
+            ( ( inv right-unit) ∙
+              ( inv
+                ( left-whisker-concat
+                  ( ap pr1 α)
+                  ( 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) (x , x))
+            ( inv (ap-diagonal (ap pr2 α)))))
+
+  abstract
+    is-retraction-map-inv-fold-cone-standard-pullback :
+      is-retraction
+        ( map-fold-cone-standard-pullback)
+        ( map-inv-fold-cone-standard-pullback)
+    is-retraction-map-inv-fold-cone-standard-pullback (a , b , p) =
+      map-extensionality-standard-pullback f g
+        ( refl)
+        ( refl)
+        ( inv
+          ( ( right-whisker-concat
+              ( ( right-whisker-concat
+                  ( ap-pr1-eq-pair p refl)
+                  ( inv (ap pr2 (eq-pair p refl)))) ∙
+                ( ap (λ t → p ∙ inv t) (ap-pr2-eq-pair p refl)) ∙
+                ( right-unit))
+              ( refl)) ∙
+            ( right-unit)))
+
+  abstract
+    is-equiv-map-fold-cone-standard-pullback :
+      is-equiv map-fold-cone-standard-pullback
+    is-equiv-map-fold-cone-standard-pullback =
+      is-equiv-is-invertible
+        ( map-inv-fold-cone-standard-pullback)
+        ( is-section-map-inv-fold-cone-standard-pullback)
+        ( is-retraction-map-inv-fold-cone-standard-pullback)
+
+  triangle-map-fold-cone-standard-pullback :
+    {l4 : Level} {C : UU l4} (c : cone f g C) →
+    gap (map-product f g) (diagonal X) (fold-cone c) ~
+    map-fold-cone-standard-pullback ∘ gap f g c
+  triangle-map-fold-cone-standard-pullback c = refl-htpy
+```
+
 ## Properties
 
 ### The equivalence on standard pullbacks induced by parallel cospans
diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md
index d351347122..2b8c5788c9 100644
--- a/src/foundation/universal-property-cartesian-product-types.lagda.md
+++ b/src/foundation/universal-property-cartesian-product-types.lagda.md
@@ -9,6 +9,7 @@ module foundation.universal-property-cartesian-product-types where
 ```agda
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
+open import foundation.standard-pullbacks
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -19,7 +20,6 @@ open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.pullbacks
-open import foundation-core.standard-pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
 
diff --git a/src/foundation/universal-property-fiber-products.lagda.md b/src/foundation/universal-property-fiber-products.lagda.md
index 22d91cd153..6a4c8732c1 100644
--- a/src/foundation/universal-property-fiber-products.lagda.md
+++ b/src/foundation/universal-property-fiber-products.lagda.md
@@ -10,6 +10,7 @@ module foundation.universal-property-fiber-products where
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
+open import foundation.standard-pullbacks
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
@@ -21,7 +22,6 @@ open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.pullbacks
-open import foundation-core.standard-pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
 
diff --git a/tables/pullbacks.md b/tables/pullbacks.md
index 552cde2fd8..77407e39b5 100644
--- a/tables/pullbacks.md
+++ b/tables/pullbacks.md
@@ -6,8 +6,7 @@
 | 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)                                         |
 | The universal property of fiber products              | [`foundation.universal-property-fiber-products`](foundation.universal-property-fiber-products.md)                               |
-| Standard pullbacks (foundation-core)                  | [`foundation-core.standard-pullbacks`](foundation-core.standard-pullbacks.md)                                                   |
-| Standard pullbacks (foundation)                       | [`foundation.standard-pullbacks`](foundation.standard-pullbacks.md)                                                             |
+| Standard pullbacks                                    | [`foundation.standard-pullbacks`](foundation.standard-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)                                                   |