Other Agda modules in this section (52)
Corresponding book passages
# Framed squares as morphisms in the arrow category
A framed square is a morphism between its left and right arrow families.
Evaluating at the two interval endpoints gives its horizontal sides. Their
comparisons with the prescribed top and bottom are comparisons of framed
families, so they include all four corner equations.
Horizontal composition is composition in the arrow category. Preservation
under evaluation and change of endpoint frames identify the resulting top
and bottom with the prescribed composites. This is the algebra of squares;
constructing such data by gluing geometric triangles is a separate step.
```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.FramedSquares where
open import SCT.VolumeI.Chapter01.Section01.Vocabulary
open Operations
import Agda.Builtin.Sigma as Data
open import SCT.VolumeI.Chapter02.Section01.Morphisms
using (Ar; ev₀; ev₁; MorphismFamily; MorphismFamilyIdentification)
open import SCT.VolumeI.Chapter02.Section01.MorphismFunctor using (map-morphism-family)
open import SCT.VolumeI.Chapter02.Section01.MorphismFamilyOperations
using (retarget-family; retarget-family-comparison)
open import SCT.VolumeI.Chapter02.Section01.MorphismFamilyComparisons using (compose-family-comparisons)
open import SCT.VolumeI.Chapter02.Section01.Triangles using (short-edges)
open import SCT.VolumeI.Chapter02.Section02.MorphismCompositionComparisons using (module CompositionComparisons)
open import SCT.VolumeI.Chapter02.Section02.MorphismCompositionTransport using (module CompositionTransport)
open import SCT.VolumeI.Chapter02.Section02.MorphismCompositionPostcomposition using (module FunctorComposition)
import SCT.VolumeI.Chapter02.Section02.MorphismComposition as MC
module _ {Γ : Context} where
framed-image : {P C D : CAT Γ} (F : MAP C D) {f g : MAP P C}
(alpha : MorphismFamily f g) {x y : MAP P D}
→ (F ∘ f) =₁ x → (F ∘ g) =₁ y → MorphismFamily x y
framed-image F alpha p q = retarget-family (map-morphism-family F alpha) p q
FramedSquare : {P C : CAT Γ} {x y z w : MAP P C}
(top : MorphismFamily x y) (right : MorphismFamily y z)
(left : MorphismFamily x w) (bottom : MorphismFamily w z) → Set m
FramedSquare {C = C} top right left bottom =
Data.Σ (MorphismFamily (MorphismFamily.arrow left) (MorphismFamily.arrow right)) λ vertical →
Data.Σ (MorphismFamilyIdentification One
(framed-image (ev₀ {C = C}) vertical (MorphismFamily.source-frame left)
(MorphismFamily.source-frame right)) top) λ _ →
MorphismFamilyIdentification One
(framed-image (ev₁ {C = C}) vertical (MorphismFamily.target-frame left)
(MorphismFamily.target-frame right)) bottom
framed-square : {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
(vertical : MorphismFamily (MorphismFamily.arrow left) (MorphismFamily.arrow right))
→ MorphismFamilyIdentification One
(framed-image (ev₀ {C = C}) vertical (MorphismFamily.source-frame left)
(MorphismFamily.source-frame right)) top
→ MorphismFamilyIdentification One
(framed-image (ev₁ {C = C}) vertical (MorphismFamily.target-frame left)
(MorphismFamily.target-frame right)) bottom
→ FramedSquare top right left bottom
framed-square vertical top bottom = Data._,_ vertical (Data._,_ top bottom)
module SquareFamily {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
(given : FramedSquare top right left bottom) where
vertical : MorphismFamily (MorphismFamily.arrow left) (MorphismFamily.arrow right)
vertical = Data.fst given
top-edge : MorphismFamilyIdentification One
(framed-image (ev₀ {C = C}) vertical (MorphismFamily.source-frame left)
(MorphismFamily.source-frame right)) top
top-edge = Data.fst (Data.snd given)
bottom-edge : MorphismFamilyIdentification One
(framed-image (ev₁ {C = C}) vertical (MorphismFamily.target-frame left)
(MorphismFamily.target-frame right)) bottom
bottom-edge = Data.snd (Data.snd given)
module SquareComposition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) (arrow-segal : IsEquiv (short-edges (Ar C))) where
private
module Base = MC.Composition C segal
module Arrow = MC.Composition (Ar C) arrow-segal
module Comparisons = CompositionComparisons C segal
module Transport = CompositionTransport C segal
evaluated-composition : {P : CAT Γ} {l k r : MAP P (Ar C)}
(B : MorphismFamily k r) (A : MorphismFamily l k) (v : MAP (Ar C) C)
{x y z : MAP P C} (p : (v ∘ l) =₁ x) (q : (v ∘ k) =₁ y) (s : (v ∘ r) =₁ z)
→ MorphismFamilyIdentification One (framed-image v (Arrow.compose B A) p s)
(Base.compose (framed-image v B q s) (framed-image v A p q))
evaluated-composition B A v p q s = compose-family-comparisons
(Transport.retarget-composition (map-morphism-family v B) (map-morphism-family v A) p q s)
(retarget-family-comparison p s
(FunctorComposition.preserves-composition v arrow-segal segal B A))
module Compose {P : CAT Γ} {x₀ x₁ x₂ y₀ y₁ y₂ : MAP P C}
{top₀ : MorphismFamily x₀ x₁} {top₁ : MorphismFamily x₁ x₂}
{bottom₀ : MorphismFamily y₀ y₁} {bottom₁ : MorphismFamily y₁ y₂}
{left : MorphismFamily x₀ y₀} {middle : MorphismFamily x₁ y₁} {right : MorphismFamily x₂ y₂}
(A : FramedSquare top₀ middle left bottom₀) (B : FramedSquare top₁ right middle bottom₁) where
private
module S = SquareFamily A
module T = SquareFamily B
module L = MorphismFamily left
module M = MorphismFamily middle
module R = MorphismFamily right
value : FramedSquare (Base.compose top₁ top₀) right left (Base.compose bottom₁ bottom₀)
value = framed-square (Arrow.compose T.vertical S.vertical)
(compose-family-comparisons (Comparisons.composition-comparison T.top-edge S.top-edge)
(evaluated-composition T.vertical S.vertical ev₀ L.source-frame M.source-frame R.source-frame))
(compose-family-comparisons (Comparisons.composition-comparison T.bottom-edge S.bottom-edge)
(evaluated-composition T.vertical S.vertical ev₁ L.target-frame M.target-frame R.target-frame))
```