| description |
|---|
Segal conditions.
|
module Segal whereWe start by defining a notion of spine, which is a list of
data Spine {ℓ ℓ'} {X : Type ℓ} (H : X → X → Type ℓ') : Nat → Type (ℓ ⊔ ℓ')
vertex : ∀ {ℓ ℓ'} {X : Type ℓ} {H : X → X → Type ℓ'} {n} → Fin (suc n) → Spine H n → X
data Spine {X = X} H where
ι : X → Spine H 0
_⨾_ : ∀ {n} {x} → (s : Spine H n) → H x (vertex fzero s) → Spine H (suc n)
vertex i (ι x) = x
vertex fzero (_⨾_ {x = x} hs h) = x
vertex (fsuc i) (_⨾_ hs h) = vertex i hsWe can also index edges.
edge
: ∀ {ℓ ℓ'} {X : Type ℓ} {H : X → X → Type ℓ'} {n}
→ (i : Fin n) (hs : Spine H n)
→ H (vertex (weaken i) hs) (vertex (fsuc i) hs)
edge fzero (hs ⨾ h) = h
edge (fsuc i) (hs ⨾ h) = edge i hsWe also take the time to define a combinator for forming pathps of spines.
_⨾ₚ_/ₚ_
: ∀ {n} {X : Type ℓ} {H : X → X → Type ℓ'}
→ {hs hs' : Spine H n} {x y : X} {h : H x (vertex 0 hs)} {h' : H y (vertex 0 hs')}
→ (p : hs ≡ hs')
→ (q : x ≡ y)
→ PathP (λ i → H (q i) (vertex 0 (p i))) h h'
→ hs ⨾ h ≡ hs' ⨾ h'
_⨾ₚ_/ₚ_ p q r i = (p i) ⨾ (r i)
Our next move is to define simplicial sets. For ease of use, we give
an unfolded definition, instead of the compact definition as a functor
out of
record SSet (ℓ : Level) : Type (lsuc ℓ) where
field
Cell : Nat → Type ℓ
Cell-is-set : ∀ {n} → is-set (Cell n)
-- Face and degeneracy maps
∂ : ∀ {n} → Fin (suc (suc n)) → Cell (suc n) → Cell n
σ : ∀ {n} → Fin (suc n) → Cell n → Cell (suc n)
-- Simplicial identities
face-face
: ∀ {n} {i j}
→ {x : Cell (suc (suc n))}
→ ⦃ _ : i ≤ j ⦄ → ∂ i (∂ (fsuc j) x) ≡ ∂ j (∂ (weaken i) x)
degen-degen
: ∀ {n} {i j}
→ {x : Cell n}
→ ⦃ _ : j < i ⦄ → σ (fsuc i) (σ j x) ≡ σ (weaken j) (σ i x)
face-degen-lt
: ∀ {n} {i j}
→ {x : Cell (suc n)}
→ ⦃ _ : i < fsuc j ⦄ → ∂ (weaken i) (σ (fsuc j) x) ≡ σ j (∂ i x)
face-degen-weaken
: ∀ {n} {i}
→ {x : Cell n}
→ ∂ (weaken i) (σ i x) ≡ x
face-degen-fsuc
: ∀ {n} {i}
→ {x : Cell n}
→ ∂ (fsuc i) (σ i x) ≡ x
face-degen-gt
: ∀ {n} {i j}
→ {x : Cell (suc n)}
→ ⦃ _ : weaken j < i ⦄ → ∂ (fsuc i) (σ (weaken j) x) ≡ σ j (∂ i x)Next, we define the type of 1-cells with a designated source and target.
Ob : Type ℓ
Ob = Cell 0
1-Cell : Ob → Ob → Type ℓ
1-Cell x y = Σ[ f ∈ Cell 1 ] (∂ 0 f ≡ x × ∂ 1 f ≡ y)
retarget : ∀ {x y y'} → y ≡ y' → 1-Cell x y → 1-Cell x y'
retarget p (f , s , t) = f , s , t ∙ pSimplicial sets are sets, so the paths that designate a source/target
do not impact the identity type of 1-Cell.
1-cell-pathp
: ∀ {x x' y y' f g}
→ {p : x ≡ x'} {q : y ≡ y'}
→ f .fst ≡ g .fst
→ PathP (λ i → 1-Cell (p i) (q i)) f g
1-cell-pathp =
Σ-prop-pathp (λ i f → ×-is-hlevel 1 (Cell-is-set _ _) (Cell-is-set _ _))We also define some accessors to project out 0-cells and 1-cells from an
n-cell. Note that the order of indexing on ob is backwards: ob f 0
is the terminal vertex in f, whereas ob f (from-nat n) is the initial
vertex. This makes the programing much easier, but unfortunately is confusing.
ob : ∀ {n} → (f : Cell n) → Fin (1 + n) → Ob
ob {zero} f _ = f
ob {suc n} f fzero = ob (∂ (from-nat (suc n)) f) 0
ob {suc n} f (fsuc i) = ob (∂ 0 f) i
1-cell
: ∀ {n}
→ (f : Cell (suc n))
→ ∀ i → 1-Cell (ob (∂ 0 f) i) (ob (∂ (from-nat (suc n)) f) i)
1-cell {n = zero} f i = f , refl , refl
1-cell {n = suc n} f fzero =
let (h , s , t) = 1-cell (∂ (from-nat (2 + n)) f) 0
in h , s ∙ ap (λ f → ob f fzero) (face-face {i = 0} {j = from-nat (suc n)} {x = f}) , t
1-cell {n = suc n} f (fsuc i) =
let (h , s , t) = 1-cell (∂ 0 f) i
in h , s , t ∙ ap (λ f → ob f i) (sym face-face)Finally, we define a of function segal that unpacks an n-cell into
a chain of composable 1-cells. In other words, we compute the spine
of the n-cell. Typically, these maps are known as the Segal maps.
segal : ∀ {n} → (f : Cell n) → Spine 1-Cell n
segal-src
: ∀ {n}
→ (f : Cell n)
→ ob f (from-nat n) ≡ vertex 0 (segal f)
segal {n = zero} x = ι x
segal {n = suc n} f =
segal (∂ (from-nat (suc n)) f) ⨾
retarget (segal-src (∂ (from-nat (suc n)) f)) (1-cell f (from-nat n))
segal-src {n = zero} f = refl
segal-src {n = suc n} f = reflNow for the final trick. Let
record Segal {ℓ} (C : SSet ℓ) : Type ℓ where
open SSet C
field
segal-is-equiv : ∀ (n : Nat) → is-equiv (segal {n})
module segal n = Equiv (_ , segal-is-equiv n)This lets us define a composition operation on 1-cells.
_∘_ : ∀ {x y z} → 1-Cell y z → 1-Cell x y → 1-Cell x z
f ∘ g =
∂ 1 (segal.from 2 (ι _ ⨾ f ⨾ g))
, face-face ∙ ap (vertex 0) (segal.ε 2 (ι _ ⨾ f ⨾ g))
, sym face-face ∙ ap (vertex 2) (segal.ε 2 (ι _ ⨾ f ⨾ g))There are a couple of notes here: first, segal.from 2 (ι _ ⨾ f ⨾ g) gives
us a 2-cell, so we need to use ∂ 1 to access the resulting composite
(∂ 0 and ∂ 2 would give us g and f, resp.). Moreover, we need
to use the fact that segal is an equivalence to ensure that the
source and target of the resulting composite are correct.
Identities are mercifully easy, and just come from degeneracies.
id : ∀ {x} → 1-Cell x x
id {x} = σ fzero x , face-degen-weaken , face-degen-fsucMoreover, we can prove the left identity law from the Segal condition. Unfortunately, the proof is quite brutal, and involves a lot of simplicial identity munging. There is no intuition to be gained here!
idl : ∀ {x y} → (f : 1-Cell x y) → id ∘ f ≡ f
idl {x} {y} f =
1-cell-pathp $
∂ 1 (segal.from 2 (ι y ⨾ id ⨾ f)) ≡⟨ ap (∂ 1) (ap (segal.from 2) spine-path) ⟩
∂ 1 (segal.from 2 (segal (σ 0 (f .fst)))) ≡⟨ ap (∂ 1) (segal.η 2 (σ 0 (f .fst))) ⟩
∂ 1 (σ 0 (f .fst)) ≡⟨ face-degen-fsuc ⟩
f .fst ∎
where
spine-path : (ι y ⨾ id ⨾ f) ≡ segal (σ 0 (f .fst))
spine-path =
ap ι (sym (face-face ∙ ap (∂ 1) face-degen-fsuc ∙ f .snd .snd))
⨾ₚ sym (face-face ∙ ap (∂ 1) face-degen-weaken ∙ f .snd .snd)
/ₚ 1-cell-pathp (sym (face-degen-gt ∙ ap (σ 0) (f .snd .snd)))
⨾ₚ sym (ap (∂ 0) face-degen-weaken ∙ f .snd .fst)
/ₚ 1-cell-pathp (sym face-degen-weaken)The right identity follows a similar pattern, though we do not bother attempting to format it.
idr : ∀ {x y} → (f : 1-Cell x y) → f ∘ id ≡ f
idr {x} {y} f =
1-cell-pathp $
ap (∂ 1) (ap (segal.from 2)
(ap ι (sym (face-face ∙ ap (∂ 1) face-degen-weaken ∙ f .snd .snd))
⨾ₚ sym (ap (∂ 0) face-degen-fsuc ∙ f .snd .fst)
/ₚ 1-cell-pathp (sym face-degen-fsuc)
⨾ₚ sym (ap (∂ 0) face-degen-lt ∙ face-degen-weaken ∙ f .snd .fst)
/ₚ 1-cell-pathp (sym (face-degen-lt ∙ ap (σ 0) (f .snd .fst)))))
∙ ap (∂ 1) (segal.η 2 (σ 1 (f .fst)))
∙ face-degen-weakenNow for the brutal one: associativity. The basic idea is that the two
nested composites ∂ 1 (segal.from 2 (ι z ⨾ f ⨾ (g ∘ h))) and
∂ 1 (segal.from 2 (ι z ⨾ (f ∘ g) ⨾ h)) are both equal to part of an
unbiased composite segal.from 3 (ι z ⨾ f ⨾ g ⨾ h). Unfortunately,
actully proving this is extremely tedious.
We start by presenting the core of the argument.
assoc
: ∀ {w x y z}
→ (f : 1-Cell y z) (g : 1-Cell x y) (h : 1-Cell w x)
→ f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h
assoc {w} {x} {y} {z} f g h =
1-cell-pathp $
∂ 1 (segal.from 2 (ι z ⨾ f ⨾ (g ∘ h))) ≡˘⟨ ap (∂ 1 ⊙ segal.from 2) f[gh]-spine ⟩
∂ 1 (segal.from 2 (segal (∂ 2 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h))))) ≡⟨ ap (∂ 1) (segal.η 2 (∂ 2 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h)))) ⟩
∂ 1 (∂ 2 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h))) ≡⟨ face-face ⟩
∂ 1 (∂ 1 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h))) ≡˘⟨ ap (∂ 1) (segal.η 2 (∂ 1 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h)))) ⟩
∂ 1 (segal.from 2 (segal (∂ 1 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h))))) ≡⟨ ap (∂ 1 ⊙ segal.from 2) [fg]h-spine ⟩
∂ 1 (segal.from 2 (ι z ⨾ (f ∘ g) ⨾ h)) ∎Now for the pain. This is not a place of honor, and absolutely no intuition is to be gained here: just one big slog through simplicial identities.
where
fg-spine : segal (∂ 3 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h))) ≡ ι z ⨾ f ⨾ g
fg-spine =
ap ι (ap (vertex 3) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h)))
⨾ₚ ap (vertex 2) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h))
/ₚ 1-cell-pathp (ap (fst ⊙ edge 2) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h)))
⨾ₚ ap (vertex 1) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h))
/ₚ 1-cell-pathp (ap (fst ⊙ edge 1) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h)))
gh-spine : segal (∂ 0 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h))) ≡ ι y ⨾ g ⨾ h
gh-spine =
ap ι (ap (∂ 1) (sym face-face) ∙ sym face-face ∙ ap (vertex 2) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h)) )
⨾ₚ ap (∂ 0) (sym face-face) ∙ ap (vertex 1) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h))
/ₚ 1-cell-pathp (sym face-face ∙ ap (fst ⊙ edge 1) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h)))
⨾ₚ ap (vertex 0) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h))
/ₚ 1-cell-pathp (ap (fst ⊙ edge 0) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h)))
fg-face : ∂ 3 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h)) ≡ segal.from 2 (ι z ⨾ f ⨾ g)
fg-face =
∂ 3 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h)) ≡˘⟨ segal.η 2 _ ⟩
segal.from 2 (segal (∂ 3 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h)))) ≡⟨ ap (segal.from 2) fg-spine ⟩
segal.from 2 (ι z ⨾ f ⨾ g) ∎
gh-face : ∂ 0 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h)) ≡ segal.from 2 (ι y ⨾ g ⨾ h)
gh-face =
∂ 0 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h)) ≡˘⟨ segal.η 2 _ ⟩
segal.from 2 (segal (∂ 0 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h)))) ≡⟨ ap (segal.from 2) gh-spine ⟩
segal.from 2 (ι y ⨾ g ⨾ h) ∎
f[gh]-spine : segal (∂ 2 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h))) ≡ ι z ⨾ f ⨾ (g ∘ h)
f[gh]-spine =
ap ι (ap (∂ 1) (sym face-face) ∙ ap (vertex 3) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h)))
⨾ₚ ap (∂ 0) (sym face-face) ∙ ap (vertex 2) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h))
/ₚ 1-cell-pathp (sym face-face ∙ ap (fst ⊙ edge 2) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h)))
⨾ₚ ap (∂ 0) face-face ∙ face-face ∙ ap (vertex 0) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h))
/ₚ 1-cell-pathp (face-face ∙ ap (∂ 1) gh-face)
[fg]h-spine : segal (∂ 1 (segal.from 3 (ι z ⨾ f ⨾ g ⨾ h))) ≡ ι z ⨾ (f ∘ g) ⨾ h
[fg]h-spine =
ap ι (ap (∂ 1) (sym face-face) ∙ sym face-face ∙ (ap (vertex 3) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h))))
⨾ₚ ap (∂ 0) (sym face-face) ∙ face-face ∙ ap (vertex 1) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h))
/ₚ 1-cell-pathp (sym face-face ∙ ap (∂ 1) fg-face)
⨾ₚ ap (∂ 0) face-face ∙ ap (vertex 0) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h))
/ₚ 1-cell-pathp (face-face ∙ ap (fst ⊙ edge 0) (segal.ε 3 (ι z ⨾ f ⨾ g ⨾ h)))The payoff for all this hard work is that we get back to the normal definition of a category.
segal-cat : Precategory ℓ ℓ
segal-cat .Precategory.Ob = Ob
segal-cat .Precategory.Hom = 1-Cell
segal-cat .Precategory.Hom-set _ _ =
Σ-is-hlevel 2 (Cell-is-set) λ _ →
×-is-hlevel 2
(Path-is-hlevel 2 Cell-is-set)
(Path-is-hlevel 2 Cell-is-set)
segal-cat .Precategory.id = id
segal-cat .Precategory._∘_ = _∘_
segal-cat .Precategory.idr = idr
segal-cat .Precategory.idl = idl
segal-cat .Precategory.assoc = assoc