SCT.VolumeI.Chapter01.Section06.Cospans.CospanCartesian

Complete compiler-highlighted source. Follow a symbol to its declaration.

# A cartesian map of cospans

If the left object map is an equivalence and the right square is a
pullback, pasting shows that the induced pullback map is an equivalence.
More generally, the square on the left projections is a pullback.
The proof retains the two specified squares of the cospan map.

```agda
{-# OPTIONS --safe --without-K #-}
open import Agda.Primitive using (Level)
open import SCT.VolumeI.Chapter01.Theory using (Theory)
import SCT.VolumeI.Chapter01.Section04.Setup as Setup
import SCT.VolumeI.Chapter01.Section06.PullbackLaws as Laws
import SCT.VolumeI.Chapter01.Section03.ProductCalculus.PairingNaturality as PN

module SCT.VolumeI.Chapter01.Section06.Cospans.CospanCartesian
  {c m a : Level} (𝒯 : Theory c m a) (P : Laws.PullbackStructure 𝒯) where

open Setup 𝒯
open Laws.PullbackStructure P
open import SCT.VolumeI.Chapter01.Section06.ConeCalculus.ConePasting 𝒯
open import SCT.VolumeI.Chapter01.Section06.ConeCalculus.ConeArrowChange 𝒯 using (changeLeft)
open import SCT.VolumeI.Chapter01.Section06.ConeCalculus.ConeSymmetry 𝒯 using (coneSwap; cone-match-change)
open import SCT.VolumeI.Chapter01.Section06.ConeCalculus.InverseCalculus 𝒯
open import SCT.VolumeI.Chapter01.Section06.PullbackFunctor 𝒯 P
open import SCT.VolumeI.Chapter01.Section06.PullbackSquares 𝒯 P
  using (IsPullback; pullbackCone-isPullback; pullback-cone-invariant)
open import SCT.VolumeI.Chapter01.Section06.PullbackEquivalences 𝒯 P
open import SCT.VolumeI.Chapter01.Section06.PullbackSymmetry 𝒯 P using (pullback-swap)
open import SCT.VolumeI.Chapter01.Section06.PullbackArrowChange 𝒯 P using (module ChangeLeft)
open import SCT.VolumeI.Chapter01.Section06.PastingLemma 𝒯 P using (module Pasting)
open PN vocabulary terminal products productLaws composition vertical whiskering using (cancel-right)

prefix-assoc : {C D : CAT} {f₀ f₁ f₂ f₃ f₄ : MAP C D}
  (a₃ : f₃ =₁ f₄) (a₂ : f₂ =₁ f₃) (a₁ : f₁ =₁ f₂) (a₀ : f₀ =₁ f₁) →
  (a₃ ∙ (a₂ ∙ (a₁ ∙ a₀))) =₂ ((a₃ ∙ (a₂ ∙ a₁)) ∙ a₀)
prefix-assoc a₃ a₂ a₁ a₀ = (isoComp-assoc-at a₃ (a₂ ∙ a₁) a₀) ⁻¹ ∙
  isoComp-cong (idIso a₃) ((isoComp-assoc-at a₂ a₁ a₀) ⁻¹)

rightSquareOf : {C D E C′ D′ E′ : CAT} {f : MAP C E} {g : MAP D E}
  {f′ : MAP C′ E′} {g′ : MAP D′ E′} (F : CospanMap f g f′ g′) →
  Cone g′ (CospanMap.base F) D
rightSquareOf F = record { left = CospanMap.right F ; right = _ ; match = CospanMap.rightSquare F }

module CartesianProjection {C D E C′ D′ E′ : CAT}
  {f : MAP C E} {g : MAP D E} {f′ : MAP C′ E′} {g′ : MAP D′ E′}
  (F : CospanMap f g f′ g′)
  (right-pullback : IsPullback (rightSquareOf F)) where

  open CospanMap F renaming (left to u; right to v; base to w; leftSquare to α; rightSquare to β)
  source = pullbackCone f g
  target = pullbackCone f′ g′
  p = Cone.left source
  q = Cone.right source
  H = pullbackMap
  legLeft = ConeIso.leftIso pullbackMap-β
  ρ = ConeIso.rightIso pullbackMap-β
  σ = Cone.match (mapCone source)

  rightSquare : Cone g′ w D
  rightSquare = record { left = v ; right = g ; match = β }
  rightCone = coneSwap rightSquare
  right-isPullback = pullback-swap rightSquare right-pullback
  module RightPaste = Pasting f w g′ rightCone right-isPullback
  pasted = RightPaste.Paste.flatten source
  changed = changeLeft (α ⁻¹) pasted

  outerMapped : Cone (f′ ∘ u) g′ (Pullback f g)
  outerMapped = record { left = p ; right = v ∘ q ; match = σ ∙ comp-assoc p u f′ }

  changed-comparison : ConeIso changed outerMapped
  changed-comparison = cone-match-change _ _ _ _
    (normalized ⁻¹ ∙
      isoComp-cong (idIso (Cone.match pasted)) (inverse-inverse (α ▷ p) ∙ (＝-inv ◁ pre-inverse α p)))
    where
    ar = comp-assoc q v g′
    br = β ⁻¹ ▷ q
    cr = (comp-assoc q g w) ⁻¹
    dr = w ◁ Cone.match source
    er = comp-assoc p f w
    fr = α ▷ p
    assocLeft = comp-assoc p u f′
    prefix = ar ∙ (br ∙ cr)
    σ-normal : σ =₂ ((Cone.match pasted ∙ fr) ∙ assocLeft ⁻¹)
    σ-normal = (isoComp-assoc-at (Cone.match pasted) fr (assocLeft ⁻¹)) ⁻¹ ∙
      ((isoComp-assoc-at prefix (dr ∙ er) (fr ∙ assocLeft ⁻¹)) ⁻¹ ∙
      (isoComp-cong (idIso prefix) ((isoComp-assoc-at dr er (fr ∙ assocLeft ⁻¹)) ⁻¹) ∙
        prefix-assoc ar br cr (dr ∙ (er ∙ (fr ∙ assocLeft ⁻¹)))))
    normalized : (σ ∙ assocLeft) =₂ (Cone.match pasted ∙ fr)
    normalized = isoComp-unitʳ-at (Cone.match pasted ∙ fr) ∙
      (isoComp-cong (idIso (Cone.match pasted ∙ fr)) (isoComp-inverseˡ-at assocLeft) ∙
      (isoComp-assoc-at (Cone.match pasted ∙ fr) (assocLeft ⁻¹) assocLeft ∙
        isoComp-cong σ-normal (idIso assocLeft)))

  outer-isPullback : IsPullback outerMapped
  outer-isPullback = pullback-cone-invariant changed-comparison
    (ChangeLeft.preserve (α ⁻¹) g′ pasted
      (RightPaste.paste-isPullback source (pullbackCone-isPullback f g)))

  projectionSquare : Cone u (Cone.left target) (Pullback f g)
  projectionSquare = record { left = p ; right = H ; match = legLeft ⁻¹ }
  module TargetPaste = Pasting u f′ g′ target (pullbackCone-isPullback f′ g′)

  outer-comparison : ConeIso (TargetPaste.Paste.flatten projectionSquare) outerMapped
  outer-comparison = compositeCone-compatible u f′ _ _ (idIso p) ρ
    (isoComp-cong (idIso (g′ ◁ ρ)) ((TargetPaste.Paste.flatten-match projectionSquare) ⁻¹) ∙
    (isoComp-assoc-at (g′ ◁ ρ) ν (f′ ◁ legLeft ⁻¹) ∙
    (cancel ⁻¹ ∙
    (isoComp-unitʳ-at σ ∙
      isoComp-cong (cancel-right (comp-assoc p u f′) σ)
        (postWhisker-idIso f′ (u ∘ p) ∙ (postWhisker f′ ◁ postWhisker-idIso u p))))))
    where
    ν = Cone.match (conePre H target)
    inverseImage = postWhisker-idIso f′ (u ∘ p) ∙
      ((postWhisker f′ ◁ isoComp-inverseʳ-at legLeft) ∙ (postWhisker-isoComp-at f′ legLeft (legLeft ⁻¹)) ⁻¹)
    cancel : (((g′ ◁ ρ) ∙ ν) ∙ (f′ ◁ legLeft ⁻¹)) =₂ σ
    cancel = isoComp-unitʳ-at σ ∙
      (isoComp-cong (idIso σ) inverseImage ∙
      (isoComp-assoc-at σ (f′ ◁ legLeft) (f′ ◁ legLeft ⁻¹) ∙
        isoComp-cong ((ConeIso.compatible pullbackMap-β) ⁻¹) (idIso (f′ ◁ legLeft ⁻¹))))

  projection-square-isPullback : IsPullback projectionSquare
  projection-square-isPullback = TargetPaste.cancel-isPullback projectionSquare
    (pullback-cone-invariant (coneIso-inverse outer-comparison) outer-isPullback)

module CospanCartesian {C D E C′ D′ E′ : CAT}
  {f : MAP C E} {g : MAP D E} {f′ : MAP C′ E′} {g′ : MAP D′ E′}
  (F : CospanMap f g f′ g′) (eu : IsEquiv (CospanMap.left F))
  (right-pullback : IsPullback (rightSquareOf F)) where
  open CartesianProjection F right-pullback public

  pullbackMap-isEquiv : IsEquiv (CospanMap.pullbackMap F)
  pullbackMap-isEquiv = degenerate-pullback-converse eu (coneSwap projectionSquare)
    (pullback-swap projectionSquare projection-square-isPullback)
```