# Pullback squares

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-28.

module foundation.pullback-squares where

Imports
open import foundation.cones-over-cospans
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.commuting-squares-of-maps
open import foundation-core.universal-property-pullbacks


## Idea

A pullback square, or cartesian square, is a commuting square of maps that satisfies the universal property of being a pullback.

## Definitions

### Pullback cones

module _
{l1 l2 l3 l4 : Level} (l : Level) {A : UU l1} {B : UU l2} {C : UU l3}
(f : A → C) (g : B → C) (X : UU l4)
where

pullback-cone : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
pullback-cone = Σ (cone f g X) (universal-property-pullback l f g)


### Pullback squares

module _
{l1 l2 l3 l4 : Level} (l : Level) (A : UU l1) (B : UU l2) (C : UU l3)
(X : UU l4)
where

pullback-square : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
pullback-square =
Σ ( A → C)
( λ f →
Σ ( B → C)
( λ g →
Σ ( cone f g X)
( universal-property-pullback l f g)))


### Components of a pullback cone

module _
{l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
(f : A → C) (g : B → C) (c : pullback-cone l f g X)
where

cone-pullback-cone : cone f g X
cone-pullback-cone = pr1 c

vertical-map-pullback-cone : X → A
vertical-map-pullback-cone = vertical-map-cone f g cone-pullback-cone

horizontal-map-pullback-cone : X → B
horizontal-map-pullback-cone = horizontal-map-cone f g cone-pullback-cone

coherence-square-pullback-cone :
coherence-square-maps horizontal-map-pullback-cone
( vertical-map-pullback-cone)
( g)
( f)
coherence-square-pullback-cone = coherence-square-cone f g cone-pullback-cone

universal-property-pullback-cone : universal-property-pullback l f g (pr1 c)
universal-property-pullback-cone = pr2 c