Other Agda modules in this section (28)
# Mapping animae preserve and detect pullback squares
The mapped cone is the specified evaluation followed by currying. Its
complete matching remains part of the construction. Currying and reflection
use an anima witness for the categorical term source; uncurrying and
restriction do not. Detection tests every categorical T.
```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.MappingPullbacks 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-assoc; module Composition; module Boundaries)
open Composition
open Boundaries using (SquareCell₌)
open import SCT.VolumeI.Chapter01.Section02.Products
open Calculus
open import SCT.VolumeI.Chapter01.Section02.Specialization
open import SCT.VolumeI.Chapter01.Section02.IdentificationSquares
open import SCT.VolumeI.Chapter01.Section03.ProductConstructions
using (productMap; product-unitʳ-inverse; product-unitʳ-isEquiv)
open import SCT.VolumeI.Chapter01.Section03.Identifications.Inverses
open import SCT.VolumeI.Chapter01.Section03.Identifications.EndpointTransport
using (changeEndpoints; changeEndpoints-iterated; transport-square;
reflect-transported-square; restore-boundaries)
open import SCT.VolumeI.Chapter01.Section03.Equivalences
using (equiv-transport; equiv-compose; equiv-cancel-left)
import SCT.VolumeI.Chapter01.Section03.Factorizations as Fact
open import SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence
using (factor-through-preWhisker)
open import SCT.VolumeI.Chapter01.Section04.MappingAnimae
using (Map; map-isAn; mapEval; uncurry; mapCurry; mapCurry-β)
open import SCT.VolumeI.Chapter01.Section04.Currying
using (uncurry⁼; uncurry⁼-cong; uncurry⁼-composition; uncurry⁼-identity;
uncurry-reflect; uncurry-reflect-β; uncurry⁼-reflect; uncurry-restrict)
open import SCT.VolumeI.Chapter01.Section04.Functoriality
using (mapPost; mapPost-β; mapPost-uncurry; mapPost-isEquiv)
open import SCT.VolumeI.Chapter01.Section04.UncurryingRestriction
using (mapPost-uncurry-inputs; mapPost-uncurry-restrict; uncurry-restrict-inputs)
open import SCT.VolumeI.Chapter01.Section04.EquivalenceDetection using (post-tests-all)
open import SCT.VolumeI.Chapter01.Section06.Cones
open import SCT.VolumeI.Chapter01.Section06.ConeIdentifications
open import SCT.VolumeI.Chapter01.Section06.ConeTransport
using (cone-change-legs; cone-change-legs-β; cone-retarget-match-identification)
open import SCT.VolumeI.Chapter01.Section06.Pullbacks
open import SCT.VolumeI.Chapter01.Section06.PullbackSquares
module _ {Γ : Context} where
private
module _ {A C D X : CAT Γ} where
open Terms.InContext A using (Term)
open Terms.Equalities X using (_＝_)
uncurry⁼-inverse : {x y : Term (Map C D)} (α : x ＝ y)
→ uncurry⁼ (α ⁻¹) =₁ ((uncurry⁼ α) ⁻¹)
uncurry⁼-inverse {x = x} α =
(inverse-unique (uncurry⁼ α) (uncurry⁼ (α ⁻¹))
(uncurry⁼-identity x ∙
(uncurry⁼-cong (comp₌-inverseˡ α) ∙
(uncurry⁼-composition (α ⁻¹) α) ⁻¹))) ⁻¹
replace-cone-identification : {C D E X : CAT Γ}
{f : MAP C E} {g : MAP D E} {s t : Cone f g X}
(Φ : ConeIdentification₁ s t)
(α : Cone.left s =₁ Cone.left t) (β : Cone.right s =₁ Cone.right t)
→ ConeIdentification₁.left Φ =₂ α → ConeIdentification₁.right Φ =₂ β
→ ConeIdentification₁ s t
replace-cone-identification {f = f} {g} Φ α β p q = record
{ left = α; right = β
; compatible = replace-edges₌ (postWhisker f ◁ p) (postWhisker g ◁ q)
(ConeIdentification₁.compatible Φ) }
```
## Uncurrying and currying cones
The four actual postcomposition comparisons transport the matching square.
CurriedCone retains the chosen legs, reflected matching and complete
uncurrying law. ReflectedCone uses the specified images of its recovered
legs before reflecting full compatibility.
```agda
uncurry-cone : {X T C D E : CAT Γ} {f : MAP C E} {g : MAP D E} →
Cone (mapPost {C = T} f) (mapPost g) X → Cone f g (X × T)
uncurry-cone {f = f} {g} s = record
{ left = uncurry (Cone.left s) ; right = uncurry (Cone.right s)
; match = mapPost-uncurry g (Cone.right s) ∙
(uncurry⁼ (Cone.match s) ∙ (mapPost-uncurry f (Cone.left s)) ⁻¹) }
uncurry-cone-identification : {X T C D E : CAT Γ} {f : MAP C E} {g : MAP D E}
{s t : Cone (mapPost {C = T} f) (mapPost g) X} → ConeIdentification₁ s t → ConeIdentification₁ (uncurry-cone s) (uncurry-cone t)
uncurry-cone-identification {X} {T} {C} {D} {E} {f} {g} {s} {t} Φ = record
{ left = uncurry⁼ α ; right = uncurry⁼ β
; compatible = transport-square fs ft gs gt τs τt raw-left raw-right native-left native-right
(unconst-sides₌ (mapPost-uncurry-inputs f α)) (unconst-sides₌ (mapPost-uncurry-inputs g β)) rawSquare }
where
α : (Cone.left s) =₁ (Cone.left t)
α = ConeIdentification₁.left Φ
β : (Cone.right s) =₁ (Cone.right t)
β = ConeIdentification₁.right Φ
fs : (uncurry (mapPost f ∘ Cone.left s)) =₁ (f ∘ uncurry (Cone.left s))
fs = mapPost-uncurry f (Cone.left s)
ft : (uncurry (mapPost f ∘ Cone.left t)) =₁ (f ∘ uncurry (Cone.left t))
ft = mapPost-uncurry f (Cone.left t)
gs : (uncurry (mapPost g ∘ Cone.right s)) =₁ (g ∘ uncurry (Cone.right s))
gs = mapPost-uncurry g (Cone.right s)
gt : (uncurry (mapPost g ∘ Cone.right t)) =₁ (g ∘ uncurry (Cone.right t))
gt = mapPost-uncurry g (Cone.right t)
τs : (uncurry (mapPost f ∘ Cone.left s)) =₁ (uncurry (mapPost g ∘ Cone.right s))
τs = uncurry⁼ (Cone.match s)
τt : (uncurry (mapPost f ∘ Cone.left t)) =₁ (uncurry (mapPost g ∘ Cone.right t))
τt = uncurry⁼ (Cone.match t)
native-left : (f ∘ uncurry (Cone.left s)) =₁ (f ∘ uncurry (Cone.left t))
native-left = f ◁ uncurry⁼ α
raw-left : (uncurry (mapPost f ∘ Cone.left s)) =₁ (uncurry (mapPost f ∘ Cone.left t))
raw-left = uncurry⁼ (mapPost f ◁ α)
raw-right : (uncurry (mapPost g ∘ Cone.right s)) =₁ (uncurry (mapPost g ∘ Cone.right t))
raw-right = uncurry⁼ (mapPost g ◁ β)
native-right : (g ∘ uncurry (Cone.right s)) =₁ (g ∘ uncurry (Cone.right t))
native-right = g ◁ uncurry⁼ β
rawSquare : (τt ∙ raw-left) =₂ (raw-right ∙ τs)
rawSquare = uncurry⁼-composition (mapPost g ◁ β) (Cone.match s) ∙
((uncurry⁼-cong (ConeIdentification₁.compatible Φ)) ∙
(uncurry⁼-composition (Cone.match t) (mapPost f ◁ α)) ⁻¹)
module CurriedCone {X T C D E : CAT Γ} {f : MAP C E} {g : MAP D E}
(xAn : isAn X) (s : Cone f g (X × T)) where
left : MAP X (Map T C)
left = mapCurry xAn (Cone.left s)
right : MAP X (Map T D)
right = mapCurry xAn (Cone.right s)
left-β : (uncurry left) =₁ (Cone.left s)
left-β = mapCurry-β xAn (Cone.left s)
right-β : (uncurry right) =₁ (Cone.right s)
right-β = mapCurry-β xAn (Cone.right s)
wanted : Cone f g (X × T)
wanted = cone-change-legs s (uncurry left) (uncurry right) (left-β ⁻¹) (right-β ⁻¹)
desired : (f ∘ uncurry left) =₁ (g ∘ uncurry right)
desired = Cone.match wanted
leftChange : (uncurry (mapPost f ∘ left)) =₁ (f ∘ uncurry left)
leftChange = mapPost-uncurry f left
rightChange : (uncurry (mapPost g ∘ right)) =₁ (g ∘ uncurry right)
rightChange = mapPost-uncurry g right
rawMatch : (uncurry (mapPost f ∘ left)) =₁ (uncurry (mapPost g ∘ right))
rawMatch = rightChange ⁻¹ ∙ (desired ∙ leftChange)
value : Cone (mapPost f) (mapPost g) X
value = record
{ left = left ; right = right
; match = uncurry-reflect xAn _ _ rawMatch }
match-β : (Cone.match (uncurry-cone value)) =₂ desired
match-β = restore-boundaries leftChange rightChange desired
(uncurry⁼ (Cone.match value))
(uncurry-reflect-β xAn _ _ rawMatch)
abstract
uncurry-law : ConeIdentification₁ (uncurry-cone value) s
uncurry-law = cone-compose
(cone-inverse (cone-change-legs-β s _ _ (left-β ⁻¹) (right-β ⁻¹)))
(cone-retarget-match-identification (uncurry-cone value) desired match-β)
module ReflectedCone {X T C D E : CAT Γ} {f : MAP C E} {g : MAP D E}
(xAn : isAn X) (s t : Cone (mapPost {C = T} f) (mapPost g) X)
(Φ : ConeIdentification₁ (uncurry-cone s) (uncurry-cone t)) where
left : (Cone.left s) =₁ (Cone.left t)
left = uncurry-reflect xAn _ _ (ConeIdentification₁.left Φ)
right : (Cone.right s) =₁ (Cone.right t)
right = uncurry-reflect xAn _ _ (ConeIdentification₁.right Φ)
adjusted : ConeIdentification₁ (uncurry-cone s) (uncurry-cone t)
adjusted = replace-cone-identification Φ (uncurry⁼ left) (uncurry⁼ right)
((uncurry-reflect-β xAn _ _ (ConeIdentification₁.left Φ)) ⁻¹)
((uncurry-reflect-β xAn _ _ (ConeIdentification₁.right Φ)) ⁻¹)
fs : (uncurry (mapPost f ∘ Cone.left s)) =₁ (f ∘ uncurry (Cone.left s))
fs = mapPost-uncurry f (Cone.left s)
ft : (uncurry (mapPost f ∘ Cone.left t)) =₁ (f ∘ uncurry (Cone.left t))
ft = mapPost-uncurry f (Cone.left t)
gs : (uncurry (mapPost g ∘ Cone.right s)) =₁ (g ∘ uncurry (Cone.right s))
gs = mapPost-uncurry g (Cone.right s)
gt : (uncurry (mapPost g ∘ Cone.right t)) =₁ (g ∘ uncurry (Cone.right t))
gt = mapPost-uncurry g (Cone.right t)
τs : (uncurry (mapPost f ∘ Cone.left s)) =₁ (uncurry (mapPost g ∘ Cone.right s))
τs = uncurry⁼ (Cone.match s)
τt : (uncurry (mapPost f ∘ Cone.left t)) =₁ (uncurry (mapPost g ∘ Cone.right t))
τt = uncurry⁼ (Cone.match t)
α : (uncurry (mapPost f ∘ Cone.left s)) =₁ (uncurry (mapPost f ∘ Cone.left t))
α = uncurry⁼ (mapPost f ◁ left)
β : (uncurry (mapPost g ∘ Cone.right s)) =₁ (uncurry (mapPost g ∘ Cone.right t))
β = uncurry⁼ (mapPost g ◁ right)
rawSquare : (τt ∙ α) =₂ (β ∙ τs)
rawSquare = reflect-transported-square fs gs ft gt τs τt
α β (f ◁ uncurry⁼ left) (g ◁ uncurry⁼ right)
(unconst-sides₌ (mapPost-uncurry-inputs f left)) (unconst-sides₌ (mapPost-uncurry-inputs g right))
(ConeIdentification₁.compatible adjusted)
identification : ConeIdentification₁ s t
identification = record
{ left = left ; right = right
; compatible = uncurry⁼-reflect xAn _ _
((uncurry⁼-composition (mapPost g ◁ right) (Cone.match s)) ⁻¹ ∙
(rawSquare ∙ uncurry⁼-composition (Cone.match t) (mapPost f ◁ left))) }
```
## Restriction of uncurried cones
Both leg comparisons are the selected uncurrying restriction. Their full
matching square uses the actual postcomposition restriction routes and the
uncurrying input square. Intermediate endpoint normalizations are explicit.
```agda
module UncurriedRestriction {X Y T C D E : CAT Γ} {f : MAP C E} {g : MAP D E}
(r : MAP Y X) (s : Cone (mapPost {C = T} f) (mapPost g) X) where
p : MAP X (Map T C)
p = Cone.left s
q : MAP X (Map T D)
q = Cone.right s
F : MAP (Map T C) (Map T E)
F = mapPost {C = T} f
G : MAP (Map T D) (Map T E)
G = mapPost {C = T} g
τ : (F ∘ p) =₁ (G ∘ q)
τ = Cone.match s
R : MAP (Y × T) (X × T)
R = productMap r (id T)
af : ((F ∘ p) ∘ r) =₁ (F ∘ (p ∘ r))
af = comp-assoc r p F
ag : ((G ∘ q) ∘ r) =₁ (G ∘ (q ∘ r))
ag = comp-assoc r q G
bf : (uncurry ((F ∘ p) ∘ r)) =₁ (uncurry (F ∘ p) ∘ R)
bf = uncurry-restrict {C = T} {D = E} (F ∘ p) r
bg : (uncurry ((G ∘ q) ∘ r)) =₁ (uncurry (G ∘ q) ∘ R)
bg = uncurry-restrict {C = T} {D = E} (G ∘ q) r
Ef : (uncurry ((F ∘ p) ∘ r)) =₁ (f ∘ uncurry (p ∘ r))
Ef = mapPost-uncurry {C = T} f (p ∘ r) ∙ uncurry⁼ {C = T} {D = E} af
Eg : (uncurry ((G ∘ q) ∘ r)) =₁ (g ∘ uncurry (q ∘ r))
Eg = mapPost-uncurry {C = T} g (q ∘ r) ∙ uncurry⁼ {C = T} {D = E} ag
Ef′ : (uncurry (F ∘ p) ∘ R) =₁ (f ∘ (uncurry p ∘ R))
Ef′ = comp-assoc R (uncurry p) f ∙ (mapPost-uncurry {C = T} f p ▷ R)
Eg′ : (uncurry (G ∘ q) ∘ R) =₁ (g ∘ (uncurry q ∘ R))
Eg′ = comp-assoc R (uncurry q) g ∙ (mapPost-uncurry {C = T} g q ▷ R)
ℓ : (uncurry (p ∘ r)) =₁ (uncurry p ∘ R)
ℓ = uncurry-restrict p r
ρ : (uncurry (q ∘ r)) =₁ (uncurry q ∘ R)
ρ = uncurry-restrict q r
source : Cone f g (Y × T)
source = uncurry-cone {f = f} {g = g} (cone-restrict r s)
target : Cone f g (Y × T)
target = cone-restrict R (uncurry-cone {f = f} {g = g} s)
rawSource : (f ∘ uncurry (p ∘ r)) =₁ (g ∘ uncurry (q ∘ r))
rawSource = changeEndpoints Ef Eg (uncurry⁼ {C = T} {D = E} (τ ▷ r))
rawTarget : (f ∘ (uncurry p ∘ R)) =₁ (g ∘ (uncurry q ∘ R))
rawTarget = changeEndpoints Ef′ Eg′ (uncurry⁼ {C = T} {D = E} τ ▷ R)
abstract
source-normal : (Cone.match source) =₂ rawSource
source-normal = changeEndpoints-iterated (uncurry⁼ {C = T} {D = E} af) (uncurry⁼ {C = T} {D = E} ag)
(mapPost-uncurry {C = T} f (p ∘ r)) (mapPost-uncurry {C = T} g (q ∘ r)) (uncurry⁼ {C = T} {D = E} (τ ▷ r)) ∙
comp₌-cong (id₌ (mapPost-uncurry {C = T} g (q ∘ r)))
(comp₌-cong
(comp₌-cong (id₌ (uncurry⁼ {C = T} {D = E} ag))
(comp₌-cong (id₌ (uncurry⁼ {C = T} {D = E} (τ ▷ r))) (uncurry⁼-inverse {C = T} {D = E} af) ∙
uncurry⁼-composition {C = T} {D = E} (τ ▷ r) (af ⁻¹)) ∙
uncurry⁼-composition {C = T} {D = E} ag ((τ ▷ r) ∙ af ⁻¹))
(id₌ ((mapPost-uncurry {C = T} f (p ∘ r)) ⁻¹)))
target-normal : (Cone.match target) =₂ rawTarget
target-normal = changeEndpoints-iterated (mapPost-uncurry {C = T} f p ▷ R) (mapPost-uncurry {C = T} g q ▷ R)
(comp-assoc R (uncurry p) f) (comp-assoc R (uncurry q) g) (uncurry⁼ {C = T} {D = E} τ ▷ R) ∙
comp₌-cong (id₌ (comp-assoc R (uncurry q) g))
(comp₌-cong
(comp₌-cong (id₌ (mapPost-uncurry {C = T} g q ▷ R))
(comp₌-cong (id₌ (uncurry⁼ {C = T} {D = E} τ ▷ R)) (preWhisker-inverse (mapPost-uncurry {C = T} f p) R) ∙
preWhisker-comp₌ (uncurry⁼ {C = T} {D = E} τ) ((mapPost-uncurry {C = T} f p) ⁻¹) R) ∙
preWhisker-comp₌ (mapPost-uncurry {C = T} g q) (uncurry⁼ {C = T} {D = E} τ ∙ (mapPost-uncurry {C = T} f p) ⁻¹) R)
(id₌ ((comp-assoc R (uncurry p) f) ⁻¹)))
abstract
rawSquare : (rawTarget ∙ (f ◁ ℓ)) =₂ ((g ◁ ρ) ∙ rawSource)
rawSquare = transport-square Ef Ef′ Eg Eg′
(uncurry⁼ (τ ▷ r)) (uncurry⁼ τ ▷ R) bf bg (f ◁ ℓ) (g ◁ ρ)
(((mapPost-uncurry-restrict f p r) ⁻¹) ∙
comp₌-assoc (comp-assoc R (uncurry p) f) (mapPost-uncurry f p ▷ R) bf)
(((mapPost-uncurry-restrict g q r) ⁻¹) ∙
comp₌-assoc (comp-assoc R (uncurry q) g) (mapPost-uncurry g q ▷ R) bg)
(transpose-square₌ (unconst-sides₌ (uncurry-restrict-inputs τ r)))
identification : ConeIdentification₁ source target
identification = record { left = ℓ ; right = ρ
; compatible = comp₌-cong (id₌ (g ◁ ρ)) (source-normal ⁻¹) ∙
(rawSquare ∙ comp₌-cong target-normal (id₌ (f ◁ ℓ))) }
uncurry-cone-restrict : {X Y T C D E : CAT Γ} {f : MAP C E} {g : MAP D E}
(r : MAP Y X) (s : Cone (mapPost {C = T} f) (mapPost g) X) →
ConeIdentification₁ (uncurry-cone (cone-restrict r s)) (cone-restrict (productMap r (id T)) (uncurry-cone s))
uncurry-cone-restrict = UncurriedRestriction.identification
```
## The mapped cone and its actual evaluation
Evaluation followed by chosen currying supplies the matching. The evaluation
comparison retains the complete cone law at every categorical probe source.
```agda
module MappedCone {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(T : CAT Γ) (s : Cone f g S) where
module Curried = CurriedCone (map-isAn T S) (cone-restrict mapEval s)
value : Cone (mapPost {C = T} f) (mapPost g) (Map T S)
value = Curried.value
opaque
evaluate : {X : CAT Γ} (h : MAP X (Map T S)) →
ConeIdentification₁ (uncurry-cone (cone-restrict h value)) (cone-restrict (uncurry h) s)
evaluate h = cone-compose (cone-restrict-assoc (productMap h (id T)) mapEval s)
(cone-compose (cone-identification-restrict-One (productMap h (id T)) Curried.uncurry-law)
(uncurry-cone-restrict {f = f} {g = g} h value))
mapped-cone : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(T : CAT Γ) → Cone f g S → Cone (mapPost {C = T} f) (mapPost g) (Map T S)
mapped-cone = MappedCone.value
opaque
mapped-cone-identification : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(T : CAT Γ) {s t : Cone f g S} → ConeIdentification₁ s t → ConeIdentification₁ (mapped-cone T s) (mapped-cone T t)
mapped-cone-identification {S = S} {f = f} {g = g} T {s} {t} Φ = ReflectedCone.identification {f = f} {g = g}
(map-isAn T S) (mapped-cone T s) (mapped-cone T t)
(cone-compose (cone-inverse (MappedCone.Curried.uncurry-law T t))
(cone-compose (cone-identification-restrict-One mapEval Φ) (MappedCone.Curried.uncurry-law T s)))
opaque
mapped-cone-restrict : {C D E S R : CAT Γ} {f : MAP C E} {g : MAP D E}
(T : CAT Γ) (r : MAP R S) (s : Cone f g S) →
ConeIdentification₁ (cone-restrict (mapPost r) (mapped-cone T s)) (mapped-cone T (cone-restrict r s))
mapped-cone-restrict {R = R} {f = f} {g = g} T r s = ReflectedCone.identification {f = f} {g = g} (map-isAn T R)
(cone-restrict (mapPost r) (mapped-cone T s)) (mapped-cone T (cone-restrict r s))
(cone-compose (cone-inverse (MappedCone.Curried.uncurry-law T (cone-restrict r s)))
(cone-compose (cone-inverse (cone-restrict-assoc mapEval r s))
(cone-compose (cone-action-One s (mapPost-β r)) (MappedCone.evaluate T s (mapPost r)))))
```
## Preservation and all-category detection
The inverse factors the uncurried cone and curries that factor. Recognition
uses reflection only at the mapped vertex, where its anima hypothesis holds.
The factorization comparison then proves preservation and all-category
detection through post-tests-all.
```agda
module MappingPullback {C D E : CAT Γ} (T : CAT Γ) (f : MAP C E) (g : MAP D E) where
S : CAT Γ
S = Map T (Pullback f g)
F : MAP (Map T C) (Map T E)
F = mapPost {C = T} f
G : MAP (Map T D) (Map T E)
G = mapPost {C = T} g
R : CAT Γ
R = Pullback F G
original : Cone f g (Pullback f g)
original = pullback-cone f g
square : Cone F G S
square = mapped-cone T original
module FactorCone {X : CAT Γ} (xAn : isAn X) (s : Cone F G X) where
uncurried : Cone f g (X × T)
uncurried = uncurry-cone {f = f} {g = g} s
uncurried-factor : MAP (X × T) (Pullback f g)
uncurried-factor = pullback-factor uncurried
factor : MAP X S
factor = mapCurry xAn uncurried-factor
abstract
factor-law : ConeIdentification₁ (cone-restrict factor square) s
factor-law = ReflectedCone.identification {f = f} {g = g} xAn (cone-restrict factor square) s
(cone-compose (pullback-factor-β uncurried)
(cone-compose (cone-action-One original (mapCurry-β xAn uncurried-factor)) (MappedCone.evaluate T original factor)))
opaque
reflect : {X : CAT Γ} → isAn X → (h k : MAP X S) →
ConeIdentification₁ (cone-restrict h square) (cone-restrict k square) → h =₁ k
reflect xAn h k Φ = uncurry-reflect xAn h k (pullback-reflect {f = f} {g = g} (uncurry h) (uncurry k)
(cone-compose (MappedCone.evaluate T original k)
(cone-compose (uncurry-cone-identification {f = f} {g = g} Φ) (cone-inverse (MappedCone.evaluate T original h)))))
forward : MAP S R
forward = pullback-factor square
module Inverse = FactorCone (pullback-isAn F G (map-isAn T C) (map-isAn T D) (map-isAn T E)) (pullback-cone F G)
inverse : MAP R S
inverse = Inverse.factor
opaque
square-isPullback : IsPullback square
square-isPullback = isPullback-from-factor-and-reflection square inverse Inverse.factor-law
(reflect (map-isAn T (Pullback f g)))
mapped-cone-factorization : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(T : CAT Γ) (s : Cone f g S) →
(pullback-factor (mapped-cone T s)) =₁ (pullback-factor (mapped-cone T (pullback-cone f g)) ∘ mapPost (pullback-factor s))
mapped-cone-factorization {f = f} {g} T s = pullback-factor-restrict (mapPost (pullback-factor s)) (mapped-cone T (pullback-cone f g)) ∙
(pullback-factor-cong (cone-compose (mapped-cone-identification T (pullback-factor-β s))
(mapped-cone-restrict T (pullback-factor s) (pullback-cone f g)))) ⁻¹
map-preserves-pullback : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(T : CAT Γ) (s : Cone f g S) → IsPullback s → IsPullback (mapped-cone T s)
map-preserves-pullback {f = f} {g} T s es = equiv-transport ((mapped-cone-factorization T s) ⁻¹)
(equiv-compose (mapPost (pullback-factor s)) (pullback-factor (mapped-cone T (pullback-cone f g)))
(mapPost-isEquiv (pullback-factor s) es) (MappingPullback.square-isPullback T f g))
map-detects-pullback : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g S) → ((T : CAT Γ) → IsPullback (mapped-cone T s)) → IsPullback s
map-detects-pullback {f = f} {g} s tests = post-tests-all (pullback-factor s) (λ T →
equiv-cancel-left (mapPost (pullback-factor s)) (pullback-factor (mapped-cone T (pullback-cone f g)))
(MappingPullback.square-isPullback T f g)
(equiv-transport (mapped-cone-factorization T s) (tests T)))
```
## The terminal mapping test
A pullback after Map One supplies factorization, its full beta and reflection
for anima sources X. This retains the selected right-unit insertion and its
projection law, and asserts only this consequence of the single test.
```agda
module TerminalTest {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g S) (mapped-isPullback : IsPullback (mapped-cone One s)) where
module U = UniversalCone (mapped-cone One s) mapped-isPullback
module Factor {X : CAT Γ} (xAn : isAn X) (t : Cone f g X) where
module Curried = CurriedCone xAn (cone-restrict (pr₁ {C = X} {D = One}) t)
mapped-factor : MAP X (Map One S)
mapped-factor = U.factor Curried.value
factor : MAP X S
factor = uncurry mapped-factor ∘ product-unitʳ-inverse X
abstract
factor-law : ConeIdentification₁ (cone-restrict factor s) t
factor-law = cone-compose (cone-restrict-id t)
(cone-compose (cone-action-One t (pair-β₁ (id X) (terminate X)))
(cone-compose (cone-restrict-assoc (product-unitʳ-inverse X) pr₁ t)
(cone-compose (cone-identification-restrict-One (product-unitʳ-inverse X)
(cone-compose Curried.uncurry-law
(cone-compose (uncurry-cone-identification (U.β Curried.value))
(cone-inverse (MappedCone.evaluate One s mapped-factor)))))
(cone-inverse (cone-restrict-assoc (product-unitʳ-inverse X) (uncurry mapped-factor) s)))))
factor : {X : CAT Γ} → isAn X → Cone f g X → MAP X S
factor = Factor.factor
factor-β : {X : CAT Γ} (xAn : isAn X) (t : Cone f g X) →
ConeIdentification₁ (cone-restrict (factor xAn t) s) t
factor-β = Factor.factor-law
module Reflection {X : CAT Γ} (xAn : isAn X) (h k : MAP X S)
(Φ : ConeIdentification₁ (cone-restrict h s) (cone-restrict k s)) where
curried-h : MAP X (Map One S)
curried-h = mapCurry xAn (h ∘ pr₁ {C = X} {D = One})
curried-k : MAP X (Map One S)
curried-k = mapCurry xAn (k ∘ pr₁ {C = X} {D = One})
evaluate : (z : MAP X S) → ConeIdentification₁
(uncurry-cone (cone-restrict (mapCurry xAn (z ∘ pr₁ {C = X} {D = One})) (mapped-cone One s)))
(cone-restrict pr₁ (cone-restrict z s))
evaluate z = cone-compose (cone-inverse (cone-restrict-assoc pr₁ z s))
(cone-compose (cone-action-One s (mapCurry-β xAn (z ∘ pr₁)))
(MappedCone.evaluate One s (mapCurry xAn (z ∘ pr₁))))
curried-identification : curried-h =₁ curried-k
curried-identification = U.reflect curried-h curried-k (ReflectedCone.identification xAn _ _
(cone-compose (cone-inverse (evaluate k))
(cone-compose (cone-identification-restrict-One pr₁ Φ) (evaluate h))))
identification : h =₁ k
identification = Fact.factor (factor-through-preWhisker (pr₁ {C = X} {D = One})
(product-unitʳ-isEquiv X)
(mapCurry-β xAn (k ∘ pr₁) ∙
(uncurry⁼ curried-identification ∙ (mapCurry-β xAn (h ∘ pr₁)) ⁻¹)))
reflect : {X : CAT Γ} (xAn : isAn X) (h k : MAP X S) →
ConeIdentification₁ (cone-restrict h s) (cone-restrict k s) → h =₁ k
reflect = Reflection.identification
```