SCT.VolumeI.Chapter01.Section08.PushoutComparison

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

# Prescribed comparisons between pushout extensions

A comparison of the two restricted cocones lifts to a comparison of the
extensions. Both restrictions of this lift agree with the prescribed
legs. These identifications are needed when cancelling a pushout square.

```agda
{-# OPTIONS --safe --without-K #-}
open import Agda.Primitive using (Level)
open import SCT.VolumeI.Chapter01.Theory using (Theory)
import SCT.VolumeI.Chapter01.Section04.MappingAnimae as Mapping
import SCT.VolumeI.Chapter01.Section06.PullbackLaws as Laws
import SCT.VolumeI.Chapter01.Section08.MappingCalculus.Decoding.DecodeRestrictionCones as Decode
import SCT.VolumeI.Chapter01.Section08.MappingCalculus.Decoding.DecodeSquareEvaluation as Evaluation
import SCT.VolumeI.Chapter01.Section06.ConeCalculus.UniversalConeLifting as Lifting

module SCT.VolumeI.Chapter01.Section08.PushoutComparison
  {c m a : Level} (𝒯 : Theory c m a) (M : Mapping.MappingAnimae 𝒯)
  (P : Laws.PullbackStructure 𝒯) where

open import SCT.VolumeI.Chapter01.Section05.Setup 𝒯 M
open import SCT.VolumeI.Chapter01.Section04.Substitution.CoherenceTransport 𝒯
open import SCT.VolumeI.Chapter01.Section06.ConeCalculus.InverseCalculus 𝒯 using (pre-inverse)
open import SCT.VolumeI.Chapter01.Section06.PullbackSquares 𝒯 P
open import SCT.VolumeI.Chapter01.Section08.PushoutSquares 𝒯 M P
open import SCT.VolumeI.Chapter01.Section08.Squares 𝒯 using (squareCocone)
open import SCT.VolumeI.Chapter01.Section08.Cocones 𝒯
open import SCT.VolumeI.Chapter01.Section08.CoconeCalculus.CoconeUniversality 𝒯
open import SCT.VolumeI.Chapter01.Section08.CoconeCalculus.CoconePostcomposition 𝒯 using (coconePost; cocone-action)
open import SCT.VolumeI.Chapter01.Section08.MappingCalculus.Decoding.DecodingCalculus 𝒯 M
open import SCT.VolumeI.Chapter01.Section08.MappingCalculus.Decoding.DecodedLegCalculus 𝒯
module DC = Decode 𝒯 M

module PrescribedComparison {A B C D E : CAT}
  {u : MAP A B} {l : MAP A C} {r : MAP B D} {v : MAP C D}
  (s : Square u l r v) (universal : IsPushout s)
  (f g : MAP D E)
  (Φ : CoconeIso (coconePost f (squareCocone s)) (coconePost g (squareCocone s))) where

  ordinary : Cocone u l D
  ordinary = squareCocone s
  f′ : Obj-abs (Map D E)
  f′ = nameMap f
  g′ : Obj-abs (Map D E)
  g′ = nameMap g
  evaluate : (h : Obj-abs (Map D E)) →
    CoconeIso (DC.decodeRestriction {u = u} {v = l} (conePre h (mappingOut s E)))
      (coconePost (decodeMap h) ordinary)
  evaluate = Evaluation.Evaluation.comparison 𝒯 M P s

  decoded-comparison : CoconeIso
    (DC.decodeRestriction {u = u} {v = l} (conePre f′ (mappingOut s E)))
    (DC.decodeRestriction (conePre g′ (mappingOut s E)))
  decoded-comparison = coconeIso-compose (coconeIso-inverse (evaluate g′))
    (coconeIso-compose (coconeIso-inverse (cocone-action ordinary (decode-name g)))
    (coconeIso-compose Φ
    (coconeIso-compose (cocone-action ordinary (decode-name f)) (evaluate f′))))

  module Encoded = DC.ReflectDecodedRestriction
    (conePre f′ (mappingOut s E)) (conePre g′ (mappingOut s E)) decoded-comparison
  module Lift = Lifting.UniversalLift 𝒯 P (mappingOut s E) (universal E)
    f′ g′ Encoded.comparison

  decoded-lift : (decodeMap f′) =₁ (decodeMap g′)
  decoded-lift = decodeMapIso Lift.lift
  lift : f =₁ g
  lift = decode-name g ∙ (decoded-lift ∙ (decode-name f) ⁻¹)

  abstract
    leg-image : {T : CAT} (j : MAP T D) (γ : (f ∘ j) =₁ (g ∘ j)) →
      (decodeMapIso (mapPre j ◁ Lift.lift)) =₂
        ((decodePre j g′) ⁻¹ ∙
          ((decode-name g ▷ j) ⁻¹ ∙
            (γ ∙ ((decode-name f ▷ j) ∙ decodePre j f′)))) →
      (lift ▷ j) =₂ γ
    leg-image j γ prescribed =
      decoded-leg (decodePre j f′) (decodePre j g′)
        (decode-name f ▷ j) (decode-name g ▷ j) γ
        (decodeMapIso (mapPre j ◁ Lift.lift)) (decoded-lift ▷ j)
        (decodePre-absolute j Lift.lift) prescribed ∙ normal
      where
      normal : (lift ▷ j) =₂
        (changeEndpoints (decode-name f ▷ j) (decode-name g ▷ j) (decoded-lift ▷ j))
      normal = isoComp-cong (idIso (decode-name g ▷ j))
        (isoComp-cong (idIso (decoded-lift ▷ j)) (pre-inverse (decode-name f) j) ∙
          preWhisker-isoComp-at decoded-lift ((decode-name f) ⁻¹) j) ∙
        preWhisker-isoComp-at (decode-name g) (decoded-lift ∙ (decode-name f) ⁻¹) j

    left-image : (lift ▷ r) =₂ (CoconeIso.leftIso Φ)
    left-image = leg-image r (CoconeIso.leftIso Φ)
      (Encoded.left-image ∙ (decodeMap-isoMap _ _ ◁ Lift.left-image))

    right-image : (lift ▷ v) =₂ (CoconeIso.rightIso Φ)
    right-image = leg-image v (CoconeIso.rightIso Φ)
      (Encoded.right-image ∙ (decodeMap-isoMap _ _ ◁ Lift.right-image))

  comparison : CoconeComparisonLift ordinary f g Φ
  comparison = record { lift = lift ; left-image = left-image ; right-image = right-image }
```