From 93d4161877fa29fd2ba18b09d0a01e1aa5511a97 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 26 Feb 2024 12:35:54 +0100 Subject: [PATCH] idea pullbacks --- src/foundation-core/pullbacks.lagda.md | 27 ++++++++++++++------------ src/foundation/pullbacks.lagda.md | 27 ++++++++++++++------------ 2 files changed, 30 insertions(+), 24 deletions(-) diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md index 060401aa42..5309099cd4 100644 --- a/src/foundation-core/pullbacks.lagda.md +++ b/src/foundation-core/pullbacks.lagda.md @@ -31,25 +31,28 @@ open import foundation-core.universal-property-pullbacks ## Idea -Given a [cospan of types](foundation.cospans.md) +Consider a [cone](foundation.cones-over-cospan-diagrams.md) over a +[cospan diagram of types](foundation.cospan-diagrams.md) `f : A -> X <- B : g,` ```text - f : A → X ← B : g, + C ------> B + | | + | | g + ∨ ∨ + A ------> X. + f ``` -we want to pose the question of whether a certain -[cone](foundation.cones-over-cospan-diagrams.md) over it is a +we want to pose the question of whether this cone is a {{#concept "pullback cone" Disambiguation="types" Agda=is-pullback}}. Although this concept is captured by [the universal property of the pullback](foundation-core.universal-property-pullbacks.md), -this is a large proposition, which is not suitable for all purposes. - -Therefore, as our main definition of a pullback cone we consider -{{#concept "the small predicate of being a pullback" Agda=is-pullback}}: given -the existence of the -[standard pullback type](foundation-core.standard-pullbacks.md) `A ×_X B`, we -can characterize pullback cones as those for which the gap map into the standard -pullback is an [equivalence](foundation-core.equivalences.md). +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) +`A ×_X B`, a cone is a _pullback_ if gap map into the standard pullback is an +[equivalence](foundation-core.equivalences.md). ## Definitions diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md index acd402fbea..2fb7fdc448 100644 --- a/src/foundation/pullbacks.lagda.md +++ b/src/foundation/pullbacks.lagda.md @@ -45,25 +45,28 @@ open import foundation-core.whiskering-identifications-concatenation ## Idea -Given a [cospan of types](foundation.cospans.md) +Consider a [cone](foundation.cones-over-cospan-diagrams.md) over a +[cospan diagram of types](foundation.cospan-diagrams.md) `f : A -> X <- B : g,` ```text - f : A → X ← B : g, + C ------> B + | | + | | g + ∨ ∨ + A ------> X. + f ``` -we want to pose the question of whether a certain -[cone](foundation.cones-over-cospan-diagrams.md) over it is a +we want to pose the question of whether this cone is a {{#concept "pullback cone" Disambiguation="types" Agda=is-pullback}}. Although this concept is captured by [the universal property of the pullback](foundation-core.universal-property-pullbacks.md), -this is a large proposition, which is not suitable for all purposes. - -Therefore, as our main definition of a pullback cone we consider -{{#concept "the small predicate of being a pullback" Agda=is-pullback}}: given -the existence of the -[standard pullback type](foundation-core.standard-pullbacks.md) `A ×_X B`, we -can characterize pullback cones as those for which the gap map into the standard -pullback is an [equivalence](foundation-core.equivalences.md). +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) +`A ×_X B`, a cone is a _pullback_ if gap map into the standard pullback is an +[equivalence](foundation-core.equivalences.md). ## Properties