Other Agda modules in this section (52)
Corresponding book passages
# The boundary of a chosen completion
The Segal construction uses the inverse of the triangle comparison. Its
complete short-edge comparison follows from the whole cone beta and the
chosen right inverse law. In particular, the junction matching is retained.
The base triangle and its compatibility are supplied separately by the
relative inverse laws.
```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.SegalComposition where
open import SCT.VolumeI.Chapter01.Section01.Vocabulary
open Operations
open import SCT.VolumeI.Chapter01.Section02.Coherence using (module Composition)
open Composition
open import SCT.VolumeI.Chapter01.Section06.Cones
open import SCT.VolumeI.Chapter01.Section06.ConeIdentifications
open import SCT.VolumeI.Chapter01.Section06.Pullbacks
open import SCT.VolumeI.Chapter01.Section06.PullbackSquares using (IsPullback)
private
module _ {Γ : Context} {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} where
inverse-cone-comparison : (s : Cone f g T) (e : IsPullback s)
→ ConeIdentification₁
(cone-restrict (IsEquiv.inverse e) s) (pullback-cone f g)
inverse-cone-comparison s e =
cone-compose (cone-restrict-id (pullback-cone f g))
(cone-compose
(cone-action-One (pullback-cone f g) ((IsEquiv.right-inverse-law e) ⁻¹))
(cone-compose
(cone-restrict-assoc (IsEquiv.inverse e) (pullback-factor s) (pullback-cone f g))
(cone-inverse
(cone-identification-restrict-One (IsEquiv.inverse e) (pullback-factor-β s)))))
```
The Segal equivalence chooses completion over all three vertices. Its
right and left laws retain the base triangles. Passing to the long edge
gives composition over the outer two vertices. A prescribed triangle is
compared with this completion from a supplied complete short-edge
comparison over the three vertices.
This construction takes the exact Segal equivalence as input. It does
not postulate that equivalence or derive it from weaker data.
```agda
open import SCT.VolumeI.Chapter01.Section01.Vocabulary
open Operations
open import SCT.VolumeI.Chapter01.Section02.Coherence
using (id₌; comp-assoc; comp-unitˡ; module Composition)
open Composition
open import SCT.VolumeI.Chapter01.Section02.Specialization using (comp₌-assoc; comp₌-cong)
open import SCT.VolumeI.Chapter01.Section03.RelativeFunctors
open import SCT.VolumeI.Chapter01.Section03.Identifications.OverBase
open import SCT.VolumeI.Chapter01.Section09.RelativeInverseLaws
open import SCT.VolumeI.Chapter02.Section01.Triangles
open import SCT.VolumeI.Chapter02.Section01.Morphisms using (Ar; ev₀; ev₁)
private
module PrescribedTriangle {Γ : Context} {S : CAT Γ}
{triangles pairs family : CategoryOverBase S}
(q : FunctorOverBase triangles pairs)
(e : IsEquiv (FunctorOverBase.functor q))
(σ : FunctorOverBase family triangles)
(p : FunctorOverBase family pairs)
(given : IdentificationOver {A = One} (comp-over q σ) p) where
completion : FunctorOverBase family triangles
completion = comp-over (inverse-over q e) p
short-edge-image : IdentificationOver {A = One}
(comp-over q completion) (comp-over q σ)
short-edge-image = comp-identification-over
(inverse-identification-over given)
(comp-identification-over
(identification-over (comp-unitˡ (FunctorOverBase.functor p))
(identification-over-unitˡ p))
(comp-identification-over
(identification-over
(IdentificationOver.identification (RelativeInverse.right-law q e) ▷
FunctorOverBase.functor p)
(identification-over-pre p
(IdentificationOver.over (RelativeInverse.right-law q e))))
(inverse-identification-over
(identification-over
(comp-assoc (FunctorOverBase.functor p)
(IsEquiv.inverse e) (FunctorOverBase.functor q))
(identification-over-assoc q (inverse-over q e) p)))))
module Comparison = RelativeCancellation q e completion σ short-edge-image
triangle : IdentificationOver {A = One} completion σ
triangle = Comparison.value
image : (FunctorOverBase.functor q ◁ IdentificationOver.identification triangle)
=₂ IdentificationOver.identification short-edge-image
image = Comparison.image
long-edge-cell-image : {Γ : Context} {S B : CAT Γ}
(k : MAP S B) {X Y : CategoryOverBase S} {Z : CategoryOverBase B}
(H : FunctorOverMap k Y Z) (F : FunctorOverBase X Y)
→ FunctorOverBase.cell (comp-over H (postcompose-over k F)) =₂
FunctorOverBase.cell (comp-over-map k H F)
long-edge-cell-image k {Y = Y} {Z} H F =
comp₌-assoc (k ◁ FunctorOverBase.cell F)
(comp-assoc (FunctorOverBase.functor F) (CategoryOverBase.map Y) k)
((FunctorOverBase.cell H ▷ FunctorOverBase.functor F) ∙
(comp-assoc (FunctorOverBase.functor F)
(FunctorOverBase.functor H) (CategoryOverBase.map Z)) ⁻¹)
module LongEdgeComparison {Γ : Context} {S B : CAT Γ}
(k : MAP S B) {triangles family : CategoryOverBase S}
{arrows : CategoryOverBase B}
(long-edge : FunctorOverMap k triangles arrows)
{U V : FunctorOverBase family triangles}
(α : IdentificationOver {A = One} U V) where
private
ordinary : (F : FunctorOverBase family triangles)
→ FunctorOverBase (postcompose-base k family) arrows
ordinary F = comp-over long-edge (postcompose-over k F)
cell-image : (F : FunctorOverBase family triangles)
→ FunctorOverBase.cell (ordinary F) =₂
FunctorOverBase.cell (comp-over-map k long-edge F)
cell-image = long-edge-cell-image k {X = family} long-edge
ordinary-over : IsIdentificationOver (ordinary U) (ordinary V)
(FunctorOverBase.functor long-edge ◁ IdentificationOver.identification α)
ordinary-over = identification-over-post long-edge
(identification-over-postcompose k (IdentificationOver.over α))
value : IdentificationOver {A = One}
(comp-over-map k long-edge U) (comp-over-map k long-edge V)
value = identification-over
(FunctorOverBase.functor long-edge ◁ IdentificationOver.identification α)
(compatible-to-over
(cell-image U ∙
(over-to-compatible ordinary-over ∙
comp₌-cong ((cell-image V) ⁻¹)
(id₌ (CategoryOverBase.map arrows ◁
(FunctorOverBase.functor long-edge ◁ IdentificationOver.identification α))))))
module LongEdgeAssociation {Γ : Context} {S B : CAT Γ}
(k : MAP S B) {X Y Z : CategoryOverBase S} {W : CategoryOverBase B}
(H : FunctorOverMap k Z W) (G : FunctorOverBase Y Z)
(F : FunctorOverBase X Y) where
private
f = FunctorOverBase.functor F
g = FunctorOverBase.functor G
h = FunctorOverBase.functor H
π = CategoryOverBase.map W
F′ = postcompose-over k F
G′ = postcompose-over k G
HG = comp-over-map k H G
left-cell : FunctorOverBase.cell (comp-over (comp-over H G′) F′) =₂
FunctorOverBase.cell (comp-over-map k HG F)
left-cell = long-edge-cell-image k HG F ∙
comp₌-cong (id₌ (FunctorOverBase.cell F′))
(comp₌-cong (preWhisker f ◁ long-edge-cell-image k H G)
(id₌ ((comp-assoc f (h ∘ g) π) ⁻¹)))
right-cell : FunctorOverBase.cell (comp-over H (comp-over G′ F′)) =₂
FunctorOverBase.cell (comp-over-map k H (comp-over G F))
right-cell = long-edge-cell-image k H (comp-over G F) ∙
comp₌-cong
(postcompose-compose k (CategoryOverBase.map Z) g f
(FunctorOverBase.cell G) (FunctorOverBase.cell F))
(id₌ ((FunctorOverBase.cell H ▷ (g ∘ f)) ∙
((comp-assoc (g ∘ f) h π) ⁻¹)))
value : IdentificationOver {A = One}
(comp-over-map k (comp-over-map k H G) F)
(comp-over-map k H (comp-over G F))
value = identification-over (comp-assoc f g h)
(compatible-to-over
(left-cell ∙
(over-to-compatible (identification-over-assoc H G′ F′) ∙
comp₌-cong (right-cell ⁻¹) (id₌ (π ◁ comp-assoc f g h)))))
module CompositionFromTriangle {Γ : Context} {S B : CAT Γ}
(k : MAP S B) {triangles pairs family : CategoryOverBase S}
{arrows : CategoryOverBase B}
(long-edge : FunctorOverMap k triangles arrows)
(q : FunctorOverBase triangles pairs)
(e : IsEquiv (FunctorOverBase.functor q))
(σ : FunctorOverBase family triangles)
(p : FunctorOverBase family pairs)
(given : IdentificationOver {A = One} (comp-over q σ) p) where
private
module Chosen = PrescribedTriangle q e σ p given
value : IdentificationOver {A = One}
(comp-over-map k (comp-over-map k long-edge (inverse-over q e)) p)
(comp-over-map k long-edge σ)
value = comp-identification-over
(LongEdgeComparison.value k long-edge Chosen.triangle)
(LongEdgeAssociation.value k long-edge (inverse-over q e) p)
module ChosenComposition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) where
completion-over : FunctorOverBase (pairs-over C) (triangles-over C)
completion-over = inverse-over (short-edges-over C) segal
completion : MAP (Composable C) (Triangles C)
completion = FunctorOverBase.functor completion-over
completion-image : ConeIdentification₁
(cone-restrict completion (triangle-cone C)) (pullback-cone (ev₁ {C = C}) ev₀)
completion-image = inverse-cone-comparison (triangle-cone C) segal
completion-right-law : IdentificationOver {A = One}
(comp-over (short-edges-over C) completion-over) (id-over (pairs-over C))
completion-right-law = RelativeInverse.right-law (short-edges-over C) segal
completion-left-law : IdentificationOver {A = One}
(comp-over completion-over (short-edges-over C)) (id-over (triangles-over C))
completion-left-law = RelativeInverse.left-law (short-edges-over C) segal
composition-over : FunctorOverMap outer-vertices (pairs-over C) (arrows-over C)
composition-over = comp-over-map outer-vertices (long-edge-over C) completion-over
composition : MAP (Composable C) (Ar C)
composition = FunctorOverBase.functor composition-over
module PresentedTriangle {family : CategoryOverBase (Vertices C)}
(σ : FunctorOverBase family (triangles-over C))
(p : FunctorOverBase family (pairs-over C))
(given : IdentificationOver {A = One} (comp-over (short-edges-over C) σ) p) where
private
module Chosen = PrescribedTriangle (short-edges-over C) segal σ p given
triangle : IdentificationOver {A = One} (comp-over completion-over p) σ
triangle = Chosen.triangle
short-edge-image : IdentificationOver {A = One}
(comp-over (short-edges-over C) (comp-over completion-over p))
(comp-over (short-edges-over C) σ)
short-edge-image = Chosen.short-edge-image
image : (short-edges C ◁ IdentificationOver.identification triangle)
=₂ IdentificationOver.identification short-edge-image
image = Chosen.image
composite : IdentificationOver {A = One}
(comp-over-map outer-vertices composition-over p)
(comp-over-map outer-vertices (long-edge-over C) σ)
composite = CompositionFromTriangle.value outer-vertices (long-edge-over C)
(short-edges-over C) segal σ p given
```
The image law identifies the actual whiskered identification terms. Both
comparisons separately retain their complete base laws; no higher equality
of the entire relative records is inferred. Units and preservation of
composition must supply the complete relative short-edge comparison,
including its base compatibility, before using PresentedTriangle.