Other Agda modules in this section (52)
Corresponding book passages
# Associativity with specified endpoints
For three composable morphism families, glue the first composite triangle
to its source-unit triangle, and the second composite triangle to its
target-unit triangle. The two squares share the original middle arrow.
Their horizontal composition has the two bracketings as horizontal edges
and the original identity families as vertical edges.
This is the square construction in `prop:Composition_Is_Associative`.
All data are families in an arbitrary categorical parameter `P`; the
framed-square interface retains every prescribed endpoint comparison.
The endpoint-preserving commutativity comparison for that square, followed
by the two unit comparisons, identifies the bottom edge with the top edge.
Taking `P` to be the category of composable triples gives naturality.
```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
open import SCT.VolumeI.Chapter01.Section01.Vocabulary
open Operations
open import SCT.VolumeI.Chapter01.Section02.Coherence using (id₌; comp-assoc; module Composition)
open Composition
open import SCT.VolumeI.Chapter01.Section02.Specialization using (comp₌-cong)
open import SCT.VolumeI.Chapter01.Section02.Products using (module Calculus)
open Calculus using (pair)
open import SCT.VolumeI.Chapter01.Section03.Identifications.Inverses using (comp₌-unitˡ-One)
open import SCT.VolumeI.Chapter01.Section03.Products.Pairing using (pair⁼-id-One)
open import SCT.VolumeI.Chapter01.Section03.Products.PairingRestriction using (pair-evaluation-natural-One)
open import SCT.VolumeI.Chapter01.Section03.RelativeFunctors
using (category-over; FunctorOverBase; functor-over)
open import SCT.VolumeI.Chapter01.Section03.Identifications.OverBase
using (CompatibleOver; IdentificationOver; compatible-to-over)
open import SCT.VolumeI.Chapter01.Section06.Cones using (Cone; cone-restrict)
open import SCT.VolumeI.Chapter01.Section06.Pullbacks
using (Pullback; pullback-cone; pullback₁; pullback₂; pullback-match)
open import SCT.VolumeI.Chapter02.Section01.Morphisms
using (Ar; ev₀; ev₁; MorphismFamily; MorphismFamilyIdentification; identity-family)
open import SCT.VolumeI.Chapter02.Section01.MorphismFamilyOperations using (module FamilyComparison)
open import SCT.VolumeI.Chapter02.Section01.MorphismFamilyComparisons
using (compose-family-comparisons; inverse-family-comparison)
open import SCT.VolumeI.Chapter02.Section01.MorphismFraming using (endpoint-triangle)
open import SCT.VolumeI.Chapter02.Section01.Triangles using (Composable)
open import SCT.VolumeI.Chapter02.Section02.SegalAxiom using (segal-isEquiv)
import SCT.VolumeI.Chapter02.Section02.MorphismComposition as MC
open MC using (module ComposableFamilies)
open import SCT.VolumeI.Chapter02.Section02.SegalComposition using (module ChosenComposition)
open import SCT.VolumeI.Chapter02.Section02.MorphismCompositionComparisons
using (module CompositionComparisons)
open import SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits
using (module FamilyUnitPresentations; module MorphismCompositionUnits)
open import SCT.VolumeI.Chapter02.Section02.GluedFramedSquares
using (module Glue)
open import SCT.VolumeI.Chapter02.Section02.FramedSquares
using (FramedSquare; module SquareComposition)
import SCT.VolumeI.Chapter02.Section02.FramedSquareCommutativity as SquareCommutativity
private
module _ {Γ : Context} {P C : CAT Γ} {x w : MAP P C} where
family-comparison-over-endpoints : (alpha beta : MorphismFamily x w)
→ MorphismFamilyIdentification One alpha beta
→ IdentificationOver {A = One}
{X = category-over P (pair x w)}
{Y = category-over (Ar C) (pair ev₀ ev₁)}
(functor-over (MorphismFamily.arrow alpha) (endpoint-triangle alpha))
(functor-over (MorphismFamily.arrow beta) (endpoint-triangle beta))
family-comparison-over-endpoints alpha beta given = record
{ identification = Compared.identification
; over = compatible-to-over paired-compatible }
where
module A = MorphismFamily alpha
module B = MorphismFamily beta
module Compared = FamilyComparison given using (identification; source; target)
paired-compatible : CompatibleOver (pair ev₀ ev₁)
(endpoint-triangle alpha) (endpoint-triangle beta) Compared.identification
paired-compatible = comp₌-unitˡ-One (endpoint-triangle alpha) ∙
(comp₌-cong (pair⁼-id-One x w) (id₌ (endpoint-triangle alpha)) ∙
pair-evaluation-natural-One ev₀ ev₁ Compared.identification
A.source-frame B.source-frame A.target-frame B.target-frame
(id₌ x) (id₌ w)
((comp₌-unitˡ-One A.source-frame) ⁻¹ ∙ Compared.source)
((comp₌-unitˡ-One A.target-frame) ⁻¹ ∙ Compared.target))
module AssociativitySquare {Γ : Context} {P C : CAT Γ}
{x y z w : MAP P C}
(alpha : MorphismFamily x y) (beta : MorphismFamily y z)
(gamma : MorphismFamily z w) where
private
module Chosen = MC.Composition C (segal-isEquiv C) using (compose)
module Presentations = CompositionComparisons C (segal-isEquiv C)
using (composition-presentation)
first-composite : MorphismFamily x z
first-composite = Chosen.compose beta alpha
second-composite : MorphismFamily y w
second-composite = Chosen.compose gamma beta
first-square : FramedSquare alpha beta (identity-family x) first-composite
first-square = Glue.value
(Presentations.composition-presentation beta alpha)
(FamilyUnitPresentations.source first-composite)
second-square : FramedSquare second-composite (identity-family w) beta gamma
second-square = Glue.value
(FamilyUnitPresentations.target second-composite)
(Presentations.composition-presentation gamma beta)
top : MorphismFamily x w
top = Chosen.compose second-composite alpha
bottom : MorphismFamily x w
bottom = Chosen.compose gamma first-composite
value : FramedSquare top (identity-family w) (identity-family x) bottom
value = SquareComposition.Compose.value C (segal-isEquiv C)
(segal-isEquiv (Ar C)) first-square second-square
module _ {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C} where
associativity : (alpha : MorphismFamily x y) (beta : MorphismFamily y z)
(gamma : MorphismFamily z w)
→ MorphismFamilyIdentification One
(MC.Composition.compose C (segal-isEquiv C) gamma
(MC.Composition.compose C (segal-isEquiv C) beta alpha))
(MC.Composition.compose C (segal-isEquiv C)
(MC.Composition.compose C (segal-isEquiv C) gamma beta) alpha)
associativity alpha beta gamma = compose-family-comparisons
(MorphismCompositionUnits.target-unit C (segal-isEquiv C) Square.top)
(compose-family-comparisons
(SquareCommutativity.comparison C (segal-isEquiv C) Square.value)
(inverse-family-comparison
(MorphismCompositionUnits.source-unit C (segal-isEquiv C) Square.bottom)))
where
module Square = AssociativitySquare alpha beta gamma using (top; bottom; value)
```
## The universal composable triple
The iterated pullback below retains its actual two matching identifications.
The second and third universal arrows use their inverses as source frames.
The input cones for chosen composition are then formed from these framed
families, and their complete factorization comparisons are retained. They
are not silently identified with another choice of triple projections.
```agda
module UniversalTriple {Γ : Context} (C : CAT Γ) where
private
pair-target : MAP (Composable C) C
pair-target = ev₁ ∘ pullback₂ {f = ev₁ {C = C}} {g = ev₀}
Triples : CAT Γ
Triples = Pullback pair-target (ev₀ {C = C})
pairs : MAP Triples (Composable C)
pairs = pullback₁ {f = pair-target} {g = ev₀ {C = C}}
third-arrow : MAP Triples (Ar C)
third-arrow = pullback₂ {f = pair-target} {g = ev₀ {C = C}}
first-pair : Cone (ev₁ {C = C}) ev₀ Triples
first-pair = cone-restrict pairs (pullback-cone (ev₁ {C = C}) ev₀)
first-arrow : MAP Triples (Ar C)
first-arrow = Cone.left first-pair
second-arrow : MAP Triples (Ar C)
second-arrow = Cone.right first-pair
first-matching : (ev₁ ∘ first-arrow) =₁ (ev₀ ∘ second-arrow)
first-matching = Cone.match first-pair
second-matching : (pair-target ∘ pairs) =₁ (ev₀ ∘ third-arrow)
second-matching = pullback-match {f = pair-target} {g = ev₀ {C = C}}
x y z w : MAP Triples C
x = ev₀ ∘ first-arrow
y = ev₁ ∘ first-arrow
z = ev₁ ∘ second-arrow
w = ev₁ ∘ third-arrow
first : MorphismFamily x y
first = record { arrow = first-arrow; source-frame = id₌ x; target-frame = id₌ y }
second : MorphismFamily y z
second = record
{ arrow = second-arrow; source-frame = first-matching ⁻¹; target-frame = id₌ z }
third : MorphismFamily z w
third = record
{ arrow = third-arrow
; source-frame = comp-assoc pairs (pullback₂ {f = ev₁ {C = C}} {g = ev₀}) ev₁ ∙
(second-matching ⁻¹)
; target-frame = id₌ w }
private
module Chosen = MC.Composition C (segal-isEquiv C) using (compose)
first-composite : MorphismFamily x z
first-composite = Chosen.compose second first
second-composite : MorphismFamily y w
second-composite = Chosen.compose third second
module FirstInput = ComposableFamilies first second using (cone; pair-map; pair-image)
module SecondInput = ComposableFamilies second third using (cone; pair-map; pair-image)
module LeftInput = ComposableFamilies first second-composite using (cone; pair-map; pair-image)
module RightInput = ComposableFamilies first-composite third using (cone; pair-map; pair-image)
left-bracketing right-bracketing : MorphismFamily x w
left-bracketing = Chosen.compose third first-composite
right-bracketing = Chosen.compose second-composite first
comparison : MorphismFamilyIdentification One left-bracketing right-bracketing
comparison = associativity first second third
left-functor right-functor : MAP Triples (Ar C)
left-functor = ChosenComposition.composition C (segal-isEquiv C) ∘ RightInput.pair-map
right-functor = ChosenComposition.composition C (segal-isEquiv C) ∘ LeftInput.pair-map
left-over : FunctorOverBase (category-over Triples (pair x w))
(category-over (Ar C) (pair ev₀ ev₁))
left-over = functor-over left-functor (endpoint-triangle left-bracketing)
right-over : FunctorOverBase (category-over Triples (pair x w))
(category-over (Ar C) (pair ev₀ ev₁))
right-over = functor-over right-functor (endpoint-triangle right-bracketing)
naturality : IdentificationOver {A = One} left-over right-over
naturality = family-comparison-over-endpoints left-bracketing right-bracketing comparison
```