Other Agda modules in this section (28)
# Encoding and restricting cone identifications
The two leg identification animae map into the identification anima between
opposite corners. Their maps are the specified composites with the two cone
matchings. Encoding and decoding transport along their evaluation triangles.
The higher decoding law retains the square between matching compatibilities.
```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.ConeIdentifications where
open import SCT.VolumeI.Chapter01.Section01.Vocabulary hiding (_＝_)
import SCT.VolumeI.Chapter01.Section01.Terms as Terms
open Terms using (Equal)
open Operations
open import SCT.VolumeI.Chapter01.Section01.Terminal using (terminate; module Constructions)
open Constructions
open import SCT.VolumeI.Chapter01.Section02.Coherence
using (id₌; postWhisker-id₌; 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.Whiskering using (whisker-mixed)
open import SCT.VolumeI.Chapter01.Section02.IdentificationSquares
open import SCT.VolumeI.Chapter01.Section03.Identifications.EndpointTransport
using (transport-square; cancel-endpoint-changes)
open import SCT.VolumeI.Chapter01.Section03.Identifications.FunctorCoherence
using (whisker-mixed-One; pentagon-whiskered-right; right-unitor-comp)
open import SCT.VolumeI.Chapter01.Section03.Equivalences using (terminal-unique₂)
open import SCT.VolumeI.Chapter01.Section03.Identifications.Triangles using (post-triangle-inner; restrict-triangle; restrict-triangle-id; restrict-triangle-assoc)
open import SCT.VolumeI.Chapter01.Section03.Products.PairingRestriction
using (comp₌-evaluate-natural-One; const-comp-evaluate; comp-const-evaluate;
const-comp-evaluate-natural; comp-const-evaluate-natural)
open import SCT.VolumeI.Chapter01.Section06.Cones
module _ {Γ : Context} where
private
constant-restriction-square : {X K C : CAT Γ} (x : Obj-abs C)
{r s : MAP X K} (δ : r =₁ s)
→ SquareCell₌ (const x ◁ δ) (id₌ (const {P = X} x)) (const-pre x r) (const-pre x s)
constant-restriction-square {X} {K} x {r} {s} δ =
replace-edges₌ (id₌ (const x ◁ δ)) (postWhisker-id₌ x (terminate X))
(unconst-sides₌
(post-triangle-inner x (terminate K) δ (id₌ (terminate X))
(terminal-identification (terminate K ∘ r) (terminate X))
(terminal-identification (terminate K ∘ s) (terminate X))
(const-sides₌ (terminal-unique₂ _ _))))
module IdentificationBoundary {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
(s t : Cone f g T) where
Left : CAT Γ
Left = Equal (Cone.left s) (Cone.left t)
Right : CAT Γ
Right = Equal (Cone.right s) (Cone.right t)
Middle : CAT Γ
Middle = Equal (f ∘ Cone.left s) (g ∘ Cone.right t)
left-map : MAP Left Middle
left-map = const (Cone.match t) ∙ postWhisker f
right-map : MAP Right Middle
right-map = postWhisker g ∙ const (Cone.match s)
left-evaluation : {X : CAT Γ} (α : MAP X Left)
→ (left-map ∘ α) =₁ (const (Cone.match t) ∙ (f ◁ α))
left-evaluation α = comp₌-evaluate-One (const (Cone.match t)) (postWhisker f) α
(const-pre (Cone.match t) α) (id₌ (f ◁ α))
right-evaluation : {X : CAT Γ} (β : MAP X Right)
→ (right-map ∘ β) =₁ ((g ◁ β) ∙ const (Cone.match s))
right-evaluation β = comp₌-evaluate-One (postWhisker g) (const (Cone.match s)) β
(id₌ (g ◁ β)) (const-pre (Cone.match s) β)
encode : {X : CAT Γ} → ConeIdentification X s t → Cone left-map right-map X
encode Φ = record
{ left = ConeIdentification.left Φ
; right = ConeIdentification.right Φ
; match = (right-evaluation (ConeIdentification.right Φ)) ⁻¹ ∙
(ConeIdentification.compatible Φ ∙ left-evaluation (ConeIdentification.left Φ)) }
decode : {X : CAT Γ} → Cone left-map right-map X → ConeIdentification X s t
decode z = record
{ left = Cone.left z
; right = Cone.right z
; compatible = right-evaluation (Cone.right z) ∙
(Cone.match z ∙ (left-evaluation (Cone.left z)) ⁻¹) }
opaque
decode-identification : {X : CAT Γ} {z z′ : Cone left-map right-map X}
→ ConeIdentification₁ z z′ → ConeIdentificationEquality (decode z) (decode z′)
decode-identification {z = z} {z′} Ω = record
{ left = ConeIdentification₁.left Ω
; right = ConeIdentification₁.right Ω
; compatible = transport-square
(left-evaluation (Cone.left z)) (left-evaluation (Cone.left z′))
(right-evaluation (Cone.right z)) (right-evaluation (Cone.right z′))
(Cone.match z) (Cone.match z′)
(left-map ◁ ConeIdentification₁.left Ω) (right-map ◁ ConeIdentification₁.right Ω)
(comp₌-cong (id₌ (const (Cone.match t))) (postWhisker f ◁ ConeIdentification₁.left Ω))
(comp₌-cong (postWhisker g ◁ ConeIdentification₁.right Ω) (id₌ (const (Cone.match s))))
(comp₌-evaluate-natural-One (const (Cone.match t)) (postWhisker f)
(ConeIdentification₁.left Ω)
(const-pre (Cone.match t) (Cone.left z)) (const-pre (Cone.match t) (Cone.left z′))
(id₌ _) (id₌ _) (id₌ (const (Cone.match t))) (postWhisker f ◁ ConeIdentification₁.left Ω)
(constant-restriction-square (Cone.match t) (ConeIdentification₁.left Ω))
(unconst-sides₌ (identity-square₌ (postWhisker f ◁ ConeIdentification₁.left Ω))))
(comp₌-evaluate-natural-One (postWhisker g) (const (Cone.match s))
(ConeIdentification₁.right Ω) (id₌ _) (id₌ _)
(const-pre (Cone.match s) (Cone.right z)) (const-pre (Cone.match s) (Cone.right z′))
(postWhisker g ◁ ConeIdentification₁.right Ω) (id₌ (const (Cone.match s)))
(unconst-sides₌ (identity-square₌ (postWhisker g ◁ ConeIdentification₁.right Ω)))
(constant-restriction-square (Cone.match s) (ConeIdentification₁.right Ω)))
(ConeIdentification₁.compatible Ω) }
decode-into : {X : CAT Γ} (z : Cone left-map right-map X) (Φ : ConeIdentification X s t)
→ ConeIdentification₁ z (encode Φ) → ConeIdentificationEquality (decode z) Φ
decode-into z Φ Ω = record
{ left = ConeIdentificationEquality.left Ξ
; right = ConeIdentificationEquality.right Ξ
; compatible = ConeIdentificationEquality.compatible Ξ ∙
comp₌-cong ((cancel-endpoint-changes
(left-evaluation (ConeIdentification.left Φ))
(right-evaluation (ConeIdentification.right Φ)) (ConeIdentification.compatible Φ)) ⁻¹)
(id₌ (comp₌-cong (id₌ (const (Cone.match t)))
(postWhisker f ◁ ConeIdentificationEquality.left Ξ))) }
where
Ξ : ConeIdentificationEquality (decode z) (decode (encode Φ))
Ξ = decode-identification Ω
```
The absolute view keeps the original evaluation triangles and the original
encoding route used by the pullback restriction axiom. At One these triangles
evaluate constant functors, rather than treating them as their values.
```agda
left-evaluation-One : (α : Obj-abs Left)
→ (left-map ∘ α) =₁ (Cone.match t ∙ (f ◁ α))
left-evaluation-One α = const-comp-evaluate (Cone.match t) (postWhisker f) α
right-evaluation-One : (β : Obj-abs Right)
→ (right-map ∘ β) =₁ ((g ◁ β) ∙ Cone.match s)
right-evaluation-One β = comp-const-evaluate (postWhisker g) (Cone.match s) β
encode-One : ConeIdentification₁ s t → Cone left-map right-map One
encode-One Φ = record
{ left = ConeIdentification₁.left Φ
; right = ConeIdentification₁.right Φ
; match = (right-evaluation-One (ConeIdentification₁.right Φ)) ⁻¹ ∙
(ConeIdentification₁.compatible Φ ∙ left-evaluation-One (ConeIdentification₁.left Φ)) }
decode-One : Cone left-map right-map One → ConeIdentification₁ s t
decode-One z = record
{ left = Cone.left z
; right = Cone.right z
; compatible = right-evaluation-One (Cone.right z) ∙
(Cone.match z ∙ (left-evaluation-One (Cone.left z)) ⁻¹) }
opaque
decode-identification-One : {z z′ : Cone left-map right-map One}
→ ConeIdentification₁ z z′ → ConeIdentification₂ (decode-One z) (decode-One z′)
decode-identification-One {z} {z′} Ω = record
{ left = ConeIdentification₁.left Ω
; right = ConeIdentification₁.right Ω
; compatible = transport-square
(left-evaluation-One (Cone.left z)) (left-evaluation-One (Cone.left z′))
(right-evaluation-One (Cone.right z)) (right-evaluation-One (Cone.right z′))
(Cone.match z) (Cone.match z′)
(left-map ◁ ConeIdentification₁.left Ω) (right-map ◁ ConeIdentification₁.right Ω)
(comp₌-cong (id₌ (Cone.match t)) (postWhisker f ◁ ConeIdentification₁.left Ω))
(comp₌-cong (postWhisker g ◁ ConeIdentification₁.right Ω) (id₌ (Cone.match s)))
(const-comp-evaluate-natural (Cone.match t) (postWhisker f) (ConeIdentification₁.left Ω))
(comp-const-evaluate-natural (postWhisker g) (Cone.match s) (ConeIdentification₁.right Ω))
(ConeIdentification₁.compatible Ω) }
decode-into-One : (z : Cone left-map right-map One) (Φ : ConeIdentification₁ s t)
→ ConeIdentification₁ z (encode-One Φ) → ConeIdentification₂ (decode-One z) Φ
decode-into-One z Φ Ω = record
{ left = ConeIdentification₂.left Ξ
; right = ConeIdentification₂.right Ξ
; compatible = ConeIdentification₂.compatible Ξ ∙
comp₌-cong ((cancel-endpoint-changes
(left-evaluation-One (ConeIdentification₁.left Φ))
(right-evaluation-One (ConeIdentification₁.right Φ))
(ConeIdentification₁.compatible Φ)) ⁻¹)
(id₌ (comp₌-cong (id₌ (Cone.match t)) (postWhisker f ◁ ConeIdentification₂.left Ξ))) }
where
Ξ : ConeIdentification₂ (decode-One z) (decode-One (encode-One Φ))
Ξ = decode-identification-One Ω
```
## The actual action cone
The action on the vertex has the two postwhiskering functors as its legs.
Its matching is the family action evaluated at the identity family, with
the same unitor normalizations and evaluation triangles. Factoring this
particular cone will define the pullback restriction functor.
```agda
module ConeAction {C D E S T : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g T) (h k : MAP S T) where
module Boundary = IdentificationBoundary (cone-restrict h s) (cone-restrict k s)
p : MAP T C
p = Cone.left s
q : MAP T D
q = Cone.right s
left-evaluation : (Boundary.left-map ∘ postWhisker p) =₁
(const (Cone.match (cone-restrict k s)) ∙ (f ◁ postWhisker p))
left-evaluation = Boundary.left-evaluation (postWhisker p)
right-evaluation : (Boundary.right-map ∘ postWhisker q) =₁
((g ◁ postWhisker q) ∙ const (Cone.match (cone-restrict h s)))
right-evaluation = Boundary.right-evaluation (postWhisker q)
matching : (Boundary.left-map ∘ postWhisker p) =₁ (Boundary.right-map ∘ postWhisker q)
matching = right-evaluation ⁻¹ ∙
(comp₌-cong (postWhisker g ◁ comp-unitʳ (postWhisker q)) (id₌ _) ∙
(cone-action-square s (id (Equal h k)) ∙
((comp₌-cong (id₌ _) (postWhisker f ◁ comp-unitʳ (postWhisker p))) ⁻¹ ∙
left-evaluation)))
identification-cone : Cone Boundary.left-map Boundary.right-map (Equal h k)
identification-cone = record { left = postWhisker p ; right = postWhisker q ; match = matching }
module _ {X : CAT Γ} where
open Terms.Equalities X using (_＝_)
cone-action : {C D E S T : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g T) {h k : MAP S T} → h ＝ k
→ ConeIdentification X (cone-restrict h s) (cone-restrict k s)
cone-action s {h} {k} δ = ConeAction.Boundary.decode s h k
(cone-restrict δ (ConeAction.identification-cone s h k))
cone-action-One : {C D E S T : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g T) {h k : MAP S T} → h =₁ k
→ ConeIdentification₁ (cone-restrict h s) (cone-restrict k s)
cone-action-One s {h} {k} δ = ConeAction.Boundary.decode-One s h k
(cone-restrict δ (ConeAction.identification-cone s h k))
```
## Restriction of matching squares
Restriction acts on both legs of a cone identification. Transporting the
restricted matching square along the two associators preserves its full
compatibility. Absolute composition and inversion explicitly pass through
the family interface.
```agda
cone-compose : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
{s t u : Cone f g T} → ConeIdentification₁ t u → ConeIdentification₁ s t
→ ConeIdentification₁ s u
cone-compose Ψ Φ = cone-identification-One
(cone-identification-compose (cone-identification Ψ) (cone-identification Φ))
cone-inverse : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
{s t : Cone f g T} → ConeIdentification₁ s t → ConeIdentification₁ t s
cone-inverse Φ = cone-identification-One (cone-identification-inverse (cone-identification Φ))
cone-identification-restrict-One : {C D E S T : CAT Γ}
{f : MAP C E} {g : MAP D E} {s t : Cone f g T}
(r : MAP S T) → ConeIdentification₁ s t
→ ConeIdentification₁ (cone-restrict r s) (cone-restrict r t)
cone-identification-restrict-One {f = f} {g} {s} {t} r Φ = record
{ left = ConeIdentification₁.left Φ ▷ r
; right = ConeIdentification₁.right Φ ▷ r
; compatible = transport-square
(comp-assoc r (Cone.left s) f) (comp-assoc r (Cone.left t) f)
(comp-assoc r (Cone.right s) g) (comp-assoc r (Cone.right t) g)
(Cone.match s ▷ r) (Cone.match t ▷ r)
((f ◁ ConeIdentification₁.left Φ) ▷ r) ((g ◁ ConeIdentification₁.right Φ) ▷ r)
(f ◁ (ConeIdentification₁.left Φ ▷ r)) (g ◁ (ConeIdentification₁.right Φ ▷ r))
(whisker-mixed-One (ConeIdentification₁.left Φ) r f)
(whisker-mixed-One (ConeIdentification₁.right Φ) r g)
(pre-square₌ r (ConeIdentification₁.compatible Φ)) }
```
## Successive restriction
The associativity square is the pasting of the corresponding triangle
square with the associator pentagon on the right leg. Restriction's unit
law is the triangle unit law followed by the right-unitor comparison.
```agda
cone-restrict-assoc : {C D E Q R T : CAT Γ} {f : MAP C E} {g : MAP D E}
(r : MAP Q R) (u : MAP R T) (s : Cone f g T)
→ ConeIdentification₁ (cone-restrict r (cone-restrict u s)) (cone-restrict (u ∘ r) s)
cone-restrict-assoc {f = f} {g} r u s = record
{ left = comp-assoc r u (Cone.left s)
; right = comp-assoc r u (Cone.right s)
; compatible = replace-sides₌ normalize (id₌ _)
(paste-square₌
(restrict-triangle-assoc f (Cone.left s) (Cone.match s) u r)
(pentagon-whiskered-right r u (Cone.right s) g)) }
where
outer-associator = comp-assoc u (Cone.right s) g
restricted-associator = comp-assoc r (Cone.right s ∘ u) g
whiskered-associator = outer-associator ▷ r
whiskered-triangle = restrict-triangle f (Cone.left s) (Cone.match s) u ▷ r
inverse-associator = (comp-assoc r (Cone.left s ∘ u) f) ⁻¹
normalize : ((restricted-associator ∙ whiskered-associator) ∙ (whiskered-triangle ∙ inverse-associator)) =₂ Cone.match (cone-restrict r (cone-restrict u s))
normalize = comp₌-cong (id₌ restricted-associator)
(comp₌-cong ((preWhisker-comp₌ outer-associator (restrict-triangle f (Cone.left s) (Cone.match s) u) r) ⁻¹)
(id₌ inverse-associator) ∙ (comp₌-assoc whiskered-associator whiskered-triangle inverse-associator) ⁻¹) ∙
comp₌-assoc restricted-associator whiskered-associator (whiskered-triangle ∙ inverse-associator)
cone-restrict-id : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g T) → ConeIdentification₁ (cone-restrict (id T) s) s
cone-restrict-id {f = f} {g} s = record
{ left = comp-unitʳ (Cone.left s)
; right = comp-unitʳ (Cone.right s)
; compatible = comp₌-assoc (g ◁ comp-unitʳ (Cone.right s))
(comp-assoc (id _) (Cone.right s) g) tail ∙
(comp₌-cong (right-unitor-comp (Cone.right s) g) (id₌ tail) ∙
(restrict-triangle-id f (Cone.left s) (g ∘ Cone.right s) (Cone.match s)) ⁻¹) }
where
tail = restrict-triangle f (Cone.left s) (Cone.match s) (id _)
```