Other Agda modules in this section (28)
# Elementary pullback constructions
Base change preserves equivalences. The proof factors the inverse cone and
uses recovery of a cone identification from one leg when the opposite
cospan arrow is an equivalence. Recovery retains the prescribed image and
the complete matching square.
```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.PullbackConstructions where
open import SCT.VolumeI.Chapter01.Section01.Vocabulary hiding (_＝_)
import SCT.VolumeI.Chapter01.Section01.Terms as Terms
open Operations
open import SCT.VolumeI.Chapter01.Section01.Terminal
open Constructions
open import SCT.VolumeI.Chapter01.Section02.Coherence
using (id₌; comp-unitˡ; comp-unitʳ; comp-assoc; module Composition)
open Composition
open import SCT.VolumeI.Chapter01.Section02.Specialization
open import SCT.VolumeI.Chapter01.Section02.Products
open Calculus
open import SCT.VolumeI.Chapter01.Section03.Equivalences
import SCT.VolumeI.Chapter01.Section03.Factorizations as Fact
open import SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence using (factor-through-postWhisker)
open import SCT.VolumeI.Chapter01.Section03.ProductConstructions
open import SCT.VolumeI.Chapter01.Section06.Cones
open import SCT.VolumeI.Chapter01.Section06.ConeIdentifications
open import SCT.VolumeI.Chapter01.Section06.ConeTransport
open import SCT.VolumeI.Chapter01.Section06.ConeUniversality
open import SCT.VolumeI.Chapter01.Section06.Pullbacks
open import SCT.VolumeI.Chapter01.Section06.PullbackSquares
module _ {Γ : Context} where
module _ {X C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} where
open Terms.Equalities X using (_＝_)
module RightLegRecovery (eg : IsEquiv g) (s t : Cone f g T)
(α : Cone.left s ＝ Cone.left t) where
private
τ = const {P = X} (Cone.match s)
boundary = const (Cone.match t) ∙ (f ◁ α)
chosen : Fact.Factorization (postWhisker g) (boundary ∙ τ ⁻¹)
chosen = factor-through-postWhisker g eg (boundary ∙ τ ⁻¹)
right : Cone.right s ＝ Cone.right t
right = Fact.factor chosen
right-image : (g ◁ right) =₁ (boundary ∙ τ ⁻¹)
right-image = Fact.triangle chosen
identification : ConeIdentification X s t
identification = record
{ left = α; right = right
; compatible = comp₌-cong (right-image ⁻¹) (id₌ τ) ∙
(inv-comp-right boundary τ) ⁻¹ }
module _ {X C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} where
open Terms.Equalities X using (_＝_)
cone-identification-from-left : IsEquiv g → (s t : Cone f g T)
→ Cone.left s ＝ Cone.left t → ConeIdentification X s t
cone-identification-from-left = RightLegRecovery.identification
cone-identification-from-left-One : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
→ IsEquiv g → (s t : Cone f g T)
→ Cone.left s =₁ Cone.left t → ConeIdentification₁ s t
cone-identification-from-left-One eg s t α = cone-identification-One
(RightLegRecovery.identification eg s t α)
cone-identification-over-One : {C D T : CAT Γ} {f : MAP C One} {g : MAP D One}
(s t : Cone f g T) → Cone.left s =₁ Cone.left t
→ Cone.right s =₁ Cone.right t → ConeIdentification₁ s t
cone-identification-over-One s t α β = record
{ left = α; right = β; compatible = terminal-unique₂ _ _ }
```
## Base change of an equivalence
Factoring f through the equivalence g supplies a cone with identity left leg.
Its pullback factor is an inverse to the first projection. The other inverse
law follows by reflecting the complete cone identification supplied above.
```agda
module BaseChangeEquivalence {C D E : CAT Γ} (f : MAP C E) (g : MAP D E)
(eg : IsEquiv g) where
private
chosen = Fact.factor-through-equiv eg f
inverse-cone : Cone f g C
inverse-cone = record
{ left = id C; right = Fact.factor chosen
; match = (Fact.triangle chosen) ⁻¹ ∙ comp-unitʳ f }
inverse : MAP C (Pullback f g)
inverse = pullback-factor inverse-cone
projection-inverse : (pullback₁ ∘ inverse) =₁ id C
projection-inverse = pullback-factor-β₁ inverse-cone
inverse-projection : (inverse ∘ pullback₁) =₁ id (Pullback f g)
inverse-projection = pullback-reflect _ _
(cone-identification-from-left-One eg _ _
((comp-unitʳ pullback₁) ⁻¹ ∙
(comp-unitˡ pullback₁ ∙
((projection-inverse ▷ pullback₁) ∙ (comp-assoc pullback₁ inverse pullback₁) ⁻¹))))
projection-isEquiv : IsEquiv (pullback₁ {f = f} {g = g})
projection-isEquiv = record
{ inverse = inverse
; left-inverse-law = inverse-projection ⁻¹
; right-inverse-law = projection-inverse ⁻¹ }
pullback₁-isEquiv : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E)
→ IsEquiv g → IsEquiv (pullback₁ {f = f} {g = g})
pullback₁-isEquiv = BaseChangeEquivalence.projection-isEquiv
isPullback-from-left-isEquiv : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
→ IsEquiv g → (s : Cone f g T) → IsEquiv (Cone.left s) → IsPullback s
isPullback-from-left-isEquiv {f = f} {g} eg s es =
equiv-cancel-left (pullback-factor s) pullback₁ (pullback₁-isEquiv f g eg)
(equiv-transport ((pullback-factor-β₁ s) ⁻¹) es)
left-isEquiv-from-isPullback : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
→ IsEquiv g → (s : Cone f g T) → IsPullback s → IsEquiv (Cone.left s)
left-isEquiv-from-isPullback {f = f} {g} eg s es = equiv-transport (pullback-factor-β₁ s)
(equiv-compose (pullback-factor s) pullback₁ es (pullback₁-isEquiv f g eg))
```
## Chosen symmetry and units
The chosen pullback cone is universal: its factor agrees with the identity
by full cone reflection. General symmetry of universal cones therefore
makes its chosen swap map an equivalence. This chooses the inverse supplied
by recognition, rather than selecting the reverse swap as in the first
rebuild. The explicit double-swap equation below remains available; no
equality of the two equivalence witnesses is asserted.
```agda
pullback-cone-isPullback : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E)
→ IsPullback (pullback-cone f g)
pullback-cone-isPullback f g = equiv-transport
((pullback-reflect _ _
(cone-compose (cone-inverse (cone-restrict-id (pullback-cone f g)))
(pullback-factor-β (pullback-cone f g)))) ⁻¹)
(id-isEquiv (Pullback f g))
pullback-swap : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E)
→ MAP (Pullback f g) (Pullback g f)
pullback-swap f g = pullback-factor (cone-swap (pullback-cone f g))
pullback-swap-isEquiv : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E)
→ IsEquiv (pullback-swap f g)
pullback-swap-isEquiv f g = SwappedCone.isPullback (pullback-cone f g) (pullback-cone-isPullback f g)
pullback₂-isEquiv : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E)
→ IsEquiv f → IsEquiv (pullback₂ {f = f} {g = g})
pullback₂-isEquiv f g ef = equiv-transport (pullback-factor-β₁ (cone-swap (pullback-cone f g)))
(equiv-compose (pullback-swap f g) pullback₁ (pullback-swap-isEquiv f g) (pullback₁-isEquiv g f ef))
pullback-unitˡ : {C E : CAT Γ} (f : MAP C E)
→ IsEquiv (pullback₁ {f = f} {g = id E})
pullback-unitˡ {E = E} f = pullback₁-isEquiv f (id E) (id-isEquiv E)
pullback-unitʳ : {C E : CAT Γ} (f : MAP C E)
→ IsEquiv (pullback₂ {f = id E} {g = f})
pullback-unitʳ {E = E} f = pullback₂-isEquiv (id E) f (id-isEquiv E)
```
## Computation of symmetry
The double swap and the swap of a factor retain their full cone comparisons.
```agda
pullback-swap-swap : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) →
(pullback-swap g f ∘ pullback-swap f g) =₁ (id (Pullback f g))
pullback-swap-swap f g = pullback-reflect _ _
(cone-compose (cone-inverse (cone-restrict-id (pullback-cone f g)))
(cone-compose (cone-swap-twice (pullback-cone f g))
(cone-compose (cone-swap-identification (pullback-factor-β (cone-swap (pullback-cone f g))))
(cone-compose (cone-swap-restrict (pullback-swap f g) (pullback-cone g f))
(cone-compose (cone-identification-restrict-One (pullback-swap f g) (pullback-factor-β (cone-swap (pullback-cone g f))))
(cone-inverse (cone-restrict-assoc (pullback-swap f g) (pullback-swap g f) (pullback-cone f g))))))))
pullback-factor-swap : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g T) → (pullback-factor (cone-swap s)) =₁ (pullback-swap f g ∘ pullback-factor s)
pullback-factor-swap {f = f} {g} s = pullback-reflect _ _
(cone-compose (cone-inverse swapped-factor-law) (pullback-factor-β (cone-swap s)))
where
swapped-factor-law : ConeIdentification₁
(cone-restrict (pullback-swap f g ∘ pullback-factor s) (pullback-cone g f)) (cone-swap s)
swapped-factor-law = cone-compose (cone-swap-identification (pullback-factor-β s))
(cone-compose (cone-swap-restrict (pullback-factor s) (pullback-cone f g))
(cone-compose (cone-identification-restrict-One (pullback-factor s) (pullback-factor-β (cone-swap (pullback-cone f g))))
(cone-inverse (cone-restrict-assoc (pullback-factor s) (pullback-swap f g) (pullback-cone g f)))))
```
## Terminal base and products
The product and swapped product presentations retain their actual maps,
inverse witnesses and the swapped-coordinate beta laws.
```agda
module _ {Γ : Context} where
module TerminalBase {C D : CAT Γ} (f : MAP C One) (g : MAP D One) where
product-cone : Cone f g (C × D)
product-cone = record { left = pr₁ ; right = pr₂ ; match = terminal-identification _ _ }
to-product : MAP (Pullback f g) (C × D)
to-product = pair pullback₁ pullback₂
from-product : MAP (C × D) (Pullback f g)
from-product = pullback-factor product-cone
to-from : (to-product ∘ from-product) =₁ (id (C × D))
to-from = pair-projections ∙
(pair⁼ (pullback-factor-β₁ product-cone) (pullback-factor-β₂ product-cone) ∙ pair-pre pullback₁ pullback₂ from-product)
from-to : (from-product ∘ to-product) =₁ (id (Pullback f g))
from-to = pullback-reflect _ _ (cone-identification-over-One _ _
((comp-unitʳ pullback₁) ⁻¹ ∙
(pair-β₁ pullback₁ pullback₂ ∙ ((pullback-factor-β₁ product-cone ▷ to-product) ∙
(comp-assoc to-product from-product pullback₁) ⁻¹)))
((comp-unitʳ pullback₂) ⁻¹ ∙
(pair-β₂ pullback₁ pullback₂ ∙ ((pullback-factor-β₂ product-cone ▷ to-product) ∙
(comp-assoc to-product from-product pullback₂) ⁻¹))))
to-product-isEquiv : IsEquiv to-product
to-product-isEquiv = record
{ inverse = from-product ; left-inverse-law = from-to ⁻¹ ; right-inverse-law = to-from ⁻¹ }
product-cone-isPullback : IsPullback product-cone
product-cone-isPullback = record
{ inverse = to-product ; left-inverse-law = to-from ⁻¹ ; right-inverse-law = from-to ⁻¹ }
to-swapped : MAP (Pullback f g) (D × C)
to-swapped = pair pullback₂ pullback₁
from-swapped : MAP (D × C) (Pullback f g)
from-swapped = from-product ∘ swap {C = D} {D = C}
to-swapped-isEquiv : IsEquiv to-swapped
to-swapped-isEquiv = equiv-transport
(pair⁼ (pair-β₂ pullback₁ pullback₂) (pair-β₁ pullback₁ pullback₂) ∙ pair-pre pr₂ pr₁ to-product)
(equiv-compose to-product (swap {C = C} {D = D}) to-product-isEquiv (swap-isEquiv C D))
from-swapped-isEquiv : IsEquiv from-swapped
from-swapped-isEquiv = equiv-compose (swap {C = D} {D = C}) from-product (swap-isEquiv D C) product-cone-isPullback
from-swapped-β₁ : (pullback₁ ∘ from-swapped) =₁ (pr₂ {C = D} {D = C})
from-swapped-β₁ = pair-β₁ pr₂ pr₁ ∙
((pullback-factor-β₁ product-cone ▷ swap {C = D} {D = C}) ∙ (comp-assoc (swap {C = D} {D = C}) from-product pullback₁) ⁻¹)
from-swapped-β₂ : (pullback₂ ∘ from-swapped) =₁ (pr₁ {C = D} {D = C})
from-swapped-β₂ = pair-β₂ pr₂ pr₁ ∙
((pullback-factor-β₂ product-cone ▷ swap {C = D} {D = C}) ∙ (comp-assoc (swap {C = D} {D = C}) from-product pullback₂) ⁻¹)
module PullbackProduct (C D : CAT Γ) = TerminalBase (terminate C) (terminate D)
```