Other Agda modules in this section (5)
# Native evaluation and encoding of restriction cocones
Native Fun precomposition cones represent cocones on the actual product
restriction. Their independent identification families retain the complete
matching square. Chosen currying encodes a product cocone and computes its
whole image. Mapping encoding additionally requires its actual anima source
witness, for the concrete converse and terminal adapters.
A private span-retraction calculation chooses reverse cells by reflection
against the given corner retractions and derives their complete matching
comparison. The swap client uses the specified swap-swap identifications;
the terminal client uses the actual projection and insertion retractions.
Only the roundtrip over the original span is required. Terminal encoding
keeps the selected Points.name legs, and its decoded comparison is
explicitly normalized to the existing Points.decode-name betas.
```agda
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorMappingOutEvaluation 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 using (module Constructions)
open Constructions
open import SCT.VolumeI.Chapter01.Section02.Coherence using (id₌; inv₌; preWhisker-id₌; comp-unitˡ; comp-unitʳ; comp-assoc; module Composition; module Boundaries)
open Composition
open Boundaries using (SquareCell₌)
open import SCT.VolumeI.Chapter01.Section02.Specialization
open import SCT.VolumeI.Chapter01.Section02.IdentificationSquares
open import SCT.VolumeI.Chapter01.Section02.Whiskering using (preWhisker-comp; preWhisker-id; whisker-mixed)
open import SCT.VolumeI.Chapter01.Section02.Products using (module Calculus)
open Calculus
open import SCT.VolumeI.Chapter01.Section03.ProductConstructions using (productMap; swap; swap-swap; swap-isEquiv; product-unitˡ-inverse; product-unitˡ-pr₂-inverse; product-unitˡ-isEquiv)
open import SCT.VolumeI.Chapter01.Section03.Identifications.Inverses using (cancel-right; comp₌-inverseˡ-One; cancel-left; inverse-identity; comp₌-unitʳ-One; comp₌-unitˡ-One; inverse-composite; inverse-inverse; preWhisker-inverse; postWhisker-inverse)
open import SCT.VolumeI.Chapter01.Section03.Identifications.EndpointTransport
using (changeEndpoints; changeEndpoints-cong; transport-square; reflect-transported-square; restore-boundaries; changeEndpoints-iterated; square-to-changeEndpoints; postWhisker-changeEndpoints; changeEndpoints-extend-square)
import SCT.VolumeI.Chapter01.Section03.Factorizations as Fact
open import SCT.VolumeI.Chapter01.Section03.Squares using (Square; comp-square)
import SCT.VolumeI.Chapter01.Section03.Squares as Squares
open import SCT.VolumeI.Chapter01.Section03.Products.PairingRestriction using (pair-evaluation-over₁-One; pair-evaluation-over₂-One; pair-pre-over₁-One; pair-pre-over₂-One)
open import SCT.VolumeI.Chapter01.Section08.PushoutSquares using (mappingOut)
open import SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence using (factor-through-postWhisker; factor-through-postWhisker₂)
open import SCT.VolumeI.Chapter01.Section03.Identifications.Triangles using (post-triangle; restrict-triangle; lies-over-inverse; restrict-change-square-One; restrict-square-One; post-triangle-outer; post-square-cell; post-square-cell-id; post-square-cell-comp; post-square-cell-outer; lies-over-comp)
open import SCT.VolumeI.Chapter01.Section03.Identifications.TriangleCoherence using (post-triangle-change; post-restrict-triangle; post-triangle-comp)
open import SCT.VolumeI.Chapter01.Section03.Identifications.FunctorCoherence using (left-unitor-comp; postWhisker-id-One; triangle-whiskered; right-unitor-comp; whisker-mixed-One; postWhisker-comp-One)
open import SCT.VolumeI.Chapter01.Section03.Products.ProductRestriction using (product-restriction; restriction-compositor; parameter-separation-composition; product-square; module SeparationSecondInput)
open import SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor using (productMap-cong-triangle₁; productMap-cong; productMap-cong₂; productMap-cong-triangle₂)
open import SCT.VolumeI.Chapter01.Section03.Products.ProductFunctorCoherence using (productMap-separate; productMap-first-comp)
open import SCT.VolumeI.Chapter01.Section04.MappingAnimae using (Map; uncurry; mapCurry; mapCurry-β)
open import SCT.VolumeI.Chapter01.Section04.Currying using (module CurriedRepresentation; uncurry⁼; uncurry-reflect; uncurry-reflect-β)
open import SCT.VolumeI.Chapter01.Section04.Functoriality using (mapPre; mapPre-uncurry)
open import SCT.VolumeI.Chapter01.Section04.Points using (name; name-representation; decode; decode-name)
open import SCT.VolumeI.Chapter01.Section06.Cones
open import SCT.VolumeI.Chapter01.Section07.Evaluation
open import SCT.VolumeI.Chapter01.Section07.EvaluationRepresentation using (evaluate-restrict-inputs; evaluate-restrict-substitution)
open import SCT.VolumeI.Chapter01.Section07.FunctorCategories
open import SCT.VolumeI.Chapter01.Section07.Currying using (funCurry; funCurry-β; funUncurry; reflect; reflect-β; reflect-β-One; evaluation-reflection₂)
open import SCT.VolumeI.Chapter01.Section07.Functoriality using (funPre; funPre⁼; funPre⁼-evaluation; funPre-β; funPre-comp; funPre-uncurry; funPre-uncurry-inputs)
import SCT.VolumeI.Chapter01.Section07.PreEvaluationSubstitution as Pre
open import SCT.VolumeI.Chapter01.Section08.Cocones
open import SCT.VolumeI.Chapter01.Section08.MappingOutEvaluation using (module MappingOutEvaluation; module ParameterizedSquareEvaluation)
import SCT.VolumeI.Chapter01.Section03.Identifications.OverBase as OverBase
import SCT.VolumeI.Chapter01.Section03.Products.FirstFactorSubstitution as FirstFactor
open import SCT.VolumeI.Chapter01.Section03.Products.Pairing using (pair₌-extensionality)
open import SCT.VolumeI.Chapter01.Section07.EvaluationSubstitution using (evaluate-restrict-assoc)
private
module _ {Γ : Context} {X : CAT Γ} where
open Terms.Equalities X using (_＝_)
constant-endpoints : {A B : CAT Γ} {x x′ y y′ : MAP A B}
(p : x =₁ x′) (q : y =₁ y′) (α : x =₁ y)
→ changeEndpoints (const {P = X} p) (const q) (const α) =₁ const (changeEndpoints p q α)
constant-endpoints p q α = const-comp q (α ∙ p ⁻¹) ∙
comp₌-cong (id₌ (const q))
(const-comp α (p ⁻¹) ∙ comp₌-cong (id₌ (const α)) ((const-inv p) ⁻¹))
module _ {F K D T : CAT Γ} (e : MAP (F × K) D) where
evaluation-square : {f g f′ g′ : MAP T F}
{α : f ＝ g} {β : f′ ＝ g′} {p : f ＝ f′} {q : g ＝ g′}
→ SquareCell₌ α β p q
→ SquareCell₌ (evaluate⁼ e α) (evaluate⁼ e β) (evaluate⁼ e p) (evaluate⁼ e q)
evaluation-square {α = α} {β} {p} {q} square = evaluate⁼-composition e β p ∙
(evaluate⁼-cong e square ∙ (evaluate⁼-composition e q α) ⁻¹)
evaluation-fixed-square : {f g f′ g′ : MAP T F}
{α : f ＝ g} {β : f′ ＝ g′} {p : f =₁ f′} {q : g =₁ g′}
→ SquareCell₌ α β (const p) (const q)
→ SquareCell₌ (evaluate⁼ e α) (evaluate⁼ e β)
(const (evaluate-cong e p)) (const (evaluate-cong e q))
evaluation-fixed-square {p = p} {q} square = replace-sides₌
(evaluate⁼-constant e p) (evaluate⁼-constant e q) (evaluation-square square)
```
A represented matching square determines a native matching through the
specified endpoint frames. The image below removes those frames and uses
the actual evaluation action. Higher reflection retains its chosen factor
and image triangle. The reflected legs are supplied by each client.
```agda
private
module _ {Γ : Context} {X : CAT Γ} where
open Terms.Equalities X using (_＝_)
module _ {F K D T : CAT Γ} (e : MAP (F × K) D)
{f₀ g₀ f₁ g₁ : MAP T F}
(σ₀ : f₀ =₁ g₀) (σ₁ : f₁ =₁ g₁) (α : f₀ ＝ f₁) (β : g₀ ＝ g₁)
{a₀ b₀ a₁ b₁ : MAP (T × K) D}
(p₀ : evaluate e f₀ =₁ a₀) (q₀ : evaluate e g₀ =₁ b₀)
(p₁ : evaluate e f₁ =₁ a₁) (q₁ : evaluate e g₁ =₁ b₁)
{a : a₀ ＝ a₁} {b : b₀ ＝ b₁}
(L : SquareCell₌ (evaluate⁼ e α) a (const p₀) (const p₁))
(R : SquareCell₌ (evaluate⁼ e β) b (const q₀) (const q₁))
(Ψ : SquareCell₌ a b
(const (changeEndpoints p₀ q₀ (evaluate-cong e σ₀)))
(const (changeEndpoints p₁ q₁ (evaluate-cong e σ₁)))) where
framed-matching-image :
(evaluation-action e f₀ g₁ ∘ (const σ₁ ∙ α)) =₁
(evaluation-action e f₀ g₁ ∘ (β ∙ const σ₀))
framed-matching-image =
(evaluation-action-evaluate e (β ∙ const σ₀)) ⁻¹ ∙
((target-image ⁻¹ ∙ (native-square ∙ source-image)) ∙
evaluation-action-evaluate e (const σ₁ ∙ α))
where
transported : SquareCell₌ a b
(changeEndpoints (const p₀) (const q₀) (const (evaluate-cong e σ₀)))
(changeEndpoints (const p₁) (const q₁) (const (evaluate-cong e σ₁)))
transported = replace-sides₌
((constant-endpoints p₀ q₀ (evaluate-cong e σ₀)) ⁻¹)
((constant-endpoints p₁ q₁ (evaluate-cong e σ₁)) ⁻¹) Ψ
native-square : SquareCell₌ (evaluate⁼ e α) (evaluate⁼ e β)
(const (evaluate-cong e σ₀)) (const (evaluate-cong e σ₁))
native-square = reflect-transported-square
(const p₀) (const q₀) (const p₁) (const q₁)
(const (evaluate-cong e σ₀)) (const (evaluate-cong e σ₁))
(evaluate⁼ e α) (evaluate⁼ e β) a b L R transported
source-image : evaluate⁼ e (const σ₁ ∙ α) =₁
(const (evaluate-cong e σ₁) ∙ evaluate⁼ e α)
source-image = comp₌-cong (evaluate⁼-constant e σ₁) (id₌ (evaluate⁼ e α)) ∙
evaluate⁼-composition e (const σ₁) α
target-image : evaluate⁼ e (β ∙ const σ₀) =₁
(evaluate⁼ e β ∙ const (evaluate-cong e σ₀))
target-image = comp₌-cong (id₌ (evaluate⁼ e β)) (evaluate⁼-constant e σ₀) ∙
evaluate⁼-composition e β (const σ₀)
private
module _ {Γ : Context} {X : CAT Γ} where
open Terms.Equalities X using (_＝_)
constant-inverse-three : {A B : CAT Γ} {a b c d : MAP A B}
(p : c =₁ d) (q : b =₁ d) (r : a =₁ b)
→ ((const {P = X} p) ⁻¹ ∙ (const q ∙ const r)) =₁
const (p ⁻¹ ∙ (q ∙ r))
constant-inverse-three p q r = const-comp (p ⁻¹) (q ∙ r) ∙
comp₌-cong ((const-inv p) ⁻¹) (const-comp q r)
module ChangeSpan {Γ : Context} {A B C A′ B′ C′ E : CAT Γ}
(u : MAP A B) (l : MAP A C) (u′ : MAP A′ B′) (l′ : MAP A′ C′)
(pA : MAP A′ A) (pB : MAP B′ B) (pC : MAP C′ C)
(δu : (pB ∘ u′) =₁ (u ∘ pA)) (δl : (pC ∘ l′) =₁ (l ∘ pA)) where
module Route {T T′ : CAT Γ} (f : MAP A T) (f′ : MAP A′ T′)
(p : MAP T′ T) (δ : (p ∘ f′) =₁ (f ∘ pA)) where
ρ : (h : MAP T E) → ((h ∘ p) ∘ f′) =₁ ((h ∘ f) ∘ pA)
ρ h = (comp-assoc pA f h) ⁻¹ ∙ ((h ◁ δ) ∙ comp-assoc f′ p h)
module _ {X : CAT Γ} where
open Terms.Equalities X using (_＝_)
natural : {h k : MAP T E} (α : h ＝ k)
→ SquareCell₌ ((α ▷ p) ▷ f′) ((α ▷ f) ▷ pA)
(const (ρ h)) (const (ρ k))
natural {h} {k} α = replace-sides₌
(constant-inverse-three (comp-assoc pA f h) (h ◁ δ) (comp-assoc f′ p h))
(constant-inverse-three (comp-assoc pA f k) (k ◁ δ) (comp-assoc f′ p k))
(paste-square₌
(paste-square₌ (preWhisker-comp α p f′) ((interchange-fixedInner α δ) ⁻¹))
(inverse-square₌ (preWhisker-comp α f pA)))
module L = Route u u′ pB δu
using (natural; ρ)
module R = Route l l′ pC δl
using (natural; ρ)
value : Cocone u l E → Cocone u′ l′ E
value s = record
{ left = Cocone.left s ∘ pB
; right = Cocone.right s ∘ pC
; match = (R.ρ (Cocone.right s)) ⁻¹ ∙
((Cocone.match s ▷ pA) ∙ L.ρ (Cocone.left s)) }
module _ {X : CAT Γ} where
open Terms.Equalities X using (_＝_)
identification : {s t : Cocone u l E}
→ CoconeIdentification X s t → CoconeIdentification X (value s) (value t)
identification {s} {t} Φ = record
{ left = CoconeIdentification.left Φ ▷ pB
; right = CoconeIdentification.right Φ ▷ pC
; compatible = replace-sides₌
(constant-inverse-three (R.ρ (Cocone.right s))
(Cocone.match s ▷ pA) (L.ρ (Cocone.left s)))
(constant-inverse-three (R.ρ (Cocone.right t))
(Cocone.match t ▷ pA) (L.ρ (Cocone.left t)))
(paste-square₌
(paste-square₌ (L.natural (CoconeIdentification.left Φ))
(replace-sides₌ (pre-constant (Cocone.match s) pA)
(pre-constant (Cocone.match t) pA)
(pre-square₌ pA (CoconeIdentification.compatible Φ))))
(inverse-square₌ (R.natural (CoconeIdentification.right Φ)))) }
private
module _ {Γ : Context} {A B C A′ B′ C′ T E : CAT Γ}
(u : MAP A B) (l : MAP A C) (u′ : MAP A′ B′) (l′ : MAP A′ C′)
(pA : MAP A′ A) (pB : MAP B′ B) (pC : MAP C′ C)
(δu : (pB ∘ u′) =₁ (u ∘ pA)) (δl : (pC ∘ l′) =₁ (l ∘ pA))
(H : MAP T E) (s : Cocone u l T) where
private
module Before = ChangeSpan {E = T} u l u′ l′ pA pB pC δu δl
using (value; module L; module R)
module After = ChangeSpan {E = E} u l u′ l′ pA pB pC δu δl
using (value; module L; module R)
x = Cocone.left s
y = Cocone.right s
σ = Cocone.match s
ρx = Before.L.ρ x
ρy = Before.R.ρ y
hx = After.L.ρ (H ∘ x)
hy = After.R.ρ (H ∘ y)
nx = post-square-cell H pA (x ∘ u) (x ∘ pB) u′ ρx
ny = post-square-cell H pA (y ∘ l) (y ∘ pC) l′ ρy
ηx = comp-assoc u x H
ηy = comp-assoc l y H
ζx = comp-assoc pA (x ∘ u) H
ζy = comp-assoc pA (y ∘ l) H
ωx = comp-assoc u′ (x ∘ pB) H
ωy = comp-assoc l′ (y ∘ pC) H
λx = comp-assoc pB x H
λy = comp-assoc pC y H
q₀ = Cocone.match (cocone-postcompose H s) ▷ pA
q₁ = (H ◁ σ) ▷ pA
q₂ = H ◁ (σ ▷ pA)
endpoints-cong : {K Z : CAT Γ} {a b a′ b′ : MAP K Z}
{p p′ : a =₁ a′} {q q′ : b =₁ b′} {α α′ : a =₁ b}
→ p =₂ p′ → q =₂ q′ → α =₂ α′
→ changeEndpoints p q α =₂ changeEndpoints p′ q′ α′
endpoints-cong dp dq dα = comp₌-cong dq (comp₌-cong dα (inv₌ ◁ dp))
source-normal : changeEndpoints (hx ⁻¹) (hy ⁻¹) q₀
=₂ Cocone.match (After.value (cocone-postcompose H s))
source-normal = comp₌-cong (id₌ (hy ⁻¹))
(comp₌-cong (id₌ q₀) (inverse-inverse hx))
original-normal : changeEndpoints (ρx ⁻¹) (ρy ⁻¹) (σ ▷ pA)
=₂ Cocone.match (Before.value s)
original-normal = comp₌-cong (id₌ (ρy ⁻¹))
(comp₌-cong (id₌ (σ ▷ pA)) (inverse-inverse ρx))
mixed-normal : changeEndpoints ζx ζy q₁ =₂ q₂
mixed-normal = square-to-changeEndpoints ζx ζy q₁ q₂
(whisker-mixed-One σ pA H)
middle-normal : changeEndpoints ((H ◁ ρx) ⁻¹) ((H ◁ ρy) ⁻¹) q₂
=₂ H ◁ Cocone.match (Before.value s)
middle-normal = (postWhisker H ◁ original-normal) ∙
(endpoints-cong (postWhisker-inverse H ρx) (postWhisker-inverse H ρy)
(id₌ q₂) ∙ postWhisker-changeEndpoints H (ρx ⁻¹) (ρy ⁻¹) (σ ▷ pA)) ⁻¹
final-normal : changeEndpoints (ωx ⁻¹) (ωy ⁻¹)
(H ◁ Cocone.match (Before.value s))
=₂ Cocone.match (cocone-postcompose H (Before.value s))
final-normal = comp₌-cong (id₌ (ωy ⁻¹))
(comp₌-cong (id₌ (H ◁ Cocone.match (Before.value s))) (inverse-inverse ωx))
left-inverse : nx ⁻¹ =₂ ((ωx ⁻¹ ∙ (H ◁ ρx) ⁻¹) ∙ ζx)
left-inverse = (comp₌-cong (inverse-composite (H ◁ ρx) ωx) (inverse-inverse ζx) ∙
inverse-composite (ζx ⁻¹) ((H ◁ ρx) ∙ ωx))
right-inverse : ny ⁻¹ =₂ ((ωy ⁻¹ ∙ (H ◁ ρy) ⁻¹) ∙ ζy)
right-inverse = (comp₌-cong (inverse-composite (H ◁ ρy) ωy) (inverse-inverse ζy) ∙
inverse-composite (ζy ⁻¹) ((H ◁ ρy) ∙ ωy))
iterated-normal :
changeEndpoints (ωx ⁻¹) (ωy ⁻¹)
(changeEndpoints ((H ◁ ρx) ⁻¹) ((H ◁ ρy) ⁻¹)
(changeEndpoints ζx ζy q₁))
=₂ changeEndpoints (nx ⁻¹) (ny ⁻¹) q₁
iterated-normal = endpoints-cong (left-inverse ⁻¹) (right-inverse ⁻¹) (id₌ q₁) ∙
(changeEndpoints-iterated ζx ζy
(ωx ⁻¹ ∙ (H ◁ ρx) ⁻¹) (ωy ⁻¹ ∙ (H ◁ ρy) ⁻¹) q₁ ∙
changeEndpoints-iterated ((H ◁ ρx) ⁻¹) ((H ◁ ρy) ⁻¹)
(ωx ⁻¹) (ωy ⁻¹) (changeEndpoints ζx ζy q₁))
target-normal : changeEndpoints (nx ⁻¹) (ny ⁻¹) q₁
=₂ Cocone.match (cocone-postcompose H (Before.value s))
target-normal = final-normal ∙
(endpoints-cong (id₌ (ωx ⁻¹)) (id₌ (ωy ⁻¹)) middle-normal ∙
(endpoints-cong (id₌ (ωx ⁻¹)) (id₌ (ωy ⁻¹))
(endpoints-cong (id₌ ((H ◁ ρx) ⁻¹)) (id₌ ((H ◁ ρy) ⁻¹)) mixed-normal) ∙
iterated-normal ⁻¹))
raw-middle : SquareCell₌ ηx ηy (Cocone.match (cocone-postcompose H s)) (H ◁ σ)
raw-middle = (comp-inv-left ηy ((H ◁ σ) ∙ ηx)) ⁻¹
raw-square : SquareCell₌ (λx ▷ u′) (λy ▷ l′)
(changeEndpoints (hx ⁻¹) (hy ⁻¹) q₀)
(changeEndpoints (nx ⁻¹) (ny ⁻¹) q₁)
raw-square = transport-square (hx ⁻¹) (nx ⁻¹) (hy ⁻¹) (ny ⁻¹)
q₀ q₁ (ηx ▷ pA) (ηy ▷ pA) (λx ▷ u′) (λy ▷ l′)
(inverse-square₌ (post-square-cell-comp pA u pB u′ δu x H))
(inverse-square₌ (post-square-cell-comp pA l pC l′ δl y H))
(pre-square₌ pA raw-middle)
change-span-postcomposition : CoconeIdentification₁
(After.value (cocone-postcompose H s)) (cocone-postcompose H (Before.value s))
change-span-postcomposition = record
{ left = λx
; right = λy
; compatible = replace-sides₌ source-normal target-normal raw-square }
private
module _ {Γ : Context} {A B C T : CAT Γ} {u : MAP A B} {l : MAP A C}
(s : Cocone u l T) where
postcompose-unit : CoconeIdentification₁ (cocone-postcompose (id T) s) s
postcompose-unit = record
{ left = comp-unitˡ (Cocone.left s)
; right = comp-unitˡ (Cocone.right s)
; compatible = (post-square-cell-id l (Cocone.right s) (Cocone.left s)
u (Cocone.match s)) ⁻¹ }
postcompose-assoc : {E Z : CAT Γ} (g : MAP T E) (f : MAP E Z)
→ CoconeIdentification₁ (cocone-postcompose (f ∘ g) s)
(cocone-postcompose f (cocone-postcompose g s))
postcompose-assoc g f = record
{ left = comp-assoc (Cocone.left s) g f
; right = comp-assoc (Cocone.right s) g f
; compatible = post-square-cell-comp l (Cocone.right s) (Cocone.left s)
u (Cocone.match s) g f }
private
module _ {Γ : Context} {A B C T E : CAT Γ} {u : MAP A B} {l : MAP A C}
(H : MAP T E) {s t : Cocone u l T} (Φ : CoconeIdentification₁ s t) where
private
α = CoconeIdentification₁.left Φ
β = CoconeIdentification₁.right Φ
fs = (comp-assoc u (Cocone.left s) H) ⁻¹
ft = (comp-assoc u (Cocone.left t) H) ⁻¹
gs = (comp-assoc l (Cocone.right s) H) ⁻¹
gt = (comp-assoc l (Cocone.right t) H) ⁻¹
σs = H ◁ Cocone.match s
σt = H ◁ Cocone.match t
matching-normal : (z : Cocone u l T)
→ changeEndpoints ((comp-assoc u (Cocone.left z) H) ⁻¹)
((comp-assoc l (Cocone.right z) H) ⁻¹) (H ◁ Cocone.match z)
=₂ Cocone.match (cocone-postcompose H z)
matching-normal z = comp₌-cong (id₌ ((comp-assoc l (Cocone.right z) H) ⁻¹))
(comp₌-cong (id₌ (H ◁ Cocone.match z))
(inverse-inverse (comp-assoc u (Cocone.left z) H)))
fixed-postcomposition : CoconeIdentification₁
(cocone-postcompose H s) (cocone-postcompose H t)
fixed-postcomposition = record
{ left = H ◁ α
; right = H ◁ β
; compatible = replace-sides₌ (matching-normal s) (matching-normal t)
(transport-square fs ft gs gt σs σt
(H ◁ (α ▷ u)) (H ◁ (β ▷ l)) ((H ◁ α) ▷ u) ((H ◁ β) ▷ l)
(inverse-square₌ (whisker-mixed-One α u H))
(inverse-square₌ (whisker-mixed-One β l H))
(post-square₌ H (CoconeIdentification₁.compatible Φ))) }
private
module CoconePostcompositionRecovery {Γ : Context} {X A B C T E : CAT Γ}
{u : MAP A B} {l : MAP A C} (H : MAP T E) (hEquiv : IsEquiv H)
(s t : Cocone u l T)
(Φ : CoconeIdentification X (cocone-postcompose H s) (cocone-postcompose H t)) where
open Terms.Equalities X using (_＝_)
private
left-factor = factor-through-postWhisker H hEquiv (CoconeIdentification.left Φ)
right-factor = factor-through-postWhisker H hEquiv (CoconeIdentification.right Φ)
left : Cocone.left s ＝ Cocone.left t
left = Fact.factor left-factor
right : Cocone.right s ＝ Cocone.right t
right = Fact.factor right-factor
left-image : (H ◁ left) =₁ CoconeIdentification.left Φ
left-image = Fact.triangle left-factor
right-image : (H ◁ right) =₁ CoconeIdentification.right Φ
right-image = Fact.triangle right-factor
private
frame-left : (z : Cocone u l T)
→ (H ∘ (Cocone.left z ∘ u)) =₁ ((H ∘ Cocone.left z) ∘ u)
frame-left z = (comp-assoc u (Cocone.left z) H) ⁻¹
frame-right : (z : Cocone u l T)
→ (H ∘ (Cocone.right z ∘ l)) =₁ ((H ∘ Cocone.right z) ∘ l)
frame-right z = (comp-assoc l (Cocone.right z) H) ⁻¹
fs = const {P = X} (frame-left s)
gs = const {P = X} (frame-right s)
ft = const {P = X} (frame-left t)
gt = const {P = X} (frame-right t)
σs = H ◁ const {P = X} (Cocone.match s)
σt = H ◁ const {P = X} (Cocone.match t)
raw-left = H ◁ (left ▷ u)
raw-right = H ◁ (right ▷ l)
middle-left = (H ◁ left) ▷ u
middle-right = (H ◁ right) ▷ l
matching-frame : (z : Cocone u l T)
→ changeEndpoints (const {P = X} (frame-left z)) (const (frame-right z))
(H ◁ const (Cocone.match z)) =₁ const (Cocone.match (cocone-postcompose H z))
matching-frame z = const-cong
(comp₌-cong (id₌ (frame-right z))
(comp₌-cong (id₌ (H ◁ Cocone.match z))
(inverse-inverse (comp-assoc u (Cocone.left z) H)))) ∙
(constant-endpoints (frame-left z) (frame-right z) (H ◁ Cocone.match z) ∙
comp₌-cong (id₌ (const (frame-right z)))
(comp₌-cong (post-constant H (Cocone.match z))
(id₌ ((const (frame-left z)) ⁻¹))))
left-square : SquareCell₌ raw-left middle-left fs ft
left-square = replace-sides₌
((const-inv (comp-assoc u (Cocone.left s) H)) ⁻¹)
((const-inv (comp-assoc u (Cocone.left t) H)) ⁻¹)
(inverse-square₌ (whisker-mixed left u H))
right-square : SquareCell₌ raw-right middle-right gs gt
right-square = replace-sides₌
((const-inv (comp-assoc l (Cocone.right s) H)) ⁻¹)
((const-inv (comp-assoc l (Cocone.right t) H)) ⁻¹)
(inverse-square₌ (whisker-mixed right l H))
transported : SquareCell₌ middle-left middle-right
(changeEndpoints fs gs σs) (changeEndpoints ft gt σt)
transported = replace-sides₌ ((matching-frame s) ⁻¹) ((matching-frame t) ⁻¹)
(replace-edges₌ ((preWhisker u ◁ left-image) ⁻¹)
((preWhisker l ◁ right-image) ⁻¹) (CoconeIdentification.compatible Φ))
native-square : SquareCell₌ raw-left raw-right σs σt
native-square = reflect-transported-square fs gs ft gt σs σt
raw-left raw-right middle-left middle-right left-square right-square transported
source-boundary = const {P = X} (Cocone.match t) ∙ (left ▷ u)
target-boundary = (right ▷ l) ∙ const {P = X} (Cocone.match s)
private
source-image = postWhisker-comp₌ H (const (Cocone.match t)) (left ▷ u)
target-image = postWhisker-comp₌ H (right ▷ l) (const (Cocone.match s))
wanted-image : (H ◁ source-boundary) =₁ (H ◁ target-boundary)
wanted-image = target-image ⁻¹ ∙ (native-square ∙ source-image)
matching-factor = factor-through-postWhisker₂ H hEquiv source-boundary target-boundary wanted-image
compatible : SquareCell₌ (left ▷ u) (right ▷ l)
(const (Cocone.match s)) (const (Cocone.match t))
compatible = Fact.factor matching-factor
matching-image : ((postWhisker (postWhisker H)) ∘ compatible) =₁ wanted-image
matching-image = Fact.triangle matching-factor
value : CoconeIdentification X s t
value = record { left = left; right = right; compatible = compatible }
private
module RecoveredSpanCell {Γ : Context} {A A′ B B′ : CAT Γ}
(J : MAP A B) (H : MAP A′ B′)
(pA : MAP A′ A) (pB : MAP B′ B) (qA : MAP A A′) (qB : MAP B B′)
(εA : (pA ∘ qA) =₁ id A) (εB : (pB ∘ qB) =₁ id B)
(pBEquiv : IsEquiv pB) (transpose-cell : (pB ∘ H) =₁ (J ∘ pA)) where
reverse-image : (pB ∘ (qB ∘ J)) =₁ (pB ∘ (H ∘ qA))
reverse-image = comp-assoc qA H pB ∙
((transpose-cell ⁻¹ ▷ qA) ∙
((comp-assoc qA pA J) ⁻¹ ∙
((J ◁ εA ⁻¹) ∙
((comp-unitʳ J) ⁻¹ ∙
(comp-unitˡ J ∙ ((εB ▷ J) ∙ (comp-assoc J qB pB) ⁻¹))))))
reverse-factor : Fact.Factorization (postWhisker pB) reverse-image
reverse-factor = factor-through-postWhisker pB pBEquiv reverse-image
reverse-cell : (qB ∘ J) =₁ (H ∘ qA)
reverse-cell = Fact.factor reverse-factor
reverse-cell-image : (pB ◁ reverse-cell) =₂ reverse-image
reverse-cell-image = Fact.triangle reverse-factor
private
module _ {C D : CAT Γ} {w x y z : MAP C D} where
strip-left : (p : y =₁ z) (t : x =₁ y) (r : w =₁ x)
→ (p ⁻¹ ∙ ((p ∙ t) ∙ r)) =₂ (t ∙ r)
strip-left p t r = comp₌-cong (inv-comp-left p t) (id₌ r) ∙
(comp₌-assoc (p ⁻¹) (p ∙ t) r) ⁻¹
strip-inverse : (p : y =₁ z) (t : x =₁ z) (r : w =₁ x)
→ (p ∙ ((p ⁻¹ ∙ t) ∙ r)) =₂ (t ∙ r)
strip-inverse p t r = comp₌-cong (comp-inv-left p t) (id₌ r) ∙
(comp₌-assoc p (p ⁻¹ ∙ t) r) ⁻¹
source-assoc = comp-assoc J qB pB
target-assoc = comp-assoc qA H pB
middle = transpose-cell ▷ qA
corner-assoc = comp-assoc qA pA J
unit = J ◁ εA
right-unit = comp-unitʳ J
left-unit = comp-unitˡ J
source-unit = εB ▷ J
desired = left-unit ∙ source-unit
tail₄ = desired ∙ source-assoc ⁻¹
tail₃ = right-unit ⁻¹ ∙ tail₄
tail₂ = unit ⁻¹ ∙ tail₃
tail₁ = corner-assoc ⁻¹ ∙ tail₂
tail₀ = middle ⁻¹ ∙ tail₁
normalized = target-assoc ∙ tail₀
normalized-image : (pB ◁ reverse-cell) =₂ normalized
normalized-image = comp₌-cong (id₌ target-assoc)
(comp₌-cong (preWhisker-inverse transpose-cell qA)
(comp₌-cong (id₌ (corner-assoc ⁻¹))
(comp₌-cong (postWhisker-inverse J εA)
(comp₌-cong (id₌ (right-unit ⁻¹))
((comp₌-assoc left-unit source-unit (source-assoc ⁻¹)) ⁻¹))))) ∙
reverse-cell-image
Ω : ((pB ∘ qB) ∘ J) =₁ (J ∘ (pA ∘ qA))
Ω = corner-assoc ∙
(middle ∙ (target-assoc ⁻¹ ∙ ((pB ◁ reverse-cell) ∙ source-assoc)))
composed-cell-compatible :
(comp-unitʳ J ∙ ((J ◁ εA) ∙ Ω)) =₂ (comp-unitˡ J ∙ (εB ▷ J))
composed-cell-compatible =
inv-comp-right desired source-assoc ∙
(strip-inverse right-unit tail₄ source-assoc ∙
(comp₌-cong (id₌ right-unit) (strip-inverse unit tail₃ source-assoc) ∙
(comp₌-cong (id₌ right-unit)
(comp₌-cong (id₌ unit) (strip-inverse corner-assoc tail₂ source-assoc)) ∙
(comp₌-cong (id₌ right-unit)
(comp₌-cong (id₌ unit)
(comp₌-cong (id₌ corner-assoc) (strip-inverse middle tail₁ source-assoc))) ∙
(comp₌-cong (id₌ right-unit)
(comp₌-cong (id₌ unit)
(comp₌-cong (id₌ corner-assoc)
(comp₌-cong (id₌ middle) (strip-left target-assoc tail₀ source-assoc)))) ∙
comp₌-cong (id₌ right-unit)
(comp₌-cong (id₌ unit)
(comp₌-cong (id₌ corner-assoc)
(comp₌-cong (id₌ middle)
(comp₌-cong (id₌ (target-assoc ⁻¹))
(comp₌-cong normalized-image (id₌ source-assoc)))))))))))
private
restored-source = desired ∙ source-assoc ⁻¹
restored-target = right-unit ∙ (unit ∙ corner-assoc)
restricted = middle ∙ target-assoc ⁻¹
image = pB ◁ reverse-cell
joined = restored-target ∙ (restricted ∙ image)
nested = middle ∙ (target-assoc ⁻¹ ∙ (image ∙ source-assoc))
expand-boundary : (joined ∙ source-assoc) =₂ (right-unit ∙ (unit ∙ Ω))
expand-boundary = comp₌-cong (id₌ right-unit)
(comp₌-assoc unit corner-assoc nested) ∙
(comp₌-assoc right-unit (unit ∙ corner-assoc) nested ∙
(comp₌-cong (id₌ restored-target)
(comp₌-assoc middle (target-assoc ⁻¹) (image ∙ source-assoc)) ∙
(comp₌-cong (id₌ restored-target)
(comp₌-assoc restricted image source-assoc) ∙
comp₌-assoc restored-target (restricted ∙ image) source-assoc)))
joined-image : joined =₂ restored-source
joined-image = comp₌-cong (composed-cell-compatible ∙ expand-boundary)
(id₌ (source-assoc ⁻¹)) ∙ (comp-inv-right joined source-assoc) ⁻¹
split-image : ((restored-target ∙ restricted) ∙ image) =₂ restored-source
split-image = joined-image ∙ comp₌-assoc restored-target restricted image
recovered-span-square : SquareCell₌ (pB ◁ reverse-cell ⁻¹) restored-target
(restrict-triangle pB H transpose-cell qA) restored-source
recovered-span-square = comp-inv-right (restored-target ∙ restricted) image ∙
(comp₌-cong (split-image ⁻¹) (id₌ (image ⁻¹)) ∙
comp₌-cong (id₌ restored-source) (postWhisker-inverse pB reverse-cell))
post-recovered-span : {E : CAT Γ} (h : MAP B E)
→ (post-triangle h pB (qB ∘ J) restored-source ∙
(((h ∘ pB) ◁ reverse-cell ⁻¹) ∙ comp-assoc qA H (h ∘ pB))) =₂
((h ◁ restored-target) ∙
(comp-assoc qA (J ∘ pA) h ∙ (post-triangle h pB H transpose-cell ▷ qA)))
post-recovered-span h = post-triangle-change h pB H qA (qB ∘ J)
(reverse-cell ⁻¹) transpose-cell restored-source restored-target recovered-span-square
corner-β : {E : CAT Γ} (h : MAP B E) → ((h ∘ pB) ∘ qB) =₁ h
corner-β h = comp-unitʳ h ∙ post-triangle h pB qB εB
corner-β-restrict : {E : CAT Γ} (h : MAP B E)
→ (post-triangle h pB (qB ∘ J) restored-source ∙ comp-assoc J qB (h ∘ pB)) =₂
(corner-β h ▷ J)
corner-β-restrict h = (preWhisker-comp₌ (comp-unitʳ h) (post-triangle h pB qB εB) J) ⁻¹ ∙
(comp₌-cong ((triangle-whiskered J h) ⁻¹) (id₌ (post-triangle h pB qB εB ▷ J)) ∙
((comp₌-assoc (h ◁ left-unit) (comp-assoc J (id B) h)
(post-triangle h pB qB εB ▷ J)) ⁻¹ ∙
(post-restrict-triangle h pB qB J εB left-unit ∙
(comp₌-cong
(postWhisker h ◁ comp₌-assoc left-unit source-unit (source-assoc ⁻¹))
(id₌ (comp-assoc (qB ∘ J) pB h ∙ comp-assoc J qB (h ∘ pB))) ∙
comp₌-assoc (h ◁ restored-source) (comp-assoc (qB ∘ J) pB h)
(comp-assoc J qB (h ∘ pB))))))
source-corner-β : {E : CAT Γ} (h : MAP B E)
→ (((h ∘ J) ∘ pA) ∘ qA) =₁ (h ∘ J)
source-corner-β h = comp-unitʳ (h ∘ J) ∙ post-triangle (h ∘ J) pA qA εA
forward-frame : {E : CAT Γ} (h : MAP B E)
→ ((h ∘ pB) ∘ H) =₁ ((h ∘ J) ∘ pA)
forward-frame h = (comp-assoc pA J h) ⁻¹ ∙ post-triangle h pB H transpose-cell
reverse-frame : {E : CAT Γ} (h : MAP B E)
→ (((h ∘ pB) ∘ qB) ∘ J) =₁ (((h ∘ pB) ∘ H) ∘ qA)
reverse-frame h = (comp-assoc qA H (h ∘ pB)) ⁻¹ ∙
post-triangle (h ∘ pB) qB J reverse-cell
private
module FrameCalculation {E : CAT Γ} (h : MAP B E) where
L = h ◁ restored-target
B₀ = comp-assoc qA (J ∘ pA) h
A₀ = comp-assoc pA J h ▷ qA
t = post-triangle h pB H transpose-cell ▷ qA
Q = comp-assoc qA H (h ∘ pB)
S = comp-assoc J qB (h ∘ pB)
M = (h ∘ pB) ◁ reverse-cell
tail = ((h ∘ pB) ◁ reverse-cell ⁻¹) ∙ Q
known = post-triangle h pB (qB ∘ J) restored-source
source-corner-post : source-corner-β h =₂ (L ∙ (B₀ ∙ A₀))
source-corner-post = comp₌-cong
((postWhisker-comp₌ h right-unit (post-triangle J pA qA εA)) ⁻¹)
(id₌ (B₀ ∙ A₀)) ∙
((comp₌-assoc (h ◁ right-unit) (h ◁ post-triangle J pA qA εA) (B₀ ∙ A₀)) ⁻¹ ∙
(comp₌-cong (id₌ (h ◁ right-unit)) (post-triangle-comp h J pA qA εA) ∙
(comp₌-assoc (h ◁ right-unit) (comp-assoc (id A) J h)
(post-triangle (h ∘ J) pA qA εA) ∙
comp₌-cong (right-unitor-comp J h) (id₌ (post-triangle (h ∘ J) pA qA εA)))))
forward-normal : (forward-frame h ▷ qA) =₂ (A₀ ⁻¹ ∙ t)
forward-normal = comp₌-cong (preWhisker-inverse (comp-assoc pA J h) qA) (id₌ t) ∙
preWhisker-comp₌ ((comp-assoc pA J h) ⁻¹) (post-triangle h pB H transpose-cell) qA
source-forward-normal : (source-corner-β h ∙ (forward-frame h ▷ qA)) =₂ (L ∙ (B₀ ∙ t))
source-forward-normal = comp₌-cong (id₌ L)
(comp₌-cong (id₌ B₀) (comp-inv-left A₀ t)) ∙
(comp₌-cong (id₌ L) (comp₌-assoc B₀ A₀ (A₀ ⁻¹ ∙ t)) ∙
(comp₌-assoc L (B₀ ∙ A₀) (A₀ ⁻¹ ∙ t) ∙
comp₌-cong source-corner-post forward-normal))
reverse-inverse : (reverse-frame h) ⁻¹ =₂ (S ⁻¹ ∙ tail)
reverse-inverse = comp₌-cong (id₌ (S ⁻¹))
(comp₌-cong ((postWhisker-inverse (h ∘ pB) reverse-cell) ⁻¹) (id₌ Q)) ∙
(comp₌-assoc (S ⁻¹) (M ⁻¹) Q ∙
(comp₌-cong (inverse-composite M S) (inverse-inverse Q) ∙
inverse-composite (Q ⁻¹) (M ∙ S)))
left-normal : ((corner-β h ▷ J) ∙ (reverse-frame h) ⁻¹) =₂ (known ∙ tail)
left-normal = comp₌-cong (id₌ known) (comp-inv-left S tail) ∙
(comp₌-assoc known S (S ⁻¹ ∙ tail) ∙
comp₌-cong ((corner-β-restrict h) ⁻¹) reverse-inverse)
post-comparison : ((corner-β h ▷ J) ∙ (reverse-frame h) ⁻¹) =₂
(source-corner-β h ∙ (forward-frame h ▷ qA))
post-comparison = source-forward-normal ⁻¹ ∙ (post-recovered-span h ∙ left-normal)
combined-frame : {E : CAT Γ} (h : MAP B E)
→ (source-corner-β h ∙ ((forward-frame h ▷ qA) ∙ reverse-frame h)) =₂ (corner-β h ▷ J)
combined-frame h = inv-comp-right (corner-β h ▷ J) (reverse-frame h) ∙
(comp₌-cong ((FrameCalculation.post-comparison h) ⁻¹) (id₌ (reverse-frame h)) ∙
(comp₌-assoc (source-corner-β h) (forward-frame h ▷ qA) (reverse-frame h)) ⁻¹)
private
module CornerRestriction {Γ : Context} {A A′ E : CAT Γ}
(p : MAP A′ A) (q : MAP A A′) (ε : (p ∘ q) =₁ id A) where
β : (h : MAP A E) → ((h ∘ p) ∘ q) =₁ h
β h = comp-unitʳ h ∙ ((h ◁ ε) ∙ comp-assoc q p h)
module _ {X : CAT Γ} where
open Terms.Equalities X using (_＝_)
private
constant-three : {C D : CAT Γ} {w x y z : MAP C D}
(c : y =₁ z) (b : x =₁ y) (a : w =₁ x)
→ (const {P = X} c ∙ (const b ∙ const a)) =₁ const (c ∙ (b ∙ a))
constant-three c b a = const-comp c (b ∙ a) ∙
comp₌-cong (id₌ (const c)) (const-comp b a)
natural : {h k : MAP A E} (α : h ＝ k)
→ SquareCell₌ ((α ▷ p) ▷ q) α (const (β h)) (const (β k))
natural {h} {k} α = replace-sides₌
(constant-three (comp-unitʳ h) (h ◁ ε) (comp-assoc q p h))
(constant-three (comp-unitʳ k) (k ◁ ε) (comp-assoc q p k))
(paste-square₌
(paste-square₌ (preWhisker-comp α p q) ((interchange-fixedInner α ε) ⁻¹))
(preWhisker-id α))
module CoconeSpanRetraction {Γ : Context} {A A′ B B′ C C′ E : CAT Γ}
(u : MAP A B) (l : MAP A C) (u′ : MAP A′ B′) (l′ : MAP A′ C′)
(pA : MAP A′ A) (pB : MAP B′ B) (pC : MAP C′ C)
(qA : MAP A A′) (qB : MAP B B′) (qC : MAP C C′)
(εA : (pA ∘ qA) =₁ id A) (εB : (pB ∘ qB) =₁ id B) (εC : (pC ∘ qC) =₁ id C)
(pBEquiv : IsEquiv pB) (pCEquiv : IsEquiv pC)
(δu : (pB ∘ u′) =₁ (u ∘ pA)) (δl : (pC ∘ l′) =₁ (l ∘ pA)) where
private
module U = RecoveredSpanCell u u′ pA pB qA qB εA εB pBEquiv δu
using (combined-frame; corner-β; forward-frame; reverse-cell; reverse-frame; source-corner-β)
module L = RecoveredSpanCell l l′ pA pC qA qC εA εC pCEquiv δl
using (combined-frame; corner-β; forward-frame; reverse-cell; reverse-frame; source-corner-β)
module Forward = ChangeSpan {E = E} u l u′ l′ pA pB pC δu δl
using (identification; value)
module Back = ChangeSpan {E = E} u′ l′ u l qA qB qC U.reverse-cell L.reverse-cell
using (identification; value)
module Corner = CornerRestriction {E = E} pA qA εA
using (natural)
forward : Cocone u l E → Cocone u′ l′ E
forward = Forward.value
back : Cocone u′ l′ E → Cocone u l E
back = Back.value
back-postcomposition : {Z : CAT Γ} (H : MAP E Z) (s : Cocone u′ l′ E)
→ CoconeIdentification₁
(ChangeSpan.value {E = Z} u′ l′ u l qA qB qC U.reverse-cell L.reverse-cell
(cocone-postcompose H s))
(cocone-postcompose H (back s))
back-postcomposition H s = change-span-postcomposition
u′ l′ u l qA qB qC U.reverse-cell L.reverse-cell H s
forward-identification : {X : CAT Γ} {s t : Cocone u l E}
→ CoconeIdentification X s t → CoconeIdentification X (forward s) (forward t)
forward-identification = Forward.identification
back-identification : {X : CAT Γ} {s t : Cocone u′ l′ E}
→ CoconeIdentification X s t → CoconeIdentification X (back s) (back t)
back-identification = Back.identification
twice : Cocone u l E → Cocone u l E
twice s = back (forward s)
module Calculation (s : Cocone u l E) where
private
h = Cocone.left s
k = Cocone.right s
σ = Cocone.match s
lT = U.forward-frame h
rT = L.forward-frame k
lB = U.reverse-frame h
rB = L.reverse-frame k
lT′ = lT ▷ qA
rT′ = rT ▷ qA
raw = (σ ▷ pA) ▷ qA
combined-left = lT′ ∙ lB
combined-right = rT′ ∙ rB
left-source = U.source-corner-β h
right-source = L.source-corner-β k
left-target = U.corner-β h ▷ u
right-target = L.corner-β k ▷ l
tail = raw ∙ combined-left
match-whisker : (Cocone.match (Forward.value s) ▷ qA) =₂
(rT′ ⁻¹ ∙ (raw ∙ lT′))
match-whisker = comp₌-cong (preWhisker-inverse rT qA)
(preWhisker-comp₌ (σ ▷ pA) lT qA) ∙
preWhisker-comp₌ (rT ⁻¹) ((σ ▷ pA) ∙ lT) qA
matching-normal : Cocone.match (twice s) =₂ (combined-right ⁻¹ ∙ tail)
matching-normal = comp₌-cong ((inverse-composite rT′ rB) ⁻¹) (id₌ tail) ∙
((comp₌-assoc (rB ⁻¹) (rT′ ⁻¹) tail) ⁻¹ ∙
(comp₌-cong (id₌ (rB ⁻¹))
(comp₌-cong (id₌ (rT′ ⁻¹)) (comp₌-assoc raw lT′ lB)) ∙
(comp₌-cong (id₌ (rB ⁻¹)) (comp₌-assoc (rT′ ⁻¹) (raw ∙ lT′) lB) ∙
comp₌-cong (id₌ (rB ⁻¹)) (comp₌-cong match-whisker (id₌ lB)))))
corner-square : SquareCell₌ raw σ left-source right-source
corner-square = unconst-sides₌ (Corner.natural {X = One} σ)
left-normal : (σ ∙ left-target) =₂ (right-source ∙ tail)
left-normal = comp₌-assoc right-source raw combined-left ∙
(comp₌-cong (corner-square ⁻¹) (id₌ combined-left) ∙
((comp₌-assoc σ left-source combined-left) ⁻¹ ∙
comp₌-cong (id₌ σ) ((U.combined-frame h) ⁻¹)))
right-normal : (right-target ∙ Cocone.match (twice s)) =₂ (right-source ∙ tail)
right-normal = comp₌-cong (id₌ right-source) (comp-inv-left combined-right tail) ∙
(comp₌-assoc right-source combined-right (combined-right ⁻¹ ∙ tail) ∙
comp₌-cong ((L.combined-frame k) ⁻¹) matching-normal)
comparison : CoconeIdentification₁ (twice s) s
comparison = record
{ left = U.corner-β h
; right = L.corner-β k
; compatible = right-normal ⁻¹ ∙ left-normal }
private
module SwapRestriction {Γ : Context} {P A B : CAT Γ} (f : MAP A B) where
J : MAP (P × A) (P × B)
J = product-restriction f
H : MAP (A × P) (B × P)
H = productMap f (id P)
pA : MAP (A × P) (P × A)
pA = swap
pB : MAP (B × P) (P × B)
pB = swap
qA : MAP (P × A) (A × P)
qA = swap
qB : MAP (P × B) (B × P)
qB = swap
εA : (pA ∘ qA) =₁ id (P × A)
εA = swap-swap P A
εB : (pB ∘ qB) =₁ id (P × B)
εB = swap-swap P B
left₁ : (pr₂ ∘ H) =₁ (id P ∘ pr₂)
left₁ = pair-β₂ (f ∘ pr₁) (id P ∘ pr₂)
left₂ : (pr₁ ∘ H) =₁ (f ∘ pr₁)
left₂ = pair-β₁ (f ∘ pr₁) (id P ∘ pr₂)
right₁ : ((id P ∘ pr₁) ∘ pA) =₁ (id P ∘ pr₂)
right₁ = (id P ◁ pair-β₁ pr₂ pr₁) ∙ comp-assoc pA pr₁ (id P)
right₂ : ((f ∘ pr₂) ∘ pA) =₁ (f ∘ pr₁)
right₂ = (f ◁ pair-β₂ pr₂ pr₁) ∙ comp-assoc pA pr₂ f
transpose-cell : (pB ∘ H) =₁ (J ∘ pA)
transpose-cell = (pair-pre (id P ∘ pr₁) (f ∘ pr₂) pA) ⁻¹ ∙
(pair⁼ (right₁ ⁻¹ ∙ left₁) (right₂ ⁻¹ ∙ left₂) ∙ pair-pre pr₂ pr₁ H)
private
module TerminalRestriction {Γ : Context} {A B : CAT Γ} (f : MAP A B) where
J : MAP A B
J = f
H : MAP (One × A) (One × B)
H = product-restriction f
pA : MAP (One × A) A
pA = pr₂
pB : MAP (One × B) B
pB = pr₂
qA : MAP A (One × A)
qA = product-unitˡ-inverse A
qB : MAP B (One × B)
qB = product-unitˡ-inverse B
εA : (pA ∘ qA) =₁ id A
εA = product-unitˡ-pr₂-inverse A
εB : (pB ∘ qB) =₁ id B
εB = product-unitˡ-pr₂-inverse B
transpose-cell : (pB ∘ H) =₁ (J ∘ pA)
transpose-cell = pair-β₂ (id One ∘ pr₁) (f ∘ pr₂)
private
module SwapCoconeRoundtrip {Γ : Context} {P A B C E : CAT Γ} (u : MAP A B) (l : MAP A C) =
CoconeSpanRetraction {E = E}
(SwapRestriction.J {P = P} u) (SwapRestriction.J {P = P} l)
(SwapRestriction.H {P = P} u) (SwapRestriction.H {P = P} l)
(SwapRestriction.pA {P = P} u) (SwapRestriction.pB {P = P} u) (SwapRestriction.pB {P = P} l)
(SwapRestriction.qA {P = P} u) (SwapRestriction.qB {P = P} u) (SwapRestriction.qB {P = P} l)
(SwapRestriction.εA {P = P} u) (SwapRestriction.εB {P = P} u) (SwapRestriction.εB {P = P} l)
(swap-isEquiv B P) (swap-isEquiv C P)
(SwapRestriction.transpose-cell {P = P} u) (SwapRestriction.transpose-cell {P = P} l)
module TerminalCoconeRoundtrip {Γ : Context} {A B C E : CAT Γ} (u : MAP A B) (l : MAP A C) =
CoconeSpanRetraction {E = E}
(TerminalRestriction.J u) (TerminalRestriction.J l)
(TerminalRestriction.H u) (TerminalRestriction.H l)
(TerminalRestriction.pA u) (TerminalRestriction.pB u) (TerminalRestriction.pB l)
(TerminalRestriction.qA u) (TerminalRestriction.qB u) (TerminalRestriction.qB l)
(TerminalRestriction.εA u) (TerminalRestriction.εB u) (TerminalRestriction.εB l)
(product-unitˡ-isEquiv B) (product-unitˡ-isEquiv C)
(TerminalRestriction.transpose-cell u) (TerminalRestriction.transpose-cell l)
private
module ProjectionCompositor {Γ : Context} {P A B C : CAT Γ}
(f : MAP A B) (g : MAP B C) where
private
Jf = product-restriction {P = P} f
Jg = product-restriction {P = P} g
product-compositor = restriction-compositor {P = P} f g
βf = pair-β₂ (id P ∘ pr₁) (f ∘ pr₂)
βg = pair-β₂ (id P ∘ pr₁) (g ∘ pr₂)
βgf = pair-β₂ (id P ∘ pr₁) ((g ∘ f) ∘ pr₂)
coordinate = post-square-cell g pr₂ f pr₂ Jf βf
first-coordinate = post-square-cell (id P) pr₁ (id P) pr₁ Jf
(pair-β₁ (id P ∘ pr₁) (f ∘ pr₂))
first = pair-evaluation-over₂-One (id P ∘ pr₁) (g ∘ pr₂) Jf
first-coordinate coordinate
second = unconst-sides₌
(productMap-cong-triangle₂ (comp-unitˡ (id P)) (id₌ (g ∘ f)))
bottom-normal : ((id₌ (g ∘ f) ▷ pr₂) ∙ coordinate) =₂ coordinate
bottom-normal = comp₌-unitˡ-One coordinate ∙
comp₌-cong (preWhisker-id₌ (g ∘ f) pr₂) (id₌ coordinate)
square : SquareCell₌ (pr₂ ◁ product-compositor) coordinate
(restrict-triangle pr₂ Jg βg Jf) βgf
square = replace-edges₌ (id₌ (pr₂ ◁ product-compositor)) bottom-normal
(lies-over-comp pr₂ first second)
private
module ProjectionSquare {Γ : Context} {P A B C D : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) where
private
u = Square.source-map s
v = Square.target-map s
σ = Square.cell s
Ju = product-restriction {P = P} u
Jl = product-restriction {P = P} l
Jr = product-restriction {P = P} r
Jv = product-restriction {P = P} v
pA = pr₂ {C = P} {D = A}
pB = pr₂ {C = P} {D = B}
pC = pr₂ {C = P} {D = C}
pD = pr₂ {C = P} {D = D}
βu = pair-β₂ (id P ∘ pr₁) (u ∘ pr₂)
βl = pair-β₂ (id P ∘ pr₁) (l ∘ pr₂)
βr = pair-β₂ (id P ∘ pr₁) (r ∘ pr₂)
βv = pair-β₂ (id P ∘ pr₁) (v ∘ pr₂)
module Forward = ChangeSpan {E = D} u l Ju Jl pA pB pC βu βl
using (value)
module Left = ProjectionCompositor {P = P} u r
using (square)
module Right = ProjectionCompositor {P = P} l v
using (square)
Al = comp-assoc Ju Jr pD
Ar = comp-assoc Jl Jv pD
L = pD ◁ restriction-compositor {P = P} u r
R = pD ◁ restriction-compositor {P = P} l v
M = pD ◁ productMap-cong (id₌ (id P)) σ
coordinate-left = post-square-cell r pA u pB Ju βu
coordinate-right = post-square-cell v pA l pC Jl βl
raw = pD ◁ Square.cell (product-square {P = P} s)
expanded = R ⁻¹ ∙ (M ∙ L)
target-match = coordinate-right ⁻¹ ∙ ((σ ▷ pA) ∙ coordinate-left)
middle : SquareCell₌ M (σ ▷ pA)
(pair-β₂ (id P ∘ pr₁) ((r ∘ u) ∘ pr₂))
(pair-β₂ (id P ∘ pr₁) ((v ∘ l) ∘ pr₂))
middle = unconst-sides₌ (productMap-cong-triangle₂ (id₌ (id P)) σ)
raw-normal : raw =₂ expanded
raw-normal = comp₌-cong (postWhisker-inverse pD (restriction-compositor l v))
(postWhisker-comp₌ pD (productMap-cong (id₌ (id P)) σ) (restriction-compositor u r)) ∙
postWhisker-comp₌ pD ((restriction-compositor l v) ⁻¹)
(productMap-cong (id₌ (id P)) σ ∙ restriction-compositor u r)
raw-square : SquareCell₌ raw target-match
((βr ▷ Ju) ∙ Al ⁻¹) ((βv ▷ Jl) ∙ Ar ⁻¹)
raw-square = replace-edges₌ (raw-normal ⁻¹) (id₌ target-match)
(inv-comp-square₌ (adjoin-square₌ Left.square middle) Right.square)
source-normal : changeEndpoints (Al ⁻¹) (Ar ⁻¹) raw =₂
(Ar ⁻¹ ∙ (raw ∙ Al))
source-normal = comp₌-cong (id₌ (Ar ⁻¹))
(comp₌-cong (id₌ raw) (inverse-inverse Al))
source : Cocone Ju Jl D
source = cocone-postcompose pD (square-cocone (product-square {P = P} s))
target : Cocone Ju Jl D
target = Forward.value (square-cocone s)
matching : SquareCell₌ (βr ▷ Ju) (βv ▷ Jl) (Cocone.match source) (Cocone.match target)
matching = transpose-square₌
(replace-sides₌ (comp-inv-right (βr ▷ Ju) (Al ⁻¹))
(comp-inv-right (βv ▷ Jl) (Ar ⁻¹))
(replace-edges₌ source-normal (id₌ target-match)
(changeEndpoints-extend-square (Al ⁻¹) (Ar ⁻¹) raw raw-square)))
comparison : CoconeIdentification₁ source target
comparison = record { left = βr; right = βv; compatible = matching }
private
module _ {Γ : Context} {A B C T : CAT Γ} {u : MAP A B} {l : MAP A C} where
compose-cocone₁ : {s t z : Cocone u l T}
→ CoconeIdentification₁ t z → CoconeIdentification₁ s t → CoconeIdentification₁ s z
compose-cocone₁ Ψ Φ = cocone-identification-One
(cocone-identification-compose (cocone-identification Ψ) (cocone-identification Φ))
inverse-cocone₁ : {s t : Cocone u l T}
→ CoconeIdentification₁ s t → CoconeIdentification₁ t s
inverse-cocone₁ Φ = cocone-identification-One
(cocone-identification-inverse (cocone-identification Φ))
module TerminalProductSquare {Γ : Context} {A B C D : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) where
private
u = Square.source-map s
ordinary = square-cocone s
product = square-cocone (product-square {P = One} s)
p = pr₂ {C = One} {D = D}
q = product-unitˡ-inverse D
ε = product-unitˡ-pr₂-inverse D
module Product = TerminalCoconeRoundtrip {E = One × D} u l
using (back; back-postcomposition)
module Ordinary = TerminalCoconeRoundtrip {E = D} u l
using (back; back-identification; twice; module Calculation)
module Projection = ProjectionSquare {P = One} s
using (comparison)
recovered = Product.back product
inserted = cocone-postcompose q ordinary
back-projection : CoconeIdentification₁
(cocone-postcompose p recovered) (Ordinary.back (cocone-postcompose p product))
back-projection = inverse-cocone₁ (Product.back-postcomposition p product)
back-square : CoconeIdentification₁
(Ordinary.back (cocone-postcompose p product)) (Ordinary.twice ordinary)
back-square = cocone-identification-One
(Ordinary.back-identification (cocone-identification Projection.comparison))
projected-recovered : CoconeIdentification₁ (cocone-postcompose p recovered) ordinary
projected-recovered = compose-cocone₁ (Ordinary.Calculation.comparison ordinary)
(compose-cocone₁ back-square back-projection)
retraction-action : CoconeIdentification₁
(cocone-postcompose (p ∘ q) ordinary) (cocone-postcompose (id D) ordinary)
retraction-action = cocone-identification-One (record
{ left = ε ▷ Cocone.left ordinary
; right = ε ▷ Cocone.right ordinary
; compatible = post-square-cell-outer l (Cocone.right ordinary)
(Cocone.left ordinary) u (Cocone.match ordinary) ε })
projected-inserted : CoconeIdentification₁ (cocone-postcompose p inserted) ordinary
projected-inserted = compose-cocone₁ (postcompose-unit ordinary)
(compose-cocone₁ retraction-action (inverse-cocone₁ (postcompose-assoc ordinary q p)))
projected-comparison : CoconeIdentification₁
(cocone-postcompose p recovered) (cocone-postcompose p inserted)
projected-comparison = compose-cocone₁ (inverse-cocone₁ projected-inserted) projected-recovered
module Recovery = CoconePostcompositionRecovery p (product-unitˡ-isEquiv D)
recovered inserted (cocone-identification projected-comparison)
using (value)
comparison : CoconeIdentification₁
(Product.back product) (cocone-postcompose q ordinary)
comparison = cocone-identification-One Recovery.value
module _ {Γ : Context} where
module NativeRestrictionCocones {P A B C E : CAT Γ} (u : MAP A B) (l : MAP A C) where
Ju : MAP (P × A) (P × B)
Ju = product-restriction u
Jl : MAP (P × A) (P × C)
Jl = product-restriction l
private
eA = funEval {C = A} {D = E}
eB = funEval {C = B} {D = E}
eC = funEval {C = C} {D = E}
F = funPre {D = E} u
G = funPre {D = E} l
represented : Cone F G P → Cocone Ju Jl E
represented s = record
{ left = evaluate eB (Cone.left s); right = evaluate eC (Cone.right s)
; match = changeEndpoints (funPre-uncurry u (Cone.left s)) (funPre-uncurry l (Cone.right s))
(evaluate-cong eA (Cone.match s)) }
evaluate-identification : {X : CAT Γ} {s t : Cone F G P}
→ ConeIdentification X s t → CoconeIdentification X (represented s) (represented t)
evaluate-identification {X = X} {s} {t} Φ = record
{ left = evaluate⁼ eB (ConeIdentification.left Φ)
; right = evaluate⁼ eC (ConeIdentification.right Φ)
; compatible = replace-sides₌
(constant-endpoints {X = X} (funPre-uncurry u (Cone.left s)) (funPre-uncurry l (Cone.right s))
(evaluate-cong eA (Cone.match s)))
(constant-endpoints {X = X} (funPre-uncurry u (Cone.left t)) (funPre-uncurry l (Cone.right t))
(evaluate-cong eA (Cone.match t)))
(transport-square
(const {P = X} (funPre-uncurry u (Cone.left s))) (const (funPre-uncurry u (Cone.left t)))
(const (funPre-uncurry l (Cone.right s))) (const (funPre-uncurry l (Cone.right t)))
(const (evaluate-cong eA (Cone.match s))) (const (evaluate-cong eA (Cone.match t)))
(evaluate⁼ eA (F ◁ ConeIdentification.left Φ)) (evaluate⁼ eA (G ◁ ConeIdentification.right Φ))
(evaluate⁼ eB (ConeIdentification.left Φ) ▷ Ju) (evaluate⁼ eC (ConeIdentification.right Φ) ▷ Jl)
(funPre-uncurry-inputs u (ConeIdentification.left Φ))
(funPre-uncurry-inputs l (ConeIdentification.right Φ))
(evaluation-fixed-square {X = X} eA (ConeIdentification.compatible Φ))) }
module CurriedCocone (s : Cocone Ju Jl E) where
left = funCurry {C = B} {D = E} (Cocone.left s)
right = funCurry {C = C} {D = E} (Cocone.right s)
left-β = funCurry-β {C = B} {D = E} (Cocone.left s)
right-β = funCurry-β {C = C} {D = E} (Cocone.right s)
private
input = left-β ▷ Ju
output = right-β ▷ Jl
desired = output ⁻¹ ∙ (Cocone.match s ∙ input)
left-change = funPre-uncurry u left
right-change = funPre-uncurry l right
raw-match = right-change ⁻¹ ∙ (desired ∙ left-change)
value : Cone F G P
value = record
{ left = left; right = right
; match = reflect eA (funUniversal A E) (F ∘ left) (G ∘ right) raw-match }
abstract
matching-image : Cocone.match (represented value) =₂ desired
matching-image = restore-boundaries left-change right-change desired
(evaluate-cong eA (Cone.match value))
(reflect-β-One eA (funUniversal A E) (F ∘ left) (G ∘ right) raw-match)
compatible : SquareCell₌ (left-β ▷ Ju) (right-β ▷ Jl)
(Cocone.match (represented value)) (Cocone.match s)
compatible = comp₌-cong (id₌ output) (matching-image ⁻¹) ∙
(comp-inv-left output (Cocone.match s ∙ input)) ⁻¹
comparison : CoconeIdentification₁ (represented value) s
comparison = record { left = left-β; right = right-β; compatible = compatible }
module ReflectedCocone {X : CAT Γ} (s t : Cone F G P)
(Φ : CoconeIdentification X (represented s) (represented t)) where
open Terms.Equalities X using (_＝_)
left : Cone.left s ＝ Cone.left t
left = reflect eB (funUniversal B E) (Cone.left s) (Cone.left t) (CoconeIdentification.left Φ)
right : Cone.right s ＝ Cone.right t
right = reflect eC (funUniversal C E) (Cone.right s) (Cone.right t) (CoconeIdentification.right Φ)
left-image : evaluate⁼ eB left =₁ CoconeIdentification.left Φ
left-image = reflect-β eB (funUniversal B E) (Cone.left s) (Cone.left t) (CoconeIdentification.left Φ)
right-image : evaluate⁼ eC right =₁ CoconeIdentification.right Φ
right-image = reflect-β eC (funUniversal C E) (Cone.right s) (Cone.right t) (CoconeIdentification.right Φ)
private
left-square : SquareCell₌ (evaluate⁼ eA (F ◁ left)) (CoconeIdentification.left Φ ▷ Ju)
(const (funPre-uncurry u (Cone.left s))) (const (funPre-uncurry u (Cone.left t)))
left-square = replace-edges₌ (id₌ (evaluate⁼ eA (F ◁ left)))
(preWhisker Ju ◁ left-image) (funPre-uncurry-inputs u left)
right-square : SquareCell₌ (evaluate⁼ eA (G ◁ right)) (CoconeIdentification.right Φ ▷ Jl)
(const (funPre-uncurry l (Cone.right s))) (const (funPre-uncurry l (Cone.right t)))
right-square = replace-edges₌ (id₌ (evaluate⁼ eA (G ◁ right)))
(preWhisker Jl ◁ right-image) (funPre-uncurry-inputs l right)
source-boundary = const {P = X} (Cone.match t) ∙ (F ◁ left)
target-boundary = (G ◁ right) ∙ const {P = X} (Cone.match s)
native-action = evaluation-action eA (F ∘ Cone.left s) (G ∘ Cone.right t)
wanted-image : (native-action ∘ source-boundary) =₁ (native-action ∘ target-boundary)
wanted-image = framed-matching-image eA (Cone.match s) (Cone.match t) (F ◁ left) (G ◁ right)
(funPre-uncurry u (Cone.left s)) (funPre-uncurry l (Cone.right s))
(funPre-uncurry u (Cone.left t)) (funPre-uncurry l (Cone.right t))
left-square right-square (CoconeIdentification.compatible Φ)
matching-factor : Fact.Factorization (postWhisker native-action) wanted-image
matching-factor = evaluation-reflection₂ eA (funUniversal A E)
source-boundary target-boundary wanted-image
compatible : SquareCell₌ (F ◁ left) (G ◁ right) (const (Cone.match s)) (const (Cone.match t))
compatible = Fact.factor matching-factor
matching-image : (postWhisker native-action ∘ compatible) =₁ wanted-image
matching-image = Fact.triangle matching-factor
value : ConeIdentification X s t
value = record { left = left; right = right; compatible = compatible }
curry-represented : (s : Cone F G P)
→ ConeIdentification₁ (CurriedCocone.value (represented s)) s
curry-represented s = cone-identification-One
(ReflectedCocone.value (CurriedCocone.value (represented s)) s
(cocone-identification (CurriedCocone.comparison (represented s))))
module MappingCoconeEncoding {P A B C E : CAT Γ} (pAn : isAn P)
(u : MAP A B) (l : MAP A C)
(s : Cocone (product-restriction {P = P} u) (product-restriction l) E) where
private
module M = MappingOutEvaluation {P = P} {E = E} u l
using (represented)
Ju = product-restriction {P = P} u
Jl = product-restriction {P = P} l
left = mapCurry pAn (Cocone.left s)
right = mapCurry pAn (Cocone.right s)
left-β = mapCurry-β pAn (Cocone.left s)
right-β = mapCurry-β pAn (Cocone.right s)
private
input = left-β ▷ Ju
output = right-β ▷ Jl
desired = output ⁻¹ ∙ (Cocone.match s ∙ input)
left-change = mapPre-uncurry u left
right-change = mapPre-uncurry l right
raw-match = right-change ⁻¹ ∙ (desired ∙ left-change)
value : Cone (mapPre {D = E} u) (mapPre l) P
value = record
{ left = left; right = right
; match = uncurry-reflect pAn (mapPre u ∘ left) (mapPre l ∘ right) raw-match }
abstract
matching-image : Cocone.match (M.represented value) =₂ desired
matching-image = restore-boundaries left-change right-change desired
(uncurry⁼ (Cone.match value))
(uncurry-reflect-β pAn (mapPre u ∘ left) (mapPre l ∘ right) raw-match)
compatible : SquareCell₌ (left-β ▷ Ju) (right-β ▷ Jl)
(Cocone.match (M.represented value)) (Cocone.match s)
compatible = comp₌-cong (id₌ output) (matching-image ⁻¹) ∙
(comp-inv-left output (Cocone.match s ∙ input)) ⁻¹
comparison : CoconeIdentification₁ (M.represented value) s
comparison = record { left = left-β; right = right-β; compatible = compatible }
module _ {Γ : Context} where
module NativeOrdinaryCocones {P A B C E : CAT Γ} (u : MAP A B) (l : MAP A C) where
Hu : MAP (A × P) (B × P)
Hu = productMap u (id P)
Hl : MAP (A × P) (C × P)
Hl = productMap l (id P)
private
e = funEval {C = P} {D = E}
represented : Cocone u l (Fun P E) → Cocone Hu Hl E
represented s = record
{ left = evaluate e (Cocone.left s)
; right = evaluate e (Cocone.right s)
; match = changeEndpoints (evaluate-restrict e (Cocone.left s) u)
(evaluate-restrict e (Cocone.right s) l) (evaluate-cong e (Cocone.match s)) }
evaluate-identification : {X : CAT Γ} {s t : Cocone u l (Fun P E)}
→ CoconeIdentification X s t → CoconeIdentification X (represented s) (represented t)
evaluate-identification {X} {s} {t} Φ = record
{ left = evaluate⁼ e (CoconeIdentification.left Φ)
; right = evaluate⁼ e (CoconeIdentification.right Φ)
; compatible = replace-sides₌
(constant-endpoints {X = X} (evaluate-restrict e (Cocone.left s) u)
(evaluate-restrict e (Cocone.right s) l) (evaluate-cong e (Cocone.match s)))
(constant-endpoints {X = X} (evaluate-restrict e (Cocone.left t) u)
(evaluate-restrict e (Cocone.right t) l) (evaluate-cong e (Cocone.match t)))
(transport-square
(const {P = X} (evaluate-restrict e (Cocone.left s) u))
(const (evaluate-restrict e (Cocone.left t) u))
(const (evaluate-restrict e (Cocone.right s) l))
(const (evaluate-restrict e (Cocone.right t) l))
(const (evaluate-cong e (Cocone.match s))) (const (evaluate-cong e (Cocone.match t)))
(evaluate⁼ e (CoconeIdentification.left Φ ▷ u))
(evaluate⁼ e (CoconeIdentification.right Φ ▷ l))
(evaluate⁼ e (CoconeIdentification.left Φ) ▷ Hu)
(evaluate⁼ e (CoconeIdentification.right Φ) ▷ Hl)
(evaluate-restrict-inputs e (CoconeIdentification.left Φ) u)
(evaluate-restrict-inputs e (CoconeIdentification.right Φ) l)
(evaluation-fixed-square {X = X} e (CoconeIdentification.compatible Φ))) }
module CurriedCocone (s : Cocone Hu Hl E) where
left = funCurry {C = P} {D = E} (Cocone.left s)
right = funCurry {C = P} {D = E} (Cocone.right s)
left-β = funCurry-β {C = P} {D = E} (Cocone.left s)
right-β = funCurry-β {C = P} {D = E} (Cocone.right s)
private
input = left-β ▷ Hu
output = right-β ▷ Hl
desired = output ⁻¹ ∙ (Cocone.match s ∙ input)
left-change = evaluate-restrict e left u
right-change = evaluate-restrict e right l
raw-match = right-change ⁻¹ ∙ (desired ∙ left-change)
value : Cocone u l (Fun P E)
value = record
{ left = left; right = right
; match = reflect e (funUniversal P E) (left ∘ u) (right ∘ l) raw-match }
abstract
matching-image : Cocone.match (represented value) =₂ desired
matching-image = restore-boundaries left-change right-change desired
(evaluate-cong e (Cocone.match value))
(reflect-β-One e (funUniversal P E) (left ∘ u) (right ∘ l) raw-match)
compatible : SquareCell₌ (left-β ▷ Hu) (right-β ▷ Hl)
(Cocone.match (represented value)) (Cocone.match s)
compatible = comp₌-cong (id₌ output) (matching-image ⁻¹) ∙
(comp-inv-left output (Cocone.match s ∙ input)) ⁻¹
comparison : CoconeIdentification₁ (represented value) s
comparison = record { left = left-β; right = right-β; compatible = compatible }
module _ {Γ : Context} where
module TransposedRestrictionCocones {P A B C E : CAT Γ} (u : MAP A B) (l : MAP A C) where
Ju : MAP (P × A) (P × B)
Ju = product-restriction u
Jl : MAP (P × A) (P × C)
Jl = product-restriction l
Hu : MAP (A × P) (B × P)
Hu = productMap u (id P)
Hl : MAP (A × P) (C × P)
Hl = productMap l (id P)
private
module O = NativeOrdinaryCocones {P = P} {E = E} u l
using (represented; module CurriedCocone)
module Roundtrip = SwapCoconeRoundtrip {P = P} {E = E} u l
using (back; back-identification; forward; forward-identification; twice; module Calculation)
transposed : Cocone Ju Jl E → Cocone Hu Hl E
transposed = Roundtrip.forward
transpose-identification : {X : CAT Γ} {s t : Cocone Ju Jl E}
→ CoconeIdentification X s t → CoconeIdentification X (transposed s) (transposed t)
transpose-identification = Roundtrip.forward-identification
untransposed : Cocone Hu Hl E → Cocone Ju Jl E
untransposed = Roundtrip.back
untranspose-identification : {X : CAT Γ} {s t : Cocone Hu Hl E}
→ CoconeIdentification X s t → CoconeIdentification X (untransposed s) (untransposed t)
untranspose-identification = Roundtrip.back-identification
twice-transposed : Cocone Ju Jl E → Cocone Ju Jl E
twice-transposed = Roundtrip.twice
transpose-roundtrip : (s : Cocone Ju Jl E) → CoconeIdentification₁ (twice-transposed s) s
transpose-roundtrip = Roundtrip.Calculation.comparison
module CurriedCocone (s : Cocone Ju Jl E) where
private
module Curried = O.CurriedCocone (transposed s)
using (comparison; value)
value : Cocone u l (Fun P E)
value = Curried.value
comparison : CoconeIdentification₁ (O.represented value) (transposed s)
comparison = Curried.comparison
private
module _ {Γ : Context} {X : CAT Γ} where
constant-cocone-identification : {A B C E : CAT Γ} {u : MAP A B} {l : MAP A C}
{s t : Cocone u l E} → CoconeIdentification₁ s t → CoconeIdentification X s t
constant-cocone-identification {u = u} {l} Φ = record
{ left = const {P = X} (CoconeIdentification₁.left Φ)
; right = const {P = X} (CoconeIdentification₁.right Φ)
; compatible = replace-edges₌
((pre-constant (CoconeIdentification₁.left Φ) u) ⁻¹)
((pre-constant (CoconeIdentification₁.right Φ) l) ⁻¹)
(constant-square₌ (CoconeIdentification₁.compatible Φ)) }
module _ {Γ : Context} where
module OrdinaryMappingCocones {A B C E : CAT Γ} (u : MAP A B) (l : MAP A C) where
private
module Roundtrip = TerminalCoconeRoundtrip {E = E} u l
using (back; back-identification; forward; forward-identification; module Calculation)
module M = MappingOutEvaluation {P = One} {E = E} u l
using (evaluate-identification; represented; module RecoveredIdentification)
product-cocone : Cocone u l E → Cocone (product-restriction {P = One} u) (product-restriction l) E
product-cocone = Roundtrip.forward
encoded : Cocone u l E → Cone (mapPre {D = E} u) (mapPre l) One
encoded s = MappingCoconeEncoding.value one-isAn u l (product-cocone s)
decoded : Cone (mapPre {D = E} u) (mapPre l) One → Cocone u l E
decoded s = Roundtrip.back (M.represented s)
encoded-left-name : (s : Cocone u l E) → Cone.left (encoded s) =₁ name (Cocone.left s)
encoded-left-name s = id₌ (name (Cocone.left s))
encoded-right-name : (s : Cocone u l E) → Cone.right (encoded s) =₁ name (Cocone.right s)
encoded-right-name s = id₌ (name (Cocone.right s))
decoded-left : (s : Cone (mapPre {D = E} u) (mapPre l) One)
→ Cocone.left (decoded s) =₁ decode (Cone.left s)
decoded-left s = id₌ (decode (Cone.left s))
decoded-right : (s : Cone (mapPre {D = E} u) (mapPre l) One)
→ Cocone.right (decoded s) =₁ decode (Cone.right s)
decoded-right s = id₌ (decode (Cone.right s))
module _ {X : CAT Γ} where
encoded-identification : {s t : Cocone u l E}
→ CoconeIdentification X s t → ConeIdentification X (encoded s) (encoded t)
encoded-identification {s} {t} Φ = M.RecoveredIdentification.identification one-isAn (encoded s) (encoded t)
(cocone-identification-compose
(cocone-identification-inverse
(constant-cocone-identification (MappingCoconeEncoding.comparison one-isAn u l (product-cocone t))))
(cocone-identification-compose (Roundtrip.forward-identification Φ)
(constant-cocone-identification (MappingCoconeEncoding.comparison one-isAn u l (product-cocone s)))))
decoded-identification : {s t : Cone (mapPre {D = E} u) (mapPre l) One}
→ ConeIdentification X s t → CoconeIdentification X (decoded s) (decoded t)
decoded-identification Φ = Roundtrip.back-identification (M.evaluate-identification Φ)
private
leg-normal : {T : CAT Γ} (h : MAP T E)
→ ((comp-unitʳ h ∙ ((h ◁ product-unitˡ-pr₂-inverse T) ∙
comp-assoc (product-unitˡ-inverse T) pr₂ h)) ∙
(mapCurry-β one-isAn (h ∘ pr₂) ▷ product-unitˡ-inverse T)) =₂ decode-name h
leg-normal {T} h = comp₌-cong (id₌ (comp-unitʳ h))
(comp₌-assoc (h ◁ product-unitˡ-pr₂-inverse T)
(comp-assoc (product-unitˡ-inverse T) pr₂ h)
(mapCurry-β one-isAn (h ∘ pr₂) ▷ product-unitˡ-inverse T)) ∙
comp₌-assoc (comp-unitʳ h)
((h ◁ product-unitˡ-pr₂-inverse T) ∙ comp-assoc (product-unitˡ-inverse T) pr₂ h)
(mapCurry-β one-isAn (h ∘ pr₂) ▷ product-unitˡ-inverse T)
module DecodeEncoding (s : Cocone u l E) where
raw : CoconeIdentification₁ (decoded (encoded s)) s
raw = cocone-identification-One
(cocone-identification-compose
(cocone-identification (Roundtrip.Calculation.comparison s))
(Roundtrip.back-identification (cocone-identification
(MappingCoconeEncoding.comparison one-isAn u l (product-cocone s)))))
comparison : CoconeIdentification₁ (decoded (encoded s)) s
comparison = record
{ left = decode-name (Cocone.left s)
; right = decode-name (Cocone.right s)
; compatible = replace-edges₌
(preWhisker u ◁ leg-normal (Cocone.left s))
(preWhisker l ◁ leg-normal (Cocone.right s))
(CoconeIdentification₁.compatible raw) }
decoded-encoded : (s : Cocone u l E) → CoconeIdentification₁ (decoded (encoded s)) s
decoded-encoded = DecodeEncoding.comparison
module NativeCompositorEvaluation {Γ : Context} {A B C E : CAT Γ}
(f : MAP A B) (g : MAP B C) where
private
eA = funEval {C = A} {D = E}
eB = funEval {C = B} {D = E}
eC = funEval {C = C} {D = E}
Jf = product-restriction {P = Fun C E} f
Jg = product-restriction {P = Fun C E} g
before = (funPre-β {D = E} g ▷ Jf) ∙ funPre-uncurry f (funPre {D = E} g)
after = funPre-β {D = E} (g ∘ f)
route = (eC ◁ restriction-compositor {P = Fun C E} f g) ∙ comp-assoc Jf Jg eC
input = after ⁻¹ ∙
((eC ◁ restriction-compositor {P = Fun C E} f g) ∙
(comp-assoc Jf Jg eC ∙ before))
private
image : evaluate-cong eA (funPre-comp {D = E} f g) =₂ input
image = reflect-β-One eA (funUniversal A E) _ _ input
base-square : SquareCell₌ (evaluate-cong eA (funPre-comp {D = E} f g)) route before after
base-square = (comp₌-assoc (eC ◁ restriction-compositor f g) (comp-assoc Jf Jg eC) before) ⁻¹ ∙
(comp-inv-left after
((eC ◁ restriction-compositor f g) ∙ (comp-assoc Jf Jg eC ∙ before)) ∙
comp₌-cong (id₌ after) image)
private
module Calculation = Pre.PrecompositionCompositor eA eB eC f g
(funPre {D = E} f) (funPre g) (funPre (g ∘ f))
(funPre-β f) (funPre-β g) (funPre-β (g ∘ f)) (funPre-comp f g)
using (comparison)
square : {P : CAT Γ} (h : MAP P (Fun C E))
→ SquareCell₌ (evaluate-cong eA (funPre-comp {D = E} f g ▷ h))
((funUncurry h ◁ restriction-compositor {P = P} f g) ∙
comp-assoc (product-restriction {P = P} f)
(product-restriction {P = P} g) (funUncurry h))
((funPre-uncurry g h ▷ product-restriction {P = P} f) ∙
(funPre-uncurry f (funPre g ∘ h) ∙
evaluate-cong eA (comp-assoc h (funPre g) (funPre f))))
(funPre-uncurry (g ∘ f) h)
square h = Calculation.comparison base-square h
module _ {Γ : Context} where
module NativeParameterizedInputEvaluation {P A B E : CAT Γ}
(h : MAP P (Fun B E)) {f g : MAP A B} (α : f =₁ g) where
private
Q : CAT Γ
Q = Fun B E
RA = productMap h (id A)
RB = productMap h (id B)
JQf = product-restriction {P = Q} f
JQg = product-restriction {P = Q} g
JPf = product-restriction {P = P} f
JPg = product-restriction {P = P} g
δQ = productMap-cong (id₌ (id Q)) α
δP = productMap-cong (id₌ (id P)) α
e : MAP (Q × B) E
e = funEval {C = B} {D = E}
eA = funEval {C = A} {D = E}
first : SquareCell₌ (evaluate-cong eA (funPre⁼ {D = E} α ▷ h))
(evaluate-cong eA (funPre⁼ α) ▷ RA)
(evaluate-restrict eA (funPre f) h) (evaluate-restrict eA (funPre g) h)
first = replace-edges₌
(evaluate⁼-absolute eA (funPre⁼ α ▷ h))
(preWhisker RA ◁ evaluate⁼-absolute eA (funPre⁼ α))
(unconst-sides₌ (evaluate-restrict-inputs eA (funPre⁼ α) h))
base : SquareCell₌ (evaluate-cong eA (funPre⁼ {D = E} α)) (e ◁ δQ)
(funPre-β f) (funPre-β g)
base = replace-edges₌ (evaluate⁼-absolute eA (funPre⁼ α))
(postWhisker e ◁ productMap-cong₂ (const-One (id₌ (id Q))) (id₌ α))
(unconst-sides₌ (funPre⁼-evaluation α))
second : SquareCell₌ (evaluate-cong eA (funPre⁼ {D = E} α) ▷ RA)
((e ◁ δQ) ▷ RA) (funPre-β f ▷ RA) (funPre-β g ▷ RA)
second = pre-square₌ RA base
third : SquareCell₌ ((e ◁ δQ) ▷ RA) (e ◁ (δQ ▷ RA))
(comp-assoc RA JQf e) (comp-assoc RA JQg e)
third = whisker-mixed-One δQ RA e
fourth : SquareCell₌ (e ◁ (δQ ▷ RA)) (e ◁ (RB ◁ δP))
(e ◁ productMap-separate h f) (e ◁ productMap-separate h g)
fourth = post-square₌ e (SeparationSecondInput.compatibility h α)
fifth : SquareCell₌ (e ◁ (RB ◁ δP)) (funUncurry h ◁ δP)
((comp-assoc JPf RB e) ⁻¹) ((comp-assoc JPg RB e) ⁻¹)
fifth = inverse-square₌ (postWhisker-comp-One δP RB e)
compatibility : SquareCell₌ (evaluate-cong eA (funPre⁼ {D = E} α ▷ h))
(funUncurry h ◁ productMap-cong (id₌ (id P)) α)
(funPre-uncurry f h) (funPre-uncurry g h)
compatibility = paste-square₌
(paste-square₌ (paste-square₌ (paste-square₌ first second) third) fourth) fifth
module _ {Γ : Context} where
module OrdinaryParameterizedSquareEvaluation {A B C D E : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) (z : MAP One (Map D E)) where
private
u = Square.source-map s
h = uncurry z
q = product-unitˡ-inverse D
ordinary = square-cocone s
product = square-cocone (product-square {P = One} s)
module O = OrdinaryMappingCocones {E = E} u l
using (decoded)
module R = TerminalCoconeRoundtrip {E = E} u l
using (back; back-identification)
module M = MappingOutEvaluation {P = One} {E = E} u l
module Actual = ParameterizedSquareEvaluation {P = One} s z
using (identification)
module Terminal = TerminalProductSquare s
using (comparison)
decoded-actual : CoconeIdentification₁
(O.decoded (cone-restrict z (mappingOut s E)))
(R.back (cocone-postcompose h product))
decoded-actual = cocone-identification-One
(R.back-identification (cocone-identification Actual.identification))
commuting : CoconeIdentification₁
(R.back (cocone-postcompose h product))
(cocone-postcompose h (TerminalCoconeRoundtrip.back {E = One × D} u l product))
commuting = TerminalCoconeRoundtrip.back-postcomposition {E = One × D} u l h product
inserted : CoconeIdentification₁
(cocone-postcompose h (TerminalCoconeRoundtrip.back {E = One × D} u l product))
(cocone-postcompose h (cocone-postcompose q ordinary))
inserted = fixed-postcomposition h Terminal.comparison
associated : CoconeIdentification₁
(cocone-postcompose h (cocone-postcompose q ordinary))
(cocone-postcompose (decode z) ordinary)
associated = inverse-cocone₁ (postcompose-assoc ordinary q h)
identification : CoconeIdentification₁
(O.decoded (cone-restrict z (mappingOut s E)))
(cocone-postcompose (decode z) ordinary)
identification = compose-cocone₁ associated
(compose-cocone₁ inserted (compose-cocone₁ commuting decoded-actual))
```
```agda
private
module ScalarEvaluation {Γ : Context} {F C E : CAT Γ} (e : MAP (F × C) E) where
on-identification : {T : CAT Γ} {f g : MAP T F}
→ f =₁ g → evaluate e f =₁ evaluate e g
on-identification = evaluate-cong e
congruence : {T : CAT Γ} {f g : MAP T F} {α β : f =₁ g}
→ α =₂ β → on-identification α =₂ on-identification β
congruence {α = α} {β} p = evaluate⁼-absolute e β ∙
(evaluate⁼-cong e p ∙ (evaluate⁼-absolute e α) ⁻¹)
composition : {T : CAT Γ} {f g h : MAP T F} (β : g =₁ h) (α : f =₁ g)
→ on-identification (β ∙ α) =₂ (on-identification β ∙ on-identification α)
composition β α = comp₌-cong (evaluate⁼-absolute e β) (evaluate⁼-absolute e α) ∙
(evaluate⁼-composition e β α ∙ (evaluate⁼-absolute e (β ∙ α)) ⁻¹)
identity : {T : CAT Γ} (f : MAP T F)
→ on-identification (id₌ f) =₂ id₌ (evaluate e f)
identity f = const-One (id₌ (evaluate e f)) ∙
(evaluate⁼-identity e f ∙
(evaluate⁼-cong e ((const-One (id₌ f)) ⁻¹) ∙ (evaluate⁼-absolute e (id₌ f)) ⁻¹))
inverse : {T : CAT Γ} {f g : MAP T F} (α : f =₁ g)
→ on-identification (α ⁻¹) =₂ (on-identification α) ⁻¹
inverse {f = f} α = cancel-right (on-identification α)
((comp₌-inverseˡ-One (on-identification α)) ⁻¹ ∙
(identity f ∙ (congruence (comp₌-inverseˡ-One α) ∙ (composition (α ⁻¹) α) ⁻¹)))
private
module ProductSquareParameterChange {Γ : Context} {P Q A B C D : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) (h : MAP P Q) where
private
u : MAP A B
u = Square.source-map s
v : MAP C D
v = Square.target-map s
σ : (r ∘ u) =₁ (v ∘ l)
σ = Square.cell s
JPu = product-restriction {P = P} u
JPl = product-restriction {P = P} l
JPr = product-restriction {P = P} r
JPv = product-restriction {P = P} v
JQu = product-restriction {P = Q} u
JQl = product-restriction {P = Q} l
JQr = product-restriction {P = Q} r
JQv = product-restriction {P = Q} v
RA : MAP (P × A) (Q × A)
RA = productMap h (id A)
RB : MAP (P × B) (Q × B)
RB = productMap h (id B)
RC : MAP (P × C) (Q × C)
RC = productMap h (id C)
RD : MAP (P × D) (Q × D)
RD = productMap h (id D)
Su = productMap-separate h u
Sl = productMap-separate h l
Sr = productMap-separate h r
Sv = productMap-separate h v
Sru = productMap-separate h (r ∘ u)
Svl = productMap-separate h (v ∘ l)
κQu = restriction-compositor {P = Q} u r
κQl = restriction-compositor {P = Q} l v
κPu = restriction-compositor {P = P} u r
κPl = restriction-compositor {P = P} l v
σQ = productMap-cong (id₌ (id Q)) σ
σP = productMap-cong (id₌ (id P)) σ
module Change = ChangeSpan {E = Q × D} JQu JQl JPu JPl RA RB RC (Su ⁻¹) (Sl ⁻¹)
using (value; module L; module R)
ρr = Change.L.ρ JQr
ρv = Change.R.ρ JQv
Ar = comp-assoc RA JQu JQr
Av = comp-assoc RA JQl JQv
Br = comp-assoc JPu RB JQr
Bv = comp-assoc JPl RC JQv
L = comp-assoc JPu JPr RD
R = comp-assoc JPl JPv RD
α = Sr ▷ JPu
β = Sv ▷ JPl
left-total = L ∙ (α ∙ ρr ⁻¹)
right-total = R ∙ (β ∙ ρv ⁻¹)
raw-source = Square.cell (product-square {P = Q} s) ▷ RA
raw-target = RD ◁ Square.cell (product-square {P = P} s)
post-inverse-inverse : {K Z : CAT Γ} (F : MAP K Z)
{V : CAT Γ} {f g : MAP V K} (δ : f =₁ g)
→ ((F ◁ δ ⁻¹) ⁻¹) =₂ (F ◁ δ)
post-inverse-inverse F δ = inverse-inverse (F ◁ δ) ∙ (inv₌ ◁ postWhisker-inverse F δ)
inverse-left-frame : ρr ⁻¹ =₂ (Br ⁻¹ ∙ ((JQr ◁ Su) ∙ Ar))
inverse-left-frame = comp₌-cong (id₌ (Br ⁻¹))
(comp₌-cong (post-inverse-inverse JQr Su) (id₌ Ar)) ∙
(comp₌-assoc (Br ⁻¹) ((JQr ◁ Su ⁻¹) ⁻¹) Ar ∙
(comp₌-cong (inverse-composite (JQr ◁ Su ⁻¹) Br) (inverse-inverse Ar) ∙
inverse-composite (Ar ⁻¹) ((JQr ◁ Su ⁻¹) ∙ Br)))
inverse-right-frame : ρv ⁻¹ =₂ (Bv ⁻¹ ∙ ((JQv ◁ Sl) ∙ Av))
inverse-right-frame = comp₌-cong (id₌ (Bv ⁻¹))
(comp₌-cong (post-inverse-inverse JQv Sl) (id₌ Av)) ∙
(comp₌-assoc (Bv ⁻¹) ((JQv ◁ Sl ⁻¹) ⁻¹) Av ∙
(comp₌-cong (inverse-composite (JQv ◁ Sl ⁻¹) Bv) (inverse-inverse Av) ∙
inverse-composite (Av ⁻¹) ((JQv ◁ Sl ⁻¹) ∙ Bv)))
left-square : SquareCell₌ (κQu ▷ RA) (RD ◁ κPu) left-total Sru
left-square =
(comp₌-cong (id₌ (RD ◁ κPu))
(comp₌-cong (id₌ L) (comp₌-cong (id₌ α) inverse-left-frame))) ⁻¹ ∙
parameter-separation-composition h u r
middle-square : SquareCell₌ (σQ ▷ RA) (RD ◁ σP) Sru Svl
middle-square = SeparationSecondInput.compatibility h σ
right-square : SquareCell₌ (κQl ▷ RA) (RD ◁ κPl) right-total Svl
right-square =
(comp₌-cong (id₌ (RD ◁ κPl))
(comp₌-cong (id₌ R) (comp₌-cong (id₌ β) inverse-right-frame))) ⁻¹ ∙
parameter-separation-composition h l v
source-normal : raw-source =₂ ((κQl ▷ RA) ⁻¹ ∙ ((σQ ▷ RA) ∙ (κQu ▷ RA)))
source-normal = comp₌-cong (preWhisker-inverse κQl RA)
(preWhisker-comp₌ σQ κQu RA) ∙ preWhisker-comp₌ (κQl ⁻¹) (σQ ∙ κQu) RA
target-normal : raw-target =₂ ((RD ◁ κPl) ⁻¹ ∙ ((RD ◁ σP) ∙ (RD ◁ κPu)))
target-normal = comp₌-cong (postWhisker-inverse RD κPl)
(postWhisker-comp₌ RD σP κPu) ∙ postWhisker-comp₌ RD (κPl ⁻¹) (σP ∙ κPu)
raw-square : SquareCell₌ raw-source raw-target left-total right-total
raw-square = replace-edges₌ (source-normal ⁻¹) (target-normal ⁻¹)
(inv-comp-square₌ (adjoin-square₌ left-square middle-square) right-square)
source : Cocone JPu JPl (Q × D)
source = Change.value (square-cocone (product-square {P = Q} s))
target : Cocone JPu JPl (Q × D)
target = cocone-postcompose RD (square-cocone (product-square {P = P} s))
private
source-matching-normal : changeEndpoints (ρr ⁻¹) (ρv ⁻¹) raw-source =₂ Cocone.match source
source-matching-normal = comp₌-cong (id₌ (ρv ⁻¹))
(comp₌-cong (id₌ raw-source) (inverse-inverse ρr))
target-matching-normal : changeEndpoints (L ⁻¹) (R ⁻¹) raw-target =₂ Cocone.match target
target-matching-normal = comp₌-cong (id₌ (R ⁻¹))
(comp₌-cong (id₌ raw-target) (inverse-inverse L))
abstract
matching : SquareCell₌ α β (Cocone.match source) (Cocone.match target)
matching = replace-sides₌ source-matching-normal target-matching-normal
(transport-square (ρr ⁻¹) (L ⁻¹) (ρv ⁻¹) (R ⁻¹) raw-source raw-target
left-total right-total α β
(inv-comp-left L (α ∙ ρr ⁻¹))
(inv-comp-left R (β ∙ ρv ⁻¹)) (transpose-square₌ raw-square))
comparison : CoconeIdentification₁ source target
comparison = record { left = Sr; right = Sv; compatible = matching }
private
module NativeConeParameterChange {Γ : Context} {P Q A B C E : CAT Γ}
(u : MAP A B) (l : MAP A C) (h : MAP P Q)
(s : Cone (funPre {D = E} u) (funPre l) Q) where
private
eA = funEval {C = A} {D = E}
eB = funEval {C = B} {D = E}
eC = funEval {C = C} {D = E}
module Action = ScalarEvaluation eA
using (composition; inverse)
module NP = NativeRestrictionCocones {P = P} {E = E} u l
using (Jl; Ju; represented)
module NQ = NativeRestrictionCocones {P = Q} {E = E} u l
using (Jl; Ju; represented)
p = Cone.left s
q = Cone.right s
τ = Cone.match s
F = funPre {D = E} u
G = funPre {D = E} l
RA = productMap h (id A)
RB = productMap h (id B)
RC = productMap h (id C)
Su = productMap-separate h u
Sl = productMap-separate h l
module Change = ChangeSpan {E = E} NQ.Ju NQ.Jl NP.Ju NP.Jl RA RB RC (Su ⁻¹) (Sl ⁻¹)
using (value; module L; module R)
module U = Pre.RepresentedPrecomposition eA eB u F (funPre-β u)
using (substitution)
module L = Pre.RepresentedPrecomposition eA eC l G (funPre-β l)
using (substitution)
μu = funPre-uncurry u p
μl = funPre-uncurry l q
ρu = Change.L.ρ (evaluate eB p)
ρl = Change.R.ρ (evaluate eC q)
af = comp-assoc h p F
ag = comp-assoc h q G
Ef = funPre-uncurry u (p ∘ h) ∙ evaluate-cong eA af
Eg = funPre-uncurry l (q ∘ h) ∙ evaluate-cong eA ag
route : {Z : CAT Γ} (f : MAP A Z) (k : MAP Q (Fun Z E))
→ (evaluate eA (funPre f ∘ k) ∘ RA) =₁
((evaluate (funEval {C = Z} {D = E}) k ∘ productMap h (id Z)) ∘ product-restriction {P = P} f)
route {Z} f k =
(comp-assoc (product-restriction {P = P} f) (productMap h (id Z))
(evaluate (funEval {C = Z} {D = E}) k)) ⁻¹ ∙
((evaluate (funEval {C = Z} {D = E}) k ◁ productMap-separate h f) ∙
(comp-assoc RA (product-restriction {P = Q} f) (evaluate (funEval {C = Z} {D = E}) k) ∙
(funPre-uncurry f k ▷ RA)))
Ef′ = route u p
Eg′ = route l q
bf = evaluate-restrict eA (F ∘ p) h
bg = evaluate-restrict eA (G ∘ q) h
endpoints : {T : CAT Γ} {x x′ y y′ : MAP T (Fun A E)}
(a : x =₁ x′) (b : y =₁ y′) (δ : x =₁ y)
→ evaluate-cong eA (changeEndpoints a b δ) =₂
changeEndpoints (evaluate-cong eA a) (evaluate-cong eA b) (evaluate-cong eA δ)
endpoints a b δ = comp₌-cong (id₌ (evaluate-cong eA b))
(comp₌-cong (id₌ (evaluate-cong eA δ)) (Action.inverse a) ∙ Action.composition δ (a ⁻¹)) ∙
Action.composition b (δ ∙ a ⁻¹)
pre-endpoints : {K T Z : CAT Γ} {x x′ y y′ : MAP T Z}
(a : x =₁ x′) (b : y =₁ y′) (δ : x =₁ y) (k : MAP K T)
→ (changeEndpoints a b δ ▷ k) =₂ changeEndpoints (a ▷ k) (b ▷ k) (δ ▷ k)
pre-endpoints a b δ k = comp₌-cong (id₌ (b ▷ k))
(comp₌-cong (id₌ (δ ▷ k)) (preWhisker-inverse a k) ∙ preWhisker-comp₌ δ (a ⁻¹) k) ∙
preWhisker-comp₌ b (δ ∙ a ⁻¹) k
module Leg {Z : CAT Γ} (f : MAP A Z) (k : MAP Q (Fun Z E)) where
ez = funEval {C = Z} {D = E}
μ = funPre-uncurry f k
RZ = productMap h (id Z)
JQ = product-restriction {P = Q} f
JP = product-restriction {P = P} f
S = productMap-separate h f
input-assoc = comp-assoc RA JQ (evaluate ez k)
output-assoc = comp-assoc JP RZ (evaluate ez k)
ρ = input-assoc ⁻¹ ∙ ((evaluate ez k ◁ S ⁻¹) ∙ output-assoc)
module K = Pre.RepresentedPrecomposition eA ez f (funPre f) (funPre-β f)
double-inverse : ((evaluate ez k ◁ S ⁻¹) ⁻¹) =₂ (evaluate ez k ◁ S)
double-inverse = inverse-inverse (evaluate ez k ◁ S) ∙
(inv₌ ◁ postWhisker-inverse (evaluate ez k) S)
inverse-frame : ρ ⁻¹ =₂ (output-assoc ⁻¹ ∙ ((evaluate ez k ◁ S) ∙ input-assoc))
inverse-frame = comp₌-cong (id₌ (output-assoc ⁻¹))
(comp₌-cong double-inverse (id₌ input-assoc)) ∙
(comp₌-assoc (output-assoc ⁻¹) ((evaluate ez k ◁ S ⁻¹) ⁻¹) input-assoc ∙
(comp₌-cong (inverse-composite (evaluate ez k ◁ S ⁻¹) output-assoc) (inverse-inverse input-assoc) ∙
inverse-composite (input-assoc ⁻¹) ((evaluate ez k ◁ S ⁻¹) ∙ output-assoc)))
frame : ((ρ ⁻¹) ∙ (μ ▷ RA)) =₂ route f k
frame = comp₌-cong (id₌ (output-assoc ⁻¹)) (comp₌-assoc (evaluate ez k ◁ S) input-assoc (μ ▷ RA)) ∙
(comp₌-assoc (output-assoc ⁻¹) ((evaluate ez k ◁ S) ∙ input-assoc) (μ ▷ RA) ∙
comp₌-cong inverse-frame (id₌ (μ ▷ RA)))
source : Cocone NP.Ju NP.Jl E
source = NP.represented (cone-restrict h s)
target : Cocone NP.Ju NP.Jl E
target = Change.value (NQ.represented s)
left = evaluate-restrict eB p h
right = evaluate-restrict eC q h
private
rawSource = changeEndpoints Ef Eg (evaluate-cong eA (τ ▷ h))
rawTarget = changeEndpoints Ef′ Eg′ (evaluate-cong eA τ ▷ RA)
source-normal : Cocone.match source =₂ rawSource
source-normal = changeEndpoints-iterated (evaluate-cong eA af) (evaluate-cong eA ag)
(funPre-uncurry u (p ∘ h)) (funPre-uncurry l (q ∘ h)) (evaluate-cong eA (τ ▷ h)) ∙
changeEndpoints-cong (funPre-uncurry u (p ∘ h)) (funPre-uncurry l (q ∘ h))
(endpoints af ag (τ ▷ h))
target-frame-normal : Cocone.match target =₂
changeEndpoints (ρu ⁻¹) (ρl ⁻¹) (Cocone.match (NQ.represented s) ▷ RA)
target-frame-normal = comp₌-cong (id₌ (ρl ⁻¹))
(comp₌-cong (id₌ (Cocone.match (NQ.represented s) ▷ RA)) ((inverse-inverse ρu) ⁻¹))
target-normal : Cocone.match target =₂ rawTarget
target-normal = comp₌-cong (Leg.frame l q)
(comp₌-cong (id₌ (evaluate-cong eA τ ▷ RA)) (inv₌ ◁ Leg.frame u p)) ∙
(changeEndpoints-iterated (μu ▷ RA) (μl ▷ RA) (ρu ⁻¹) (ρl ⁻¹) (evaluate-cong eA τ ▷ RA) ∙
changeEndpoints-cong (ρu ⁻¹) (ρl ⁻¹) (pre-endpoints μu μl (evaluate-cong eA τ) RA) ∙
target-frame-normal)
middle : SquareCell₌ (evaluate-cong eA (τ ▷ h)) (evaluate-cong eA τ ▷ RA) bf bg
middle = unconst-sides₌ (replace-edges₌ (evaluate⁼-absolute eA (τ ▷ h))
(preWhisker RA ◁ evaluate⁼-absolute eA τ) (evaluate-restrict-inputs eA τ h))
raw-square : SquareCell₌ (left ▷ NP.Ju) (right ▷ NP.Jl) rawSource rawTarget
raw-square = transport-square Ef Ef′ Eg Eg′
(evaluate-cong eA (τ ▷ h)) (evaluate-cong eA τ ▷ RA)
bf bg (left ▷ NP.Ju) (right ▷ NP.Jl)
((U.substitution p h) ⁻¹)
((L.substitution q h) ⁻¹)
(transpose-square₌ middle)
comparison : CoconeIdentification₁ source target
comparison = record { left = left; right = right
; compatible = replace-sides₌ (source-normal ⁻¹) (target-normal ⁻¹) raw-square }
module _ {Γ : Context} where
module DirectCurriedFunctorSquare {A B C D : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) (E : CAT Γ) where
private
u = Square.source-map s
v = Square.target-map s
Q = Fun D E
e = funEval {C = D} {D = E}
module NQ = NativeRestrictionCocones {P = Q} {E = E} u l
using (Jl; Ju; represented; module CurriedCocone)
universal-product : Cocone NQ.Ju NQ.Jl E
universal-product = cocone-postcompose e (square-cocone (product-square {P = Q} s))
module Encoded = NQ.CurriedCocone universal-product
using (comparison; value)
value : Cone (funPre {D = E} u) (funPre l) (Fun D E)
value = Encoded.value
module Parameterized {P : CAT Γ} (h : MAP P (Fun D E)) where
private
module NP = NativeRestrictionCocones {P = P} {E = E} u l
using (Jl; Ju; represented)
module Restriction = NativeConeParameterChange u l h value
using (comparison)
module Product = ProductSquareParameterChange s h
using (comparison; source; target)
RA = productMap h (id A)
RB = productMap h (id B)
RC = productMap h (id C)
RD = productMap h (id D)
Su = productMap-separate h u
Sl = productMap-separate h l
module Change = ChangeSpan {E = E} NQ.Ju NQ.Jl NP.Ju NP.Jl RA RB RC (Su ⁻¹) (Sl ⁻¹)
using (identification; value)
parameter-product = square-cocone (product-square {P = P} s)
restricted-encoding : CoconeIdentification₁
(Change.value (NQ.represented value)) (Change.value universal-product)
restricted-encoding = cocone-identification-One
(Change.identification (cocone-identification Encoded.comparison))
commuting : CoconeIdentification₁
(Change.value universal-product) (cocone-postcompose e Product.source)
commuting = change-span-postcomposition NQ.Ju NQ.Jl NP.Ju NP.Jl
RA RB RC (Su ⁻¹) (Sl ⁻¹) e
(square-cocone (product-square {P = Q} s))
product-image : CoconeIdentification₁
(cocone-postcompose e Product.source) (cocone-postcompose e Product.target)
product-image = fixed-postcomposition e Product.comparison
associated : CoconeIdentification₁
(cocone-postcompose e Product.target)
(cocone-postcompose (funUncurry h) parameter-product)
associated = inverse-cocone₁ (postcompose-assoc parameter-product RD e)
source : Cocone NP.Ju NP.Jl E
source = NP.represented (cone-restrict h value)
target : Cocone NP.Ju NP.Jl E
target = cocone-postcompose (funUncurry h) parameter-product
comparison : CoconeIdentification₁ source target
comparison = compose-cocone₁ associated
(compose-cocone₁ product-image
(compose-cocone₁ commuting
(compose-cocone₁ restricted-encoding Restriction.comparison)))
```
```agda
private
module _ {Γ : Context} {A B C T E : CAT Γ} {u : MAP A B} {l : MAP A C}
(s : Cocone u l T) {h k : MAP T E} (α : h =₁ k) where
postcomposition-cong₁ : CoconeIdentification₁ (cocone-postcompose h s) (cocone-postcompose k s)
postcomposition-cong₁ = cocone-identification-One (record
{ left = α ▷ Cocone.left s
; right = α ▷ Cocone.right s
; compatible = post-square-cell-outer l (Cocone.right s) (Cocone.left s)
u (Cocone.match s) α })
module _ {Γ : Context} where
module OrdinaryPostcompositionEncoding {A B C D E : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) (h : MAP D E) where
private
u : MAP A B
u = Square.source-map s
Ju : MAP (One × A) (One × B)
Ju = product-restriction u
Jl : MAP (One × A) (One × C)
Jl = product-restriction l
pA : MAP (One × A) A
pA = pr₂
pB : MAP (One × B) B
pB = pr₂
pC : MAP (One × C) C
pC = pr₂
pD : MAP (One × D) D
pD = pr₂
ordinary : Cocone u l D
ordinary = square-cocone s
product : Cocone Ju Jl (One × D)
product = square-cocone (product-square {P = One} s)
module M = MappingOutEvaluation {P = One} {E = E} u l
using (represented; module RecoveredIdentification)
module O = OrdinaryMappingCocones {E = E} u l
using (encoded)
module R = TerminalCoconeRoundtrip {E = E} u l
using (forward)
module RD = TerminalCoconeRoundtrip {E = D} u l
using (forward)
module Actual = ParameterizedSquareEvaluation {P = One} s (name h)
using (identification; source)
module Projection = ProjectionSquare {P = One} s
using (comparison)
name-beta : uncurry (name h) =₁ (h ∘ pD)
name-beta = CurriedRepresentation.evaluation (name-representation h)
evaluation-comparison : CoconeIdentification₁ Actual.source (cocone-postcompose (h ∘ pD) product)
evaluation-comparison = compose-cocone₁ (postcomposition-cong₁ product name-beta) Actual.identification
projected-comparison : CoconeIdentification₁
(cocone-postcompose (h ∘ pD) product) (cocone-postcompose h (RD.forward ordinary))
projected-comparison = compose-cocone₁
(fixed-postcomposition h Projection.comparison) (postcompose-assoc product pD h)
commuting : CoconeIdentification₁
(R.forward (cocone-postcompose h ordinary)) (cocone-postcompose h (RD.forward ordinary))
commuting = change-span-postcomposition u l Ju Jl pA pB pC
(pair-β₂ (id One ∘ pr₁) (u ∘ pr₂))
(pair-β₂ (id One ∘ pr₁) (l ∘ pr₂)) h ordinary
represented-comparison : CoconeIdentification₁
(M.represented (cone-restrict (name h) (mappingOut s E)))
(R.forward (cocone-postcompose h ordinary))
represented-comparison = compose-cocone₁ (inverse-cocone₁ commuting)
(compose-cocone₁ projected-comparison evaluation-comparison)
encoded-comparison : CoconeIdentification₁
(M.represented (cone-restrict (name h) (mappingOut s E)))
(M.represented (O.encoded (cocone-postcompose h ordinary)))
encoded-comparison = compose-cocone₁
(inverse-cocone₁ (MappingCoconeEncoding.comparison one-isAn u l
(R.forward (cocone-postcompose h ordinary)))) represented-comparison
identification : ConeIdentification₁
(cone-restrict (name h) (mappingOut s E)) (O.encoded (cocone-postcompose h ordinary))
identification = cone-identification-One
(M.RecoveredIdentification.identification one-isAn
(cone-restrict (name h) (mappingOut s E)) (O.encoded (cocone-postcompose h ordinary))
(cocone-identification encoded-comparison))
private
module FirstFactorSquare {Γ : Context} (P : CAT Γ) {A B C D : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) where
u = Square.source-map s
v = Square.target-map s
Hu = productMap u (id P)
Hl = productMap l (id P)
Hr = productMap r (id P)
Hv = productMap v (id P)
κu = productMap-first-comp {C = P} r u
κl = productMap-first-comp {C = P} v l
middle = productMap-cong (Square.cell s) (id₌ (id P))
value : Cocone Hu Hl (D × P)
value = record { left = Hr; right = Hv; match = κl ⁻¹ ∙ (middle ∙ κu) }
module OrdinaryFirstFactorSquareEvaluation {Γ : Context} {P A B C D E : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) (g : MAP D (Fun P E)) where
private
module H = FirstFactorSquare P s
using (Hl; Hr; Hu; Hv; middle; u; v; value; κl; κu)
module O = NativeOrdinaryCocones {P = P} {E = E} H.u l
using (represented)
e = funEval {C = P} {D = E}
module Action = ScalarEvaluation e
using (composition; inverse)
k = funUncurry g
u = H.u
v = H.v
σ = Square.cell s
left-leg = evaluate-restrict e g r
right-leg = evaluate-restrict e g v
μu = evaluate-restrict e (g ∘ r) u
μl = evaluate-restrict e (g ∘ v) l
Au = comp-assoc H.Hu H.Hr k
Al = comp-assoc H.Hl H.Hv k
α = left-leg ▷ H.Hu
β = right-leg ▷ H.Hl
left-total = Au ∙ (α ∙ μu)
right-total = Al ∙ (β ∙ μl)
assoc-u = comp-assoc u r g
assoc-l = comp-assoc l v g
eu = evaluate-cong e assoc-u
el = evaluate-cong e assoc-l
em = evaluate-cong e (g ◁ σ)
κu = k ◁ H.κu
κl = k ◁ H.κl
middle = k ◁ H.middle
ru = evaluate-restrict e g (r ∘ u)
vl = evaluate-restrict e g (v ∘ l)
ordinary = cocone-postcompose g (square-cocone s)
raw = evaluate-cong e (Cocone.match ordinary)
δ = k ◁ Cocone.match H.value
raw-normal : raw =₂ (el ⁻¹ ∙ (em ∙ eu))
raw-normal = comp₌-cong (Action.inverse assoc-l)
(Action.composition (g ◁ σ) assoc-u) ∙ Action.composition (assoc-l ⁻¹) ((g ◁ σ) ∙ assoc-u)
product-normal : δ =₂ (κl ⁻¹ ∙ (middle ∙ κu))
product-normal = comp₌-cong (postWhisker-inverse k H.κl)
(postWhisker-comp₌ k H.middle H.κu) ∙ postWhisker-comp₌ k (H.κl ⁻¹) (H.middle ∙ H.κu)
left-square : SquareCell₌ eu κu left-total ru
left-square = evaluate-restrict-assoc e g r u
right-square : SquareCell₌ el κl right-total vl
right-square = evaluate-restrict-assoc e g v l
middle-square : SquareCell₌ em middle ru vl
middle-square = replace-edges₌ (evaluate⁼-absolute e (g ◁ σ))
(postWhisker k ◁ productMap-cong₂ (id₌ σ) (const-One (id₌ (id P))))
(unconst-sides₌ (evaluate-restrict-substitution e g σ))
raw-square : SquareCell₌ raw δ left-total right-total
raw-square = replace-edges₌ (raw-normal ⁻¹) (product-normal ⁻¹)
(inv-comp-square₌ (adjoin-square₌ left-square middle-square) right-square)
source : Cocone H.Hu H.Hl E
source = O.represented ordinary
target : Cocone H.Hu H.Hl E
target = cocone-postcompose k H.value
private
target-normal : changeEndpoints (Au ⁻¹) (Al ⁻¹) δ =₂ Cocone.match target
target-normal = comp₌-cong (id₌ (Al ⁻¹))
(comp₌-cong (id₌ δ) (inverse-inverse Au))
comparison : CoconeIdentification₁ source target
comparison = record { left = left-leg; right = right-leg
; compatible = replace-sides₌ (id₌ (Cocone.match source)) target-normal
(transport-square μu (Au ⁻¹) μl (Al ⁻¹) raw δ
left-total right-total α β
(inv-comp-left Au (α ∙ μu)) (inv-comp-left Al (β ∙ μl))
(transpose-square₌ raw-square)) }
private
module SwapRestrictionCoordinates {Γ : Context} {P A B : CAT Γ} (f : MAP A B) where
private
module S = SwapRestriction {P = P} f
using (H; left₁; left₂; pA; right₁; right₂; transpose-cell)
δ₁ = S.right₁ ⁻¹ ∙ S.left₁
δ₂ = S.right₂ ⁻¹ ∙ S.left₂
source₁ = project-pair₁ pr₂ pr₁ S.H
source₂ = project-pair₂ pr₂ pr₁ S.H
target₁ = project-pair₁ (id P ∘ pr₁) (f ∘ pr₂) S.pA
target₂ = project-pair₂ (id P ∘ pr₁) (f ∘ pr₂) S.pA
remove-id₁ : ((id₌ ((id P ∘ pr₁) ∘ S.pA)) ⁻¹ ∙ δ₁) =₂ δ₁
remove-id₁ = comp₌-unitˡ-One δ₁ ∙
comp₌-cong (inverse-identity ((id P ∘ pr₁) ∘ S.pA)) (id₌ δ₁)
remove-id₂ : ((id₌ ((f ∘ pr₂) ∘ S.pA)) ⁻¹ ∙ δ₂) =₂ δ₂
remove-id₂ = comp₌-unitˡ-One δ₂ ∙
comp₌-cong (inverse-identity ((f ∘ pr₂) ∘ S.pA)) (id₌ δ₂)
projection₁ : SquareCell₌ (pr₁ ◁ S.transpose-cell) δ₁ source₁ target₁
projection₁ = replace-edges₌ (id₌ (pr₁ ◁ S.transpose-cell)) remove-id₁
(lies-over-comp pr₁
(pair-evaluation-over₁-One pr₂ pr₁ S.H δ₁ δ₂)
(lies-over-inverse pr₁ (pair-pre-over₁-One (id P ∘ pr₁) (f ∘ pr₂) S.pA)))
projection₂ : SquareCell₌ (pr₂ ◁ S.transpose-cell) δ₂ source₂ target₂
projection₂ = replace-edges₌ (id₌ (pr₂ ◁ S.transpose-cell)) remove-id₂
(lies-over-comp pr₂
(pair-evaluation-over₂-One pr₂ pr₁ S.H δ₁ δ₂)
(lies-over-inverse pr₂ (pair-pre-over₂-One (id P ∘ pr₁) (f ∘ pr₂) S.pA)))
private
module SwapRestrictionOverProjections {Γ : Context} {P A B : CAT Γ} (f : MAP A B) where
private
module S = SwapRestriction {P = P} f
using (H; J; left₁; left₂; pA; right₁; right₂; transpose-cell)
module Images = SwapRestrictionCoordinates {P = P} f
using (projection₁; projection₂)
project-source₁ = project-pair₁ pr₂ pr₁ S.H
project-source₂ = project-pair₂ pr₂ pr₁ S.H
project-target₁ = project-pair₁ (id P ∘ pr₁) (f ∘ pr₂) S.pA
project-target₂ = project-pair₂ (id P ∘ pr₁) (f ∘ pr₂) S.pA
δ = S.transpose-cell
varying-source = S.left₂ ∙ project-source₂
varying-target = S.right₂ ∙ project-target₂
fixed-source = (comp-unitˡ pr₂ ∙ S.left₁) ∙ project-source₁
fixed-target = pair-β₁ pr₂ pr₁ ∙
restrict-triangle pr₁ S.J
(comp-unitˡ pr₁ ∙ pair-β₁ (id P ∘ pr₁) (f ∘ pr₂)) S.pA
private
close-common : {K Z : CAT Γ} {x y z z′ t : MAP K Z}
(a : x =₁ t) (b : y =₁ t) (p : z =₁ x) (q : z′ =₁ y)
(ε : z =₁ z′)
→ SquareCell₌ ε (b ⁻¹ ∙ a) p q
→ ((b ∙ q) ∙ ε) =₂ (a ∙ p)
close-common a b p q ε square = comp-inv-left b (a ∙ p) ∙
(comp₌-cong (id₌ b) (comp₌-assoc (b ⁻¹) a p) ∙
(comp₌-cong (id₌ b) square ∙ comp₌-assoc b q ε))
fixed-before : ((S.right₁ ∙ project-target₁) ∙ (pr₁ ◁ δ)) =₂
(S.left₁ ∙ project-source₁)
fixed-before = close-common S.left₁ S.right₁ project-source₁ project-target₁
(pr₁ ◁ δ) Images.projection₁
fixed-unit = comp-unitˡ (pr₂ {C = A} {D = P})
swapped-unit : (fixed-unit ∙ S.right₁) =₂
(pair-β₁ pr₂ pr₁ ∙ (comp-unitˡ pr₁ ▷ S.pA))
swapped-unit = comp₌-cong (id₌ (pair-β₁ pr₂ pr₁)) (left-unitor-comp S.pA pr₁) ∙
(comp₌-assoc (pair-β₁ pr₂ pr₁) (comp-unitˡ (pr₁ ∘ S.pA))
(comp-assoc S.pA pr₁ (id P)) ∙
(comp₌-cong (postWhisker-id-One (pair-β₁ pr₂ pr₁))
(id₌ (comp-assoc S.pA pr₁ (id P)))) ∙
(comp₌-assoc fixed-unit (id P ◁ pair-β₁ pr₂ pr₁)
(comp-assoc S.pA pr₁ (id P))) ⁻¹)
fixed-target-normal : (fixed-unit ∙ (S.right₁ ∙ project-target₁)) =₂ fixed-target
fixed-target-normal = comp₌-cong (id₌ (pair-β₁ pr₂ pr₁))
(comp₌-cong ((preWhisker-comp₌ (comp-unitˡ pr₁)
(pair-β₁ (id P ∘ pr₁) (f ∘ pr₂)) S.pA) ⁻¹)
(id₌ ((comp-assoc S.pA S.J pr₁) ⁻¹))) ∙
(comp₌-cong (id₌ (pair-β₁ pr₂ pr₁))
((comp₌-assoc (comp-unitˡ pr₁ ▷ S.pA)
(pair-β₁ (id P ∘ pr₁) (f ∘ pr₂) ▷ S.pA)
((comp-assoc S.pA S.J pr₁) ⁻¹)) ⁻¹) ∙
(comp₌-assoc (pair-β₁ pr₂ pr₁) (comp-unitˡ pr₁ ▷ S.pA) project-target₁ ∙
(comp₌-cong swapped-unit (id₌ project-target₁) ∙
(comp₌-assoc fixed-unit S.right₁ project-target₁) ⁻¹)))
varying : ((varying-target) ∙ (pr₂ ◁ δ)) =₂ varying-source
varying = close-common S.left₂ S.right₂ project-source₂ project-target₂
(pr₂ ◁ δ) Images.projection₂
fixed : ((fixed-target) ∙ (pr₁ ◁ δ)) =₂ fixed-source
fixed = (comp₌-assoc fixed-unit S.left₁ project-source₁) ⁻¹ ∙
(comp₌-cong (id₌ fixed-unit) fixed-before ∙
(comp₌-assoc fixed-unit (S.right₁ ∙ project-target₁) (pr₁ ◁ δ) ∙
comp₌-cong (fixed-target-normal ⁻¹) (id₌ (pr₁ ◁ δ))))
private
module SwapProjectionPasting {Γ : Context} {X₀ X₁ X₂ Y₀ Y₁ Y₂ T : CAT Γ}
(p₀ : MAP X₀ T) (p₁ : MAP X₁ T) (p₂ : MAP X₂ T)
(q₀ : MAP Y₀ T) (q₁ : MAP Y₁ T) (q₂ : MAP Y₂ T)
(x₀ : MAP X₀ Y₀) (x₁ : MAP X₁ Y₁) (x₂ : MAP X₂ Y₂)
(f : MAP X₀ X₁) (g : MAP X₁ X₂) (F : MAP Y₀ Y₁) (G : MAP Y₁ Y₂)
(bf : (p₁ ∘ f) =₁ p₀) (bg : (p₂ ∘ g) =₁ p₁)
(bF : (q₁ ∘ F) =₁ q₀) (bG : (q₂ ∘ G) =₁ q₁)
(bx₀ : (q₀ ∘ x₀) =₁ p₀) (bx₁ : (q₁ ∘ x₁) =₁ p₁)
(bx₂ : (q₂ ∘ x₂) =₁ p₂)
(α : (x₁ ∘ f) =₁ (F ∘ x₀)) (β : (x₂ ∘ g) =₁ (G ∘ x₁)) where
b₀ = OverBase.compose-triangle q₂ x₂ bx₂ (g ∘ f) (OverBase.compose-triangle p₂ g bg f bf)
b₁ = OverBase.compose-triangle q₂ (x₂ ∘ g) (OverBase.compose-triangle q₂ x₂ bx₂ g bg) f bf
b₂ = OverBase.compose-triangle q₂ (G ∘ x₁) (OverBase.compose-triangle q₂ G bG x₁ bx₁) f bf
b₃ = OverBase.compose-triangle q₂ G bG (x₁ ∘ f) (OverBase.compose-triangle q₁ x₁ bx₁ f bf)
b₄ = OverBase.compose-triangle q₂ G bG (F ∘ x₀) (OverBase.compose-triangle q₁ F bF x₀ bx₀)
b₅ = OverBase.compose-triangle q₂ (G ∘ F) (OverBase.compose-triangle q₂ G bG F bF) x₀ bx₀
pasted : (x₂ ∘ (g ∘ f)) =₁ ((G ∘ F) ∘ x₀)
pasted = Square.cell (comp-square (Squares.square g G β) (Squares.square f F α))
compatible :
OverBase.CompatibleOver q₁ (OverBase.compose-triangle q₁ x₁ bx₁ f bf)
(OverBase.compose-triangle q₁ F bF x₀ bx₀) α
→ OverBase.CompatibleOver q₂ (OverBase.compose-triangle q₂ x₂ bx₂ g bg)
(OverBase.compose-triangle q₂ G bG x₁ bx₁) β
→ OverBase.CompatibleOver q₂ b₀ b₅ pasted
compatible first second =
let e₁ = (comp-assoc f g x₂) ⁻¹
e₂ = β ▷ f
e₃ = comp-assoc f x₁ G
e₄ = G ◁ α
e₅ = (comp-assoc x₀ F G) ⁻¹
s₁ = OverBase.compatible-inverse q₂ b₁ b₀ (comp-assoc f g x₂)
(OverBase.compatible-assoc q₂ x₂ g f bx₂ bg bf)
s₂ = OverBase.compatible-pre q₂ f
(OverBase.compose-triangle q₂ x₂ bx₂ g bg) (OverBase.compose-triangle q₂ G bG x₁ bx₁) bf β second
s₃ = OverBase.compatible-assoc q₂ G x₁ f bG bx₁ bf
s₄ = OverBase.compatible-post q₂ G bG
(OverBase.compose-triangle q₁ x₁ bx₁ f bf) (OverBase.compose-triangle q₁ F bF x₀ bx₀) α first
s₅ = OverBase.compatible-inverse q₂ b₅ b₄ (comp-assoc x₀ F G)
(OverBase.compatible-assoc q₂ G F x₀ bG bF bx₀)
in OverBase.compatible-comp q₂ b₀ b₄ b₅ e₅ (e₄ ∙ (e₃ ∙ (e₂ ∙ e₁))) s₅
(OverBase.compatible-comp q₂ b₀ b₃ b₄ e₄ (e₃ ∙ (e₂ ∙ e₁)) s₄
(OverBase.compatible-comp q₂ b₀ b₂ b₃ e₃ (e₂ ∙ e₁) s₃
(OverBase.compatible-comp q₂ b₀ b₁ b₂ e₂ e₁ s₂ s₁)))
private
module FixedCompositorNormalization {Γ : Context} {X Y Z P : CAT Γ}
(πX : MAP X P) (πY : MAP Y P) (πZ : MAP Z P)
(F : MAP X Y) (G : MAP Y Z) (K : MAP X Z)
(ξ : (G ∘ F) =₁ K)
(βF : (πY ∘ F) =₁ (id P ∘ πX))
(βG : (πZ ∘ G) =₁ (id P ∘ πY))
(βK : (πZ ∘ K) =₁ (id P ∘ πX))
(image : SquareCell₌ (πZ ◁ ξ) (βF ∙ (comp-unitˡ πY ▷ F))
(restrict-triangle πZ G βG F) βK) where
private
raw-source = restrict-triangle πZ G βG F
unitX = comp-unitˡ πX
unitY = comp-unitˡ πY
Ainv = (comp-assoc F G πZ) ⁻¹
source = OverBase.compose-triangle πZ G (unitY ∙ βG) F (unitX ∙ βF)
target = unitX ∙ βK
private
source-normal : source =₂ (unitX ∙ ((βF ∙ (unitY ▷ F)) ∙ raw-source))
source-normal = reassociateFour unitX βF (unitY ▷ F) raw-source ∙
(comp₌-cong (id₌ (unitX ∙ βF))
(comp₌-assoc (unitY ▷ F) (βG ▷ F) Ainv) ∙
comp₌-cong (id₌ (unitX ∙ βF))
(comp₌-cong (preWhisker-comp₌ unitY βG F) (id₌ Ainv)))
compatible : (target ∙ (πZ ◁ ξ)) =₂ source
compatible = source-normal ⁻¹ ∙
(comp₌-cong (id₌ unitX) image ∙ comp₌-assoc unitX βK (πZ ◁ ξ))
module FixedProductCompositorCoordinates {Γ : Context} (P : CAT Γ)
{A B C : CAT Γ} (f : MAP A B) (g : MAP B C) where
private
Jf = product-restriction {P = P} f
Jg = product-restriction {P = P} g
Jgf = product-restriction {P = P} (g ∘ f)
Hf = productMap f (id P)
Hg = productMap g (id P)
Hgf = productMap (g ∘ f) (id P)
βJf = pair-β₁ (id P ∘ pr₁) (f ∘ pr₂)
βJg = pair-β₁ (id P ∘ pr₁) (g ∘ pr₂)
βJgf = pair-β₁ (id P ∘ pr₁) ((g ∘ f) ∘ pr₂)
βHf = pair-β₂ (f ∘ pr₁) (id P ∘ pr₂)
βHg = pair-β₂ (g ∘ pr₁) (id P ∘ pr₂)
βHgf = pair-β₂ ((g ∘ f) ∘ pr₁) (id P ∘ pr₂)
first-coordinate = post-square-cell (id P) pr₁ (id P) pr₁ Jf βJf
second-coordinate = post-square-cell g pr₂ f pr₂ Jf
(pair-β₂ (id P ∘ pr₁) (f ∘ pr₂))
J-image : SquareCell₌ (pr₁ ◁ restriction-compositor {P = P} f g)
(βJf ∙ (comp-unitˡ pr₁ ▷ Jf))
(restrict-triangle pr₁ Jg βJg Jf) βJgf
J-image = replace-edges₌ (id₌ _) (post-square-cell-id pr₁ (id P) pr₁ Jf βJf)
(lies-over-comp pr₁
(pair-evaluation-over₁-One (id P ∘ pr₁) (g ∘ pr₂) Jf first-coordinate second-coordinate)
(unconst-sides₌ (productMap-cong-triangle₁ (comp-unitˡ (id P)) (id₌ (g ∘ f)))))
H-image : SquareCell₌ (pr₂ ◁ productMap-first-comp {C = P} g f)
(βHf ∙ (comp-unitˡ pr₂ ▷ Hf))
(restrict-triangle pr₂ Hg βHg Hf) βHgf
H-image = replace-edges₌ (id₌ _) (FirstFactor.second-normalization P g f)
(FirstFactor.Coordinates.projection₂ P g f)
module J = FixedCompositorNormalization pr₁ pr₁ pr₁ Jf Jg Jgf
(restriction-compositor f g) βJf βJg βJgf J-image
using (compatible; source; target)
module H = FixedCompositorNormalization pr₂ pr₂ pr₂ Hf Hg Hgf
(productMap-first-comp g f) βHf βHg βHgf H-image
using (compatible; source; target)
restriction-source = J.source
restriction-target = J.target
first-factor-source = H.source
first-factor-target = H.target
restriction : (restriction-target ∙ (pr₁ ◁ restriction-compositor {P = P} f g)) =₂ restriction-source
restriction = J.compatible
first-factor : (first-factor-target ∙ (pr₂ ◁ productMap-first-comp {C = P} g f)) =₂ first-factor-source
first-factor = H.compatible
private
module SwapCompositorFixedCoordinate {Γ : Context} (P : CAT Γ)
{A B C : CAT Γ} (f : MAP A B) (g : MAP B C) where
private
module Sf = SwapRestriction {P = P} f
using (H; J; pA; pB; transpose-cell)
module Sg = SwapRestriction {P = P} g
using (H; J; pB; transpose-cell)
module Sgf = SwapRestriction {P = P} (g ∘ f)
using (transpose-cell)
module If = SwapRestrictionOverProjections {P = P} f
using (fixed)
module Ig = SwapRestrictionOverProjections {P = P} g
using (fixed)
module Igf = SwapRestrictionOverProjections {P = P} (g ∘ f)
using (fixed; fixed-source; fixed-target)
module K = FixedProductCompositorCoordinates P f g
using (first-factor; first-factor-source; first-factor-target; restriction; restriction-source; restriction-target)
κH = productMap-first-comp {C = P} g f
κJ = restriction-compositor {P = P} f g
module Paste = SwapProjectionPasting pr₂ pr₂ pr₂ pr₁ pr₁ pr₁
Sf.pA Sf.pB Sg.pB Sf.H Sg.H Sf.J Sg.J
(comp-unitˡ pr₂ ∙ pair-β₂ (f ∘ pr₁) (id P ∘ pr₂))
(comp-unitˡ pr₂ ∙ pair-β₂ (g ∘ pr₁) (id P ∘ pr₂))
(comp-unitˡ pr₁ ∙ pair-β₁ (id P ∘ pr₁) (f ∘ pr₂))
(comp-unitˡ pr₁ ∙ pair-β₁ (id P ∘ pr₁) (g ∘ pr₂))
(pair-β₁ pr₂ pr₁) (pair-β₁ pr₂ pr₁) (pair-β₁ pr₂ pr₁)
Sf.transpose-cell Sg.transpose-cell
using (b₀; b₅; compatible; pasted)
short = Sgf.transpose-cell ∙ (Sg.pB ◁ κH)
long = (κJ ▷ Sf.pA) ∙ Paste.pasted
private
short-compatible : (Igf.fixed-target ∙ (pr₁ ◁ short)) =₂ Paste.b₀
short-compatible = OverBase.compatible-comp pr₁ Paste.b₀ Igf.fixed-source Igf.fixed-target
Sgf.transpose-cell (Sg.pB ◁ κH) Igf.fixed
(OverBase.compatible-post pr₁ Sg.pB (pair-β₁ pr₂ pr₁)
K.first-factor-source K.first-factor-target κH K.first-factor)
long-compatible : (Igf.fixed-target ∙ (pr₁ ◁ long)) =₂ Paste.b₀
long-compatible = OverBase.compatible-comp pr₁ Paste.b₀ Paste.b₅ Igf.fixed-target
(κJ ▷ Sf.pA) Paste.pasted
(OverBase.compatible-pre pr₁ Sf.pA K.restriction-source K.restriction-target
(pair-β₁ pr₂ pr₁) κJ K.restriction)
(Paste.compatible If.fixed Ig.fixed)
comparison : (pr₁ ◁ short) =₂ (pr₁ ◁ long)
comparison = cancel-left Igf.fixed-target (long-compatible ⁻¹ ∙ short-compatible)
private
module VaryingCompositorNormalization {Γ : Context} {X Z T : CAT Γ}
(π : MAP Z T) {F K : MAP X Z} (ξ : F =₁ K)
{a b d : MAP X T} (source : (π ∘ F) =₁ a) (target : (π ∘ K) =₁ b)
(η : b =₁ d) (L : a =₁ d)
(image : SquareCell₌ (π ◁ ξ) (η ⁻¹ ∙ L) source target) where
compatible : ((η ∙ target) ∙ (π ◁ ξ)) =₂ (L ∙ source)
compatible = comp-inv-left η (L ∙ source) ∙
(comp₌-cong (id₌ η) (comp₌-assoc (η ⁻¹) L source) ∙
(comp₌-cong (id₌ η) image ∙ comp₌-assoc η target (π ◁ ξ)))
module VaryingProductCompositorCoordinates {Γ : Context} (P : CAT Γ)
{A B C : CAT Γ} (f : MAP A B) (g : MAP B C) where
private
Jf = product-restriction {P = P} f
Jg = product-restriction {P = P} g
Hf = productMap f (id P)
Hg = productMap g (id P)
βJf = pair-β₂ (id P ∘ pr₁) (f ∘ pr₂)
βJg = pair-β₂ (id P ∘ pr₁) (g ∘ pr₂)
βJgf = pair-β₂ (id P ∘ pr₁) ((g ∘ f) ∘ pr₂)
βHf = pair-β₁ (f ∘ pr₁) (id P ∘ pr₂)
βHg = pair-β₁ (g ∘ pr₁) (id P ∘ pr₂)
βHgf = pair-β₁ ((g ∘ f) ∘ pr₁) (id P ∘ pr₂)
module J = VaryingCompositorNormalization pr₂ (restriction-compositor {P = P} f g)
(restrict-triangle pr₂ Jg βJg Jf) βJgf
(comp-assoc pr₂ f g) (post-triangle g pr₂ Jf βJf)
(ProjectionCompositor.square {P = P} f g)
using (compatible)
module H = VaryingCompositorNormalization pr₁ (productMap-first-comp {C = P} g f)
(restrict-triangle pr₁ Hg βHg Hf) βHgf
(comp-assoc pr₁ f g) (post-triangle g pr₁ Hf βHf)
(FirstFactor.Coordinates.projection₁ P g f)
using (compatible)
restriction-source = OverBase.compose-triangle pr₂ Jg βJg Jf (post-triangle g pr₂ Jf βJf)
restriction-target = comp-assoc pr₂ f g ∙ βJgf
first-factor-source = OverBase.compose-triangle pr₁ Hg βHg Hf (post-triangle g pr₁ Hf βHf)
first-factor-target = comp-assoc pr₁ f g ∙ βHgf
restriction : (restriction-target ∙ (pr₂ ◁ restriction-compositor {P = P} f g)) =₂ restriction-source
restriction = J.compatible
first-factor : (first-factor-target ∙ (pr₁ ◁ productMap-first-comp {C = P} g f)) =₂ first-factor-source
first-factor = H.compatible
private
module SwapCompositorVaryingCoordinate {Γ : Context} (P : CAT Γ)
{A B C : CAT Γ} (f : MAP A B) (g : MAP B C) where
private
module Sf = SwapRestriction {P = P} f
using (H; J; pA; pB; transpose-cell)
module Sg = SwapRestriction {P = P} g
using (H; J; pB; transpose-cell)
module Sgf = SwapRestriction {P = P} (g ∘ f)
using (H; J; pB; transpose-cell)
module If = SwapRestrictionOverProjections {P = P} f
using (varying; varying-source; varying-target)
module Ig = SwapRestrictionOverProjections {P = P} g
using (varying)
module Igf = SwapRestrictionOverProjections {P = P} (g ∘ f)
using (varying; varying-source; varying-target)
module K = VaryingProductCompositorCoordinates P f g
using (first-factor; first-factor-source; first-factor-target; restriction; restriction-source; restriction-target)
κH = productMap-first-comp {C = P} g f
κJ = restriction-compositor {P = P} f g
swapA : ((pr₂ {Γ = Γ} {C = P} {D = A}) ∘ Sf.pA) =₁ (pr₁ {Γ = Γ} {C = A} {D = P})
swapA = pair-β₂ {Γ = Γ} {P = A × P} {C = P} {D = A}
(pr₂ {Γ = Γ} {C = A} {D = P}) (pr₁ {Γ = Γ} {C = A} {D = P})
swapB : ((pr₂ {Γ = Γ} {C = P} {D = B}) ∘ Sf.pB) =₁ (pr₁ {Γ = Γ} {C = B} {D = P})
swapB = pair-β₂ {Γ = Γ} {P = B × P} {C = P} {D = B}
(pr₂ {Γ = Γ} {C = B} {D = P}) (pr₁ {Γ = Γ} {C = B} {D = P})
swapC : ((pr₂ {Γ = Γ} {C = P} {D = C}) ∘ Sg.pB) =₁ (pr₁ {Γ = Γ} {C = C} {D = P})
swapC = pair-β₂ {Γ = Γ} {P = C × P} {C = P} {D = C}
(pr₂ {Γ = Γ} {C = C} {D = P}) (pr₁ {Γ = Γ} {C = C} {D = P})
Hf-base = pair-β₁ (f ∘ pr₁) (id P ∘ pr₂)
Hg-base = pair-β₁ (g ∘ pr₁) (id P ∘ pr₂)
Hgf-base = pair-β₁ ((g ∘ f) ∘ pr₁) (id P ∘ pr₂)
Jf-base = pair-β₂ (id P ∘ pr₁) (f ∘ pr₂)
Jg-base = pair-β₂ (id P ∘ pr₁) (g ∘ pr₂)
Jgf-base = pair-β₂ (id P ∘ pr₁) ((g ∘ f) ∘ pr₂)
lifted-swapA = post-triangle f pr₂ Sf.pA swapA
nested-swapA = post-triangle g (f ∘ pr₂) Sf.pA lifted-swapA
lifted-swapB = post-triangle g pr₂ Sf.pB swapB
module Paste = SwapProjectionPasting {Γ = Γ}
{X₀ = A × P} {X₁ = B × P} {X₂ = C × P}
{Y₀ = P × A} {Y₁ = P × B} {Y₂ = P × C} {T = C}
(g ∘ (f ∘ pr₁ {Γ = Γ} {C = A} {D = P})) (g ∘ pr₁ {Γ = Γ} {C = B} {D = P}) (pr₁ {Γ = Γ} {C = C} {D = P})
(g ∘ (f ∘ pr₂ {Γ = Γ} {C = P} {D = A})) (g ∘ pr₂ {Γ = Γ} {C = P} {D = B}) (pr₂ {Γ = Γ} {C = P} {D = C})
Sf.pA Sf.pB Sg.pB Sf.H Sg.H Sf.J Sg.J
(post-triangle g (pr₁ {Γ = Γ} {C = B} {D = P}) Sf.H Hf-base) Hg-base
(post-triangle g (pr₂ {Γ = Γ} {C = P} {D = B}) Sf.J Jf-base) Jg-base
nested-swapA lifted-swapB swapC Sf.transpose-cell Sg.transpose-cell
using (b₀; b₅; compatible; pasted)
ηH : ((g ∘ f) ∘ pr₁ {Γ = Γ} {C = A} {D = P}) =₁ (g ∘ (f ∘ pr₁ {Γ = Γ} {C = A} {D = P}))
ηH = comp-assoc {Γ = Γ} {B = A × P} {C = A} {D = B} {E = C}
(pr₁ {Γ = Γ} {C = A} {D = P}) f g
ηJ : ((g ∘ f) ∘ pr₂ {Γ = Γ} {C = P} {D = A}) =₁ (g ∘ (f ∘ pr₂ {Γ = Γ} {C = P} {D = A}))
ηJ = comp-assoc {Γ = Γ} {B = P × A} {C = A} {D = B} {E = C}
(pr₂ {Γ = Γ} {C = P} {D = A}) f g
final = OverBase.compose-triangle pr₂ Sgf.J K.restriction-target Sf.pA nested-swapA
middle = OverBase.compose-triangle pr₂ Sgf.pB swapC Sgf.H K.first-factor-target
first-source-normal :
OverBase.compose-triangle (g ∘ pr₂) Sf.pB lifted-swapB Sf.H (post-triangle g pr₁ Sf.H Hf-base)
=₂ post-triangle g pr₂ (Sf.pB ∘ Sf.H) If.varying-source
first-source-normal = OverBase.postcompose-compose g pr₂ Sf.pB Sf.H swapB Hf-base
first-target-normal :
OverBase.compose-triangle (g ∘ pr₂) Sf.J (post-triangle g pr₂ Sf.J Jf-base) Sf.pA nested-swapA
=₂ post-triangle g pr₂ (Sf.J ∘ Sf.pA) If.varying-target
first-target-normal = OverBase.postcompose-compose g pr₂ Sf.J Sf.pA Jf-base lifted-swapA
first-compatible : OverBase.CompatibleOver (g ∘ pr₂)
(OverBase.compose-triangle (g ∘ pr₂) Sf.pB lifted-swapB Sf.H (post-triangle g pr₁ Sf.H Hf-base))
(OverBase.compose-triangle (g ∘ pr₂) Sf.J (post-triangle g pr₂ Sf.J Jf-base) Sf.pA nested-swapA)
Sf.transpose-cell
first-compatible = first-source-normal ⁻¹ ∙
(OverBase.compatible-postcompose g pr₂ If.varying-source If.varying-target Sf.transpose-cell If.varying ∙
comp₌-cong first-target-normal (id₌ ((g ∘ pr₂) ◁ Sf.transpose-cell)))
middle-normal : middle =₂ (ηH ∙ Igf.varying-source)
middle-normal = comp₌-assoc ηH Hgf-base (restrict-triangle pr₂ Sgf.pB swapC Sgf.H)
lifted-assoc : (ηH ∙ post-triangle (g ∘ f) pr₂ Sf.pA swapA) =₂
(nested-swapA ∙ (ηJ ▷ Sf.pA))
lifted-assoc = (comp₌-assoc (g ◁ lifted-swapA)
(comp-assoc Sf.pA (f ∘ pr₂) g) (ηJ ▷ Sf.pA)) ⁻¹ ∙
post-triangle-comp g f pr₂ Sf.pA swapA
change-middle : {X Y Z T : CAT Γ} (π : MAP Z T) (k : MAP Y Z) (j : MAP X Y)
{a a′ : MAP Y T} {b b′ : MAP X T}
(base : (π ∘ k) =₁ a) (before : (a ∘ j) =₁ b)
(α : a =₁ a′) (after : (a′ ∘ j) =₁ b′) (η : b =₁ b′)
→ (η ∙ before) =₂ (after ∙ (α ▷ j))
→ OverBase.compose-triangle π k (α ∙ base) j after =₂
(η ∙ OverBase.compose-triangle π k base j before)
change-middle π k j base before α after η compatible =
let inv-assoc = (comp-assoc j k π) ⁻¹
tail = (base ▷ j) ∙ inv-assoc
in comp₌-assoc η before tail ∙
(comp₌-cong (compatible ⁻¹) (id₌ tail) ∙
((comp₌-assoc after (α ▷ j) tail) ⁻¹ ∙
comp₌-cong (id₌ after)
(comp₌-assoc (α ▷ j) (base ▷ j) inv-assoc ∙
comp₌-cong (preWhisker-comp₌ α base j) (id₌ inv-assoc))))
final-normal : final =₂ (ηH ∙ Igf.varying-target)
final-normal = change-middle pr₂ Sgf.J Sf.pA Jgf-base
(post-triangle (g ∘ f) pr₂ Sf.pA swapA) ηJ nested-swapA ηH lifted-assoc
composite-compatible : (final ∙ (pr₂ ◁ Sgf.transpose-cell)) =₂ middle
composite-compatible = middle-normal ⁻¹ ∙
(comp₌-cong (id₌ ηH) Igf.varying ∙
(comp₌-assoc ηH Igf.varying-target (pr₂ ◁ Sgf.transpose-cell) ∙
comp₌-cong final-normal (id₌ (pr₂ ◁ Sgf.transpose-cell))))
short = Sgf.transpose-cell ∙ (Sg.pB ◁ κH)
long = (κJ ▷ Sf.pA) ∙ Paste.pasted
private
short-compatible : (final ∙ (pr₂ ◁ short)) =₂ Paste.b₀
short-compatible = OverBase.compatible-comp pr₂ Paste.b₀ middle final
Sgf.transpose-cell (Sg.pB ◁ κH) composite-compatible
(OverBase.compatible-post pr₂ Sg.pB swapC
K.first-factor-source K.first-factor-target κH K.first-factor)
long-compatible : (final ∙ (pr₂ ◁ long)) =₂ Paste.b₀
long-compatible = OverBase.compatible-comp pr₂ Paste.b₀ Paste.b₅ final
(κJ ▷ Sf.pA) Paste.pasted
(OverBase.compatible-pre pr₂ Sf.pA K.restriction-source K.restriction-target
nested-swapA κJ K.restriction)
(Paste.compatible first-compatible Ig.varying)
comparison : (pr₂ ◁ short) =₂ (pr₂ ◁ long)
comparison = cancel-left final (long-compatible ⁻¹ ∙ short-compatible)
private
module FixedProductInputCoordinates {Γ : Context} (P : CAT Γ)
{A B : CAT Γ} {f g : MAP A B} (α : f =₁ g) where
private
module Normalization {X Y : CAT Γ} (π : MAP Y P) (ρ : MAP X P)
{F G : MAP X Y} (δ : F =₁ G)
(bf : (π ∘ F) =₁ (id P ∘ ρ)) (bg : (π ∘ G) =₁ (id P ∘ ρ))
(image : SquareCell₌ (π ◁ δ) (id₌ (id P) ▷ ρ) bf bg) where
raw : (bg ∙ (π ◁ δ)) =₂ bf
raw = comp₌-unitˡ-One bf ∙
(comp₌-cong (preWhisker-id₌ (id P) ρ) (id₌ bf) ∙ image)
compatible : (((comp-unitˡ ρ ∙ bg) ∙ (π ◁ δ))) =₂ (comp-unitˡ ρ ∙ bf)
compatible = comp₌-cong (id₌ (comp-unitˡ ρ)) raw ∙
comp₌-assoc (comp-unitˡ ρ) bg (π ◁ δ)
Jα = productMap-cong (id₌ (id P)) α
Hα = productMap-cong α (id₌ (id P))
Jf = product-restriction {P = P} f
Jg = product-restriction {P = P} g
Hf = productMap f (id P)
Hg = productMap g (id P)
βJf = pair-β₁ (id P ∘ pr₁) (f ∘ pr₂)
βJg = pair-β₁ (id P ∘ pr₁) (g ∘ pr₂)
βHf = pair-β₂ (f ∘ pr₁) (id P ∘ pr₂)
βHg = pair-β₂ (g ∘ pr₁) (id P ∘ pr₂)
module J = Normalization pr₁ pr₁ Jα βJf βJg
(unconst-sides₌ (productMap-cong-triangle₁ (id₌ (id P)) α))
using (compatible)
module H = Normalization pr₂ pr₂ Hα βHf βHg
(unconst-sides₌ (productMap-cong-triangle₂ α (id₌ (id P))))
using (compatible)
restriction = J.compatible
first-factor = H.compatible
module SwapRestrictionInputCompatibility {Γ : Context} (P : CAT Γ)
{A B : CAT Γ} {f g : MAP A B} (α : f =₁ g) where
private
module Sf = SwapRestriction {P = P} f
using (pA; pB; transpose-cell)
module Sg = SwapRestriction {P = P} g
using (transpose-cell)
module If = SwapRestrictionOverProjections {P = P} f
using (fixed; fixed-source; fixed-target; varying; varying-source; varying-target)
module Ig = SwapRestrictionOverProjections {P = P} g
using (fixed; fixed-source; fixed-target; varying; varying-source; varying-target)
module Fixed = FixedProductInputCoordinates P α
using (first-factor; restriction)
Jα = productMap-cong (id₌ (id P)) α
Hα = productMap-cong α (id₌ (id P))
βJf₁ = pair-β₁ (id P ∘ pr₁) (f ∘ pr₂)
βJg₁ = pair-β₁ (id P ∘ pr₁) (g ∘ pr₂)
βHf₂ = pair-β₂ (f ∘ pr₁) (id P ∘ pr₂)
βHg₂ = pair-β₂ (g ∘ pr₁) (id P ∘ pr₂)
βJf₂ = pair-β₂ (id P ∘ pr₁) (f ∘ pr₂)
βJg₂ = pair-β₂ (id P ∘ pr₁) (g ∘ pr₂)
βHf₁ = pair-β₁ (f ∘ pr₁) (id P ∘ pr₂)
βHg₁ = pair-β₁ (g ∘ pr₁) (id P ∘ pr₂)
left-route = Sg.transpose-cell ∙ (Sf.pB ◁ Hα)
right-route = (Jα ▷ Sf.pA) ∙ Sf.transpose-cell
private
left-fixed : (Ig.fixed-target ∙ (pr₁ ◁ left-route)) =₂ If.fixed-source
left-fixed = OverBase.compatible-comp pr₁ If.fixed-source Ig.fixed-source Ig.fixed-target
Sg.transpose-cell (Sf.pB ◁ Hα) Ig.fixed
(OverBase.compatible-post pr₁ Sf.pB (pair-β₁ pr₂ pr₁)
(comp-unitˡ pr₂ ∙ βHf₂) (comp-unitˡ pr₂ ∙ βHg₂) Hα Fixed.first-factor)
right-fixed : (Ig.fixed-target ∙ (pr₁ ◁ right-route)) =₂ If.fixed-source
right-fixed = OverBase.compatible-comp pr₁ If.fixed-source If.fixed-target Ig.fixed-target
(Jα ▷ Sf.pA) Sf.transpose-cell
(OverBase.compatible-pre pr₁ Sf.pA
(comp-unitˡ pr₁ ∙ βJf₁) (comp-unitˡ pr₁ ∙ βJg₁)
(pair-β₁ pr₂ pr₁) Jα Fixed.restriction) If.fixed
fixed : (pr₁ ◁ left-route) =₂ (pr₁ ◁ right-route)
fixed = cancel-left Ig.fixed-target (right-fixed ⁻¹ ∙ left-fixed)
H-variable : SquareCell₌ (pr₁ ◁ Hα) (α ▷ pr₁) βHf₁ βHg₁
H-variable = unconst-sides₌ (productMap-cong-triangle₁ α (id₌ (id P)))
J-variable : SquareCell₌ (pr₂ ◁ Jα) (α ▷ pr₂) βJf₂ βJg₂
J-variable = unconst-sides₌ (productMap-cong-triangle₂ (id₌ (id P)) α)
post-variable : SquareCell₌ (pr₂ ◁ (Sf.pB ◁ Hα)) (α ▷ pr₁)
If.varying-source Ig.varying-source
post-variable = paste-square₌
(restrict-change-square-One pr₂ Sf.pB pr₁ (pair-β₂ pr₂ pr₁) Hα) H-variable
pre-variable : SquareCell₌ (pr₂ ◁ (Jα ▷ Sf.pA)) (α ▷ pr₁)
If.varying-target Ig.varying-target
pre-variable = paste-square₌
(restrict-square-One pr₂ Jα (α ▷ pr₂) βJf₂ βJg₂ Sf.pA J-variable)
(unconst-sides₌ (post-triangle-outer α pr₂ Sf.pA (pair-β₂ pr₂ pr₁)))
left-variable : SquareCell₌ (pr₂ ◁ left-route) (α ▷ pr₁) If.varying-source Ig.varying-target
left-variable = replace-edges₌ (id₌ _) (comp₌-unitˡ-One (α ▷ pr₁))
(lies-over-comp pr₂ post-variable
((comp₌-unitˡ-One Ig.varying-source) ⁻¹ ∙ Ig.varying))
right-variable : SquareCell₌ (pr₂ ◁ right-route) (α ▷ pr₁) If.varying-source Ig.varying-target
right-variable = replace-edges₌ (id₌ _) (comp₌-unitʳ-One (α ▷ pr₁))
(lies-over-comp pr₂ ((comp₌-unitˡ-One If.varying-source) ⁻¹ ∙ If.varying) pre-variable)
varying : (pr₂ ◁ left-route) =₂ (pr₂ ◁ right-route)
varying = cancel-left Ig.varying-target (right-variable ⁻¹ ∙ left-variable)
comparison : left-route =₂ right-route
comparison = pair₌-extensionality fixed varying
private
module SwapCompositorCompatibility {Γ : Context} (P : CAT Γ)
{A B C : CAT Γ} (f : MAP A B) (g : MAP B C) where
private
module F = SwapRestriction {P = P} f
using (H; J; pA; transpose-cell)
module G = SwapRestriction {P = P} g
using (H; J; pB; transpose-cell)
module GF = SwapRestriction {P = P} (g ∘ f)
using (transpose-cell)
module Fixed = SwapCompositorFixedCoordinate P f g
using (comparison)
module Variable = SwapCompositorVaryingCoordinate P f g
using (comparison)
pasted = Square.cell (comp-square (Squares.square G.H G.J G.transpose-cell) (Squares.square F.H F.J F.transpose-cell))
comparison : (GF.transpose-cell ∙ (G.pB ◁ productMap-first-comp {C = P} g f)) =₂
((restriction-compositor {P = P} f g ▷ F.pA) ∙ pasted)
comparison = pair₌-extensionality Fixed.comparison Variable.comparison
module ProductSquareSwap {Γ : Context} (P : CAT Γ) {A B C D : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) where
private
u = Square.source-map s
v = Square.target-map s
module U = SwapRestriction {P = P} u
using (H; J; pA; pB; transpose-cell)
module L = SwapRestriction {P = P} l
using (H; J; pB; transpose-cell)
module R = SwapRestriction {P = P} r
using (H; J; pB; transpose-cell)
module V = SwapRestriction {P = P} v
using (H; J; pB; transpose-cell)
module RU = SwapRestriction {P = P} (r ∘ u)
using (transpose-cell)
module VL = SwapRestriction {P = P} (v ∘ l)
using (transpose-cell)
module H = FirstFactorSquare P s
using (middle; value; κl; κu)
module Change = ChangeSpan {E = P × D} U.J L.J U.H L.H U.pA U.pB L.pB
U.transpose-cell L.transpose-cell
using (value; module L; module R)
ρr = Change.L.ρ R.J
ρv = Change.R.ρ V.J
Ar = comp-assoc U.H R.H R.pB
Av = comp-assoc L.H V.H V.pB
α = R.transpose-cell ⁻¹ ▷ U.H
β = V.transpose-cell ⁻¹ ▷ L.H
left-total = Ar ∙ (α ∙ ρr ⁻¹)
right-total = Av ∙ (β ∙ ρv ⁻¹)
source-cell = Square.cell (product-square {P = P} s) ▷ U.pA
target-cell = R.pB ◁ Cocone.match H.value
κJu = restriction-compositor {P = P} u r ▷ U.pA
κJl = restriction-compositor {P = P} l v ▷ U.pA
κHu = R.pB ◁ H.κu
κHl = R.pB ◁ H.κl
σJ = productMap-cong (id₌ (id P)) (Square.cell s) ▷ U.pA
σH = R.pB ◁ H.middle
module CompositorLeg {X Y Z : CAT Γ} (f : MAP X Y) (g : MAP Y Z) where
private
module F = SwapRestriction {P = P} f
using (H; J; pA; pB; transpose-cell)
module G = SwapRestriction {P = P} g
using (H; J; pB; transpose-cell)
module GF = SwapRestriction {P = P} (g ∘ f)
using (transpose-cell)
module K = SwapCompositorCompatibility P f g
using (comparison; pasted)
ρ = (comp-assoc F.pA F.J G.J) ⁻¹ ∙
((G.J ◁ F.transpose-cell) ∙ comp-assoc F.H F.pB G.J)
outer-assoc = comp-assoc F.H G.H G.pB
middle-assoc = comp-assoc F.H F.pB G.J
input-assoc-inverse = (comp-assoc F.pA F.J G.J) ⁻¹
middle = G.J ◁ F.transpose-cell
tail = (G.transpose-cell ▷ F.H) ∙ outer-assoc ⁻¹
group : K.pasted =₂ (ρ ∙ tail)
group = (comp₌-assoc input-assoc-inverse (middle ∙ middle-assoc) tail) ⁻¹ ∙
comp₌-cong (id₌ input-assoc-inverse) ((comp₌-assoc middle middle-assoc tail) ⁻¹)
frame : (K.pasted ⁻¹) =₂ (outer-assoc ∙ ((G.transpose-cell ⁻¹ ▷ F.H) ∙ ρ ⁻¹))
frame = comp₌-assoc outer-assoc (G.transpose-cell ⁻¹ ▷ F.H) (ρ ⁻¹) ∙
(comp₌-cong
(comp₌-cong (inverse-inverse outer-assoc) ((preWhisker-inverse G.transpose-cell F.H) ⁻¹) ∙
inverse-composite (G.transpose-cell ▷ F.H) (outer-assoc ⁻¹)) (id₌ (ρ ⁻¹)) ∙
(inverse-composite ρ tail ∙ (inv₌ ◁ group)))
square : SquareCell₌ (restriction-compositor {P = P} f g ▷ F.pA)
(G.pB ◁ productMap-first-comp {C = P} g f)
(outer-assoc ∙ ((G.transpose-cell ⁻¹ ▷ F.H) ∙ ρ ⁻¹)) (GF.transpose-cell ⁻¹)
square = replace-sides₌ frame (id₌ (GF.transpose-cell ⁻¹))
(inverse-square₌ K.comparison)
left-square : SquareCell₌ κJu κHu left-total (RU.transpose-cell ⁻¹)
left-square = CompositorLeg.square u r
right-square : SquareCell₌ κJl κHl right-total (VL.transpose-cell ⁻¹)
right-square = CompositorLeg.square l v
middle-square : SquareCell₌ σJ σH (RU.transpose-cell ⁻¹) (VL.transpose-cell ⁻¹)
middle-square = inverse-square₌ (SwapRestrictionInputCompatibility.comparison P (Square.cell s))
source-normal : source-cell =₂ (κJl ⁻¹ ∙ (σJ ∙ κJu))
source-normal = comp₌-cong (preWhisker-inverse (restriction-compositor {P = P} l v) U.pA)
(preWhisker-comp₌ (productMap-cong (id₌ (id P)) (Square.cell s))
(restriction-compositor {P = P} u r) U.pA) ∙
preWhisker-comp₌ ((restriction-compositor {P = P} l v) ⁻¹)
(productMap-cong (id₌ (id P)) (Square.cell s) ∙ restriction-compositor {P = P} u r) U.pA
target-normal : target-cell =₂ (κHl ⁻¹ ∙ (σH ∙ κHu))
target-normal = comp₌-cong (postWhisker-inverse R.pB H.κl)
(postWhisker-comp₌ R.pB H.middle H.κu) ∙
postWhisker-comp₌ R.pB (H.κl ⁻¹) (H.middle ∙ H.κu)
raw-square : SquareCell₌ source-cell target-cell left-total right-total
raw-square = replace-edges₌ (source-normal ⁻¹) (target-normal ⁻¹)
(inv-comp-square₌ (adjoin-square₌ left-square middle-square) right-square)
source : Cocone U.H L.H (P × D)
source = Change.value (square-cocone (product-square {P = P} s))
target : Cocone U.H L.H (P × D)
target = cocone-postcompose R.pB H.value
private
source-frame-normal : changeEndpoints (ρr ⁻¹) (ρv ⁻¹) source-cell =₂ Cocone.match source
source-frame-normal = comp₌-cong (id₌ (ρv ⁻¹))
(comp₌-cong (id₌ source-cell) (inverse-inverse ρr))
target-frame-normal : changeEndpoints (Ar ⁻¹) (Av ⁻¹) target-cell =₂ Cocone.match target
target-frame-normal = comp₌-cong (id₌ (Av ⁻¹))
(comp₌-cong (id₌ target-cell) (inverse-inverse Ar))
comparison : CoconeIdentification₁ source target
comparison = record { left = R.transpose-cell ⁻¹; right = V.transpose-cell ⁻¹
; compatible = replace-sides₌ source-frame-normal target-frame-normal
(transport-square (ρr ⁻¹) (Ar ⁻¹) (ρv ⁻¹) (Av ⁻¹) source-cell target-cell
left-total right-total α β
(inv-comp-left Ar (α ∙ ρr ⁻¹)) (inv-comp-left Av (β ∙ ρv ⁻¹))
(transpose-square₌ raw-square)) }
module _ {Γ : Context} where
module TransposedOrdinarySquareEvaluation {P A B C D E : CAT Γ}
{l : MAP A C} {r : MAP B D} (s : Square l r) (g : MAP D (Fun P E)) where
private
u = Square.source-map s
module Product = ProductSquareSwap P s
using (comparison; source; target)
module H = FirstFactorSquare P s
using (value)
module T = TransposedRestrictionCocones {P = P} {E = E} u l
using (Hl; Hu; transposed)
module O = NativeOrdinaryCocones {P = P} {E = E} u l
using (represented)
product = square-cocone (product-square {P = P} s)
ordinary = square-cocone s
e = funUncurry g
pD : MAP (D × P) (P × D)
pD = swap
qD : MAP (P × D) (D × P)
qD = swap
transposed-map : MAP (P × D) E
transposed-map = e ∘ qD
source : Cocone T.Hu T.Hl E
source = T.transposed (cocone-postcompose transposed-map product)
target : Cocone T.Hu T.Hl E
target = O.represented (cocone-postcompose g ordinary)
private
commuting : CoconeIdentification₁ source (cocone-postcompose transposed-map Product.source)
commuting = change-span-postcomposition
(product-restriction {P = P} u) (product-restriction {P = P} l)
(productMap u (id P)) (productMap l (id P))
(SwapRestriction.pA {P = P} u) (SwapRestriction.pB {P = P} u) (SwapRestriction.pB {P = P} l)
(SwapRestriction.transpose-cell {P = P} u) (SwapRestriction.transpose-cell {P = P} l)
transposed-map product
swapped : CoconeIdentification₁
(cocone-postcompose transposed-map Product.source)
(cocone-postcompose transposed-map Product.target)
swapped = fixed-postcomposition transposed-map Product.comparison
associated : CoconeIdentification₁
(cocone-postcompose transposed-map Product.target)
(cocone-postcompose (transposed-map ∘ pD) H.value)
associated = inverse-cocone₁ (postcompose-assoc H.value pD transposed-map)
swap-beta : (transposed-map ∘ pD) =₁ e
swap-beta = comp-unitʳ e ∙ ((e ◁ swap-swap D P) ∙ comp-assoc pD qD e)
restored : CoconeIdentification₁ (cocone-postcompose (transposed-map ∘ pD) H.value)
(cocone-postcompose e H.value)
restored = postcomposition-cong₁ H.value swap-beta
comparison : CoconeIdentification₁ source target
comparison = compose-cocone₁
(inverse-cocone₁ (OrdinaryFirstFactorSquareEvaluation.comparison s g))
(compose-cocone₁ restored (compose-cocone₁ associated (compose-cocone₁ swapped commuting)))
module NativeOrdinaryReflectedCocone {Γ : Context} {X P A B C E : CAT Γ}
(u : MAP A B) (l : MAP A C) (s t : Cocone u l (Fun P E))
(Φ : CoconeIdentification X
(NativeOrdinaryCocones.represented {P = P} {E = E} u l s)
(NativeOrdinaryCocones.represented {P = P} {E = E} u l t)) where
private
e = funEval {C = P} {D = E}
Ju = productMap u (id P)
Jl = productMap l (id P)
open Terms.Equalities X using (_＝_)
left : Cocone.left s ＝ Cocone.left t
left = reflect e (funUniversal P E) (Cocone.left s) (Cocone.left t) (CoconeIdentification.left Φ)
right : Cocone.right s ＝ Cocone.right t
right = reflect e (funUniversal P E) (Cocone.right s) (Cocone.right t) (CoconeIdentification.right Φ)
left-image : evaluate⁼ e left =₁ CoconeIdentification.left Φ
left-image = reflect-β e (funUniversal P E) (Cocone.left s) (Cocone.left t) (CoconeIdentification.left Φ)
right-image : evaluate⁼ e right =₁ CoconeIdentification.right Φ
right-image = reflect-β e (funUniversal P E) (Cocone.right s) (Cocone.right t) (CoconeIdentification.right Φ)
private
left-square : SquareCell₌ (evaluate⁼ e (left ▷ u)) (CoconeIdentification.left Φ ▷ Ju)
(const (evaluate-restrict e (Cocone.left s) u)) (const (evaluate-restrict e (Cocone.left t) u))
left-square = replace-edges₌ (id₌ (evaluate⁼ e (left ▷ u)))
(preWhisker Ju ◁ left-image) (evaluate-restrict-inputs e left u)
right-square : SquareCell₌ (evaluate⁼ e (right ▷ l)) (CoconeIdentification.right Φ ▷ Jl)
(const (evaluate-restrict e (Cocone.right s) l)) (const (evaluate-restrict e (Cocone.right t) l))
right-square = replace-edges₌ (id₌ (evaluate⁼ e (right ▷ l)))
(preWhisker Jl ◁ right-image) (evaluate-restrict-inputs e right l)
source-boundary = const {P = X} (Cocone.match t) ∙ (left ▷ u)
target-boundary = (right ▷ l) ∙ const {P = X} (Cocone.match s)
native-action = evaluation-action e (Cocone.left s ∘ u) (Cocone.right t ∘ l)
wanted-image : (native-action ∘ source-boundary) =₁ (native-action ∘ target-boundary)
wanted-image = framed-matching-image e (Cocone.match s) (Cocone.match t) (left ▷ u) (right ▷ l)
(evaluate-restrict e (Cocone.left s) u) (evaluate-restrict e (Cocone.right s) l)
(evaluate-restrict e (Cocone.left t) u) (evaluate-restrict e (Cocone.right t) l)
left-square right-square (CoconeIdentification.compatible Φ)
matching-factor : Fact.Factorization (postWhisker native-action) wanted-image
matching-factor = evaluation-reflection₂ e (funUniversal P E)
source-boundary target-boundary wanted-image
compatible : SquareCell₌ (left ▷ u) (right ▷ l) (const (Cocone.match s)) (const (Cocone.match t))
compatible = Fact.factor matching-factor
matching-image : (postWhisker native-action ∘ compatible) =₁ wanted-image
matching-image = Fact.triangle matching-factor
value : CoconeIdentification X s t
value = record { left = left; right = right; compatible = compatible }
```