From 783c10e84394c6672c3ee84b24e17d6a166496ed Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sat, 30 Mar 2024 14:30:43 -0400 Subject: [PATCH 01/18] wip: simplex category overhaul --- src/Cat/Instances/Simplex.lagda.md | 331 ++++++++++++++++++++++++++--- 1 file changed, 298 insertions(+), 33 deletions(-) diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md index 7456e99bf..1507460ca 100644 --- a/src/Cat/Instances/Simplex.lagda.md +++ b/src/Cat/Instances/Simplex.lagda.md @@ -1,9 +1,12 @@ @@ -20,50 +23,312 @@ open Precategory # The simplex category -The simplex category, $\Delta$, is generally introduced as the category -of non-empty finite ordinals and order-preserving maps. We will, for -convenience reasons, define it _skeletally_: Rather than taking actual -finite ordinals as objects, we will use the natural numbers as ordinals, -each natural standing for the isomorphism class of ordinals of that -cardinality. + ```agda -record Δ-map (n m : Nat) : Type where - field - map : Fin (suc n) → Fin (suc m) - ascending : (x y : Fin (suc n)) → x ≤ y → map x ≤ map y +data Δ-Hom⁺ : Nat → Nat → Type where + done⁺ : Δ-Hom⁺ 0 0 + shift⁺ : ∀ {m n} → Δ-Hom⁺ m n → Δ-Hom⁺ m (suc n) + keep⁺ : ∀ {m n} → Δ-Hom⁺ m n → Δ-Hom⁺ (suc m) (suc n) + +data Δ-Hom⁻ : Nat → Nat → Type where + done⁻ : Δ-Hom⁻ 0 0 + crush⁻ : ∀ {m n} → Δ-Hom⁻ m (suc n) → Δ-Hom⁻ (suc m) (suc n) + keep⁻ : ∀ {m n} → Δ-Hom⁻ m n → Δ-Hom⁻ (suc m) (suc n) ``` - ```agda -Δ : Precategory lzero lzero -Δ .Ob = Nat -Δ .Hom n m = Δ-map n m -Δ .Hom-set _ _ = hlevel 2 +Δ⁺-map-id : ∀ (i : Fin m) → Δ⁺-map id⁺ i ≡ i +Δ⁺-map-id fzero = refl +Δ⁺-map-id (fsuc i) = ap fsuc (Δ⁺-map-id i) + +Δ⁺-map-∘ + : (f : Δ-Hom⁺ n o) (g : Δ-Hom⁺ m n) + → ∀ (i : Fin m) → Δ⁺-map (f ∘⁺ g) i ≡ Δ⁺-map f (Δ⁺-map g i) +Δ⁺-map-∘ done⁺ done⁺ () +Δ⁺-map-∘ (shift⁺ f) (shift⁺ g) i = ap fsuc (Δ⁺-map-∘ f (shift⁺ g) i) +Δ⁺-map-∘ (shift⁺ f) (keep⁺ g) i = ap fsuc (Δ⁺-map-∘ f (keep⁺ g) i) +Δ⁺-map-∘ (keep⁺ f) (shift⁺ g) i = ap fsuc (Δ⁺-map-∘ f g i) +Δ⁺-map-∘ (keep⁺ f) (keep⁺ g) fzero = refl +Δ⁺-map-∘ (keep⁺ f) (keep⁺ g) (fsuc i) = ap fsuc (Δ⁺-map-∘ f g i) +``` -Δ .id .map x = x -Δ .id .ascending x y p = p +# Categories -Δ ._∘_ f g .map x = f .map (g .map x) -Δ ._∘_ f g .ascending x y p = f .ascending _ _ (g .ascending _ _ p) +```agda +idl⁺ : ∀ (f : Δ-Hom⁺ m n) → id⁺ ∘⁺ f ≡ f +idl⁺ f = Δ⁺-map-inj _ _ λ i → + Δ⁺-map-∘ id⁺ f i ∙ Δ⁺-map-id (Δ⁺-map f i) + +idr⁺ : ∀ (f : Δ-Hom⁺ m n) → f ∘⁺ id⁺ ≡ f +idr⁺ {m = zero} f = refl +idr⁺ {m = suc m} (shift⁺ f) = ap shift⁺ (idr⁺ f) +idr⁺ {m = suc m} (keep⁺ f) = ap keep⁺ (idr⁺ f) -Δ .idr f = Δ-map-path λ x → refl -Δ .idl f = Δ-map-path λ x → refl -Δ .assoc f g h = Δ-map-path λ x → refl +assoc⁺ + : ∀ (f : Δ-Hom⁺ n o) (g : Δ-Hom⁺ m n) (h : Δ-Hom⁺ l m) + → f ∘⁺ (g ∘⁺ h) ≡ (f ∘⁺ g) ∘⁺ h +assoc⁺ f g h = Δ⁺-map-inj _ _ λ i → + Δ⁺-map-∘ f (g ∘⁺ h) i + ∙ ap (Δ⁺-map f) (Δ⁺-map-∘ g h i) + ∙ sym (Δ⁺-map-∘ f g (Δ⁺-map h i)) + ∙ sym (Δ⁺-map-∘ (f ∘⁺ g) h i) ``` + +```agda +record Δ-Hom (m n : Nat) : Type where + no-eta-equality + constructor Δ-hom + field + {middle} : Nat + hom⁺ : Δ-Hom⁺ middle n + hom⁻ : Δ-Hom⁻ m middle + +open Δ-Hom + +done : Δ-Hom 0 0 +done .middle = 0 +done .hom⁺ = done⁺ +done .hom⁻ = done⁻ + +crush : Δ-Hom m (suc n) → Δ-Hom (suc m) (suc n) +crush f with f .middle | f .hom⁺ | f .hom⁻ +... | zero | f⁺ | done⁻ = Δ-hom (keep⁺ ¡⁺) id⁻ +... | suc x | f⁺ | f⁻ = Δ-hom f⁺ (crush⁻ f⁻) + +shift : Δ-Hom m n → Δ-Hom m (suc n) +shift f .middle = f .middle +shift f .hom⁺ = shift⁺ (f .hom⁺) +shift f .hom⁻ = f .hom⁻ + +keep : Δ-Hom m n → Δ-Hom (suc m) (suc n) +keep f .middle = suc (f .middle) +keep f .hom⁺ = keep⁺ (f .hom⁺) +keep f .hom⁻ = keep⁻ (f .hom⁻) +``` + +```agda +exchange + : ∀ {m n o} + → Δ-Hom⁻ n o → Δ-Hom⁺ m n + → Δ-Hom m o +exchange done⁻ done⁺ = Δ-hom done⁺ done⁻ +exchange (crush⁻ f) (shift⁺ g) = exchange f g +exchange (crush⁻ f) (keep⁺ g) = crush (exchange f g) +exchange (keep⁻ f) (shift⁺ g) = shift (exchange f g) +exchange (keep⁻ f) (keep⁺ g) = keep (exchange f g) +``` + +```agda +Δ⁺ : Precategory lzero lzero +Δ⁺ .Ob = Nat +Δ⁺ .Hom = Δ-Hom⁺ +Δ⁺ .Hom-set _ _ = Δ-Hom⁺-is-set +Δ⁺ .id = id⁺ +Δ⁺ ._∘_ = _∘⁺_ +Δ⁺ .idr = idr⁺ +Δ⁺ .idl = idl⁺ +Δ⁺ .assoc = assoc⁺ +``` + +-- ```agda +-- Δ⁺-map-pres-< +-- : ∀ {m n} +-- → (f : Δ-Hom⁺ m n) +-- → ∀ {i j} → i < j → Δ⁺-map f i < Δ⁺-map f j +-- Δ⁺-map-pres-< (shift⁺ f) {i} {j} i Date: Mon, 1 Apr 2024 09:54:21 -0400 Subject: [PATCH 02/18] wip: more triangles --- src/1Lab/Function/Embedding.lagda.md | 8 + src/1Lab/Reflection/Record.agda | 1 + src/Cat/Instances/Simplex.lagda.md | 892 +++++++++++++++++++----- src/Cat/Morphism/Factorisation.lagda.md | 34 +- src/Data/Fin/Base.lagda.md | 14 + src/Data/Fin/Properties.lagda.md | 37 + src/Data/Nat/Order.lagda.md | 15 + src/bibliography.bibtex | 13 + 8 files changed, 825 insertions(+), 189 deletions(-) diff --git a/src/1Lab/Function/Embedding.lagda.md b/src/1Lab/Function/Embedding.lagda.md index a7a19a19d..e904c7d95 100644 --- a/src/1Lab/Function/Embedding.lagda.md +++ b/src/1Lab/Function/Embedding.lagda.md @@ -220,5 +220,13 @@ module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} where → is-hlevel A (suc n) embedding→is-hlevel n emb a-hl = Equiv→is-hlevel (suc n) (Total-equiv f) $ Σ-is-hlevel (suc n) a-hl λ x → is-prop→is-hlevel-suc (emb x) + + injective→is-set + : injective f + → is-set B + → is-set A + injective→is-set inj b-set = + embedding→is-hlevel 1 + (injective→is-embedding b-set f inj) b-set ``` --> diff --git a/src/1Lab/Reflection/Record.agda b/src/1Lab/Reflection/Record.agda index 0a5edb47c..d37178673 100644 --- a/src/1Lab/Reflection/Record.agda +++ b/src/1Lab/Reflection/Record.agda @@ -161,6 +161,7 @@ private → Iso (T A) (S.Σ A (λ fp → S.Σ (A → A) (λ f → f fp ≡ fp))) _ = eqv-extra + record T2 : Type where -- works without eta equality too field diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md index 1507460ca..f853664a3 100644 --- a/src/Cat/Instances/Simplex.lagda.md +++ b/src/Cat/Instances/Simplex.lagda.md @@ -1,3 +1,7 @@ +--- +description: | + Concrete categories +--- -# The simplex category +# The simplex category {defines="simplex-category semisimplex-category"} + +The simplex category, $\Delta$, is generally introduced as the category +of non-empty finite ordinals and order-preserving maps. Though +conceptually simple, this definition is difficult to work with: in particular, +diagrams over $\Delta$ are extremely hard to form! This is why mathematicians +prefer to work with a particular presentation of $\Delta$ as a free category +generated from 2 classes of maps: +- Face maps $\delta^{n}_{i} : [n] \to [n + 1]$ for $0 \leq i \leq n$, $0 < n$ +- Degeneracy maps $\sigma^{n}_{i} : [n + 1] \to [n]$ for $0 \leq i < n$, $0 < n$ + +Intuitively, the face maps $\delta^{n}_{i}$ are injections that skip the $i$th +element of $[n + 1]$, and degeneracy maps are surjections that take both $i$ and +$i+1$ to $i$. + +Unfortunately, we need to quotient these generators to get the correct +category; these equations are known as the **simplicial identities**, and +are quite involved. +- For all $i \leq j$, $\delta^{n + 1}_i \circ \delta^{n}_j = \delta^{n+1}_{j+1} \circ \delta^{n}_{i}$; and +- For all $i \leq j$, $\sigma^{n}_j \circ \sigma^{n+1}_i = \sigma^{n}_i \circ \sigma^{n+1}_{j + 1}$; and +- For all $i \leq j$, $\sigma^{n+1}_{j+1} \circ \delta^{n+2}_i = \delta^{n+1}_i \circ \sigma^{n}_{j}$; and +- For all $i, j$ with $i = j$ or $i = j + 1$, $\sigma{n}_j \circ \delta^{n+1}_i = id$; and +- For all $j < i$, $\sigma^{n+1}_j \circ \delta^{n+2}_{i+1} = \delta^{n+1}_{i} \circ \sigma^{n}_{j}$ + +These identities are extremely painful to work with, and we would need +to deal with them *every* time we eliminated out of the simplex category. +This is a complete non-starter, so we will need to figure out a better approach. + +Typically, the way to avoid dealing with quotients by some set of equations +is to find some sort of normal form. Luckily, the simplex category has a +particularly simple normal form: every map can be expressed uniquely as +$$ +\delta_{i_1} \circ \cdots \circ \delta_{i_k} \circ \sigma_{j_1} \circ \cdots \sigma_{j_l} +$$ +where $0 \leq i_k < \cdots < i_1$ and $0 \leq j_1 < \cdots < j_l$. +These normal forms are relatively straightforward to encode in Agda: +descending chains of face maps can be defined via an indexed inductive, +where `shift⁺`{.Agda} introduces the nth face map, and `keep⁺`{.Agda} keeps +the value of 'n' fixed. + ```agda data Δ-Hom⁺ : Nat → Nat → Type where done⁺ : Δ-Hom⁺ 0 0 shift⁺ : ∀ {m n} → Δ-Hom⁺ m n → Δ-Hom⁺ m (suc n) keep⁺ : ∀ {m n} → Δ-Hom⁺ m n → Δ-Hom⁺ (suc m) (suc n) +``` +Descending chains of degeneracies are defined in a similar fashion, where +where `crush⁻`{.Agda} introduces the nth degeneracy map. + +```agda data Δ-Hom⁻ : Nat → Nat → Type where done⁻ : Δ-Hom⁻ 0 0 crush⁻ : ∀ {m n} → Δ-Hom⁻ m (suc n) → Δ-Hom⁻ (suc m) (suc n) keep⁻ : ∀ {m n} → Δ-Hom⁻ m n → Δ-Hom⁻ (suc m) (suc n) ``` +Morphisms in $\Delta$ consist of 2 composable chains of face and degeneracy +maps. Note that we allow both `m` and `n` to be 0; this allows us to share +code between the simplex and augmented simplex category. + ```agda -id⁺ : ∀ {m} → Δ-Hom⁺ m m +record Δ-Hom (m n : Nat) : Type where + no-eta-equality + constructor Δ-hom + field + {middle} : Nat + hom⁺ : Δ-Hom⁺ middle n + hom⁻ : Δ-Hom⁻ m middle + +open Δ-Hom +``` + + + +## Face and degeneracy maps + +Identity morphisms $[n] \to [n]$ are defined via induction on $n$, +and do not contain any face or degeneracy maps. + +```agda +id⁺ : ∀ {n} → Δ-Hom⁺ n n id⁺ {zero} = done⁺ -id⁺ {suc m} = keep⁺ id⁺ +id⁺ {suc n} = keep⁺ id⁺ -id⁻ : ∀ {m} → Δ-Hom⁻ m m +id⁻ : ∀ {n} → Δ-Hom⁻ n n id⁻ {zero} = done⁻ -id⁻ {suc m} = keep⁻ id⁻ +id⁻ {suc n} = keep⁻ id⁻ +``` + +There are also face maps from $0 \to n$ and degeneracies $1 + n \to 1$ +for any $n$. + +```agda +¡⁺ : Δ-Hom⁺ 0 m +¡⁺ {m = zero} = done⁺ +¡⁺ {m = suc m} = shift⁺ ¡⁺ + +!⁻ : Δ-Hom⁻ (suc m) 1 +!⁻ {m = zero} = id⁻ +!⁻ {m = suc m} = crush⁻ !⁻ +``` + +We can also define more familiar looking versions of face and degeneracy +map that are parameterized by some $i$. + +``` +δ⁺ : Fin (suc n) → Δ-Hom⁺ n (suc n) +δ⁺ {n = _} fzero = shift⁺ id⁺ +δ⁺ {n = suc _} (fsuc i) = keep⁺ (δ⁺ i) +σ⁻ : Fin n → Δ-Hom⁻ (suc n) n +σ⁻ fzero = crush⁻ id⁻ +σ⁻ (fsuc i) = keep⁻ (σ⁻ i) +``` + +Composites of face and degeneracy maps can be defined by a somewhat +tricky induction: note that both cases are dual to one another. + +```agda _∘⁻_ : Δ-Hom⁻ n o → Δ-Hom⁻ m n → Δ-Hom⁻ m o done⁻ ∘⁻ g = g crush⁻ f ∘⁻ crush⁻ g = crush⁻ (crush⁻ f ∘⁻ g) @@ -64,92 +188,53 @@ shift⁺ f ∘⁺ shift⁺ g = shift⁺ (f ∘⁺ shift⁺ g) keep⁺ f ∘⁺ shift⁺ g = shift⁺ (f ∘⁺ g) shift⁺ f ∘⁺ keep⁺ g = shift⁺ (f ∘⁺ keep⁺ g) keep⁺ f ∘⁺ keep⁺ g = keep⁺ (f ∘⁺ g) +``` -¡⁺ : Δ-Hom⁺ 0 m -¡⁺ {m = zero} = done⁺ -¡⁺ {m = suc m} = shift⁺ ¡⁺ +### Properties of face and degeneracy maps -cast⁺ : m ≡ m' → n ≡ n' → Δ-Hom⁺ m n → Δ-Hom⁺ m' n' -cast⁺ {zero} {zero} {zero} {zero} p q done⁺ = done⁺ -cast⁺ {zero} {zero} {zero} {suc n'} p q f = absurd (Nat.zero≠suc q) -cast⁺ {zero} {zero} {suc n} {zero} p q f = absurd (Nat.suc≠zero q) -cast⁺ {zero} {zero} {suc n} {suc n'} p q (shift⁺ f) = shift⁺ (cast⁺ p (Nat.suc-inj q) f) -cast⁺ {zero} {suc m'} {n} {n'} p q f = absurd (Nat.zero≠suc p) -cast⁺ {suc m} {zero} {n} {n'} p q f = absurd (Nat.suc≠zero p) -cast⁺ {suc m} {suc m'} {suc n} {zero} p q f = absurd (Nat.suc≠zero q) -cast⁺ {suc m} {suc m'} {suc n} {suc n'} p q (shift⁺ f) = shift⁺ (cast⁺ p (Nat.suc-inj q) f) -cast⁺ {suc m} {suc m'} {suc n} {suc n'} p q (keep⁺ f) = keep⁺ (cast⁺ (Nat.suc-inj p) (Nat.suc-inj q) f) +If $f : [m] \to [n]$ is a face map, then $m \leq n$. Conversely, +if $f$ is a degeneracy, then $m \geq n$. The slogan here is that +face maps increase dimension, and degeneracies lower it. -!⁻ : Δ-Hom⁻ (suc m) 1 -!⁻ {m = zero} = id⁻ -!⁻ {m = suc m} = crush⁻ !⁻ +```agda +Δ⁺-dim-≤ : ∀ {m n} → (f : Δ-Hom⁺ m n) → m Nat.≤ n +Δ⁺-dim-≤ done⁺ = Nat.0≤x +Δ⁺-dim-≤ (shift⁺ f) = Nat.≤-sucr (Δ⁺-dim-≤ f) +Δ⁺-dim-≤ (keep⁺ f) = Nat.s≤s (Δ⁺-dim-≤ f) + +Δ⁻-dim-≤ : ∀ {m n} → (f : Δ-Hom⁻ m n) → n Nat.≤ m +Δ⁻-dim-≤ done⁻ = Nat.0≤x +Δ⁻-dim-≤ (crush⁻ f) = Nat.s≤s (Nat.weaken-< (Δ⁻-dim-≤ f)) +Δ⁻-dim-≤ (keep⁻ f) = Nat.s≤s (Δ⁻-dim-≤ f) +``` -δ⁺ : Fin (suc n) → Δ-Hom⁺ n (suc n) -δ⁺ {n = _} fzero = shift⁺ id⁺ -δ⁺ {n = suc _} (fsuc i) = keep⁺ (δ⁺ i) +Moreover, if our face/degeneracy map contains a `shift⁺`/`crush⁻`, +then we know it must *strictly* increase/decrease the dimension. -σ⁻ : Fin n → Δ-Hom⁻ (suc n) n -σ⁻ fzero = crush⁻ id⁻ -σ⁻ (fsuc i) = keep⁻ (σ⁻ i) +``` +has-shift⁺ : ∀ {m n} → Δ-Hom⁺ m n → Type +has-shift⁺ done⁺ = ⊥ +has-shift⁺ (shift⁺ f) = ⊤ +has-shift⁺ (keep⁺ f) = has-shift⁺ f + +has-crush⁻ : ∀ {m n} → Δ-Hom⁻ m n → Type +has-crush⁻ done⁻ = ⊥ +has-crush⁻ (crush⁻ f) = ⊤ +has-crush⁻ (keep⁻ f) = has-crush⁻ f + +Δ⁺-dim-< : ∀ {m n} → (f : Δ-Hom⁺ m n) → has-shift⁺ f → m Nat.< n +Δ⁺-dim-< (shift⁺ f) p = Nat.s≤s (Δ⁺-dim-≤ f) +Δ⁺-dim-< (keep⁺ f) p = Nat.s≤s (Δ⁺-dim-< f p) + +Δ⁻-dim-< : ∀ {m n} → (f : Δ-Hom⁻ m n) → has-crush⁻ f → n Nat.< m +Δ⁻-dim-< (crush⁻ f) p = Nat.s≤s (Δ⁻-dim-≤ f) +Δ⁻-dim-< (keep⁻ f) p = Nat.s≤s (Δ⁻-dim-< f p) ``` -```agda -shift⁺-inj - : ∀ {f g : Δ-Hom⁺ m n} - → shift⁺ f ≡ shift⁺ g - → f ≡ g -shift⁺-inj {m} {n} {f} {g} = ap unshift where - unshift : Δ-Hom⁺ m (suc n) → Δ-Hom⁺ m n - unshift (shift⁺ h) = h - unshift (keep⁺ h) = f - -keep⁺-inj - : ∀ {f g : Δ-Hom⁺ m n} - → keep⁺ f ≡ keep⁺ g - → f ≡ g -keep⁺-inj {m} {n} {f} {g} = ap unkeep where - unkeep : Δ-Hom⁺ (suc m) (suc n) → Δ-Hom⁺ m n - unkeep (keep⁺ h) = h - unkeep (shift⁺ h) = f - -is-shift⁺ : Δ-Hom⁺ m n → Type -is-shift⁺ done⁺ = ⊥ -is-shift⁺ (shift⁺ _) = ⊤ -is-shift⁺ (keep⁺ _) = ⊥ - -is-keep⁺ : Δ-Hom⁺ m n → Type -is-keep⁺ done⁺ = ⊥ -is-keep⁺ (shift⁺ _) = ⊥ -is-keep⁺ (keep⁺ _) = ⊤ - -shift⁺≠keep⁺ - : ∀ {f : Δ-Hom⁺ (suc m) n} {g : Δ-Hom⁺ m n} - → ¬ (shift⁺ f ≡ keep⁺ g) -shift⁺≠keep⁺ p = subst is-shift⁺ p tt - -keep⁺≠shift⁺ - : ∀ {f : Δ-Hom⁺ m n} {g : Δ-Hom⁺ (suc m) n} - → ¬ (keep⁺ f ≡ shift⁺ g) -keep⁺≠shift⁺ p = subst is-keep⁺ p tt - -instance - Discrete-Δ-Hom⁺ : Discrete (Δ-Hom⁺ m n) - Discrete-Δ-Hom⁺ {x = done⁺} {y = done⁺} = - yes refl - Discrete-Δ-Hom⁺ {x = shift⁺ x} {y = shift⁺ y} = - Dec-map (ap shift⁺) shift⁺-inj Discrete-Δ-Hom⁺ - Discrete-Δ-Hom⁺ {x = shift⁺ x} {y = keep⁺ y} = - no shift⁺≠keep⁺ - Discrete-Δ-Hom⁺ {x = keep⁺ x} {y = shift⁺ y} = - no keep⁺≠shift⁺ - Discrete-Δ-Hom⁺ {x = keep⁺ x} {y = keep⁺ y} = - Dec-map (ap keep⁺) keep⁺-inj Discrete-Δ-Hom⁺ - -Δ-Hom⁺-is-set : is-set (Δ-Hom⁺ m n) -Δ-Hom⁺-is-set = Discrete→is-set Discrete-Δ-Hom⁺ -``` - -# Semantics +### Semantics of face and degeneracy maps + +As noted in the introduciton, maps in the simplicial category can also +be represented as maps between `Fin`. ```agda Δ⁺-map : ∀ {m n} → Δ-Hom⁺ m n → Fin m → Fin n @@ -164,11 +249,55 @@ instance Δ⁻-map (keep⁻ f) (fsuc i) = fsuc (Δ⁻-map f i) ``` +Face maps are always inflationary maps, and degeneracies are always +deflationary. + +```agda +Δ⁺-map-incr + : ∀ {m n} → (f : Δ-Hom⁺ m n) + → ∀ i → to-nat i Nat.≤ to-nat (Δ⁺-map f i) +Δ⁺-map-incr (shift⁺ f) i = Nat.≤-sucr (Δ⁺-map-incr f i) +Δ⁺-map-incr (keep⁺ f) fzero = Nat.0≤x +Δ⁺-map-incr (keep⁺ f) (fsuc i) = Nat.s≤s (Δ⁺-map-incr f i) + +Δ⁻-map-decr + : ∀ {m n} → (f : Δ-Hom⁻ m n) + → ∀ i → to-nat (Δ⁻-map f i) Nat.≤ to-nat i +Δ⁻-map-decr (crush⁻ f) fzero = 0≤x +Δ⁻-map-decr (crush⁻ f) (fsuc i) = Nat.≤-sucr (Δ⁻-map-decr f i) +Δ⁻-map-decr (keep⁻ f) fzero = Nat.0≤x +Δ⁻-map-decr (keep⁻ f) (fsuc i) = Nat.s≤s (Δ⁻-map-decr f i) +``` + +A useful corollary of this is that degeneracies always map 0 to 0. + +```agda +Δ⁻-map-zero + : ∀ {m n} (f : Δ-Hom⁻ (suc m) (suc n)) + → Δ⁻-map f fzero ≡ fzero +Δ⁻-map-zero f = to-nat-inj (Nat.≤-antisym (Δ⁻-map-decr f fzero) Nat.0≤x) +``` + +Furthermore, the interpretations of face and degeneracy maps are both +injective. + ```agda Δ⁺-map-inj : ∀ (f g : Δ-Hom⁺ m n) → (∀ i → Δ⁺-map f i ≡ Δ⁺-map g i) → f ≡ g +Δ⁻-map-inj + : ∀ (f g : Δ-Hom⁻ m n) + → (∀ i → Δ⁻-map f i ≡ Δ⁻-map g i) + → f ≡ g +``` + +
+This follows from a giant case bash that isn't particularly +enlightening. + + +```agda Δ⁺-map-inj done⁺ done⁺ p = refl Δ⁺-map-inj (shift⁺ f) (shift⁺ g) p = ap shift⁺ (Δ⁺-map-inj f g (fsuc-inj ⊙ p)) @@ -178,57 +307,82 @@ instance absurd (fzero≠fsuc (p 0)) Δ⁺-map-inj (keep⁺ f) (keep⁺ g) p = ap keep⁺ (Δ⁺-map-inj f g (fsuc-inj ⊙ p ⊙ fsuc)) + +Δ⁻-map-inj {m = zero} done⁻ done⁻ p = refl +Δ⁻-map-inj {m = suc m} (crush⁻ f) (crush⁻ g) p = + ap crush⁻ (Δ⁻-map-inj f g (p ⊙ fsuc)) +Δ⁻-map-inj {m = suc (suc m)} (crush⁻ f) (keep⁻ g) p = + absurd (fzero≠fsuc (sym (Δ⁻-map-zero f) ∙ p 1)) +Δ⁻-map-inj {m = suc (suc m)} (keep⁻ f) (crush⁻ g) p = + absurd (fsuc≠fzero (p 1 ∙ Δ⁻-map-zero g)) +-- Duplicate cases to keep exact split happy +Δ⁻-map-inj {m = suc zero} (keep⁻ f) (keep⁻ g) p = + ap keep⁻ (Δ⁻-map-inj f g (fsuc-inj ⊙ p ⊙ fsuc)) +Δ⁻-map-inj {m = suc (suc m)} (keep⁻ f) (keep⁻ g) p = + ap keep⁻ (Δ⁻-map-inj f g (fsuc-inj ⊙ p ⊙ fsuc)) ``` +
+ +With a bit of work, we can show that the interpretations take +identities to identities and composites to composites. Pure more +succinctly, the interpretation functions are functorial. ```agda Δ⁺-map-id : ∀ (i : Fin m) → Δ⁺-map id⁺ i ≡ i -Δ⁺-map-id fzero = refl -Δ⁺-map-id (fsuc i) = ap fsuc (Δ⁺-map-id i) +Δ⁻-map-id : ∀ (i : Fin m) → Δ⁻-map id⁻ i ≡ i Δ⁺-map-∘ : (f : Δ-Hom⁺ n o) (g : Δ-Hom⁺ m n) → ∀ (i : Fin m) → Δ⁺-map (f ∘⁺ g) i ≡ Δ⁺-map f (Δ⁺-map g i) -Δ⁺-map-∘ done⁺ done⁺ () -Δ⁺-map-∘ (shift⁺ f) (shift⁺ g) i = ap fsuc (Δ⁺-map-∘ f (shift⁺ g) i) -Δ⁺-map-∘ (shift⁺ f) (keep⁺ g) i = ap fsuc (Δ⁺-map-∘ f (keep⁺ g) i) -Δ⁺-map-∘ (keep⁺ f) (shift⁺ g) i = ap fsuc (Δ⁺-map-∘ f g i) -Δ⁺-map-∘ (keep⁺ f) (keep⁺ g) fzero = refl -Δ⁺-map-∘ (keep⁺ f) (keep⁺ g) (fsuc i) = ap fsuc (Δ⁺-map-∘ f g i) +Δ⁻-map-∘ + : (f : Δ-Hom⁻ n o) (g : Δ-Hom⁻ m n) + → ∀ (i : Fin m) → Δ⁻-map (f ∘⁻ g) i ≡ Δ⁻-map f (Δ⁻-map g i) ``` -# Categories +
+This follows from another series of case bashes. + ```agda -idl⁺ : ∀ (f : Δ-Hom⁺ m n) → id⁺ ∘⁺ f ≡ f -idl⁺ f = Δ⁺-map-inj _ _ λ i → - Δ⁺-map-∘ id⁺ f i ∙ Δ⁺-map-id (Δ⁺-map f i) +Δ⁺-map-id fzero = refl +Δ⁺-map-id (fsuc i) = ap fsuc (Δ⁺-map-id i) -idr⁺ : ∀ (f : Δ-Hom⁺ m n) → f ∘⁺ id⁺ ≡ f -idr⁺ {m = zero} f = refl -idr⁺ {m = suc m} (shift⁺ f) = ap shift⁺ (idr⁺ f) -idr⁺ {m = suc m} (keep⁺ f) = ap keep⁺ (idr⁺ f) +Δ⁻-map-id fzero = refl +Δ⁻-map-id (fsuc i) = ap fsuc (Δ⁻-map-id i) + +Δ⁺-map-∘ done⁺ done⁺ i = fabsurd i +Δ⁺-map-∘ (shift⁺ f) (shift⁺ g) i = ap fsuc (Δ⁺-map-∘ f (shift⁺ g) i) +Δ⁺-map-∘ (shift⁺ f) (keep⁺ g) i = ap fsuc (Δ⁺-map-∘ f (keep⁺ g) i) +Δ⁺-map-∘ (keep⁺ f) (shift⁺ g) i = ap fsuc (Δ⁺-map-∘ f g i) +Δ⁺-map-∘ (keep⁺ f) (keep⁺ g) fzero = refl +Δ⁺-map-∘ (keep⁺ f) (keep⁺ g) (fsuc i) = ap fsuc (Δ⁺-map-∘ f g i) -assoc⁺ - : ∀ (f : Δ-Hom⁺ n o) (g : Δ-Hom⁺ m n) (h : Δ-Hom⁺ l m) - → f ∘⁺ (g ∘⁺ h) ≡ (f ∘⁺ g) ∘⁺ h -assoc⁺ f g h = Δ⁺-map-inj _ _ λ i → - Δ⁺-map-∘ f (g ∘⁺ h) i - ∙ ap (Δ⁺-map f) (Δ⁺-map-∘ g h i) - ∙ sym (Δ⁺-map-∘ f g (Δ⁺-map h i)) - ∙ sym (Δ⁺-map-∘ (f ∘⁺ g) h i) +-- We can reduce the number of cases by handling all 'fzero' cases +-- at once. +Δ⁻-map-∘ {n = zero} {o = zero} done⁻ done⁻ i = + fabsurd i +Δ⁻-map-∘ {n = suc n} {o = suc o} f g fzero = + Δ⁻-map (f ∘⁻ g) fzero ≡⟨ Δ⁻-map-zero (f ∘⁻ g) ⟩ + fzero ≡˘⟨ Δ⁻-map-zero f ⟩ + Δ⁻-map f fzero ≡˘⟨ ap (Δ⁻-map f) (Δ⁻-map-zero g) ⟩ + Δ⁻-map f (Δ⁻-map g fzero) ∎ +Δ⁻-map-∘ {n = suc n} {o = suc o} (crush⁻ f) (crush⁻ g) (fsuc i) = + Δ⁻-map-∘ (crush⁻ f) g i +Δ⁻-map-∘ {n = suc n} {o = suc o} (crush⁻ f) (keep⁻ g) (fsuc i) = + Δ⁻-map-∘ f g i +Δ⁻-map-∘ {n = suc n} {o = suc o} (keep⁻ f) (crush⁻ g) (fsuc i) = + Δ⁻-map-∘ (keep⁻ f) g i +Δ⁻-map-∘ {n = suc n} {o = suc o} (keep⁻ f) (keep⁻ g) (fsuc i) = + ap fsuc (Δ⁻-map-∘ f g i) ``` +
-```agda -record Δ-Hom (m n : Nat) : Type where - no-eta-equality - constructor Δ-hom - field - {middle} : Nat - hom⁺ : Δ-Hom⁺ middle n - hom⁻ : Δ-Hom⁻ m middle +## Normal forms of maps -open Δ-Hom +First, note that we can extend all of the operations on face +and degeneracies to operations on normal forms. +```agda done : Δ-Hom 0 0 done .middle = 0 done .hom⁺ = done⁺ @@ -250,85 +404,459 @@ keep f .hom⁺ = keep⁺ (f .hom⁺) keep f .hom⁻ = keep⁻ (f .hom⁻) ``` +We can also define maps $[0] \to [n]$ and $[n] \to [1]$ for any $n$; +these maps will end up witnessing $[0]$ and $[1]$ as initial and terminal +objects, resp. + +```agda +¡Δ : Δ-Hom 0 n +¡Δ {n = zero} = done +¡Δ {n = suc n} = shift ¡Δ + +!Δ : Δ-Hom n 1 +!Δ {n = zero} = ¡Δ +!Δ {n = suc n} = crush !Δ +``` + +The identity morphism consists of a the identity face and degeneracy. + +```agda +idΔ : Δ-Hom n n +idΔ .middle = _ +idΔ .hom⁺ = id⁺ +idΔ .hom⁻ = id⁻ +``` + +Unfortunately, composites are not so simple, as we need to transform +an alternating chain of face and degeneracy maps into a single pair of +face and degenerac maps. This requires us to construct the following +4-way composition map. + + +```agda +composeΔ : Δ-Hom⁺ n o → Δ-Hom⁻ m n → Δ-Hom⁺ l m → Δ-Hom⁻ k l → Δ-Hom k o +``` + +There are quite a few cases here, so we will go through each individually. +The first case is relatively straightforward: the composite of the chain +$$\id_{-} \circ \id_{0} \circ g^{+} \circ g^{-}$$ +is $g^{+} \circ g^{-}$. + ```agda -exchange - : ∀ {m n o} - → Δ-Hom⁻ n o → Δ-Hom⁺ m n - → Δ-Hom m o -exchange done⁻ done⁺ = Δ-hom done⁺ done⁻ -exchange (crush⁻ f) (shift⁺ g) = exchange f g -exchange (crush⁻ f) (keep⁺ g) = crush (exchange f g) -exchange (keep⁻ f) (shift⁺ g) = shift (exchange f g) -exchange (keep⁻ f) (keep⁺ g) = keep (exchange f g) +composeΔ done⁺ done⁻ g⁺ g⁻ = + Δ-hom g⁺ g⁻ ``` +If the first map in the chain is a composite with a face map ala +$$(\delta \circ f^{+}) \circ f^{-} \circ g^{+} \circ g^{-}$$ +then we can reassociate and recurse on the rest of the chain. + +```agda +composeΔ (shift⁺ f⁺) f⁻ g⁺ g⁻ = + shift (composeΔ f⁺ f⁻ g⁺ g⁻) +``` + +Conversely, if domain of the chain is $0$, then we know that the +entire chain must be equal to the map out of the initial object. + +```agda +composeΔ (keep⁺ f⁺) f⁻ g⁺ done⁻ = + ¡Δ +``` + +If the final map in the chain is a composite with a degeneracy like +$$f^{+} \circ f^{-} \circ g^{+} \circ (g^{-} \circ \sigma)$$ +then we can again reassociate and recurse on the rest of the chain. + +```agda +composeΔ (keep⁺ f⁺) f⁻ g⁺ (crush⁻ g⁻) = + crush (composeΔ (keep⁺ f⁺) f⁻ g⁺ g⁻) +``` + +If the inner two maps are composites with a face and degeneracy +map like +$$f^{+} \circ (f^{-} \circ \sigma) \circ (\delta \circ g^{+}) \circ g^{-}$$ +then we can eliminate the face and degeneracy map, and recurse. + +```agda +composeΔ (keep⁺ f⁺) (crush⁻ f⁻) (shift⁺ g⁺) (keep⁻ g⁻) = + composeΔ (keep⁺ f⁺) f⁻ g⁺ (keep⁻ g⁻) +``` + +If only one map in the sequence does touches the 0th position, then we can +commute the relevant face/degeneracy outwards and recurse. + ```agda -Δ⁺ : Precategory lzero lzero -Δ⁺ .Ob = Nat -Δ⁺ .Hom = Δ-Hom⁺ -Δ⁺ .Hom-set _ _ = Δ-Hom⁺-is-set -Δ⁺ .id = id⁺ -Δ⁺ ._∘_ = _∘⁺_ -Δ⁺ .idr = idr⁺ -Δ⁺ .idl = idl⁺ -Δ⁺ .assoc = assoc⁺ +composeΔ (keep⁺ f⁺) (crush⁻ f⁻) (keep⁺ g⁺) (keep⁻ g⁻) = + crush (composeΔ (keep⁺ f⁺) f⁻ g⁺ g⁻) +composeΔ (keep⁺ f⁺) (keep⁻ f⁻) (shift⁺ g⁺) (keep⁻ g⁻) = + shift (composeΔ f⁺ f⁻ g⁺ (keep⁻ g⁻)) ``` +Finally, if none of the maps touch the 0th position, then we can proceed to +compose the rest of those 4 maps. + +```agda +composeΔ (keep⁺ f⁺) (keep⁻ f⁻) (keep⁺ g⁺) (keep⁻ g⁻) = + keep (composeΔ f⁺ f⁻ g⁺ g⁻) +``` + +We can then use this 4-way composition to construct composites of normal forms. + +```agda +_∘Δ_ : Δ-Hom n o → Δ-Hom m n → Δ-Hom m o +f ∘Δ g = composeΔ (f .hom⁺) (f .hom⁻) (g .hom⁺) (g .hom⁻) +``` + +-- + +-- All three classes of maps have decidable equality. -- ```agda --- Δ⁻-map-reflect-< --- : ∀ {m n} --- → (f : Δ-Hom⁻ m n) --- → ∀ {i j} → Δ⁻-map f i < Δ⁻-map f j → i < j --- Δ⁻-map-reflect-< (crush⁻ f) {fzero} {fsuc j} fi +-- Proving this is pretty tedious though, especially for +-- general morphisms. +-- + -- ```agda --- Δ⁺-map-inj --- : ∀ {m n} --- → (f : Δ-Hom⁺ m n) --- → ∀ {i j} → Δ⁺-map f i ≡ Δ⁺-map f j → i ≡ j --- Δ⁺-map-inj (shift⁺ f) {i} {j} p = Δ⁺-map-inj f (fsuc-inj p) --- Δ⁺-map-inj (keep⁺ f) {fzero} {fzero} p = refl --- Δ⁺-map-inj (keep⁺ f) {fzero} {fsuc j} p = absurd (fzero≠fsuc p) --- Δ⁺-map-inj (keep⁺ f) {fsuc i} {fzero} p = absurd (fzero≠fsuc (sym p)) --- Δ⁺-map-inj (keep⁺ f) {fsuc i} {fsuc j} p = ap fsuc (Δ⁺-map-inj f (fsuc-inj p)) - --- Δ⁻-map-split-surj --- : ∀ {m n} --- → (f : Δ-Hom⁻ m n) --- → ∀ i → fibre (Δ⁻-map f) i --- Δ⁻-map-split-surj (crush⁻ f) i with Δ⁻-map-split-surj f i --- ... | fzero , p = fsuc fzero , p --- ... | fsuc j , p = fsuc (fsuc j) , p --- Δ⁻-map-split-surj (keep⁻ f) fzero = fzero , refl --- Δ⁻-map-split-surj (keep⁻ f) (fsuc i) = --- Σ-map fsuc (ap fsuc) (Δ⁻-map-split-surj f i) +-- Discrete-Δ-Hom⁺ {x = done⁺} {y = done⁺} = +-- yes refl +-- Discrete-Δ-Hom⁺ {x = shift⁺ x} {y = shift⁺ y} = +-- Dec-map (ap shift⁺) shift⁺-inj Discrete-Δ-Hom⁺ +-- Discrete-Δ-Hom⁺ {x = shift⁺ x} {y = keep⁺ y} = +-- no shift⁺≠keep⁺ +-- Discrete-Δ-Hom⁺ {x = keep⁺ x} {y = shift⁺ y} = +-- no keep⁺≠shift⁺ +-- Discrete-Δ-Hom⁺ {x = keep⁺ x} {y = keep⁺ y} = +-- Dec-map (ap keep⁺) keep⁺-inj Discrete-Δ-Hom⁺ + +-- Discrete-Δ-Hom⁻ {x = done⁻} {y = done⁻} = +-- yes refl +-- Discrete-Δ-Hom⁻ {x = crush⁻ x} {y = crush⁻ y} = +-- Dec-map (ap crush⁻) crush⁻-inj Discrete-Δ-Hom⁻ +-- Discrete-Δ-Hom⁻ {x = crush⁻ x} {y = keep⁻ y} = +-- no crush⁻≠keep⁻ +-- Discrete-Δ-Hom⁻ {x = keep⁻ x} {y = crush⁻ y} = +-- no keep⁻≠crush⁻ +-- Discrete-Δ-Hom⁻ {x = keep⁻ x} {y = keep⁻ y} = +-- Dec-map (ap keep⁻) keep⁻-inj Discrete-Δ-Hom⁻ + +-- Discrete-Δ-Hom {x = x} {y = y} with x .middle ≡? y .middle +-- ... | yes p with cast⁺ p refl (x .hom⁺) ≡? (y .hom⁺) | cast⁻ refl p (x .hom⁻) ≡? y .hom⁻ +-- ... | yes q | yes r = +-- yes (Δ-Hom-path p (Equiv.to (cast⁺≃pathp p refl) q) (Equiv.to (cast⁻≃pathp refl p) r)) +-- ... | yes q | no ¬r = +-- no λ s → ¬r $ +-- subst (λ e → cast⁻ refl e (x .hom⁻) ≡ y .hom⁻) +-- (Nat.Nat-is-set _ _ _ _) +-- (Equiv.from (cast⁻≃pathp refl (ap middle s)) $ ap hom⁻ s) +-- ... | no ¬q | r = +-- no λ s → ¬q $ +-- subst (λ e → cast⁺ e refl (x .hom⁺) ≡ y .hom⁺) +-- (Nat.Nat-is-set _ _ _ _) +-- (Equiv.from (cast⁺≃pathp (ap middle s) refl) $ ap hom⁺ s) +-- Discrete-Δ-Hom {x = x} {y = y} | no ¬p = no (¬p ⊙ ap middle) -- ``` +-- + +-- By [[Hedberg's theorem]], all of these morphisms form sets. -- ```agda --- test : Fin 2 → Fin 3 --- test = Δ⁺-map (keep⁺ (shift⁺ id⁺)) +-- Δ-Hom⁺-is-set : is-set (Δ-Hom⁺ m n) +-- Δ-Hom⁺-is-set = Discrete→is-set Discrete-Δ-Hom⁺ + +-- Δ-Hom⁻-is-set : is-set (Δ-Hom⁻ m n) +-- Δ-Hom⁻-is-set = Discrete→is-set Discrete-Δ-Hom⁻ --- foo : Fin 3 --- foo = {!!} +-- Δ-Hom-is-set : is-set (Δ-Hom m n) +-- Δ-Hom-is-set = Discrete→is-set Discrete-Δ-Hom -- ``` + + + + + + + + +-- -- # Categories + +-- -- ```agda +-- -- Δ⁺-concrete : make-concrete Nat Δ-Hom⁺ +-- -- Δ⁺-concrete .make-concrete.id = id⁺ +-- -- Δ⁺-concrete .make-concrete._∘_ = _∘⁺_ +-- -- Δ⁺-concrete .make-concrete.lvl = lzero +-- -- Δ⁺-concrete .make-concrete.F₀ = Fin +-- -- Δ⁺-concrete .make-concrete.F₀-is-set = hlevel! +-- -- Δ⁺-concrete .make-concrete.F₁ = Δ⁺-map +-- -- Δ⁺-concrete .make-concrete.F₁-inj = Δ⁺-map-inj _ _ +-- -- Δ⁺-concrete .make-concrete.F-id = Δ⁺-map-id +-- -- Δ⁺-concrete .make-concrete.F-∘ = Δ⁺-map-∘ + +-- -- Δ⁺ : Precategory lzero lzero +-- -- unquoteDef Δ⁺ = define-concrete-category Δ⁺ Δ⁺-concrete +-- -- ``` + +-- -- ```agda +-- -- Δ⁻-concrete : make-concrete Nat Δ-Hom⁻ +-- -- Δ⁻-concrete .make-concrete.id = id⁻ +-- -- Δ⁻-concrete .make-concrete._∘_ = _∘⁻_ +-- -- Δ⁻-concrete .make-concrete.lvl = lzero +-- -- Δ⁻-concrete .make-concrete.F₀ = Fin +-- -- Δ⁻-concrete .make-concrete.F₀-is-set = hlevel! +-- -- Δ⁻-concrete .make-concrete.F₁ = Δ⁻-map +-- -- Δ⁻-concrete .make-concrete.F₁-inj = Δ⁻-map-inj _ _ +-- -- Δ⁻-concrete .make-concrete.F-id = Δ⁻-map-id +-- -- Δ⁻-concrete .make-concrete.F-∘ = Δ⁻-map-∘ + +-- -- Δ⁻ : Precategory lzero lzero +-- -- unquoteDef Δ⁻ = define-concrete-category Δ⁻ Δ⁻-concrete +-- -- ``` + +-- -- # The simplex category + +-- -- ```agda +-- -- done : Δ-Hom 0 0 +-- -- done .middle = 0 +-- -- done .hom⁺ = done⁺ +-- -- done .hom⁻ = done⁻ + +-- -- crush : Δ-Hom m (suc n) → Δ-Hom (suc m) (suc n) +-- -- crush f with f .middle | f .hom⁺ | f .hom⁻ +-- -- ... | zero | f⁺ | done⁻ = Δ-hom (keep⁺ ¡⁺) id⁻ +-- -- ... | suc x | f⁺ | f⁻ = Δ-hom f⁺ (crush⁻ f⁻) + +-- -- shift : Δ-Hom m n → Δ-Hom m (suc n) +-- -- shift f .middle = f .middle +-- -- shift f .hom⁺ = shift⁺ (f .hom⁺) +-- -- shift f .hom⁻ = f .hom⁻ + +-- -- keep : Δ-Hom m n → Δ-Hom (suc m) (suc n) +-- -- keep f .middle = suc (f .middle) +-- -- keep f .hom⁺ = keep⁺ (f .hom⁺) +-- -- keep f .hom⁻ = keep⁻ (f .hom⁻) +-- -- ``` + +-- -- ```agda +-- -- idΔ : ∀ {n} → Δ-Hom n n +-- -- idΔ {n} .middle = n +-- -- idΔ {n} .hom⁺ = id⁺ +-- -- idΔ {n} .hom⁻ = id⁻ + +-- -- exchange +-- -- : ∀ {m n o} +-- -- → Δ-Hom⁻ n o → Δ-Hom⁺ m n +-- -- → Δ-Hom m o +-- -- exchange done⁻ done⁺ = Δ-hom done⁺ done⁻ +-- -- exchange (crush⁻ f) (shift⁺ g) = exchange f g +-- -- exchange (crush⁻ f) (keep⁺ g) = crush (exchange f g) +-- -- exchange (keep⁻ f) (shift⁺ g) = shift (exchange f g) +-- -- exchange (keep⁻ f) (keep⁺ g) = keep (exchange f g) +-- -- ``` + + + +-- -- -- ```agda +-- -- -- Δ⁺-map-pres-< +-- -- -- : ∀ {m n} +-- -- -- → (f : Δ-Hom⁺ m n) +-- -- -- → ∀ {i j} → i < j → Δ⁺-map f i < Δ⁺-map f j +-- -- -- Δ⁺-map-pres-< (shift⁺ f) {i} {j} i @@ -106,12 +104,34 @@ isomorphism between their replacements $r(f)$, $r'(f)$ which commutes with both the `mediate`{.Agda} morphism and the `forget`{.Agda} morphism. We reproduce the proof from [@Borceux:vol1, §5.5]. +```agda + is-essentially-unique-factorisation + : ∀ {a b} (f : C.Hom a b) (fa : Factorisation C E M f) + → Type _ + is-essentially-unique-factorisation f fa = + ∀ (fa' : Factorisation C E M f) + → Σ[ f ∈ fa .mediating C.≅ fa' .mediating ] + ( (f .C.to C.∘ fa .mediate ≡ fa' .mediate) + × (fa .forget C.∘ f .C.from ≡ fa' .forget)) +``` + + + ```agda factorisation-essentially-unique - : ∀ {a b} (f : C.Hom a b) (fa1 fa2 : Factorisation C E M f) - → Σ[ f ∈ fa1 .mediating C.≅ fa2 .mediating ] - ( (f .C.to C.∘ fa1 .mediate ≡ fa2 .mediate) - × (fa1 .forget C.∘ f .C.from ≡ fa2 .forget)) + : ∀ {a b} (f : C.Hom a b) (fa : Factorisation C E M f) + → is-essentially-unique-factorisation f fa factorisation-essentially-unique f fa1 fa2 = C.make-iso (upq .fst) (vp'q' .fst) vu=id uv=id , upq .snd .fst , vp'q' .snd .snd where diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md index d1c24c44b..92550ee12 100644 --- a/src/Data/Fin/Base.lagda.md +++ b/src/Data/Fin/Base.lagda.md @@ -124,6 +124,13 @@ fzero≠fsuc {n = n} path = subst distinguish path tt where distinguish (fsuc _) = ⊥ ``` + + Next, we show that `fsuc` is injective. This again follows the proof in [`Data.Nat.Base`], but some extra care must be taken to ensure that `pred`{.Agda} is well typed! @@ -304,3 +311,10 @@ delete → Fin n → A delete ρ i j = ρ (skip i j) ``` + + diff --git a/src/Data/Fin/Properties.lagda.md b/src/Data/Fin/Properties.lagda.md index e9c0cc787..d77a576f9 100644 --- a/src/Data/Fin/Properties.lagda.md +++ b/src/Data/Fin/Properties.lagda.md @@ -294,3 +294,40 @@ insert-delete {n = n} ρ fzero a p (fsuc j) = refl insert-delete {n = suc n} ρ (fsuc i) a p fzero = refl insert-delete {n = suc n} ρ (fsuc i) a p (fsuc j) = insert-delete (ρ ∘ fsuc) i a p j ``` + + diff --git a/src/Data/Nat/Order.lagda.md b/src/Data/Nat/Order.lagda.md index f47d58b8a..cab2a548f 100644 --- a/src/Data/Nat/Order.lagda.md +++ b/src/Data/Nat/Order.lagda.md @@ -227,3 +227,18 @@ an inhabited subset. ℕ-well-ordered P-dec wit = ∥-∥-rec minimal-solution-unique (λ { (n , p) → ℕ-minimal-solution _ P-dec n p }) wit ``` + + diff --git a/src/bibliography.bibtex b/src/bibliography.bibtex index fc8889024..1ceadbb2c 100644 --- a/src/bibliography.bibtex +++ b/src/bibliography.bibtex @@ -17,6 +17,19 @@ keywords = {programming languages, specifications, compilers} } +@book{CWM, + address={New York, NY}, + series={Graduate Texts in Mathematics}, + title={Categories for the Working Mathematician}, + volume={5}, ISBN={978-1-4419-3123-8}, + url={http://link.springer.com/10.1007/978-1-4757-4721-8}, + DOI={10.1007/978-1-4757-4721-8}, + publisher={Springer New York}, author={Mac Lane, Saunders}, + year={1978}, + collection={Graduate Texts in Mathematics}, + language={en} +} + @book{SIGL, address = {New York, NY}, series = {Universitext}, From 7bbc34dd1603e80f949cae616fc457ebfde16eba Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 11 Apr 2024 18:10:49 -0400 Subject: [PATCH 03/18] def: fibrewise embeddings --- src/1Lab/Equiv/Fibrewise.lagda.md | 2 +- src/1Lab/Function/Embedding.lagda.md | 46 ++++++++++++++++++++++++++++ 2 files changed, 47 insertions(+), 1 deletion(-) diff --git a/src/1Lab/Equiv/Fibrewise.lagda.md b/src/1Lab/Equiv/Fibrewise.lagda.md index fc7d2c72e..a6b96fe20 100644 --- a/src/1Lab/Equiv/Fibrewise.lagda.md +++ b/src/1Lab/Equiv/Fibrewise.lagda.md @@ -16,7 +16,7 @@ open import 1Lab.Type module 1Lab.Equiv.Fibrewise where ``` -# Fibrewise equivalences +# Fibrewise equivalences {defines="fibrewise-equivalence"} In HoTT, a type family `P : A → Type` can be seen as a [_fibration_] with total space `Σ P`, with the fibration being the projection diff --git a/src/1Lab/Function/Embedding.lagda.md b/src/1Lab/Function/Embedding.lagda.md index e904c7d95..421a80de4 100644 --- a/src/1Lab/Function/Embedding.lagda.md +++ b/src/1Lab/Function/Embedding.lagda.md @@ -121,6 +121,12 @@ Subset-proj-embedding {B = B} Bprop x = Equiv→is-hlevel 1 (Fibre-equiv B x) (B + +## Fibrewise embeddings + +Like [[fibrewise equivalences]], fibrewise embeddings are equivalent +to embeddings between total spaces. + +```agda +module _ + {ℓ ℓ' ℓ''} {A : Type ℓ} {P : A → Type ℓ'} {Q : A → Type ℓ''} + {f : ∀ (x : A) → P x → Q x} + where + + injective→injectivep + : ∀ {x y} {px} {py} + → (∀ {x} → injective (f x)) + → (p : x ≡ y) + → PathP (λ i → Q (p i)) (f x px) (f y py) + → PathP (λ i → P (p i)) px py + injective→injectivep {x = x} {y = y} {px = px} {py = py} inj p = + J (λ y p → ∀ {py} → PathP (λ i → Q (p i)) (f x px) (f y py) → PathP (λ i → P (p i)) px py) + inj p + + embedding→total + : (∀ {x} → is-embedding (f x)) + → is-embedding (total f) + embedding→total always-emb y = + iso→is-hlevel 1 + (total-fibres .fst) + (total-fibres .snd) + (always-emb (y .snd)) + + total→embedding + : is-embedding (total f) + → ∀ {x} → is-embedding (f x) + total→embedding emb {x} y = + iso→is-hlevel 1 + (total-fibres .snd .is-iso.inv) + (is-iso.inverse (total-fibres .snd)) + (emb (x , y)) +``` From 323494016066030e9041d7467efca87af1cb1088 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 11 Apr 2024 18:11:25 -0400 Subject: [PATCH 04/18] def: misc fin/nat additions --- src/Data/Fin/Base.lagda.md | 22 ++++++++++++++++++++++ src/Data/Nat/Order.lagda.md | 5 ++++- 2 files changed, 26 insertions(+), 1 deletion(-) diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md index 92550ee12..64055c139 100644 --- a/src/Data/Fin/Base.lagda.md +++ b/src/Data/Fin/Base.lagda.md @@ -316,5 +316,27 @@ delete ρ i j = ρ (skip i j) ```agda fabsurd : ∀ {ℓ} {A : Type ℓ} → Fin 0 → A fabsurd () + +Finite-one-is-prop : is-prop (Fin 1) +Finite-one-is-prop fzero fzero = refl + +fpred : ∀ {n} → Fin (2 + n) → Fin (1 + n) +fpred fzero = fzero +fpred (fsuc i) = i + +fkeep : ∀ {m n} → (Fin m → Fin n) → Fin (suc m) → Fin (suc n) +fkeep f fzero = fzero +fkeep f (fsuc i) = fsuc (f i) + +fkeep-id : ∀ {n} → ∀ (i : Fin (suc n)) → fkeep (λ x → x) i ≡ i +fkeep-id fzero = refl +fkeep-id (fsuc i) = refl + +fkeep-∘ + : ∀ {m n o} + → {f : Fin n → Fin o} {g : Fin m → Fin n} + → ∀ i → fkeep (f ∘ g) i ≡ fkeep f (fkeep g i) +fkeep-∘ fzero = refl +fkeep-∘ (fsuc i) = refl ``` --> diff --git a/src/Data/Nat/Order.lagda.md b/src/Data/Nat/Order.lagda.md index cab2a548f..eba29ab9e 100644 --- a/src/Data/Nat/Order.lagda.md +++ b/src/Data/Nat/Order.lagda.md @@ -94,11 +94,14 @@ instance --> We also have that a successor is never smaller than the number it -succeeds: +succeeds, and that a successor is always larger than zero. ```agda ¬sucx≤x : (x : Nat) → ¬ (suc x ≤ x) ¬sucx≤x (suc x) (s≤s ord) = ¬sucx≤x x ord + +¬sucx≤0 : (x : Nat) → ¬ (suc x ≤ 0) +¬sucx≤0 x () ``` We can do proofs on pairs of natural numbers by splitting into cases of From 7f8cc9c96e7292c74cfbceeb4d78cdc59571064c Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 11 Apr 2024 18:24:34 -0400 Subject: [PATCH 05/18] def: concrete categories + macro --- src/Cat/Functor/Concrete.lagda.md | 193 ++++++++++++++++++++++++++++++ 1 file changed, 193 insertions(+) create mode 100644 src/Cat/Functor/Concrete.lagda.md diff --git a/src/Cat/Functor/Concrete.lagda.md b/src/Cat/Functor/Concrete.lagda.md new file mode 100644 index 000000000..398363f54 --- /dev/null +++ b/src/Cat/Functor/Concrete.lagda.md @@ -0,0 +1,193 @@ +--- +description: | + Concrete categories +--- + +```agda +module Cat.Functor.Concrete where +``` + +# Concrete categories {defines="concrete-category"} + +A category $\cC$ is **concrete** if it comes equipped with a faithful +functor into $\Sets$. + +```agda +module _ {o ℓ} (C : Precategory o ℓ) where + open Cat.Reasoning C + + record Concrete (κ : Level) : Type (o ⊔ ℓ ⊔ lsuc κ) where + no-eta-equality + field + Forget : Functor C (Sets κ) + has-faithful : is-faithful Forget +``` + +## Constructing concrete categories + +When we construct a category, we typically prove the associativity/unitality +conditions "by hand". However, this can be quite tedious for syntactic +presentations of categories, as it involves a large amount of induction. +However, these presentations are often meant to present some +category of structured functions between sets: if the presentation is +injective, then we can derive the category laws by simply lifting the +good definitional behaviour of functions along the presentation function. + +The following record contains the data required to perform this trick. + +```agda +record make-concrete + {o ℓ : Level} + (Ob : Type o) (Hom : Ob → Ob → Type ℓ) + : Typeω + where + no-eta-equality + field + id : ∀ {x} → Hom x x + _∘_ : ∀ {x y z} → Hom y z → Hom x y → Hom x z + + {lvl} : Level + F₀ : Ob → Type lvl + F₀-is-set : ∀ {x} → is-set (F₀ x) + + F₁ : ∀ {x y} → Hom x y → F₀ x → F₀ y + F₁-inj : ∀ {x y} {f g : Hom x y} → (∀ a → F₁ f a ≡ F₁ g a) → f ≡ g + F-id : ∀ {x} → (a : F₀ x) → F₁ id a ≡ a + F-∘ : ∀ {x y z} (f : Hom y z) (g : Hom x y) (a : F₀ x) → F₁ (f ∘ g) a ≡ F₁ f (F₁ g a) +``` + +We can show that our putative hom sets are actually sets by lifting +the hlevel proof along the injection. + +```agda + abstract + make-is-set + : ∀ x y → is-set (Hom x y) + make-is-set x y = injective→is-set (F₁-inj ⊙ happly) (fun-is-hlevel 2 F₀-is-set) +``` + +Likewise, all equations can be lifted as well. + +```agda + make-idl + : ∀ {x y} (f : Hom x y) + → id ∘ f ≡ f + make-idl f = F₁-inj λ a → + F₁ (id ∘ f) a ≡⟨ F-∘ id f a ⟩ + F₁ id (F₁ f a) ≡⟨ F-id (F₁ f a) ⟩ + F₁ f a ∎ + + make-idr + : ∀ {x y} (f : Hom x y) + → f ∘ id ≡ f + make-idr f = F₁-inj λ a → + F₁ (f ∘ id) a ≡⟨ F-∘ f id a ⟩ + F₁ f (F₁ id a) ≡⟨ ap (F₁ f) (F-id a) ⟩ + F₁ f a ∎ + + make-assoc + : ∀ {w x y z} (f : Hom y z) (g : Hom x y) (h : Hom w x) + → f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h + make-assoc f g h = F₁-inj λ a → + F₁ (f ∘ (g ∘ h)) a ≡⟨ F-∘ f (g ∘ h) a ∙ ap (F₁ f) (F-∘ g h a) ⟩ + F₁ f (F₁ g (F₁ h a)) ≡˘⟨ F-∘ (f ∘ g) h a ∙ F-∘ f g (F₁ h a) ⟩ + F₁ ((f ∘ g) ∘ h) a ∎ +``` + +Used naively, `make-concrete`{.Agda} would result in unreadable goals. To avoid +this, we provide macros that expand out the proofs in `make-concrete`{.Agda} +into a top-level definition implemented via copattern matching. + +```agda +define-concrete-category + : ∀ {o ℓ} {Ob : Type o} {Hom : Ob → Ob → Type ℓ} + → Name → make-concrete Ob Hom → TC ⊤ + +declare-concrete-category + : ∀ {o ℓ} {Ob : Type o} {Hom : Ob → Ob → Type ℓ} + → Name → make-concrete Ob Hom → TC ⊤ +``` + +
+The details of the macro are omitted to spare the innocent reader. + + +```agda +make-concrete-category + : ∀ {o ℓ} {Ob : Type o} {Hom : Ob → Ob → Type ℓ} + → Bool → Name → make-concrete Ob Hom → TC Name +make-concrete-category {o} {ℓ} {Ob} {Hom} declare? nm mk = do + `mk ← quoteωTC mk + `O ← quoteTC Ob + `H ← quoteTC Hom + + ty ← quoteTC (Precategory o ℓ) + case declare? of λ where + true → declare (argN nm) ty + false → pure tt + + -- Need to use field projections to avoid issues with implicit instantiation. + define-function nm $ + clause [] [ argN (proj (quote Precategory.Ob)) ] `O ∷ + clause [] [ argN (proj (quote Precategory.Hom)) ] `H ∷ + clause + [] + [ argN (proj (quote Precategory.Hom-set)) ] + (def (quote make-is-set) [ argN `mk ]) ∷ + clause + (implicits `O ["x"]) + (argN (proj (quote Precategory.id)) ∷ implicit-patterns 1) + (def (quote id) [ argN `mk , argH (var 0 []) ]) ∷ + clause + (implicits `O ["x", "y", "z"]) + (argN (proj (quote Precategory._∘_)) ∷ implicit-patterns 3) + (def (quote _∘_) [ argN `mk , argH (var 2 []) , argH (var 1 []) , argH (var 0 []) ]) ∷ + clause + (implicits `O ["x", "y"]) + (argN (proj (quote Precategory.idr)) ∷ implicit-patterns 2) + (def (quote make-idr) [ argN `mk , argH (var 1 []) , argH (var 0 []) ]) ∷ + clause + (implicits `O ["x", "y"]) + (argN (proj (quote Precategory.idl)) ∷ implicit-patterns 2) + (def (quote make-idl) [ argN `mk , argH (var 1 []) , argH (var 0 []) ]) ∷ + clause + (implicits `O ["w", "x", "y", "z"]) + (argN (proj (quote Precategory.assoc)) ∷ implicit-patterns 4) + (def (quote make-assoc) [ argN `mk , argH (var 3 []) , argH (var 2 []) , argH (var 1 []) , argH (var 0 []) ]) ∷ + [] + pure nm + where + open make-concrete + + implicits : Term → List String → Telescope + implicits ty = map (_, argH ty) + + implicit-patterns : Nat → List (Arg Pattern) + implicit-patterns 0 = [] + implicit-patterns (suc n) = argH (var n) ∷ implicit-patterns n + + implicit-args : Nat → List (Arg Term) + implicit-args 0 = [] + implicit-args (suc n) = argH (var n []) ∷ implicit-args n + +declare-concrete-category nm mk = do + make-concrete-category true nm mk + pure tt + +define-concrete-category nm mk = do + make-concrete-category false nm mk + pure tt +``` +
From 9c9b9f7ed1ce2ff75af3185ab16357f0e4ec674a Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 11 Apr 2024 18:24:49 -0400 Subject: [PATCH 06/18] wip: simplex category --- src/Cat/Instances/Simplex.lagda.md | 1662 ++++++++++++++++++---------- 1 file changed, 1051 insertions(+), 611 deletions(-) diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md index f853664a3..d1e4c35b3 100644 --- a/src/Cat/Instances/Simplex.lagda.md +++ b/src/Cat/Instances/Simplex.lagda.md @@ -1,6 +1,6 @@ --- description: | - Concrete categories + The simplex category. --- @@ -39,8 +50,8 @@ generated from 2 classes of maps: - Degeneracy maps $\sigma^{n}_{i} : [n + 1] \to [n]$ for $0 \leq i < n$, $0 < n$ Intuitively, the face maps $\delta^{n}_{i}$ are injections that skip the $i$th -element of $[n + 1]$, and degeneracy maps are surjections that take both $i$ and -$i+1$ to $i$. +element of $[n + 1]$, and degeneracy maps are surjections that take both $i$th and +$i+1$-th element of $[n + 1]$ to $i$. Unfortunately, we need to quotient these generators to get the correct category; these equations are known as the **simplicial identities**, and @@ -72,8 +83,9 @@ private variable These normal forms are relatively straightforward to encode in Agda: descending chains of face maps can be defined via an indexed inductive, -where `shift⁺`{.Agda} introduces the nth face map, and `keep⁺`{.Agda} keeps -the value of 'n' fixed. +where `shift⁺`{.Agda} postcomposes the nth face map, and `keep⁺`{.Agda} keeps +the value of 'n' fixed. We call these maps **semisimplicial**, and the +resulting category will be denoted $\Delta^{+}$ ```agda data Δ-Hom⁺ : Nat → Nat → Type where @@ -83,57 +95,86 @@ data Δ-Hom⁺ : Nat → Nat → Type where ``` Descending chains of degeneracies are defined in a similar fashion, where -where `crush⁻`{.Agda} introduces the nth degeneracy map. +where `crush⁻`{.Agda} precomposes the nth degeneracy map. We will call +these maps **demisimplicial**, and the category they form will be denoted +$\Delta^{-}.$ ```agda data Δ-Hom⁻ : Nat → Nat → Type where done⁻ : Δ-Hom⁻ 0 0 - crush⁻ : ∀ {m n} → Δ-Hom⁻ m (suc n) → Δ-Hom⁻ (suc m) (suc n) + crush⁻ : ∀ {m n} → Δ-Hom⁻ (suc m) n → Δ-Hom⁻ (suc (suc m)) n keep⁻ : ∀ {m n} → Δ-Hom⁻ m n → Δ-Hom⁻ (suc m) (suc n) ``` -Morphisms in $\Delta$ consist of 2 composable chains of face and degeneracy +Morphisms in $\Delta$ consist of a pair of composable semi and demisimplicial maps. Note that we allow both `m` and `n` to be 0; this allows us to share code between the simplex and augmented simplex category. ```agda record Δ-Hom (m n : Nat) : Type where no-eta-equality - constructor Δ-hom + constructor Δ-factor field - {middle} : Nat - hom⁺ : Δ-Hom⁺ middle n - hom⁻ : Δ-Hom⁻ m middle + {im} : Nat + hom⁺ : Δ-Hom⁺ im n + hom⁻ : Δ-Hom⁻ m im open Δ-Hom ``` + + -## Face and degeneracy maps +## Identities and composites -Identity morphisms $[n] \to [n]$ are defined via induction on $n$, -and do not contain any face or degeneracy maps. +Identity morphisms $[n] \to [n]$ in $\Delta^{+}$ and $\Delta^{-}$ are defined +via induction on $n$, and do not contain any face or degeneracy maps. ```agda id⁺ : ∀ {n} → Δ-Hom⁺ n n @@ -145,718 +186,1117 @@ id⁻ {zero} = done⁻ id⁻ {suc n} = keep⁻ id⁻ ``` -There are also face maps from $0 \to n$ and degeneracies $1 + n \to 1$ -for any $n$. +Identity morphisms in $\Delta$ factorize as the identities in $\Delta^{+}$ +and $\Delta^{-}$. ```agda -¡⁺ : Δ-Hom⁺ 0 m -¡⁺ {m = zero} = done⁺ -¡⁺ {m = suc m} = shift⁺ ¡⁺ +idΔ : Δ-Hom n n +idΔ .im = _ +idΔ .hom⁺ = id⁺ +idΔ .hom⁻ = id⁻ +``` + +Composites of semi and demisimplicial maps can be defined by a pair of +somewhat tricky inductions. + +```agda +_∘⁺_ : Δ-Hom⁺ n o → Δ-Hom⁺ m n → Δ-Hom⁺ m o +f ∘⁺ done⁺ = f +shift⁺ f ∘⁺ shift⁺ g = shift⁺ (f ∘⁺ shift⁺ g) +keep⁺ f ∘⁺ shift⁺ g = shift⁺ (f ∘⁺ g) +shift⁺ f ∘⁺ keep⁺ g = shift⁺ (f ∘⁺ keep⁺ g) +keep⁺ f ∘⁺ keep⁺ g = keep⁺ (f ∘⁺ g) -!⁻ : Δ-Hom⁻ (suc m) 1 -!⁻ {m = zero} = id⁻ -!⁻ {m = suc m} = crush⁻ !⁻ +_∘⁻_ : Δ-Hom⁻ n o → Δ-Hom⁻ m n → Δ-Hom⁻ m o +done⁻ ∘⁻ g = g +crush⁻ f ∘⁻ crush⁻ g = crush⁻ (crush⁻ f ∘⁻ g) +crush⁻ f ∘⁻ keep⁻ (crush⁻ g) = crush⁻ (crush⁻ (f ∘⁻ g)) +crush⁻ f ∘⁻ keep⁻ (keep⁻ g) = crush⁻ (f ∘⁻ (keep⁻ g)) +keep⁻ f ∘⁻ crush⁻ g = crush⁻ (keep⁻ f ∘⁻ g) +keep⁻ f ∘⁻ keep⁻ g = keep⁻ (f ∘⁻ g) ``` -We can also define more familiar looking versions of face and degeneracy -map that are parameterized by some $i$. +Composites of simplicial maps are even more tricky, as we +need to somehow factor a string of maps $f^{+} \circ f^{-} \circ g^{+} \circ g^{-}$ +into a pair of a semisimplicial and demisimplicial maps. The crux of +the problem is factoring $f^{-} \circ g^{+}$ as a semisimplicial map +$h^{+}$ and demisimplicial map $h^{-}$; once we do this, we can +pre and post-compose $g^{-}$ and $f^{+}$, resp. +We begin by computing the image of the putative factorization of $f^{-} \circ g^{+}$. + +```agda +imΔ : Δ-Hom⁻ n o → Δ-Hom⁺ m n → Nat +imΔ done⁻ done⁺ = 0 +imΔ (crush⁻ f) (shift⁺ g) = imΔ f g +imΔ (crush⁻ f) (keep⁺ (shift⁺ g)) = imΔ f (keep⁺ g) +imΔ (crush⁻ f) (keep⁺ (keep⁺ g)) = imΔ f (keep⁺ g) +imΔ (keep⁻ f) (shift⁺ g) = imΔ f g +imΔ (keep⁻ f) (keep⁺ g) = suc (imΔ f g) ``` -δ⁺ : Fin (suc n) → Δ-Hom⁺ n (suc n) -δ⁺ {n = _} fzero = shift⁺ id⁺ -δ⁺ {n = suc _} (fsuc i) = keep⁺ (δ⁺ i) -σ⁻ : Fin n → Δ-Hom⁻ (suc n) n -σ⁻ fzero = crush⁻ id⁻ -σ⁻ (fsuc i) = keep⁻ (σ⁻ i) +Next, we can compute both the semi and demisimplicial components of +the factorization via a pair of gnarly inductions. + +```agda +_∘Δ⁺_ : (f⁻ : Δ-Hom⁻ n o) → (f⁺ : Δ-Hom⁺ m n) → Δ-Hom⁺ (imΔ f⁻ f⁺) o +_∘Δ⁺_ done⁻ done⁺ = done⁺ +_∘Δ⁺_ (crush⁻ f⁺) (shift⁺ f⁻) = f⁺ ∘Δ⁺ f⁻ +_∘Δ⁺_ (crush⁻ f⁺) (keep⁺ (shift⁺ f⁻)) = f⁺ ∘Δ⁺ (keep⁺ f⁻) +_∘Δ⁺_ (crush⁻ f⁺) (keep⁺ (keep⁺ f⁻)) = f⁺ ∘Δ⁺ (keep⁺ f⁻) +_∘Δ⁺_ (keep⁻ f⁺) (shift⁺ f⁻) = shift⁺ (f⁺ ∘Δ⁺ f⁻) +_∘Δ⁺_ (keep⁻ f⁺) (keep⁺ f⁻) = keep⁺ (f⁺ ∘Δ⁺ f⁻) + +_∘Δ⁻_ : (f⁻ : Δ-Hom⁻ n o) → (f⁺ : Δ-Hom⁺ m n) → Δ-Hom⁻ m (imΔ f⁻ f⁺) +_∘Δ⁻_ done⁻ done⁺ = done⁻ +_∘Δ⁻_ (crush⁻ f⁻) (shift⁺ f⁺) = f⁻ ∘Δ⁻ f⁺ +_∘Δ⁻_ (crush⁻ f⁻) (keep⁺ (shift⁺ f⁺)) = f⁻ ∘Δ⁻ (keep⁺ f⁺) +_∘Δ⁻_ (crush⁻ f⁻) (keep⁺ (keep⁺ f⁺)) = crush⁻ (f⁻ ∘Δ⁻ (keep⁺ f⁺)) +_∘Δ⁻_ (keep⁻ f⁻) (shift⁺ f⁺) = f⁻ ∘Δ⁻ f⁺ +_∘Δ⁻_ (keep⁻ f⁻) (keep⁺ f⁺) = keep⁻ (f⁻ ∘Δ⁻ f⁺) ``` -Composites of face and degeneracy maps can be defined by a somewhat -tricky induction: note that both cases are dual to one another. +With that hard work out of the way, constructing the composite of +simplicial maps just requires us to pre and post-compose with $g^{-}$ +and $f^{+}$, resp. ```agda -_∘⁻_ : Δ-Hom⁻ n o → Δ-Hom⁻ m n → Δ-Hom⁻ m o -done⁻ ∘⁻ g = g -crush⁻ f ∘⁻ crush⁻ g = crush⁻ (crush⁻ f ∘⁻ g) -crush⁻ f ∘⁻ keep⁻ g = crush⁻ (f ∘⁻ g) -keep⁻ f ∘⁻ crush⁻ g = crush⁻ (keep⁻ f ∘⁻ g) -keep⁻ f ∘⁻ keep⁻ g = keep⁻ (f ∘⁻ g) +_∘Δ_ : Δ-Hom n o → Δ-Hom m n → Δ-Hom m o +(f ∘Δ g) .im = imΔ (f .hom⁻) (g .hom⁺) +(f ∘Δ g) .hom⁺ = f .hom⁺ ∘⁺ (f .hom⁻ ∘Δ⁺ g .hom⁺) +(f ∘Δ g) .hom⁻ = (f .hom⁻ ∘Δ⁻ g .hom⁺) ∘⁻ g .hom⁻ +``` -_∘⁺_ : Δ-Hom⁺ n o → Δ-Hom⁺ m n → Δ-Hom⁺ m o -f ∘⁺ done⁺ = f -shift⁺ f ∘⁺ shift⁺ g = shift⁺ (f ∘⁺ shift⁺ g) -keep⁺ f ∘⁺ shift⁺ g = shift⁺ (f ∘⁺ g) -shift⁺ f ∘⁺ keep⁺ g = shift⁺ (f ∘⁺ keep⁺ g) -keep⁺ f ∘⁺ keep⁺ g = keep⁺ (f ∘⁺ g) +## As maps between finite sets + +At this point, we could prove the associativity/unitality laws for +$\Delta^{+}, \Delta^{-}$, and $\Delta$ by a series of brutal inductions. +Luckily for us, there is a more elegant approach: all of these maps +have interpretations as maps `Fin m → Fin n`, and these interpretations +are both injective and functorial. This allows us to lift equations from functions +back to equations on their syntactic presentations, which gives us associativity +and unitality "for free". + +With that plan outlined, we begin by constructing interpretations +of (semi/demi) simplicial maps as functions. + +```agda +Δ-hom⁺ : ∀ {m n} → Δ-Hom⁺ m n → Fin m → Fin n +Δ-hom⁺ (shift⁺ f) = fsuc ⊙ Δ-hom⁺ f +Δ-hom⁺ (keep⁺ f) = fkeep (Δ-hom⁺ f) + +Δ-hom⁻ : ∀ {m n} → Δ-Hom⁻ m n → Fin m → Fin n +Δ-hom⁻ (crush⁻ f) = Δ-hom⁻ f ⊙ fpred +Δ-hom⁻ (keep⁻ f) = fkeep (Δ-hom⁻ f) + +Δ-hom : ∀ {m n} → Δ-Hom m n → Fin m → Fin n +Δ-hom f = Δ-hom⁺ (f .hom⁺) ⊙ Δ-hom⁻ (f .hom⁻) +``` + + + +We will denote each of these interpretations with `⟦ f ⟧ i` to avoid +too much syntactic overhead. + +```agda +instance + Δ-Hom⁺-⟦⟧-notation + : ∀ {m n} → ⟦⟧-notation (Δ-Hom⁺ m n) + Δ-Hom⁻-⟦⟧-notation + : ∀ {m n} → ⟦⟧-notation (Δ-Hom⁻ m n) + Δ-Hom-⟦⟧-notation + : ∀ {m n} → ⟦⟧-notation (Δ-Hom m n) ``` -### Properties of face and degeneracy maps + + +Note that semisimplicial maps always encode inflationary functions. ```agda -Δ⁺-dim-≤ : ∀ {m n} → (f : Δ-Hom⁺ m n) → m Nat.≤ n -Δ⁺-dim-≤ done⁺ = Nat.0≤x -Δ⁺-dim-≤ (shift⁺ f) = Nat.≤-sucr (Δ⁺-dim-≤ f) -Δ⁺-dim-≤ (keep⁺ f) = Nat.s≤s (Δ⁺-dim-≤ f) +Δ-hom⁺-incr + : ∀ (f⁺ : Δ-Hom⁺ m n) + → ∀ i → to-nat i Nat.≤ to-nat (⟦ f⁺ ⟧ i) +Δ-hom⁺-incr (shift⁺ f) i = Nat.≤-sucr (Δ-hom⁺-incr f i) +Δ-hom⁺-incr (keep⁺ f) fzero = Nat.0≤x +Δ-hom⁺-incr (keep⁺ f) (fsuc i) = Nat.s≤s (Δ-hom⁺-incr f i) +``` -Δ⁻-dim-≤ : ∀ {m n} → (f : Δ-Hom⁻ m n) → n Nat.≤ m -Δ⁻-dim-≤ done⁻ = Nat.0≤x -Δ⁻-dim-≤ (crush⁻ f) = Nat.s≤s (Nat.weaken-< (Δ⁻-dim-≤ f)) -Δ⁻-dim-≤ (keep⁻ f) = Nat.s≤s (Δ⁻-dim-≤ f) +Likewise, demisimplicial maps always encode deflationary functions. + +```agda +Δ-hom⁻-decr + : ∀ (f⁻ : Δ-Hom⁻ m n) + → ∀ i → to-nat (⟦ f⁻ ⟧ i) Nat.≤ to-nat i +Δ-hom⁻-decr (crush⁻ f) fzero = Δ-hom⁻-decr f fzero +Δ-hom⁻-decr (crush⁻ f) (fsuc i) = Nat.≤-sucr (Δ-hom⁻-decr f i) +Δ-hom⁻-decr (keep⁻ f) fzero = Nat.0≤x +Δ-hom⁻-decr (keep⁻ f) (fsuc i) = Nat.s≤s (Δ-hom⁻-decr f i) ``` -Moreover, if our face/degeneracy map contains a `shift⁺`/`crush⁻`, -then we know it must *strictly* increase/decrease the dimension. +A useful corollary of this is that demisimplicial maps always map 0 to 0. +```agda +Δ-hom⁻-zero + : ∀ {m n} (f⁻ : Δ-Hom⁻ (suc m) (suc n)) + → ⟦ f⁻ ⟧ fzero ≡ fzero +Δ-hom⁻-zero f⁻ = to-nat-inj (Nat.≤-antisym (Δ-hom⁻-decr f⁻ fzero) Nat.0≤x) ``` -has-shift⁺ : ∀ {m n} → Δ-Hom⁺ m n → Type -has-shift⁺ done⁺ = ⊥ -has-shift⁺ (shift⁺ f) = ⊤ -has-shift⁺ (keep⁺ f) = has-shift⁺ f -has-crush⁻ : ∀ {m n} → Δ-Hom⁻ m n → Type -has-crush⁻ done⁻ = ⊥ -has-crush⁻ (crush⁻ f) = ⊤ -has-crush⁻ (keep⁻ f) = has-crush⁻ f +Moreover, semisimplicial maps always encode injective functions, and +demisimplicial maps encode *split* surjections. + +```agda +Δ-hom⁺-to-inj + : ∀ {m n} + → (f : Δ-Hom⁺ m n) + → injective (Δ-hom⁺ f) +Δ-hom⁻-to-split-surj + : ∀ {m n} + → (f : Δ-Hom⁻ m n) + → ∀ (i : Fin n) → fibre (Δ-hom⁻ f) i +``` -Δ⁺-dim-< : ∀ {m n} → (f : Δ-Hom⁺ m n) → has-shift⁺ f → m Nat.< n -Δ⁺-dim-< (shift⁺ f) p = Nat.s≤s (Δ⁺-dim-≤ f) -Δ⁺-dim-< (keep⁺ f) p = Nat.s≤s (Δ⁺-dim-< f p) +
+These both follow directly via induction, so we omit the proofs. + -Δ⁻-dim-< : ∀ {m n} → (f : Δ-Hom⁻ m n) → has-crush⁻ f → n Nat.< m -Δ⁻-dim-< (crush⁻ f) p = Nat.s≤s (Δ⁻-dim-≤ f) -Δ⁻-dim-< (keep⁻ f) p = Nat.s≤s (Δ⁻-dim-< f p) +```agda +Δ-hom⁺-to-inj (shift⁺ f) p = + Δ-hom⁺-to-inj f (fsuc-inj p) +Δ-hom⁺-to-inj (keep⁺ f) {fzero} {fzero} p = + refl +Δ-hom⁺-to-inj (keep⁺ f) {fzero} {fsuc y} p = + absurd (fzero≠fsuc p) +Δ-hom⁺-to-inj (keep⁺ f) {fsuc x} {fzero} p = + absurd (fsuc≠fzero p) +Δ-hom⁺-to-inj (keep⁺ f) {fsuc x} {fsuc y} p = + ap fsuc (Δ-hom⁺-to-inj f (fsuc-inj p)) + +Δ-hom⁻-to-split-surj {m = suc m} f fzero = + fzero , Δ-hom⁻-zero f +Δ-hom⁻-to-split-surj (crush⁻ f) (fsuc i) = + Σ-map fsuc (λ p → p) (Δ-hom⁻-to-split-surj f (fsuc i)) +Δ-hom⁻-to-split-surj {m = suc m} (keep⁻ f) (fsuc i) = + Σ-map fsuc (ap fsuc) (Δ-hom⁻-to-split-surj f i) ``` +
-### Semantics of face and degeneracy maps +We also remark that semi and demisimplicial maps always encode monotonic functions. -As noted in the introduciton, maps in the simplicial category can also -be represented as maps between `Fin`. +```agda +Δ-hom⁺-pres-≤ + : ∀ (f⁺ : Δ-Hom⁺ m n) + → ∀ {i j} → i ≤ j → ⟦ f⁺ ⟧ i ≤ ⟦ f⁺ ⟧ j +Δ-hom⁺-pres-≤ (shift⁺ f) {i} {j} i≤j = Nat.s≤s (Δ-hom⁺-pres-≤ f i≤j) +Δ-hom⁺-pres-≤ (keep⁺ f) {fzero} {j} i≤j = Nat.0≤x +Δ-hom⁺-pres-≤ (keep⁺ f) {fsuc i} {fsuc j} i≤j = Nat.s≤s (Δ-hom⁺-pres-≤ f (Nat.≤-peel i≤j)) + +Δ-hom⁻-pres-≤ + : ∀ (f⁻ : Δ-Hom⁻ m n) + → ∀ {i j} → i ≤ j → ⟦ f⁻ ⟧ i ≤ ⟦ f⁻ ⟧ j +Δ-hom⁻-pres-≤ (crush⁻ f) {fzero} {j} i≤j = Nat.≤-trans (Δ-hom⁻-decr f fzero) Nat.0≤x +Δ-hom⁻-pres-≤ (crush⁻ f) {fsuc i} {fsuc j} i≤j = Δ-hom⁻-pres-≤ f (Nat.≤-peel i≤j) +Δ-hom⁻-pres-≤ (keep⁻ f) {fzero} {j} i≤j = Nat.0≤x +Δ-hom⁻-pres-≤ (keep⁻ f) {fsuc i} {fsuc j} i≤j = Nat.s≤s (Δ-hom⁻-pres-≤ f (Nat.≤-peel i≤j)) +``` + +This in turn implies that simplicial maps also encode monotonic functions. ```agda -Δ⁺-map : ∀ {m n} → Δ-Hom⁺ m n → Fin m → Fin n -Δ⁺-map (shift⁺ f) i = fsuc (Δ⁺-map f i) -Δ⁺-map (keep⁺ f) fzero = fzero -Δ⁺-map (keep⁺ f) (fsuc i) = fsuc (Δ⁺-map f i) +Δ-hom-pres-≤ + : ∀ (f : Δ-Hom m n) + → ∀ {i j} → i ≤ j → ⟦ f ⟧ i ≤ ⟦ f ⟧ j +Δ-hom-pres-≤ f i≤j = Δ-hom⁺-pres-≤ (f .hom⁺) (Δ-hom⁻-pres-≤ (f .hom⁻) i≤j) +``` -Δ⁻-map : ∀ {m n} → Δ-Hom⁻ m n → Fin m → Fin n -Δ⁻-map (crush⁻ f) fzero = fzero -Δ⁻-map (crush⁻ f) (fsuc i) = Δ⁻-map f i -Δ⁻-map (keep⁻ f) fzero = fzero -Δ⁻-map (keep⁻ f) (fsuc i) = fsuc (Δ⁻-map f i) +Semisimplicial maps are not just monotonic; they are *strictly* monotonic! + +```agda +Δ-hom⁺-pres-< + : ∀ (f⁺ : Δ-Hom⁺ m n) + → ∀ {i j} → i < j → ⟦ f⁺ ⟧ i < ⟦ f⁺ ⟧ j +Δ-hom⁺-pres-< (shift⁺ f⁺) {i} {j} i +We can show this with a rather brutal induction. + ```agda -Δ⁻-map-zero - : ∀ {m n} (f : Δ-Hom⁻ (suc m) (suc n)) - → Δ⁻-map f fzero ≡ fzero -Δ⁻-map-zero f = to-nat-inj (Nat.≤-antisym (Δ⁻-map-decr f fzero) Nat.0≤x) +Δ-hom-im-unique done⁺ done⁺ f⁻ g⁻ p = refl +Δ-hom-im-unique (shift⁺ f⁺) (shift⁺ g⁺) f⁻ g⁻ p = + Δ-hom-im-unique f⁺ g⁺ f⁻ g⁻ (fsuc-inj ⊙ p) +Δ-hom-im-unique {m = suc m} (shift⁺ f⁺) (keep⁺ g⁺) f⁻ g⁻ p = + absurd (fsuc≠fzero (p 0 ∙ ap₂ fkeep refl (Δ-hom⁻-zero g⁻))) +Δ-hom-im-unique {m = suc m} (keep⁺ f⁺) (shift⁺ g⁺) f⁻ g⁻ p = + absurd (fzero≠fsuc (ap₂ fkeep refl (sym (Δ-hom⁻-zero f⁻)) ∙ p 0)) +Δ-hom-im-unique (keep⁺ f⁺) (keep⁺ g⁺) (crush⁻ f⁻) (crush⁻ g⁻) p = + Δ-hom-im-unique (keep⁺ f⁺) (keep⁺ g⁺) f⁻ g⁻ (p ⊙ fsuc) +Δ-hom-im-unique (keep⁺ f⁺) (keep⁺ g⁺) (crush⁻ f⁻) (keep⁻ g⁻) p = + absurd (fzero≠fsuc (ap₂ fkeep refl (sym (Δ-hom⁻-zero f⁻)) ∙ p 1)) +Δ-hom-im-unique (keep⁺ f⁺) (keep⁺ g⁺) (keep⁻ f⁻) (crush⁻ g⁻) p = + absurd (fsuc≠fzero (p 1 ∙ ap₂ fkeep refl (Δ-hom⁻-zero g⁻))) +Δ-hom-im-unique (keep⁺ f⁺) (keep⁺ g⁺) (keep⁻ f⁻) (keep⁻ g⁻) p = + ap suc (Δ-hom-im-unique f⁺ g⁺ f⁻ g⁻ (fsuc-inj ⊙ p ⊙ fsuc)) ``` + -Furthermore, the interpretations of face and degeneracy maps are both -injective. +We also need to show that if a pair of factorizations is semantically +equal, then the semi and demisimplicial components are syntactically equal. ```agda -Δ⁺-map-inj - : ∀ (f g : Δ-Hom⁺ m n) - → (∀ i → Δ⁺-map f i ≡ Δ⁺-map g i) - → f ≡ g -Δ⁻-map-inj - : ∀ (f g : Δ-Hom⁻ m n) - → (∀ i → Δ⁻-map f i ≡ Δ⁻-map g i) - → f ≡ g +Δ-hom-unique⁺ + : ∀ {m n o} + → (f⁺ g⁺ : Δ-Hom⁺ n o) (f⁻ g⁻ : Δ-Hom⁻ m n) + → (∀ (i : Fin m) → ⟦ f⁺ ⟧ (⟦ f⁻ ⟧ i) ≡ ⟦ g⁺ ⟧ (⟦ g⁻ ⟧ i)) + → f⁺ ≡ g⁺ +Δ-hom-unique⁻ + : ∀ {m n o} + → (f⁺ g⁺ : Δ-Hom⁺ n o) (f⁻ g⁻ : Δ-Hom⁻ m n) + → (∀ (i : Fin m) → ⟦ f⁺ ⟧ (⟦ f⁻ ⟧ i) ≡ ⟦ g⁺ ⟧ (⟦ g⁻ ⟧ i)) + → f⁻ ≡ g⁻ ```
-This follows from a giant case bash that isn't particularly -enlightening. +These follow by some more brutal inductions that we will +shield the innocent reader from. ```agda -Δ⁺-map-inj done⁺ done⁺ p = refl -Δ⁺-map-inj (shift⁺ f) (shift⁺ g) p = - ap shift⁺ (Δ⁺-map-inj f g (fsuc-inj ⊙ p)) -Δ⁺-map-inj (shift⁺ f) (keep⁺ g) p = - absurd (fzero≠fsuc (sym (p 0))) -Δ⁺-map-inj (keep⁺ f) (shift⁺ g) p = +Δ-hom-unique⁺ done⁺ done⁺ f⁻ g⁻ p = + refl +Δ-hom-unique⁺ (shift⁺ f⁺) (shift⁺ g⁺) f⁻ g⁻ p = + ap shift⁺ (Δ-hom-unique⁺ f⁺ g⁺ f⁻ g⁻ (fsuc-inj ⊙ p)) +Δ-hom-unique⁺ {m = suc m} (shift⁺ f⁺) (keep⁺ g⁺) f⁻ g⁻ p = + absurd (fsuc≠fzero (p 0 ∙ ap₂ fkeep refl (Δ-hom⁻-zero g⁻))) +Δ-hom-unique⁺ {m = suc m} (keep⁺ f⁺) (shift⁺ g⁺) f⁻ g⁻ p = + absurd (fzero≠fsuc (sym (ap₂ fkeep refl (Δ-hom⁻-zero f⁻)) ∙ p 0)) +Δ-hom-unique⁺ (keep⁺ f⁺) (keep⁺ g⁺) (crush⁻ f⁻) (crush⁻ g⁻) p = + Δ-hom-unique⁺ (keep⁺ f⁺) (keep⁺ g⁺) f⁻ g⁻ (p ⊙ fsuc) +Δ-hom-unique⁺ (keep⁺ f⁺) (keep⁺ g⁺) (crush⁻ f⁻) (keep⁻ g⁻) p = + absurd (fzero≠fsuc (sym (ap₂ fkeep refl (Δ-hom⁻-zero f⁻)) ∙ p 1)) +Δ-hom-unique⁺ (keep⁺ f⁺) (keep⁺ g⁺) (keep⁻ f⁻) (crush⁻ g⁻) p = + absurd (fsuc≠fzero (p 1 ∙ ap₂ fkeep refl (Δ-hom⁻-zero g⁻))) +Δ-hom-unique⁺ (keep⁺ f⁺) (keep⁺ g⁺) (keep⁻ f⁻) (keep⁻ g⁻) p = + ap keep⁺ (Δ-hom-unique⁺ f⁺ g⁺ f⁻ g⁻ (fsuc-inj ⊙ p ⊙ fsuc)) + +Δ-hom-unique⁻ f⁺ g⁺ done⁻ done⁻ p = + refl +Δ-hom-unique⁻ f⁺ g⁺ (crush⁻ f⁻) (crush⁻ g⁻) p = + ap crush⁻ (Δ-hom-unique⁻ f⁺ g⁺ f⁻ g⁻ (p ⊙ fsuc)) +Δ-hom-unique⁻ f⁺ g⁺ (crush⁻ f⁻) (keep⁻ g⁻) p = + absurd (fzero≠fsuc (Δ-hom⁺-to-inj g⁺ (sym (p 0) ∙ p 1))) +Δ-hom-unique⁻ f⁺ g⁺ (keep⁻ f⁻) (crush⁻ g⁻) p = + absurd (fzero≠fsuc (Δ-hom⁺-to-inj f⁺ (p 0 ∙ sym (p 1)))) +Δ-hom-unique⁻ (shift⁺ f⁺) (shift⁺ g⁺) (keep⁻ f⁻) (keep⁻ g⁻) p = + Δ-hom-unique⁻ f⁺ g⁺ (keep⁻ f⁻) (keep⁻ g⁻) (fsuc-inj ⊙ p) +Δ-hom-unique⁻ (shift⁺ f⁺) (keep⁺ g⁺) (keep⁻ f⁻) (keep⁻ g⁻) p = + absurd (fsuc≠fzero (p 0)) +Δ-hom-unique⁻ (keep⁺ f⁺) (shift⁺ g⁺) (keep⁻ f⁻) (keep⁻ g⁻) p = absurd (fzero≠fsuc (p 0)) -Δ⁺-map-inj (keep⁺ f) (keep⁺ g) p = - ap keep⁺ (Δ⁺-map-inj f g (fsuc-inj ⊙ p ⊙ fsuc)) - -Δ⁻-map-inj {m = zero} done⁻ done⁻ p = refl -Δ⁻-map-inj {m = suc m} (crush⁻ f) (crush⁻ g) p = - ap crush⁻ (Δ⁻-map-inj f g (p ⊙ fsuc)) -Δ⁻-map-inj {m = suc (suc m)} (crush⁻ f) (keep⁻ g) p = - absurd (fzero≠fsuc (sym (Δ⁻-map-zero f) ∙ p 1)) -Δ⁻-map-inj {m = suc (suc m)} (keep⁻ f) (crush⁻ g) p = - absurd (fsuc≠fzero (p 1 ∙ Δ⁻-map-zero g)) --- Duplicate cases to keep exact split happy -Δ⁻-map-inj {m = suc zero} (keep⁻ f) (keep⁻ g) p = - ap keep⁻ (Δ⁻-map-inj f g (fsuc-inj ⊙ p ⊙ fsuc)) -Δ⁻-map-inj {m = suc (suc m)} (keep⁻ f) (keep⁻ g) p = - ap keep⁻ (Δ⁻-map-inj f g (fsuc-inj ⊙ p ⊙ fsuc)) +Δ-hom-unique⁻ (keep⁺ f⁺) (keep⁺ g⁺) (keep⁻ f⁻) (keep⁻ g⁻) p = + ap keep⁻ (Δ-hom-unique⁻ f⁺ g⁺ f⁻ g⁻ (fsuc-inj ⊙ p ⊙ fsuc)) ```
-With a bit of work, we can show that the interpretations take -identities to identities and composites to composites. Pure more -succinctly, the interpretation functions are functorial. + + +Injectivity of the interpretation of simplicial maps follows +directly from these lemmas. ```agda -Δ⁺-map-id : ∀ (i : Fin m) → Δ⁺-map id⁺ i ≡ i -Δ⁻-map-id : ∀ (i : Fin m) → Δ⁻-map id⁻ i ≡ i +Δ-hom-inj + : ∀ (f g : Δ-Hom m n) + → (∀ i → ⟦ f ⟧ i ≡ ⟦ g ⟧ i) + → f ≡ g +Δ-hom-inj {m} {n} f g p = + Δ-Hom-path (Δ-hom-im-unique (f .hom⁺) (g .hom⁺) (f .hom⁻) (g .hom⁻) p) + (Δ-hom-uniquep⁺ (f .hom⁺) (g .hom⁺) (f .hom⁻) (g .hom⁻) p) + (Δ-hom-uniquep⁻ (f .hom⁺) (g .hom⁺) (f .hom⁻) (g .hom⁻) p) +``` + +Injectivity the interpretaion of semi and demisimplicial maps follow +neatly as corollaries. + +```agda +Δ-hom⁺-inj + : ∀ (f⁺ g⁺ : Δ-Hom⁺ m n) + → (∀ i → ⟦ f⁺ ⟧ i ≡ ⟦ g⁺ ⟧ i) + → f⁺ ≡ g⁺ +Δ-hom⁺-inj f⁺ g⁺ p = Δ-hom-unique⁺ f⁺ g⁺ id⁻ id⁻ (p ⊙ Δ-hom⁻ id⁻) + +Δ-hom⁻-inj + : ∀ (f⁻ g⁻ : Δ-Hom⁻ m n) + → (∀ i → ⟦ f⁻ ⟧ i ≡ ⟦ g⁻ ⟧ i) + → f⁻ ≡ g⁻ +Δ-hom⁻-inj f⁻ g⁻ p = Δ-hom-unique⁻ id⁺ id⁺ f⁻ g⁻ (ap (Δ-hom⁺ id⁺) ⊙ p) +``` -Δ⁺-map-∘ +### Functoriality of interpretations + +Finally, we shall prove functoriality of all of our interpretations. + +Identities are mercifully simple. + +```agda +Δ-hom⁺-id : ∀ (i : Fin m) → ⟦ id⁺ ⟧ i ≡ i +Δ-hom⁺-id fzero = refl +Δ-hom⁺-id (fsuc i) = ap fsuc (Δ-hom⁺-id i) + +Δ-hom⁻-id : ∀ (i : Fin m) → ⟦ id⁻ ⟧ i ≡ i +Δ-hom⁻-id fzero = refl +Δ-hom⁻-id (fsuc i) = ap fsuc (Δ-hom⁻-id i) + +Δ-hom-id : ∀ (i : Fin m) → ⟦ idΔ ⟧ i ≡ i +Δ-hom-id i = ap ⟦ id⁺ ⟧ (Δ-hom⁻-id i) ∙ Δ-hom⁺-id i +``` + +Composites of semi and demisimplicial maps are decidedly less easy. + +```agda +Δ-hom⁺-∘ : (f : Δ-Hom⁺ n o) (g : Δ-Hom⁺ m n) - → ∀ (i : Fin m) → Δ⁺-map (f ∘⁺ g) i ≡ Δ⁺-map f (Δ⁺-map g i) -Δ⁻-map-∘ + → ∀ (i : Fin m) → ⟦ f ∘⁺ g ⟧ i ≡ ⟦ f ⟧ (⟦ g ⟧ i) +Δ-hom⁻-∘ : (f : Δ-Hom⁻ n o) (g : Δ-Hom⁻ m n) - → ∀ (i : Fin m) → Δ⁻-map (f ∘⁻ g) i ≡ Δ⁻-map f (Δ⁻-map g i) + → ∀ (i : Fin m) → ⟦ f ∘⁻ g ⟧ i ≡ ⟦ f ⟧ (⟦ g ⟧ i) ```
-This follows from another series of case bashes. +The proofs are not particularly difficult; they both +consist of some (rather large) case bashes. ```agda -Δ⁺-map-id fzero = refl -Δ⁺-map-id (fsuc i) = ap fsuc (Δ⁺-map-id i) - -Δ⁻-map-id fzero = refl -Δ⁻-map-id (fsuc i) = ap fsuc (Δ⁻-map-id i) - -Δ⁺-map-∘ done⁺ done⁺ i = fabsurd i -Δ⁺-map-∘ (shift⁺ f) (shift⁺ g) i = ap fsuc (Δ⁺-map-∘ f (shift⁺ g) i) -Δ⁺-map-∘ (shift⁺ f) (keep⁺ g) i = ap fsuc (Δ⁺-map-∘ f (keep⁺ g) i) -Δ⁺-map-∘ (keep⁺ f) (shift⁺ g) i = ap fsuc (Δ⁺-map-∘ f g i) -Δ⁺-map-∘ (keep⁺ f) (keep⁺ g) fzero = refl -Δ⁺-map-∘ (keep⁺ f) (keep⁺ g) (fsuc i) = ap fsuc (Δ⁺-map-∘ f g i) - --- We can reduce the number of cases by handling all 'fzero' cases --- at once. -Δ⁻-map-∘ {n = zero} {o = zero} done⁻ done⁻ i = - fabsurd i -Δ⁻-map-∘ {n = suc n} {o = suc o} f g fzero = - Δ⁻-map (f ∘⁻ g) fzero ≡⟨ Δ⁻-map-zero (f ∘⁻ g) ⟩ - fzero ≡˘⟨ Δ⁻-map-zero f ⟩ - Δ⁻-map f fzero ≡˘⟨ ap (Δ⁻-map f) (Δ⁻-map-zero g) ⟩ - Δ⁻-map f (Δ⁻-map g fzero) ∎ -Δ⁻-map-∘ {n = suc n} {o = suc o} (crush⁻ f) (crush⁻ g) (fsuc i) = - Δ⁻-map-∘ (crush⁻ f) g i -Δ⁻-map-∘ {n = suc n} {o = suc o} (crush⁻ f) (keep⁻ g) (fsuc i) = - Δ⁻-map-∘ f g i -Δ⁻-map-∘ {n = suc n} {o = suc o} (keep⁻ f) (crush⁻ g) (fsuc i) = - Δ⁻-map-∘ (keep⁻ f) g i -Δ⁻-map-∘ {n = suc n} {o = suc o} (keep⁻ f) (keep⁻ g) (fsuc i) = - ap fsuc (Δ⁻-map-∘ f g i) +Δ-hom⁺-∘ done⁺ done⁺ i = fabsurd i +Δ-hom⁺-∘ (shift⁺ f) (shift⁺ g) i = ap fsuc (Δ-hom⁺-∘ f (shift⁺ g) i) +Δ-hom⁺-∘ (shift⁺ f) (keep⁺ g) i = ap fsuc (Δ-hom⁺-∘ f (keep⁺ g) i) +Δ-hom⁺-∘ (keep⁺ f) (shift⁺ g) i = ap fsuc (Δ-hom⁺-∘ f g i) +Δ-hom⁺-∘ (keep⁺ f) (keep⁺ g) fzero = refl +Δ-hom⁺-∘ (keep⁺ f) (keep⁺ g) (fsuc i) = ap fsuc (Δ-hom⁺-∘ f g i) + +Δ-hom⁻-∘ done⁻ (crush⁻ g) i = sym (Δ-hom⁻-id (Δ-hom⁻ (crush⁻ g) i)) +Δ-hom⁻-∘ (crush⁻ f) (crush⁻ g) i = Δ-hom⁻-∘ (crush⁻ f) g (fpred i) +Δ-hom⁻-∘ (crush⁻ f) (keep⁻ (crush⁻ g)) fzero = + Δ-hom⁻ (f ∘⁻ g) fzero ≡⟨ Δ-hom⁻-∘ f g fzero ⟩ + Δ-hom⁻ f (Δ-hom⁻ g fzero) ≡⟨ ap (Δ-hom⁻ f) (Δ-hom⁻-zero g) ⟩ + Δ-hom⁻ f fzero ∎ +Δ-hom⁻-∘ (crush⁻ f) (keep⁻ (crush⁻ g)) (fsuc i) = Δ-hom⁻-∘ f g (fpred i) +Δ-hom⁻-∘ (crush⁻ f) (keep⁻ (keep⁻ g)) fzero = + Δ-hom⁻ (f ∘⁻ keep⁻ g) fzero ≡⟨ Δ-hom⁻-∘ f (keep⁻ g) fzero ⟩ + Δ-hom⁻ f fzero ∎ +Δ-hom⁻-∘ (crush⁻ f) (keep⁻ (keep⁻ g)) (fsuc i) = Δ-hom⁻-∘ f (keep⁻ g) i +Δ-hom⁻-∘ (keep⁻ f) (crush⁻ g) i = Δ-hom⁻-∘ (keep⁻ f) g (fpred i) +Δ-hom⁻-∘ (keep⁻ f) (keep⁻ g) fzero = refl +Δ-hom⁻-∘ (keep⁻ f) (keep⁻ g) (fsuc i) = ap fsuc (Δ-hom⁻-∘ f g i) ```
-## Normal forms of maps +Composites of simplicial maps are the most difficult of the bunch. The key lemma +is that the interpretation of the of $f^{-} \circ g^{+}$ is functorial, which +follows from yet another painful induction. -First, note that we can extend all of the operations on face -and degeneracies to operations on normal forms. +```agda +Δ-hom⁺⁻-comm + : ∀ (f⁻ : Δ-Hom⁻ n o) (f⁺ : Δ-Hom⁺ m n) + → ∀ (i : Fin m) → ⟦ f⁻ ∘Δ⁺ f⁺ ⟧ (⟦ f⁻ ∘Δ⁻ f⁺ ⟧ i) ≡ ⟦ f⁻ ⟧ (⟦ f⁺ ⟧ i) +``` +
+There really is no intuition to be gained from the proof, so we omit it. + ```agda -done : Δ-Hom 0 0 -done .middle = 0 -done .hom⁺ = done⁺ -done .hom⁻ = done⁻ +Δ-hom⁺⁻-comm done⁻ done⁺ i = fabsurd i +Δ-hom⁺⁻-comm (crush⁻ f⁻) (shift⁺ f⁺) i = Δ-hom⁺⁻-comm f⁻ f⁺ i +Δ-hom⁺⁻-comm (crush⁻ f⁻) (keep⁺ (shift⁺ f⁺)) fzero = Δ-hom⁺⁻-comm f⁻ (keep⁺ f⁺) fzero +Δ-hom⁺⁻-comm (crush⁻ f⁻) (keep⁺ (shift⁺ f⁺)) (fsuc i) = Δ-hom⁺⁻-comm f⁻ (keep⁺ f⁺) (fsuc i) +Δ-hom⁺⁻-comm (crush⁻ f⁻) (keep⁺ (keep⁺ f⁺)) fzero = Δ-hom⁺⁻-comm f⁻ (keep⁺ f⁺) fzero +Δ-hom⁺⁻-comm (crush⁻ f⁻) (keep⁺ (keep⁺ f⁺)) (fsuc fzero) = Δ-hom⁺⁻-comm f⁻ (keep⁺ f⁺) fzero +Δ-hom⁺⁻-comm (crush⁻ f⁻) (keep⁺ (keep⁺ f⁺)) (fsuc (fsuc i)) = Δ-hom⁺⁻-comm f⁻ (keep⁺ f⁺) (fsuc i) +Δ-hom⁺⁻-comm (keep⁻ f⁻) (shift⁺ f⁺) i = ap fsuc (Δ-hom⁺⁻-comm f⁻ f⁺ i) +Δ-hom⁺⁻-comm (keep⁻ f⁻) (keep⁺ f⁺) fzero = refl +Δ-hom⁺⁻-comm (keep⁻ f⁻) (keep⁺ f⁺) (fsuc i) = ap fsuc (Δ-hom⁺⁻-comm f⁻ f⁺ i) +``` +
-crush : Δ-Hom m (suc n) → Δ-Hom (suc m) (suc n) -crush f with f .middle | f .hom⁺ | f .hom⁻ -... | zero | f⁺ | done⁻ = Δ-hom (keep⁺ ¡⁺) id⁻ -... | suc x | f⁺ | f⁻ = Δ-hom f⁺ (crush⁻ f⁻) +Luckily, that was our last big induction, and we can get our final functoriality +lemma by piecing together previous results! -shift : Δ-Hom m n → Δ-Hom m (suc n) -shift f .middle = f .middle -shift f .hom⁺ = shift⁺ (f .hom⁺) -shift f .hom⁻ = f .hom⁻ +```agda +Δ-hom-∘ + : (f : Δ-Hom n o) (g : Δ-Hom m n) + → ∀ (i : Fin m) → ⟦ (f ∘Δ g) ⟧ i ≡ ⟦ f ⟧ (⟦ g ⟧ i) +Δ-hom-∘ f g i = + ⟦ f .hom⁺ ∘⁺ (f .hom⁻ ∘Δ⁺ g .hom⁺) ⟧ (⟦ (f .hom⁻ ∘Δ⁻ g .hom⁺) ∘⁻ g .hom⁻ ⟧ i) ≡⟨ Δ-hom⁺-∘ (f .hom⁺) (f .hom⁻ ∘Δ⁺ g .hom⁺) (⟦ (f .hom⁻ ∘Δ⁻ g .hom⁺) ∘⁻ g .hom⁻ ⟧ i) ⟩ + ⟦ f .hom⁺ ⟧ (⟦ f .hom⁻ ∘Δ⁺ g .hom⁺ ⟧ (⟦ (f .hom⁻ ∘Δ⁻ g .hom⁺) ∘⁻ g .hom⁻ ⟧ i)) ≡⟨ ap (⟦ f .hom⁺ ⟧ ⊙ ⟦ f .hom⁻ ∘Δ⁺ g .hom⁺ ⟧) (Δ-hom⁻-∘ (f .hom⁻ ∘Δ⁻ g .hom⁺) (g .hom⁻) i) ⟩ + ⟦ f .hom⁺ ⟧ (⟦ f .hom⁻ ∘Δ⁺ g .hom⁺ ⟧ (⟦ (f .hom⁻ ∘Δ⁻ g .hom⁺) ⟧ (⟦ g .hom⁻ ⟧ i))) ≡⟨ ap ⟦ f .hom⁺ ⟧ ( Δ-hom⁺⁻-comm (f .hom⁻) (g .hom⁺) (⟦ g .hom⁻ ⟧ i)) ⟩ + ⟦ f .hom⁺ ⟧ (⟦ f .hom⁻ ⟧ (⟦ g .hom⁺ ⟧ (⟦ g .hom⁻ ⟧ i))) ∎ +``` + +## Categories + +With all that hard work behind us, it is time to enjoy the fruit +of our labor. All of our putative categories +(both augmented and non-augmented) are equipped with injective functorial +interpretations into functions between sets, which means that they are +bona-fide [[concrete categories]]. + +```agda +Δₐ⁺-concrete : make-concrete Nat Δ-Hom⁺ +Δₐ⁻-concrete : make-concrete Nat Δ-Hom⁻ +Δₐ-concrete : make-concrete Nat Δ-Hom + +Δ⁺-concrete : make-concrete Nat (λ m n → Δ-Hom⁺ (suc m) (suc n)) +Δ⁻-concrete : make-concrete Nat (λ m n → Δ-Hom⁻ (suc m) (suc n)) +Δ-concrete : make-concrete Nat (λ m n → Δ-Hom (suc m) (suc n)) +``` + +
+We already have all the results we need, so proving that they +are concrete is just an exercise in building records. + +```agda +Δₐ⁺-concrete .make-concrete.id = id⁺ +Δₐ⁺-concrete .make-concrete._∘_ = _∘⁺_ +Δₐ⁺-concrete .make-concrete.lvl = lzero +Δₐ⁺-concrete .make-concrete.F₀ = Fin +Δₐ⁺-concrete .make-concrete.F₀-is-set = hlevel! +Δₐ⁺-concrete .make-concrete.F₁ = Δ-hom⁺ +Δₐ⁺-concrete .make-concrete.F₁-inj = Δ-hom⁺-inj _ _ +Δₐ⁺-concrete .make-concrete.F-id = Δ-hom⁺-id +Δₐ⁺-concrete .make-concrete.F-∘ = Δ-hom⁺-∘ + +Δₐ⁻-concrete .make-concrete.id = id⁻ +Δₐ⁻-concrete .make-concrete._∘_ = _∘⁻_ +Δₐ⁻-concrete .make-concrete.lvl = lzero +Δₐ⁻-concrete .make-concrete.F₀ = Fin +Δₐ⁻-concrete .make-concrete.F₀-is-set = hlevel! +Δₐ⁻-concrete .make-concrete.F₁ = Δ-hom⁻ +Δₐ⁻-concrete .make-concrete.F₁-inj = Δ-hom⁻-inj _ _ +Δₐ⁻-concrete .make-concrete.F-id = Δ-hom⁻-id +Δₐ⁻-concrete .make-concrete.F-∘ = Δ-hom⁻-∘ + +Δₐ-concrete .make-concrete.id = idΔ +Δₐ-concrete .make-concrete._∘_ = _∘Δ_ +Δₐ-concrete .make-concrete.lvl = lzero +Δₐ-concrete .make-concrete.F₀ = Fin +Δₐ-concrete .make-concrete.F₀-is-set = hlevel! +Δₐ-concrete .make-concrete.F₁ = Δ-hom +Δₐ-concrete .make-concrete.F₁-inj = Δ-hom-inj _ _ +Δₐ-concrete .make-concrete.F-id = Δ-hom-id +Δₐ-concrete .make-concrete.F-∘ = Δ-hom-∘ + +Δ⁺-concrete .make-concrete.id = id⁺ +Δ⁺-concrete .make-concrete._∘_ = _∘⁺_ +Δ⁺-concrete .make-concrete.lvl = lzero +Δ⁺-concrete .make-concrete.F₀ n = Fin (suc n) +Δ⁺-concrete .make-concrete.F₀-is-set = hlevel! +Δ⁺-concrete .make-concrete.F₁ = Δ-hom⁺ +Δ⁺-concrete .make-concrete.F₁-inj = Δ-hom⁺-inj _ _ +Δ⁺-concrete .make-concrete.F-id = Δ-hom⁺-id +Δ⁺-concrete .make-concrete.F-∘ = Δ-hom⁺-∘ + +Δ⁻-concrete .make-concrete.id = id⁻ +Δ⁻-concrete .make-concrete._∘_ = _∘⁻_ +Δ⁻-concrete .make-concrete.lvl = lzero +Δ⁻-concrete .make-concrete.F₀ n = Fin (suc n) +Δ⁻-concrete .make-concrete.F₀-is-set = hlevel! +Δ⁻-concrete .make-concrete.F₁ = Δ-hom⁻ +Δ⁻-concrete .make-concrete.F₁-inj = Δ-hom⁻-inj _ _ +Δ⁻-concrete .make-concrete.F-id = Δ-hom⁻-id +Δ⁻-concrete .make-concrete.F-∘ = Δ-hom⁻-∘ + +Δ-concrete .make-concrete.id = idΔ +Δ-concrete .make-concrete._∘_ = _∘Δ_ +Δ-concrete .make-concrete.lvl = lzero +Δ-concrete .make-concrete.F₀ n = Fin (suc n) +Δ-concrete .make-concrete.F₀-is-set = hlevel! +Δ-concrete .make-concrete.F₁ = Δ-hom +Δ-concrete .make-concrete.F₁-inj = Δ-hom-inj _ _ +Δ-concrete .make-concrete.F-id = Δ-hom-id +Δ-concrete .make-concrete.F-∘ = Δ-hom-∘ +``` +
+ +A bit of metaprogramming gives a definition of the +(augmented (demi/semi)) simplex category that will result in pretty +goals. + +```agda +Δₐ⁺ : Precategory lzero lzero +Δₐ⁻ : Precategory lzero lzero +Δₐ : Precategory lzero lzero + +unquoteDef Δₐ⁺ = define-concrete-category Δₐ⁺ Δₐ⁺-concrete +unquoteDef Δₐ⁻ = define-concrete-category Δₐ⁻ Δₐ⁻-concrete +unquoteDef Δₐ = define-concrete-category Δₐ Δₐ-concrete + +Δ⁺ : Precategory lzero lzero +Δ⁻ : Precategory lzero lzero +Δ : Precategory lzero lzero + +unquoteDef Δ⁺ = define-concrete-category Δ⁺ Δ⁺-concrete +unquoteDef Δ⁻ = define-concrete-category Δ⁻ Δ⁻-concrete +unquoteDef Δ = define-concrete-category Δ Δ-concrete + +module Δₐ⁺ = Cat.Reasoning Δₐ⁺ +module Δₐ⁻ = Cat.Reasoning Δₐ⁻ +module Δₐ = Cat.Reasoning Δₐ + +module Δ⁺ = Cat.Reasoning Δ⁺ +module Δ⁻ = Cat.Reasoning Δ⁻ +module Δ = Cat.Reasoning Δ +``` + +## Categorical structure + +Now that we actually have categories, we can start to construct some +interesting maps. We begin by constructing more familiar versions of +face and degeneracy map that are parameterized by some $i$. -keep : Δ-Hom m n → Δ-Hom (suc m) (suc n) -keep f .middle = suc (f .middle) -keep f .hom⁺ = keep⁺ (f .hom⁺) -keep f .hom⁻ = keep⁻ (f .hom⁻) ``` +δ⁺ : Fin (suc n) → Δ-Hom⁺ n (suc n) +δ⁺ {n = _} fzero = shift⁺ id⁺ +δ⁺ {n = suc _} (fsuc i) = keep⁺ (δ⁺ i) -We can also define maps $[0] \to [n]$ and $[n] \to [1]$ for any $n$; -these maps will end up witnessing $[0]$ and $[1]$ as initial and terminal -objects, resp. +σ⁻ : Fin n → Δ-Hom⁻ (suc n) n +σ⁻ fzero = crush⁻ id⁻ +σ⁻ (fsuc i) = keep⁻ (σ⁻ i) +``` + +We can extend `δ⁺`{.Agda} and `σ⁻`{.Agda} to simplicial maps by +taking the other component to be the corresponding identity map. ```agda +δ : Fin (suc n) → Δ-Hom n (suc n) +δ i .im = _ +δ i .hom⁺ = δ⁺ i +δ i .hom⁻ = id⁻ + +σ : Fin n → Δ-Hom (suc n) n +σ i .im = _ +σ i .hom⁺ = id⁺ +σ i .hom⁻ = σ⁻ i +``` + +The semantic interpretations of `δ i`{.Agda} and `σ i`{.Agda} are the +corresponding face and degenearcy maps between finite sets. + +```agda +Δ-hom⁺-δ + : ∀ (i : Fin (suc n)) + → ∀ (x : Fin n) → ⟦ δ⁺ i ⟧ x ≡ skip i x +Δ-hom-δ + : ∀ (i : Fin (suc n)) + → ∀ (x : Fin n) → ⟦ δ i ⟧ x ≡ skip i x + +Δ-hom⁻-σ + : ∀ (i : Fin n) + → ∀ (x : Fin (suc n)) → ⟦ σ⁻ i ⟧ x ≡ squish i x +Δ-hom-σ + : ∀ (i : Fin n) + → ∀ (x : Fin (suc n)) → ⟦ σ i ⟧ x ≡ squish i x +``` + +
+The proofs are straighforward, so we omit them. + + +```agda +Δ-hom⁺-δ fzero x = ap fsuc (Δ-hom⁺-id x) +Δ-hom⁺-δ (fsuc i) fzero = refl +Δ-hom⁺-δ (fsuc i) (fsuc x) = ap fsuc (Δ-hom⁺-δ i x) + +Δ-hom-δ i x = ap ⟦ δ⁺ i ⟧ (Δ-hom⁻-id x) ∙ Δ-hom⁺-δ i x + +Δ-hom⁻-σ fzero fzero = refl +Δ-hom⁻-σ fzero (fsuc x) = + ap₂ fkeep (funext Δ-hom⁻-id) refl + ∙ fkeep-id x +Δ-hom⁻-σ (fsuc i) fzero = refl +Δ-hom⁻-σ (fsuc i) (fsuc x) = ap fsuc (Δ-hom⁻-σ i x) + +Δ-hom-σ i x = Δ-hom⁺-id (⟦ σ⁻ i ⟧ x) ∙ Δ-hom⁻-σ i x +``` +
+ +Next, note that $0$ is an initial object in the augmented (semi) simplex +category. + +```agda +¡⁺ : Δ-Hom⁺ 0 n +¡⁺ {n = zero} = done⁺ +¡⁺ {n = suc n} = shift⁺ ¡⁺ + ¡Δ : Δ-Hom 0 n -¡Δ {n = zero} = done -¡Δ {n = suc n} = shift ¡Δ +¡Δ .im = 0 +¡Δ .hom⁺ = ¡⁺ +¡Δ .hom⁻ = done⁻ +``` -!Δ : Δ-Hom n 1 -!Δ {n = zero} = ¡Δ -!Δ {n = suc n} = crush !Δ +There are many ways to prove that these maps are unique, but the most +straightforward approach is to use our semantic interpretations: these +yield functions `Fin 0 → Fin n`, which are extremely easy to prove unique. + +```agda +¡⁺-unique : (f : Δ-Hom⁺ 0 n) → f ≡ ¡⁺ +¡⁺-unique f = Δ-hom⁺-inj f ¡⁺ (λ i → fabsurd i) + +¡Δ-unique : (f : Δ-Hom 0 n) → f ≡ ¡Δ +¡Δ-unique f = Δ-hom-inj f ¡Δ (λ i → fabsurd i) ``` -The identity morphism consists of a the identity face and degeneracy. + ```agda -idΔ : Δ-Hom n n -idΔ .middle = _ -idΔ .hom⁺ = id⁺ -idΔ .hom⁻ = id⁻ +-- FIXME: Rename these +¡⁺-strict : ¬ (Δ-Hom⁺ (suc n) 0) +¡⁺-strict () + +!⁻-strict : ¬ (Δ-Hom⁻ 0 (suc n)) +!⁻-strict () ``` -Unfortunately, composites are not so simple, as we need to transform -an alternating chain of face and degeneracy maps into a single pair of -face and degenerac maps. This requires us to construct the following -4-way composition map. +Likewise, $1$ is a terminal object in the (demi) simplex category. ```agda -composeΔ : Δ-Hom⁺ n o → Δ-Hom⁻ m n → Δ-Hom⁺ l m → Δ-Hom⁻ k l → Δ-Hom k o +!⁻ : Δ-Hom⁻ (suc n) 1 +!⁻ {n = zero} = id⁻ +!⁻ {n = suc n} = crush⁻ !⁻ + +!Δ : Δ-Hom (suc n) 1 +!Δ .im = 1 +!Δ .hom⁺ = id⁺ +!Δ .hom⁻ = !⁻ ``` -There are quite a few cases here, so we will go through each individually. -The first case is relatively straightforward: the composite of the chain -$$\id_{-} \circ \id_{0} \circ g^{+} \circ g^{-}$$ -is $g^{+} \circ g^{-}$. +It is also a terminal object in the augmented simplex category, as +we always have a map $0 \to 1$. However, note that it is *not* terminal +in the augmented demi-simplex category, as there is no surjective map +$0 \to 1$! ```agda -composeΔ done⁺ done⁻ g⁺ g⁻ = - Δ-hom g⁺ g⁻ +!Δₐ : Δ-Hom n 1 +!Δₐ {n = zero} = ¡Δ +!Δₐ {n = suc n} = !Δ ``` -If the first map in the chain is a composite with a face map ala -$$(\delta \circ f^{+}) \circ f^{-} \circ g^{+} \circ g^{-}$$ -then we can reassociate and recurse on the rest of the chain. +We can use the same semantic strategy to prove that these maps are +unique. ```agda -composeΔ (shift⁺ f⁺) f⁻ g⁺ g⁻ = - shift (composeΔ f⁺ f⁻ g⁺ g⁻) +!⁻-unique : (f : Δ-Hom⁻ (suc n) 1) → f ≡ !⁻ +!⁻-unique f = Δ-hom⁻-inj f !⁻ λ i → Finite-one-is-prop (⟦ f ⟧ i) (⟦ !⁻ ⟧ i) + +!Δ-unique : (f : Δ-Hom (suc n) 1) → f ≡ !Δ +!Δ-unique f = Δ-hom-inj f !Δ λ i → Finite-one-is-prop (⟦ f ⟧ i) (⟦ !Δ ⟧ i) + +!Δₐ-unique : (f : Δ-Hom n 1) → f ≡ !Δₐ +!Δₐ-unique {n = zero} = ¡Δ-unique +!Δₐ-unique {n = suc n} = !Δ-unique ``` -Conversely, if domain of the chain is $0$, then we know that the -entire chain must be equal to the map out of the initial object. + + +## Isomorphisms ```agda -composeΔ (keep⁺ f⁺) f⁻ g⁺ done⁻ = - ¡Δ +Δₐ⁺-iso-is-prop : is-prop (m Δₐ⁺.≅ n) +Δₐ⁺-iso-is-prop {m = m} f g = {!!} + where + module f = Δₐ⁺._≅_ f + module g = Δₐ⁺._≅_ g + open Order.Reasoning Nat-poset + + cool : ∀ (i : Fin m) → ⟦ f.to ⟧ i Fin.≤ ⟦ g.to ⟧ i + cool i = + to-nat (⟦ f.to ⟧ i) ≤⟨ {!!} ⟩ + to-nat (⟦ f.to ⟧ (⟦ f.from ⟧ (⟦ g.to ⟧ i))) =⟨ ap to-nat {!!} ⟩ + to-nat (⟦ g.to ⟧ i) ≤∎ ``` -If the final map in the chain is a composite with a degeneracy like -$$f^{+} \circ f^{-} \circ g^{+} \circ (g^{-} \circ \sigma)$$ -then we can again reassociate and recurse on the rest of the chain. + +## Dimension + +If $f : [m] \to [n]$ is a semisimplicial map, then $m \leq n$. Conversely, +if $f$ is a demisimplicial map then $m \geq n$. The slogan here is that +semisimplicial maps increase dimension, and demisimplicial maps lower it. ```agda -composeΔ (keep⁺ f⁺) f⁻ g⁺ (crush⁻ g⁻) = - crush (composeΔ (keep⁺ f⁺) f⁻ g⁺ g⁻) +Δ-dim⁺-≤ : ∀ {m n} → (f : Δ-Hom⁺ m n) → m Nat.≤ n +Δ-dim⁺-≤ done⁺ = Nat.0≤x +Δ-dim⁺-≤ (shift⁺ f) = Nat.≤-sucr (Δ-dim⁺-≤ f) +Δ-dim⁺-≤ (keep⁺ f) = Nat.s≤s (Δ-dim⁺-≤ f) + +Δ-dim⁻-≤ : ∀ {m n} → (f : Δ-Hom⁻ m n) → n Nat.≤ m +Δ-dim⁻-≤ done⁻ = Nat.0≤x +Δ-dim⁻-≤ (crush⁻ f) = Nat.≤-sucr (Δ-dim⁻-≤ f) +Δ-dim⁻-≤ (keep⁻ f) = Nat.s≤s (Δ-dim⁻-≤ f) ``` -If the inner two maps are composites with a face and degeneracy -map like -$$f^{+} \circ (f^{-} \circ \sigma) \circ (\delta \circ g^{+}) \circ g^{-}$$ -then we can eliminate the face and degeneracy map, and recurse. +Moreover, if a semi/demisimplicial map contains a face/degeneracy, +then we know it must *strictly* increase/decrease the dimension. ```agda -composeΔ (keep⁺ f⁺) (crush⁻ f⁻) (shift⁺ g⁺) (keep⁻ g⁻) = - composeΔ (keep⁺ f⁺) f⁻ g⁺ (keep⁻ g⁻) +has-face⁺ : ∀ {m n} → Δ-Hom⁺ m n → Type +has-face⁺ done⁺ = ⊥ +has-face⁺ (shift⁺ f) = ⊤ +has-face⁺ (keep⁺ f) = has-face⁺ f + +has-degeneracy⁻ : ∀ {m n} → Δ-Hom⁻ m n → Type +has-degeneracy⁻ done⁻ = ⊥ +has-degeneracy⁻ (crush⁻ f) = ⊤ +has-degeneracy⁻ (keep⁻ f) = has-degeneracy⁻ f + + +Δ-dim⁺-< : ∀ {m n} → (f : Δ-Hom⁺ m n) → has-face⁺ f → m Nat.< n +Δ-dim⁺-< (shift⁺ f) p = Nat.s≤s (Δ-dim⁺-≤ f) +Δ-dim⁺-< (keep⁺ f) p = Nat.s≤s (Δ-dim⁺-< f p) + +Δ-dim⁻-< : ∀ {m n} → (f : Δ-Hom⁻ m n) → has-degeneracy⁻ f → n Nat.< m +Δ-dim⁻-< (crush⁻ f) p = Nat.s≤s (Δ-dim⁻-≤ f) +Δ-dim⁻-< (keep⁻ f) p = Nat.s≤s (Δ-dim⁻-< f p) ``` -If only one map in the sequence does touches the 0th position, then we can -commute the relevant face/degeneracy outwards and recurse. +```agda +is-id⁺ : ∀ {m n} → Δ-Hom⁺ m n → Type +is-id⁺ done⁺ = ⊤ +is-id⁺ (shift⁺ f) = ⊥ +is-id⁺ (keep⁺ f) = is-id⁺ f + +is-id⁻ : ∀ {m n} → Δ-Hom⁻ m n → Type +is-id⁻ done⁻ = ⊤ +is-id⁻ (crush⁻ f) = ⊥ +is-id⁻ (keep⁻ f) = is-id⁻ f +``` + +Note that these dimension raising/lowering properties immediately imply +that the (augmented) demi/semi simplex categories are categories. ```agda -composeΔ (keep⁺ f⁺) (crush⁻ f⁻) (keep⁺ g⁺) (keep⁻ g⁻) = - crush (composeΔ (keep⁺ f⁺) f⁻ g⁺ g⁻) -composeΔ (keep⁺ f⁺) (keep⁻ f⁻) (shift⁺ g⁺) (keep⁻ g⁻) = - shift (composeΔ f⁺ f⁻ g⁺ (keep⁻ g⁻)) +Δₐ⁺-is-category : is-category Δₐ⁺ +Δₐ⁺-is-category = set-identity-system (λ _ _ → Δₐ⁺-iso-is-prop) λ f → + Nat.≤-antisym (Δ-dim⁺-≤ (Δₐ⁺.to f)) (Δ-dim⁺-≤ (Δₐ⁺.from f)) + +Δₐ⁺-is-gaunt : is-gaunt Δₐ⁺ +Δₐ⁺-is-gaunt .is-gaunt.has-category = Δₐ⁺-is-category +Δₐ⁺-is-gaunt .is-gaunt.has-strict = Nat.Nat-is-set ``` -Finally, if none of the maps touch the 0th position, then we can proceed to -compose the rest of those 4 maps. +## Decidable equality + -We can then use this 4-way composition to construct composites of normal forms. +All three classes of maps have decidable equality. ```agda -_∘Δ_ : Δ-Hom n o → Δ-Hom m n → Δ-Hom m o -f ∘Δ g = composeΔ (f .hom⁺) (f .hom⁻) (g .hom⁺) (g .hom⁻) -``` - --- - --- All three classes of maps have decidable equality. - --- ```agda --- instance --- Discrete-Δ-Hom⁺ : Discrete (Δ-Hom⁺ m n) --- Discrete-Δ-Hom⁻ : Discrete (Δ-Hom⁻ m n) --- Discrete-Δ-Hom : Discrete (Δ-Hom m n) --- ``` - ---
--- Proving this is pretty tedious though, especially for --- general morphisms. --- - --- ```agda --- Discrete-Δ-Hom⁺ {x = done⁺} {y = done⁺} = --- yes refl --- Discrete-Δ-Hom⁺ {x = shift⁺ x} {y = shift⁺ y} = --- Dec-map (ap shift⁺) shift⁺-inj Discrete-Δ-Hom⁺ --- Discrete-Δ-Hom⁺ {x = shift⁺ x} {y = keep⁺ y} = --- no shift⁺≠keep⁺ --- Discrete-Δ-Hom⁺ {x = keep⁺ x} {y = shift⁺ y} = --- no keep⁺≠shift⁺ --- Discrete-Δ-Hom⁺ {x = keep⁺ x} {y = keep⁺ y} = --- Dec-map (ap keep⁺) keep⁺-inj Discrete-Δ-Hom⁺ - --- Discrete-Δ-Hom⁻ {x = done⁻} {y = done⁻} = --- yes refl --- Discrete-Δ-Hom⁻ {x = crush⁻ x} {y = crush⁻ y} = --- Dec-map (ap crush⁻) crush⁻-inj Discrete-Δ-Hom⁻ --- Discrete-Δ-Hom⁻ {x = crush⁻ x} {y = keep⁻ y} = --- no crush⁻≠keep⁻ --- Discrete-Δ-Hom⁻ {x = keep⁻ x} {y = crush⁻ y} = --- no keep⁻≠crush⁻ --- Discrete-Δ-Hom⁻ {x = keep⁻ x} {y = keep⁻ y} = --- Dec-map (ap keep⁻) keep⁻-inj Discrete-Δ-Hom⁻ - --- Discrete-Δ-Hom {x = x} {y = y} with x .middle ≡? y .middle --- ... | yes p with cast⁺ p refl (x .hom⁺) ≡? (y .hom⁺) | cast⁻ refl p (x .hom⁻) ≡? y .hom⁻ --- ... | yes q | yes r = --- yes (Δ-Hom-path p (Equiv.to (cast⁺≃pathp p refl) q) (Equiv.to (cast⁻≃pathp refl p) r)) --- ... | yes q | no ¬r = --- no λ s → ¬r $ --- subst (λ e → cast⁻ refl e (x .hom⁻) ≡ y .hom⁻) --- (Nat.Nat-is-set _ _ _ _) --- (Equiv.from (cast⁻≃pathp refl (ap middle s)) $ ap hom⁻ s) --- ... | no ¬q | r = --- no λ s → ¬q $ --- subst (λ e → cast⁺ e refl (x .hom⁺) ≡ y .hom⁺) --- (Nat.Nat-is-set _ _ _ _) --- (Equiv.from (cast⁺≃pathp (ap middle s) refl) $ ap hom⁺ s) --- Discrete-Δ-Hom {x = x} {y = y} | no ¬p = no (¬p ⊙ ap middle) --- ``` ---
- --- By [[Hedberg's theorem]], all of these morphisms form sets. - --- ```agda --- Δ-Hom⁺-is-set : is-set (Δ-Hom⁺ m n) --- Δ-Hom⁺-is-set = Discrete→is-set Discrete-Δ-Hom⁺ - --- Δ-Hom⁻-is-set : is-set (Δ-Hom⁻ m n) --- Δ-Hom⁻-is-set = Discrete→is-set Discrete-Δ-Hom⁻ - --- Δ-Hom-is-set : is-set (Δ-Hom m n) --- Δ-Hom-is-set = Discrete→is-set Discrete-Δ-Hom --- ``` - - - - - - - - --- -- # Categories - --- -- ```agda --- -- Δ⁺-concrete : make-concrete Nat Δ-Hom⁺ --- -- Δ⁺-concrete .make-concrete.id = id⁺ --- -- Δ⁺-concrete .make-concrete._∘_ = _∘⁺_ --- -- Δ⁺-concrete .make-concrete.lvl = lzero --- -- Δ⁺-concrete .make-concrete.F₀ = Fin --- -- Δ⁺-concrete .make-concrete.F₀-is-set = hlevel! --- -- Δ⁺-concrete .make-concrete.F₁ = Δ⁺-map --- -- Δ⁺-concrete .make-concrete.F₁-inj = Δ⁺-map-inj _ _ --- -- Δ⁺-concrete .make-concrete.F-id = Δ⁺-map-id --- -- Δ⁺-concrete .make-concrete.F-∘ = Δ⁺-map-∘ - --- -- Δ⁺ : Precategory lzero lzero --- -- unquoteDef Δ⁺ = define-concrete-category Δ⁺ Δ⁺-concrete --- -- ``` - --- -- ```agda --- -- Δ⁻-concrete : make-concrete Nat Δ-Hom⁻ --- -- Δ⁻-concrete .make-concrete.id = id⁻ --- -- Δ⁻-concrete .make-concrete._∘_ = _∘⁻_ --- -- Δ⁻-concrete .make-concrete.lvl = lzero --- -- Δ⁻-concrete .make-concrete.F₀ = Fin --- -- Δ⁻-concrete .make-concrete.F₀-is-set = hlevel! --- -- Δ⁻-concrete .make-concrete.F₁ = Δ⁻-map --- -- Δ⁻-concrete .make-concrete.F₁-inj = Δ⁻-map-inj _ _ --- -- Δ⁻-concrete .make-concrete.F-id = Δ⁻-map-id --- -- Δ⁻-concrete .make-concrete.F-∘ = Δ⁻-map-∘ - --- -- Δ⁻ : Precategory lzero lzero --- -- unquoteDef Δ⁻ = define-concrete-category Δ⁻ Δ⁻-concrete --- -- ``` - --- -- # The simplex category - --- -- ```agda --- -- done : Δ-Hom 0 0 --- -- done .middle = 0 --- -- done .hom⁺ = done⁺ --- -- done .hom⁻ = done⁻ - --- -- crush : Δ-Hom m (suc n) → Δ-Hom (suc m) (suc n) --- -- crush f with f .middle | f .hom⁺ | f .hom⁻ --- -- ... | zero | f⁺ | done⁻ = Δ-hom (keep⁺ ¡⁺) id⁻ --- -- ... | suc x | f⁺ | f⁻ = Δ-hom f⁺ (crush⁻ f⁻) - --- -- shift : Δ-Hom m n → Δ-Hom m (suc n) --- -- shift f .middle = f .middle --- -- shift f .hom⁺ = shift⁺ (f .hom⁺) --- -- shift f .hom⁻ = f .hom⁻ - --- -- keep : Δ-Hom m n → Δ-Hom (suc m) (suc n) --- -- keep f .middle = suc (f .middle) --- -- keep f .hom⁺ = keep⁺ (f .hom⁺) --- -- keep f .hom⁻ = keep⁻ (f .hom⁻) --- -- ``` - --- -- ```agda --- -- idΔ : ∀ {n} → Δ-Hom n n --- -- idΔ {n} .middle = n --- -- idΔ {n} .hom⁺ = id⁺ --- -- idΔ {n} .hom⁻ = id⁻ - --- -- exchange --- -- : ∀ {m n o} --- -- → Δ-Hom⁻ n o → Δ-Hom⁺ m n --- -- → Δ-Hom m o --- -- exchange done⁻ done⁺ = Δ-hom done⁺ done⁻ --- -- exchange (crush⁻ f) (shift⁺ g) = exchange f g --- -- exchange (crush⁻ f) (keep⁺ g) = crush (exchange f g) --- -- exchange (keep⁻ f) (shift⁺ g) = shift (exchange f g) --- -- exchange (keep⁻ f) (keep⁺ g) = keep (exchange f g) --- -- ``` - - - --- -- -- ```agda --- -- -- Δ⁺-map-pres-< --- -- -- : ∀ {m n} --- -- -- → (f : Δ-Hom⁺ m n) --- -- -- → ∀ {i j} → i < j → Δ⁺-map f i < Δ⁺-map f j --- -- -- Δ⁺-map-pres-< (shift⁺ f) {i} {j} i +Proving this is pretty tedious though, especially for +general morphisms. + + +```agda + Discrete-Δ-Hom⁺ {x = done⁺} {y = done⁺} = + yes refl + Discrete-Δ-Hom⁺ {x = shift⁺ x} {y = shift⁺ y} = + Dec-map (ap shift⁺) shift⁺-inj Discrete-Δ-Hom⁺ + Discrete-Δ-Hom⁺ {x = shift⁺ x} {y = keep⁺ y} = + no shift⁺≠keep⁺ + Discrete-Δ-Hom⁺ {x = keep⁺ x} {y = shift⁺ y} = + no keep⁺≠shift⁺ + Discrete-Δ-Hom⁺ {x = keep⁺ x} {y = keep⁺ y} = + Dec-map (ap keep⁺) keep⁺-inj Discrete-Δ-Hom⁺ + + Discrete-Δ-Hom⁻ {x = done⁻} {y = done⁻} = + yes refl + Discrete-Δ-Hom⁻ {x = crush⁻ x} {y = crush⁻ y} = + Dec-map (ap crush⁻) crush⁻-inj Discrete-Δ-Hom⁻ + Discrete-Δ-Hom⁻ {x = crush⁻ x} {y = keep⁻ y} = + no crush⁻≠keep⁻ + Discrete-Δ-Hom⁻ {x = keep⁻ x} {y = crush⁻ y} = + no keep⁻≠crush⁻ + Discrete-Δ-Hom⁻ {x = keep⁻ x} {y = keep⁻ y} = + Dec-map (ap keep⁻) keep⁻-inj Discrete-Δ-Hom⁻ + + Discrete-Δ-Hom {x = x} {y = y} with x .im ≡? y .im + ... | yes p with cast⁺ p refl (x .hom⁺) ≡? (y .hom⁺) | cast⁻ refl p (x .hom⁻) ≡? y .hom⁻ + ... | yes q | yes r = + yes (Δ-Hom-path p (Equiv.to (cast⁺≃pathp p refl) q) (Equiv.to (cast⁻≃pathp refl p) r)) + ... | yes q | no ¬r = + no λ s → ¬r $ + subst (λ e → cast⁻ refl e (x .hom⁻) ≡ y .hom⁻) + (Nat.Nat-is-set _ _ _ _) + (Equiv.from (cast⁻≃pathp refl (ap im s)) $ ap hom⁻ s) + ... | no ¬q | r = + no λ s → ¬q $ + subst (λ e → cast⁺ e refl (x .hom⁺) ≡ y .hom⁺) + (Nat.Nat-is-set _ _ _ _) + (Equiv.from (cast⁺≃pathp (ap im s) refl) $ ap hom⁺ s) + Discrete-Δ-Hom {x = x} {y = y} | no ¬p = no (¬p ⊙ ap im) +``` + From 23e90e92f4b98138561d585c037bf2db3a1ed502 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Fri, 12 Apr 2024 12:56:38 -0400 Subject: [PATCH 07/18] def: antiinjective and antisurjective functions --- src/1Lab/Classical.lagda.md | 2 +- src/1Lab/Function/Antiinjection.lagda.md | 164 ++++++++++++++++++++++ src/1Lab/Function/Antisurjection.lagda.md | 128 +++++++++++++++++ src/1Lab/Function/Surjection.lagda.md | 16 +++ 4 files changed, 309 insertions(+), 1 deletion(-) create mode 100644 src/1Lab/Function/Antiinjection.lagda.md create mode 100644 src/1Lab/Function/Antisurjection.lagda.md diff --git a/src/1Lab/Classical.lagda.md b/src/1Lab/Classical.lagda.md index f29ad8023..7e6cf58e7 100644 --- a/src/1Lab/Classical.lagda.md +++ b/src/1Lab/Classical.lagda.md @@ -120,7 +120,7 @@ Surjections-split = ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → is-set A → is-set B → (f : A → B) → is-surjective f - → ∥ (∀ b → fibre f b) ∥ + → ∥ split-surjective f ∥ ``` We show that these two statements are logically equivalent^[they are also diff --git a/src/1Lab/Function/Antiinjection.lagda.md b/src/1Lab/Function/Antiinjection.lagda.md new file mode 100644 index 000000000..65786b193 --- /dev/null +++ b/src/1Lab/Function/Antiinjection.lagda.md @@ -0,0 +1,164 @@ +--- +description: | + Antiinjective functions. +--- + +```agda +module 1Lab.Function.Antiinjection where +``` + + + +# Antiinjective functions {defines="split-antiinjective antiinjective"} + +A function is **split antiinjective** if it comes equipped with a choice +of fibre that contains 2 distinct elements. Likewise, a function is +**antiinjective** if it is merely split injective. This is constructively +stronger than non-injective, as we actually know at least one obstruction +to injectivity! Moreover, note that split antiinjectivity is a structure +on a function, not a property; there may be obstructions to injectivity. + +```agda +record split-antiinjective (f : A → B) : Type (level-of A ⊔ level-of B) where + no-eta-equality + field + pt : B + x₀ : A + x₁ : A + map-to₀ : f x₀ ≡ pt + map-to₁ : f x₁ ≡ pt + distinct : ¬ (x₀ ≡ x₁) + +is-antiinjective : (A → B) → Type _ +is-antiinjective f = ∥ split-antiinjective f ∥ +``` + + + +As the name suggests, antiinjective functions are not injective. + +```agda +split-antiinj→not-injective + : {f : A → B} + → split-antiinjective f + → ¬ (injective f) +split-antiinj→not-injective f-antiinj f-inj = + f-antiinj .distinct (f-inj (f-antiinj .map-to₀ ∙ sym (f-antiinj .map-to₁))) + +is-antiinj→not-injective + : {f : A → B} + → is-antiinjective f + → ¬ (injective f) +is-antiinj→not-injective f-antiinj = + rec! split-antiinj→not-injective f-antiinj +``` + + + +Precomposition by an (split) antinjective function always yields a +(split) antiinjective function. + +```agda +split-antiinj-∘r + : {f : B → C} {g : A → B} + → split-antiinjective g + → split-antiinjective (f ∘ g) +split-antiinj-∘r {f = f} g-antiinj .pt = f (g-antiinj .pt) +split-antiinj-∘r {f = f} g-antiinj .x₀ = g-antiinj .x₀ +split-antiinj-∘r {f = f} g-antiinj .x₁ = g-antiinj .x₁ +split-antiinj-∘r {f = f} g-antiinj .map-to₀ = ap f (g-antiinj .map-to₀) +split-antiinj-∘r {f = f} g-antiinj .map-to₁ = ap f (g-antiinj .map-to₁) +split-antiinj-∘r {f = f} g-antiinj .distinct = g-antiinj .distinct + +is-antiinj-∘r + : {f : B → C} {g : A → B} + → is-antiinjective g + → is-antiinjective (f ∘ g) +is-antiinj-∘r {f = f} = ∥-∥-map (split-antiinj-∘r {f = f}) +``` + +If $f : B \to C$ is split antiinjective and $g : A \to B$ can be equipped with a choice +of fibres at the obstruction to injectivity, then $f \circ g$ is also antiinjective. + +```agda +split-antiinj+in-image→split-antiinj + : {f : B → C} {g : A → B} + → (f-ai : split-antiinjective f) + → fibre g (f-ai .x₀) → fibre g (f-ai .x₁) + → split-antiinjective (f ∘ g) +split-antiinj+in-image→split-antiinj {f = f} {g = g} f-ai (a₀ , p₀) (a₁ , p₁) = fg-ai + where + fg-ai : split-antiinjective (f ∘ g) + fg-ai .pt = f-ai .pt + fg-ai .x₀ = a₀ + fg-ai .x₁ = a₁ + fg-ai .map-to₀ = ap f p₀ ∙ f-ai .map-to₀ + fg-ai .map-to₁ = ap f p₁ ∙ f-ai .map-to₁ + fg-ai .distinct a₀=a₁ = f-ai .distinct (sym p₀ ·· ap g a₀=a₁ ·· p₁) +``` + +In particular, this means that composing a (split) antiinjection with a (split) +surjection yields a (split) antiinjection. + +```agda +split-antiinj+split-surj→split-antiinj + : {f : B → C} {g : A → B} + → split-antiinjective f + → split-surjective g + → split-antiinjective (f ∘ g) +split-antiinj+split-surj→split-antiinj f-ai g-s = + split-antiinj+in-image→split-antiinj f-ai (g-s (f-ai .x₀)) (g-s (f-ai .x₁)) + +is-antiinj+is-surj→is-antiinj + : {f : B → C} {g : A → B} + → is-antiinjective f + → is-surjective g + → is-antiinjective (f ∘ g) +is-antiinj+is-surj→is-antiinj ∥f-ai∥ g-s = do + f-ai ← ∥f-ai∥ + fib₀ ← g-s (f-ai .x₀) + fib₁ ← g-s (f-ai .x₁) + pure (split-antiinj+in-image→split-antiinj f-ai fib₀ fib₁) +``` diff --git a/src/1Lab/Function/Antisurjection.lagda.md b/src/1Lab/Function/Antisurjection.lagda.md new file mode 100644 index 000000000..8d5b4548f --- /dev/null +++ b/src/1Lab/Function/Antisurjection.lagda.md @@ -0,0 +1,128 @@ +--- +description: | + Antisurjective functions. +--- + +```agda +module 1Lab.Function.Antisurjection where +``` + + + +## Antisurjective functions {defines="antisurjective split-antisurjective"} + +A function is **antisurjective** if there merely exists some $b : B$ +with an empty fibre. This is constructively stronger than being +non-surjective, which states that it is not the case that all fibres +are (merely) inhabited. + +```agda +is-antisurjective : (A → B) → Type _ +is-antisurjective {B = B} f = ∃[ b ∈ B ] (¬ (fibre f b)) +``` + +Likewise, a function is **split antisurjective** if there is some +$b : B$ with an empty fibre. Note that this is a structure on a function, +not a property, as there may be many ways a function fails to be surjective! + +```agda +split-antisurjective : (A → B) → Type _ +split-antisurjective {B = B} f = Σ[ b ∈ B ] (¬ (fibre f b)) +``` + +As the name suggests, antisurjective functions are not surjective. + +```agda +split-antisurj→not-surjective + : {f : A → B} + → split-antisurjective f + → ¬ (is-surjective f) +split-antisurj→not-surjective (b , ¬fib) f-s = + rec! (λ a p → ¬fib (a , p)) (f-s b) + +is-antisurj→not-surjective + : {f : A → B} + → is-antisurjective f + → ¬ (is-surjective f) +is-antisurj→not-surjective f-as = + rec! (λ b ¬fib → split-antisurj→not-surjective (b , ¬fib)) f-as +``` + + + +If $f$ is antisurjective and $g$ is an arbitrary function, then $f \circ g$ +is also antisurjective. + +```agda +split-antisurj-∘l + : {f : B → C} {g : A → B} + → split-antisurjective f + → split-antisurjective (f ∘ g) +split-antisurj-∘l {g = g} (c , ¬fib) = c , ¬fib ∘ Σ-map g (λ p → p) + +is-antisurj-∘l + : {f : B → C} {g : A → B} + → is-antisurjective f + → is-antisurjective (f ∘ g) +is-antisurj-∘l {f = f} {g = g} = ∥-∥-map split-antisurj-∘l +``` + +If $f$ is injective and $g$ is antisurjective, then $f \circ g$ is +also antisurjective. + +```agda +inj+split-antisurj→split-antisurj + : {f : B → C} {g : A → B} + → injective f + → split-antisurjective g + → split-antisurjective (f ∘ g) +inj+split-antisurj→split-antisurj {f = f} f-inj (b , ¬fib) = + f b , ¬fib ∘ Σ-map₂ f-inj + +inj+is-antisurj→is-antisurj + : {f : B → C} {g : A → B} + → injective f + → is-antisurjective g + → is-antisurjective (f ∘ g) +inj+is-antisurj→is-antisurj f-inj = + ∥-∥-map (inj+split-antisurj→split-antisurj f-inj) +``` diff --git a/src/1Lab/Function/Surjection.lagda.md b/src/1Lab/Function/Surjection.lagda.md index abf1aa928..361a8f3e0 100644 --- a/src/1Lab/Function/Surjection.lagda.md +++ b/src/1Lab/Function/Surjection.lagda.md @@ -4,6 +4,7 @@ open import 1Lab.Function.Embedding open import 1Lab.Reflection.HLevel open import 1Lab.HIT.Truncation open import 1Lab.HLevel.Closure +open import 1Lab.Type.Sigma open import 1Lab.Inductive open import 1Lab.HLevel open import 1Lab.Equiv @@ -144,3 +145,18 @@ injective-surjective→is-equiv! = injective-surjective→is-equiv (hlevel 2) ``` --> + +## Split surjective functions {defines="split-surjective"} + +A function is **split surjective** if for each $b : B$ we have a designated +element of the fibre $f^*b$. Note that this is actually a *structure* +on $f$ instead of a property: in fact, the statement that every +surjection between sets is a split surjection is [equivalent to the +axiom of choice]. + +[equivalent to the axiom of choice]: 1Lab.Classical.html#axiom-of-choice + +```agda +split-surjective : (A → B) → Type _ +split-surjective f = ∀ b → fibre f b +``` From c7766074c344c6aa4f4279fe717128febd7d22c7 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Fri, 12 Apr 2024 18:28:01 -0400 Subject: [PATCH 08/18] def: version of identity system that works on loops --- src/1Lab/Path/IdentitySystem.lagda.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/1Lab/Path/IdentitySystem.lagda.md b/src/1Lab/Path/IdentitySystem.lagda.md index a2cc7a102..8b6fdca87 100644 --- a/src/1Lab/Path/IdentitySystem.lagda.md +++ b/src/1Lab/Path/IdentitySystem.lagda.md @@ -341,3 +341,20 @@ opaque ... | yes p = p ... | no ¬p = absurd (¬¬p ¬p) ``` + + From 0810e8e50139ca42ab91f023b5fb73ef4d6ce3c8 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Fri, 12 Apr 2024 18:28:45 -0400 Subject: [PATCH 09/18] def: more random nat/fin properties --- src/Data/Fin/Base.lagda.md | 14 ---- src/Data/Fin/Properties.lagda.md | 140 +++++++++++++++++++++++++++++++ src/Data/Nat/Base.lagda.md | 7 ++ src/Data/Nat/Order.lagda.md | 9 ++ 4 files changed, 156 insertions(+), 14 deletions(-) diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md index 64055c139..1db65f062 100644 --- a/src/Data/Fin/Base.lagda.md +++ b/src/Data/Fin/Base.lagda.md @@ -317,9 +317,6 @@ delete ρ i j = ρ (skip i j) fabsurd : ∀ {ℓ} {A : Type ℓ} → Fin 0 → A fabsurd () -Finite-one-is-prop : is-prop (Fin 1) -Finite-one-is-prop fzero fzero = refl - fpred : ∀ {n} → Fin (2 + n) → Fin (1 + n) fpred fzero = fzero fpred (fsuc i) = i @@ -327,16 +324,5 @@ fpred (fsuc i) = i fkeep : ∀ {m n} → (Fin m → Fin n) → Fin (suc m) → Fin (suc n) fkeep f fzero = fzero fkeep f (fsuc i) = fsuc (f i) - -fkeep-id : ∀ {n} → ∀ (i : Fin (suc n)) → fkeep (λ x → x) i ≡ i -fkeep-id fzero = refl -fkeep-id (fsuc i) = refl - -fkeep-∘ - : ∀ {m n o} - → {f : Fin n → Fin o} {g : Fin m → Fin n} - → ∀ i → fkeep (f ∘ g) i ≡ fkeep f (fkeep g i) -fkeep-∘ fzero = refl -fkeep-∘ (fsuc i) = refl ``` --> diff --git a/src/Data/Fin/Properties.lagda.md b/src/Data/Fin/Properties.lagda.md index d77a576f9..aff176447 100644 --- a/src/Data/Fin/Properties.lagda.md +++ b/src/Data/Fin/Properties.lagda.md @@ -2,6 +2,9 @@ ```agda open import 1Lab.Prelude +open import 1Lab.Function.Antisurjection +open import 1Lab.Function.Antiinjection + open import Data.Dec.Base open import Data.Fin.Base @@ -331,3 +334,140 @@ to-nat-weaken-≤ (Nat.s≤s p) (Nat.s≤s q) fzero = refl to-nat-weaken-≤ (Nat.s≤s p) (Nat.s≤s q) (fsuc i) = ap suc (to-nat-weaken-≤ p q i) ``` --> + + + + diff --git a/src/Data/Nat/Base.lagda.md b/src/Data/Nat/Base.lagda.md index 9da4870d7..6bf55f364 100644 --- a/src/Data/Nat/Base.lagda.md +++ b/src/Data/Nat/Base.lagda.md @@ -229,6 +229,13 @@ m < n = suc m ≤ n infix 3 _<_ _≤_ ``` + + As an "ordering combinator", we can define the _maximum_ of two natural numbers by recursion: The maximum of zero and a successor (on either side) is the successor, and the maximum of successors is the successor of diff --git a/src/Data/Nat/Order.lagda.md b/src/Data/Nat/Order.lagda.md index eba29ab9e..fdafe1c4e 100644 --- a/src/Data/Nat/Order.lagda.md +++ b/src/Data/Nat/Order.lagda.md @@ -145,6 +145,15 @@ weaken-< : ∀ {x y} → x < y → x ≤ y weaken-< {x} {suc y} p = ≤-sucr (≤-peel p) ``` + + ## Nat is a lattice An interesting tidbit about the ordering on $\NN$ is that it is, in some From 7954f8aeeba09cb2c1f2797906d96ae73777b4dd Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Fri, 12 Apr 2024 18:29:05 -0400 Subject: [PATCH 10/18] def: cancellation of antiinj/surj functions --- src/1Lab/Function/Antiinjection.lagda.md | 27 +++++++++++++++++++++++ src/1Lab/Function/Antisurjection.lagda.md | 17 ++++++++++++++ 2 files changed, 44 insertions(+) diff --git a/src/1Lab/Function/Antiinjection.lagda.md b/src/1Lab/Function/Antiinjection.lagda.md index 65786b193..8a53b7499 100644 --- a/src/1Lab/Function/Antiinjection.lagda.md +++ b/src/1Lab/Function/Antiinjection.lagda.md @@ -162,3 +162,30 @@ is-antiinj+is-surj→is-antiinj ∥f-ai∥ g-s = do fib₁ ← g-s (f-ai .x₁) pure (split-antiinj+in-image→split-antiinj f-ai fib₀ fib₁) ``` + +```agda +split-antiinj-cancell + : {f : B → C} {g : A → B} + → injective f + → split-antiinjective (f ∘ g) + → split-antiinjective g +split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .pt = + g (fg-ai .x₀) +split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .x₀ = + fg-ai .x₀ +split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .x₁ = + fg-ai .x₁ +split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .map-to₀ = + refl +split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .map-to₁ = + f-inj (fg-ai .map-to₁ ∙ sym (fg-ai .map-to₀)) +split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .distinct = + fg-ai .distinct + +is-antiinj-cancell + : {f : B → C} {g : A → B} + → injective f + → is-antiinjective (f ∘ g) + → is-antiinjective g +is-antiinj-cancell f-inj = ∥-∥-map (split-antiinj-cancell f-inj) +``` diff --git a/src/1Lab/Function/Antisurjection.lagda.md b/src/1Lab/Function/Antisurjection.lagda.md index 8d5b4548f..9c42fc737 100644 --- a/src/1Lab/Function/Antisurjection.lagda.md +++ b/src/1Lab/Function/Antisurjection.lagda.md @@ -126,3 +126,20 @@ inj+is-antisurj→is-antisurj inj+is-antisurj→is-antisurj f-inj = ∥-∥-map (inj+split-antisurj→split-antisurj f-inj) ``` + +```agda +split-antisurj-cancelr + : {f : B → C} {g : A → B} + → is-surjective g + → split-antisurjective (f ∘ g) + → split-antisurjective f +split-antisurj-cancelr {f = f} {g = g} surj (c , ¬fib) = + c , rec! λ b p → rec! (λ a q → ¬fib (a , ap f q ∙ p)) (surj b) + +is-antisurj-cancelr + : {f : B → C} {g : A → B} + → is-surjective g + → is-antisurjective (f ∘ g) + → is-antisurjective f +is-antisurj-cancelr surj = ∥-∥-map (split-antisurj-cancelr surj) +``` From 0400c1da73c04b81ba48bc08af2d3ad0214e28bb Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Fri, 12 Apr 2024 18:29:31 -0400 Subject: [PATCH 11/18] def: add not? to Data.Dec --- src/Data/Dec/Base.lagda.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Data/Dec/Base.lagda.md b/src/Data/Dec/Base.lagda.md index 669352fc4..b844d1baf 100644 --- a/src/Data/Dec/Base.lagda.md +++ b/src/Data/Dec/Base.lagda.md @@ -164,6 +164,10 @@ is-yes : ∀ {ℓ} {A : Type ℓ} → Dec A → Type is-yes (yes x) = ⊤ is-yes (no _) = ⊥ +not? : ∀ {ℓ} {A : Type ℓ} → Dec A → Dec (¬ A) +not? (yes p) = no (_$ p) +not? (no ¬p) = yes ¬p + decide! : ∀ {ℓ} {A : Type ℓ} ⦃ d : Dec A ⦄ {_ : is-yes d} → A decide! ⦃ yes x ⦄ = x ``` From 29b5a0c8a5b8d61a2e6720ef8598b7c48f3cdf1a Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Fri, 12 Apr 2024 18:29:48 -0400 Subject: [PATCH 12/18] def: univalence of simplex categories --- src/Cat/Instances/Simplex.lagda.md | 833 +++++++++++++++++++++++++---- 1 file changed, 723 insertions(+), 110 deletions(-) diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md index d1e4c35b3..1eb447db0 100644 --- a/src/Cat/Instances/Simplex.lagda.md +++ b/src/Cat/Instances/Simplex.lagda.md @@ -6,6 +6,9 @@ description: | ```agda open import Meta.Brackets +open import 1Lab.Function.Antisurjection +open import 1Lab.Function.Antiinjection + open import Data.Dec open import Data.Fin @@ -35,12 +38,14 @@ module Cat.Instances.Simplex where -# The simplex category {defines="simplex-category semisimplex-category"} +# The simplex category {defines="simplex-category semisimplex-category demisimplex-category"} The simplex category, $\Delta$, is generally introduced as the category + of non-empty finite ordinals and order-preserving maps. Though conceptually simple, this definition is difficult to work with: in particular, diagrams over $\Delta$ are extremely hard to form! This is why mathematicians @@ -369,11 +374,12 @@ demisimplicial maps encode *split* surjections. Δ-hom⁺-to-inj : ∀ {m n} → (f : Δ-Hom⁺ m n) - → injective (Δ-hom⁺ f) + → injective ⟦ f ⟧ + Δ-hom⁻-to-split-surj : ∀ {m n} → (f : Δ-Hom⁻ m n) - → ∀ (i : Fin n) → fibre (Δ-hom⁻ f) i + → split-surjective ⟦ f ⟧ ```
@@ -401,6 +407,16 @@ demisimplicial maps encode *split* surjections. ```
+ + We also remark that semi and demisimplicial maps always encode monotonic functions. ```agda @@ -461,6 +477,7 @@ Likewise, demisimplicial maps reflect the strict order. Nat.s≤s (Δ-hom⁻-reflect-< f⁻ (Nat.≤-peel fi + ### Functoriality of interpretations Finally, we shall prove functoriality of all of our interpretations. @@ -749,7 +795,7 @@ are concrete is just an exercise in building records. Δₐ⁺-concrete .make-concrete._∘_ = _∘⁺_ Δₐ⁺-concrete .make-concrete.lvl = lzero Δₐ⁺-concrete .make-concrete.F₀ = Fin -Δₐ⁺-concrete .make-concrete.F₀-is-set = hlevel! +Δₐ⁺-concrete .make-concrete.F₀-is-set = hlevel 2 Δₐ⁺-concrete .make-concrete.F₁ = Δ-hom⁺ Δₐ⁺-concrete .make-concrete.F₁-inj = Δ-hom⁺-inj _ _ Δₐ⁺-concrete .make-concrete.F-id = Δ-hom⁺-id @@ -759,7 +805,7 @@ are concrete is just an exercise in building records. Δₐ⁻-concrete .make-concrete._∘_ = _∘⁻_ Δₐ⁻-concrete .make-concrete.lvl = lzero Δₐ⁻-concrete .make-concrete.F₀ = Fin -Δₐ⁻-concrete .make-concrete.F₀-is-set = hlevel! +Δₐ⁻-concrete .make-concrete.F₀-is-set = hlevel 2 Δₐ⁻-concrete .make-concrete.F₁ = Δ-hom⁻ Δₐ⁻-concrete .make-concrete.F₁-inj = Δ-hom⁻-inj _ _ Δₐ⁻-concrete .make-concrete.F-id = Δ-hom⁻-id @@ -769,7 +815,7 @@ are concrete is just an exercise in building records. Δₐ-concrete .make-concrete._∘_ = _∘Δ_ Δₐ-concrete .make-concrete.lvl = lzero Δₐ-concrete .make-concrete.F₀ = Fin -Δₐ-concrete .make-concrete.F₀-is-set = hlevel! +Δₐ-concrete .make-concrete.F₀-is-set = hlevel 2 Δₐ-concrete .make-concrete.F₁ = Δ-hom Δₐ-concrete .make-concrete.F₁-inj = Δ-hom-inj _ _ Δₐ-concrete .make-concrete.F-id = Δ-hom-id @@ -779,7 +825,7 @@ are concrete is just an exercise in building records. Δ⁺-concrete .make-concrete._∘_ = _∘⁺_ Δ⁺-concrete .make-concrete.lvl = lzero Δ⁺-concrete .make-concrete.F₀ n = Fin (suc n) -Δ⁺-concrete .make-concrete.F₀-is-set = hlevel! +Δ⁺-concrete .make-concrete.F₀-is-set = hlevel 2 Δ⁺-concrete .make-concrete.F₁ = Δ-hom⁺ Δ⁺-concrete .make-concrete.F₁-inj = Δ-hom⁺-inj _ _ Δ⁺-concrete .make-concrete.F-id = Δ-hom⁺-id @@ -789,7 +835,7 @@ are concrete is just an exercise in building records. Δ⁻-concrete .make-concrete._∘_ = _∘⁻_ Δ⁻-concrete .make-concrete.lvl = lzero Δ⁻-concrete .make-concrete.F₀ n = Fin (suc n) -Δ⁻-concrete .make-concrete.F₀-is-set = hlevel! +Δ⁻-concrete .make-concrete.F₀-is-set = hlevel 2 Δ⁻-concrete .make-concrete.F₁ = Δ-hom⁻ Δ⁻-concrete .make-concrete.F₁-inj = Δ-hom⁻-inj _ _ Δ⁻-concrete .make-concrete.F-id = Δ-hom⁻-id @@ -799,7 +845,7 @@ are concrete is just an exercise in building records. Δ-concrete .make-concrete._∘_ = _∘Δ_ Δ-concrete .make-concrete.lvl = lzero Δ-concrete .make-concrete.F₀ n = Fin (suc n) -Δ-concrete .make-concrete.F₀-is-set = hlevel! +Δ-concrete .make-concrete.F₀-is-set = hlevel 2 Δ-concrete .make-concrete.F₁ = Δ-hom Δ-concrete .make-concrete.F₁-inj = Δ-hom-inj _ _ Δ-concrete .make-concrete.F-id = Δ-hom-id @@ -837,6 +883,605 @@ module Δ⁻ = Cat.Reasoning Δ⁻ module Δ = Cat.Reasoning Δ ``` +## Univalence + +All of the various semi/demi/augmented simplex categories are univalent, +though this is somewhat non-trivial to show. The proof will consist of 3 +major steps: +1. Every map that does not contain a `shift⁺`{.Agda} or a `crush⁻`{.Agda} constructor + preserves dimension. +2. Every semi/demisimplicial endomap is an identity. +3. A map is is interpreted as an equivalence if and only if it does not + contain any `shift⁺`{.Agda} or a `crush⁻`{.Agda} constructors. + +Once we have these 3 pieces, we can show that every isomorphism is an +equivalence, so it cannot contain `shift⁺`{.Agda} or a `crush⁻`{.Agda} +constructors. This means that the image of every factorization of an +isomorphism must have the same dimension as both endpoints, so both +the semi/demisimplicial components of the factorization are endomaps, +and thus identities. + +Filling out this proof sketch will involve quite a bit of work, so +let's get to it! + +### Dimension + +First, note that every semisimplicial map raises the dimension, and +every demisimplicial map lowers it. + +```agda +Δ-dim⁺-≤ : ∀ {m n} → (f : Δ-Hom⁺ m n) → m Nat.≤ n +Δ-dim⁺-≤ done⁺ = Nat.0≤x +Δ-dim⁺-≤ (shift⁺ f) = Nat.≤-sucr (Δ-dim⁺-≤ f) +Δ-dim⁺-≤ (keep⁺ f) = Nat.s≤s (Δ-dim⁺-≤ f) + +Δ-dim⁻-≤ : ∀ {m n} → (f : Δ-Hom⁻ m n) → n Nat.≤ m +Δ-dim⁻-≤ done⁻ = Nat.0≤x +Δ-dim⁻-≤ (crush⁻ f) = Nat.≤-sucr (Δ-dim⁻-≤ f) +Δ-dim⁻-≤ (keep⁻ f) = Nat.s≤s (Δ-dim⁻-≤ f) +``` + +We can tighten these bounds if $f$ contains a `shift⁺`{.Agda} or a +`crush⁻`{.Agda} constructor. + +```agda +has-shift⁺ : ∀ {m n} → Δ-Hom⁺ m n → Type +has-shift⁺ done⁺ = ⊥ +has-shift⁺ (shift⁺ f) = ⊤ +has-shift⁺ (keep⁺ f) = has-shift⁺ f + +has-crush⁻ : ∀ {m n} → Δ-Hom⁻ m n → Type +has-crush⁻ done⁻ = ⊥ +has-crush⁻ (crush⁻ f) = ⊤ +has-crush⁻ (keep⁻ f) = has-crush⁻ f + +has-shift : ∀ {m n} → Δ-Hom m n → Type +has-shift f = has-shift⁺ (f .hom⁺) + +has-crush : ∀ {m n} → Δ-Hom m n → Type +has-crush f = has-crush⁻ (f .hom⁻) + +Δ-dim⁺-< : ∀ {m n} → (f : Δ-Hom⁺ m n) → has-shift⁺ f → m Nat.< n +Δ-dim⁺-< (shift⁺ f) p = Nat.s≤s (Δ-dim⁺-≤ f) +Δ-dim⁺-< (keep⁺ f) p = Nat.s≤s (Δ-dim⁺-< f p) + +Δ-dim⁻-< : ∀ {m n} → (f : Δ-Hom⁻ m n) → has-crush⁻ f → n Nat.< m +Δ-dim⁻-< (crush⁻ f) p = Nat.s≤s (Δ-dim⁻-≤ f) +Δ-dim⁻-< (keep⁻ f) p = Nat.s≤s (Δ-dim⁻-< f p) +``` + +The converse is also true; if $f$ strictly raises or lowers the dimension +then contains a `shift⁺`{.Agda} or a `crush⁻`{.Agda} constructor. + +```agda +Δ-dim⁺-<-has-shift⁺ + : ∀ (f⁺ : Δ-Hom⁺ m n) + → m Nat.< n + → has-shift⁺ f⁺ +Δ-dim⁺-<-has-shift⁺ (shift⁺ f⁺) m + +At this point, we already have enough results to show that the +(augmented) semi and demisimplex categories are univalent! We +will only focus on the augmented semisimplex category, as all the +other cases are more are less identical. + +The key insight is that we can get a path $m = n$ from a pair of +semisimplicial maps $[m] \to [n], [n] \to [m]$ by appealing to +our antisymmetry. + +```agda +Δ-hom⁺-pair-dim + : ∀ (f : Δ-Hom⁺ m n) (f⁻¹ : Δ-Hom⁺ n m) + → m ≡ n +Δ-hom⁺-pair-dim f f⁻¹ = Nat.≤-antisym (Δ-dim⁺-≤ f) (Δ-dim⁺-≤ f⁻¹) +``` + +This gives us a way to turn isomorphisms in $\Delta_{a}^{+}$ into +paths, and there is a unique automorphism, so $\Delta_{a}^{+}$ must +be univalent. + +```agda +Δₐ⁺-is-category : is-category Δₐ⁺ +Δₐ⁺-is-category = + set-identity-system-K + (λ n f → Δₐ⁺.≅-path (Δ-endo⁺-id (Δₐ⁺.to f))) + (λ f → Δ-hom⁺-pair-dim (Δₐ⁺.to f) (Δₐ⁺.from f)) +``` + + + +Unfortunately, simplicial maps require an additional step. Our goal is to +characterise the morphisms that get interpreted as equivalence, but we will +do this in a somewhat roundabout way: instead of characterizing equivalences, we +will characterize everything that is *not* an equivalence! + +In particular, we our goal is to show that a morphism is an equivalence if +and only if it does not contain any `shift⁺`{.Agda} or a `crush⁻`{.Agda} +constructor. However, doing so will require characterizing morphisms that *do* +contain these constructors. First, note that if a semisimplicial map $f$ +contains a `shift⁺`{.Agda}, then it is [[split antisurjective]], as we can +find an element in the codomain that is not in the image of $f$. + +```agda +shift⁺-split-antisurj + : ∀ (f⁺ : Δ-Hom⁺ m n) + → split-antisurjective ⟦ shift⁺ f⁺ ⟧ +shift⁺-split-antisurj f⁺ = fzero , fsuc≠fzero ⊙ snd + +has-shift⁺→split-antisurj + : ∀ (f⁺ : Δ-Hom⁺ m n) + → has-shift⁺ f⁺ + → split-antisurjective ⟦ f⁺ ⟧ +has-shift⁺→split-antisurj (shift⁺ f⁺) shift = + shift⁺-split-antisurj f⁺ +has-shift⁺→split-antisurj (keep⁺ f⁺) shift = + fkeep-split-antisurj (has-shift⁺→split-antisurj f⁺ shift) +``` + +Similarly, if a demisimplicial map $f$ contains a `crush⁻`, then it +is [[split antiinjective]], as we can find a fibre that contains at +least 2 distinct elements. The proof of this is a bit tricky though: +we need to observe that there are no demisimplicial maps $[1 + n] \to [0]$. + + + +```agda +Δ-hom⁻-zero-strict : ¬ (Δ-Hom⁻ (suc n) 0) +Δ-hom⁻-zero-strict (crush⁻ f⁻) = Δ-hom⁻-zero-strict f⁻ + +crush⁻-split-antiinj + : ∀ (f⁻ : Δ-Hom⁻ (suc m) n) + → split-antiinjective ⟦ crush⁻ f⁻ ⟧ +crush⁻-split-antiinj {n = zero} f⁻ = absurd (Δ-hom⁻-zero-strict f⁻) +crush⁻-split-antiinj {n = suc n} f⁻ = antiinj where + open split-antiinjective + + antiinj : split-antiinjective (⟦ f⁻ ⟧ ⊙ fpred) + antiinj .pt = 0 + antiinj .x₀ = 0 + antiinj .x₁ = 1 + antiinj .map-to₀ = Δ-hom⁻-zero f⁻ + antiinj .map-to₁ = Δ-hom⁻-zero f⁻ + antiinj .distinct = fzero≠fsuc + +has-crush⁻→split-antiinj + : ∀ (f⁻ : Δ-Hom⁻ m n) + → has-crush⁻ f⁻ + → split-antiinjective ⟦ f⁻ ⟧ +has-crush⁻→split-antiinj (crush⁻ f⁻) degen = crush⁻-split-antiinj f⁻ +has-crush⁻→split-antiinj (keep⁻ f⁻) degen = + fkeep-split-antiinj (has-crush⁻→split-antiinj f⁻ degen) +``` + +The converse also holds: if $f$ is split antisurjective or antiinjective, +then $f$ has a `shift⁺`{.Agda} or a `crush⁻`{.Agda}. + +```agda +split-antisurj→has-shift⁺ + : ∀ (f⁺ : Δ-Hom⁺ m n) + → split-antisurjective ⟦ f⁺ ⟧ + → has-shift⁺ f⁺ +split-antisurj→has-shift⁺ (shift⁺ f⁺) antisurj = tt +split-antisurj→has-shift⁺ (keep⁺ f⁺) antisurj = + split-antisurj→has-shift⁺ f⁺ (fkeep-reflect-split-antisurj antisurj) + +split-antiinj→has-crush⁻ + : ∀ (f⁻ : Δ-Hom⁻ m n) + → split-antiinjective ⟦ f⁻ ⟧ + → has-crush⁻ f⁻ +split-antiinj→has-crush⁻ done⁻ antiinj = fabsurd (antiinj .pt) +split-antiinj→has-crush⁻ (crush⁻ f⁻) antiinj = tt +split-antiinj→has-crush⁻ (keep⁻ f⁻) antiinj = + split-antiinj→has-crush⁻ f⁻ (fkeep-reflect-split-antiinj antiinj) +``` + +Split antiinjective and antisurjective functions are stable under post +and precomposition respectively, so simplicial maps that contain +`shift⁺`{.Agda} or `crush⁻`{.Agda} are also split antiinjective/antisurjective. + +```agda +has-shift→split-antisurj + : (f : Δ-Hom m n) + → has-shift f + → split-antisurjective ⟦ f ⟧ +has-shift→split-antisurj f shift = + split-antisurj-∘l {f = ⟦ f .hom⁺ ⟧} {g = ⟦ f .hom⁻ ⟧} $ + has-shift⁺→split-antisurj (f .hom⁺) shift + +has-crush→split-antiinj + : (f : Δ-Hom m n) + → has-crush f + → split-antiinjective ⟦ f ⟧ +has-crush→split-antiinj f crush = + split-antiinj-∘r {f = ⟦ f .hom⁺ ⟧} {g = ⟦ f .hom⁻ ⟧} $ + has-crush⁻→split-antiinj (f .hom⁻) crush +``` + +Conversely, if a simplicial map is split antiinjective or antisurjective, +then it contains a `shift⁺`{.Agda} or a `crush⁻`{.Agda}, respectively. +We shall focus on the antisurjective case, as the antiinjective one +follows a similar argument. Recall that if $f \circ g$ is antisurjective +and $g$ is surjective, then $f$ must be antisurjective. This means that +the semisimplicial portion of the factorization must be antisurjective, +and thus must contain a shift. + +```agda +split-antisurj→has-shift + : (f : Δ-Hom m n) + → split-antisurjective ⟦ f ⟧ + → has-shift f +split-antisurj→has-shift f antisurj = + split-antisurj→has-shift⁺ (f .hom⁺) $ + split-antisurj-cancelr (Δ-hom⁻-to-surj (f .hom⁻)) antisurj +``` + +
+As noted above, antiinjectivity follows an identical argument. + +```agda +split-antiinj→has-crush + : (f : Δ-Hom m n) + → split-antiinjective ⟦ f ⟧ + → has-crush f +split-antiinj→has-crush f antiinj = + split-antiinj→has-crush⁻ (f .hom⁻) $ + split-antiinj-cancell (Δ-hom⁺-to-inj (f .hom⁺)) antiinj +``` +
+ +We also remark that $f$ does not contain a `shift⁺`{.Agda} or a +`crush⁻`{.Agda}, then $f$ is an equivalence. + +```agda +no-shift⁺→is-equiv + : ∀ (f⁺ : Δ-Hom⁺ m n) + → ¬ (has-shift⁺ f⁺) + → is-equiv ⟦ f⁺ ⟧ +no-shift⁺→is-equiv done⁺ no-shift .is-eqv i = fabsurd i +no-shift⁺→is-equiv (shift⁺ f⁺) no-shift = absurd (no-shift tt) +no-shift⁺→is-equiv (keep⁺ f⁺) no-shift = fkeep-equiv (no-shift⁺→is-equiv f⁺ no-shift) + +no-crush⁻→is-equiv + : ∀ (f⁻ : Δ-Hom⁻ m n) + → ¬ (has-crush⁻ f⁻) + → is-equiv ⟦ f⁻ ⟧ +no-crush⁻→is-equiv done⁻ no-crush .is-eqv i = fabsurd i +no-crush⁻→is-equiv (crush⁻ f⁻) no-crush = absurd (no-crush tt) +no-crush⁻→is-equiv (keep⁻ f⁻) no-crush = fkeep-equiv (no-crush⁻→is-equiv f⁻ no-crush) + +no-shift+no-crush→is-equiv + : ∀ (f : Δ-Hom m n) + → ¬ (has-shift f) → ¬ (has-crush f) + → is-equiv ⟦ f ⟧ +no-shift+no-crush→is-equiv f no-shift no-crush = + ∙-is-equiv + (no-crush⁻→is-equiv (f .hom⁻) no-crush) + (no-shift⁺→is-equiv (f .hom⁺) no-shift) +``` + +Additionally, antisurjective and antiinjective functions are never +equivalences, so $f$ is an equivalence *if and only if* it does not +contain `shift⁺`{.Agda} or `crush⁻`{.Agda}. + +```agda +is-equiv→no-shift⁺ + : ∀ (f⁺ : Δ-Hom⁺ m n) + → is-equiv ⟦ f⁺ ⟧ + → ¬ (has-shift⁺ f⁺) + +is-equiv→no-crush⁻ + : ∀ (f⁻ : Δ-Hom⁻ m n) + → is-equiv ⟦ f⁻ ⟧ + → ¬ (has-crush⁻ f⁻) + +is-equiv→no-shift + : ∀ (f : Δ-Hom m n) + → is-equiv ⟦ f ⟧ + → ¬ (has-shift f) + +is-equiv→no-crush + : ∀ (f : Δ-Hom m n) + → is-equiv ⟦ f ⟧ + → ¬ (has-crush f) +``` + +
+The proofs all follow from general results about antiinjective +and antisurjective functions, so they are not particularly enlightening. + +```agda +is-equiv→no-shift⁺ f⁺ f-eqv shift = + split-antisurj→not-equiv (has-shift⁺→split-antisurj f⁺ shift) f-eqv + +is-equiv→no-crush⁻ f⁻ f-eqv crush = + split-antiinj→not-equiv (has-crush⁻→split-antiinj f⁻ crush) f-eqv + +is-equiv→no-shift f f-eqv shift = + split-antisurj→not-equiv (has-shift→split-antisurj f shift) f-eqv + +is-equiv→no-crush f f-eqv crush = + split-antiinj→not-equiv (has-crush→split-antiinj f crush) f-eqv +``` +
+ + + +This concludes step 3, so all we need to do is put the pieces together! +We will only show the proof for the augmented simplex category, as the +non-augmented case is identical. + +Invertible simplicial maps are equivalences; so isomorphisms do not contain +any `shift⁺`{.Agda} or `crush⁻`{.Agda} constructors. + +```agda +Δₐ-iso→is-equiv + : ∀ (f : m Δₐ.≅ n) + → is-equiv ⟦ Δₐ.to f ⟧ +Δₐ-iso→is-equiv f = + is-iso→is-equiv $ + iso ⟦ from ⟧ + (λ i → sym (Δ-hom-∘ to from i) ∙ unext invl i ∙ Δ-hom-id i) + (λ i → sym (Δ-hom-∘ from to i) ∙ unext invr i ∙ Δ-hom-id i) + where open Δₐ._≅_ f +``` + + + +We can put steps 1, and 3 together to show that equivalences, and +thus isomorphisms, have images that are the same dimension as +both endpoints. + +```agda +is-equiv→im-stablel + : ∀ (f : Δ-Hom m n) + → is-equiv ⟦ f ⟧ + → m ≡ f .im +is-equiv→im-stablel f eqv = + no-crush⁻→dim-stable (f .hom⁻) $ + is-equiv→no-crush f eqv + +is-equiv→im-stabler + : ∀ (f : Δ-Hom m n) + → is-equiv ⟦ f ⟧ + → f .im ≡ n +is-equiv→im-stabler f eqv = + no-shift⁺→dim-stable (f .hom⁺) $ + is-equiv→no-shift f eqv +``` + +If we combine with with step 2, then we can show that every automorphism +is trivial. + +```agda +Δₐ-auto-id + : ∀ (f : n Δₐ.≅ n) + → f ≡ Δₐ.id-iso +Δₐ-auto-id f = + Δₐ.≅-path $ + Δ-Hom-path + (is-equiv→im-stabler f.to (Δₐ-iso→is-equiv f)) + (Δ-endo⁺-idp (f.to .hom⁺)) + (Δ-endo⁻-idp (f.to .hom⁻)) + where module f = Δₐ._≅_ f +``` + + + +Finally, equivalences (and thus isomorphisms) must preserve dimension: +this gives us a way of turning isomorphisms into paths. + +```agda +is-equiv→dim-stable + : ∀ (f : Δ-Hom m n) + → is-equiv ⟦ f ⟧ + → m ≡ n +is-equiv→dim-stable f eqv = + no-shift+no-crush→dim-stable f + (is-equiv→no-shift f eqv) + (is-equiv→no-crush f eqv) +``` + +And just like that, the proof is done! + +```agda +Δₐ-is-category : is-category Δₐ +Δₐ-is-category = + set-identity-system-K + (λ _ → Δₐ-auto-id) + (λ f → is-equiv→dim-stable (Δₐ.to f) (Δₐ-iso→is-equiv f)) +``` + + + + +Moreover, the all of the variations of the simplex are all strict, and thus +gaunt. + +```agda +Δₐ-is-gaunt : is-gaunt Δₐ +Δₐ⁺-is-gaunt : is-gaunt Δₐ⁺ +Δₐ⁻-is-gaunt : is-gaunt Δₐ⁻ + +Δ-is-gaunt : is-gaunt Δ +Δ⁺-is-gaunt : is-gaunt Δ⁺ +Δ⁻-is-gaunt : is-gaunt Δ⁻ +``` + +
+The proofs are just packaging up results we have already shown, +so they aren't very interesting. + +```agda +Δₐ-is-gaunt .is-gaunt.has-category = Δₐ-is-category +Δₐ-is-gaunt .is-gaunt.has-strict = hlevel 2 + +Δₐ⁺-is-gaunt .is-gaunt.has-category = Δₐ⁺-is-category +Δₐ⁺-is-gaunt .is-gaunt.has-strict = hlevel 2 + +Δₐ⁻-is-gaunt .is-gaunt.has-category = Δₐ⁻-is-category +Δₐ⁻-is-gaunt .is-gaunt.has-strict = hlevel 2 + +Δ-is-gaunt .is-gaunt.has-category = Δ-is-category +Δ-is-gaunt .is-gaunt.has-strict = hlevel 2 + +Δ⁺-is-gaunt .is-gaunt.has-category = Δ⁺-is-category +Δ⁺-is-gaunt .is-gaunt.has-strict = hlevel 2 + +Δ⁻-is-gaunt .is-gaunt.has-category = Δ⁻-is-category +Δ⁻-is-gaunt .is-gaunt.has-strict = hlevel 2 +``` +
+ + ## Categorical structure Now that we actually have categories, we can start to construct some @@ -929,10 +1574,10 @@ yield functions `Fin 0 → Fin n`, which are extremely easy to prove unique. ```agda ¡⁺-unique : (f : Δ-Hom⁺ 0 n) → f ≡ ¡⁺ -¡⁺-unique f = Δ-hom⁺-inj f ¡⁺ (λ i → fabsurd i) +¡⁺-unique f = ext λ i → fabsurd i ¡Δ-unique : (f : Δ-Hom 0 n) → f ≡ ¡Δ -¡Δ-unique f = Δ-hom-inj f ¡Δ (λ i → fabsurd i) +¡Δ-unique f = ext λ i → fabsurd i ``` -```agda --- FIXME: Rename these -¡⁺-strict : ¬ (Δ-Hom⁺ (suc n) 0) -¡⁺-strict () - -!⁻-strict : ¬ (Δ-Hom⁻ 0 (suc n)) -!⁻-strict () -``` - - Likewise, $1$ is a terminal object in the (demi) simplex category. ```agda @@ -988,10 +1623,10 @@ unique. ```agda !⁻-unique : (f : Δ-Hom⁻ (suc n) 1) → f ≡ !⁻ -!⁻-unique f = Δ-hom⁻-inj f !⁻ λ i → Finite-one-is-prop (⟦ f ⟧ i) (⟦ !⁻ ⟧ i) +!⁻-unique f = ext λ i → Finite-one-is-prop (⟦ f ⟧ i) (⟦ !⁻ ⟧ i) !Δ-unique : (f : Δ-Hom (suc n) 1) → f ≡ !Δ -!Δ-unique f = Δ-hom-inj f !Δ λ i → Finite-one-is-prop (⟦ f ⟧ i) (⟦ !Δ ⟧ i) +!Δ-unique f = ext λ i → Finite-one-is-prop (⟦ f ⟧ i) (⟦ !Δ ⟧ i) !Δₐ-unique : (f : Δ-Hom n 1) → f ≡ !Δₐ !Δₐ-unique {n = zero} = ¡Δ-unique @@ -1017,91 +1652,6 @@ unique. ``` --> -## Isomorphisms - -```agda -Δₐ⁺-iso-is-prop : is-prop (m Δₐ⁺.≅ n) -Δₐ⁺-iso-is-prop {m = m} f g = {!!} - where - module f = Δₐ⁺._≅_ f - module g = Δₐ⁺._≅_ g - open Order.Reasoning Nat-poset - - cool : ∀ (i : Fin m) → ⟦ f.to ⟧ i Fin.≤ ⟦ g.to ⟧ i - cool i = - to-nat (⟦ f.to ⟧ i) ≤⟨ {!!} ⟩ - to-nat (⟦ f.to ⟧ (⟦ f.from ⟧ (⟦ g.to ⟧ i))) =⟨ ap to-nat {!!} ⟩ - to-nat (⟦ g.to ⟧ i) ≤∎ -``` - - -## Dimension - -If $f : [m] \to [n]$ is a semisimplicial map, then $m \leq n$. Conversely, -if $f$ is a demisimplicial map then $m \geq n$. The slogan here is that -semisimplicial maps increase dimension, and demisimplicial maps lower it. - -```agda -Δ-dim⁺-≤ : ∀ {m n} → (f : Δ-Hom⁺ m n) → m Nat.≤ n -Δ-dim⁺-≤ done⁺ = Nat.0≤x -Δ-dim⁺-≤ (shift⁺ f) = Nat.≤-sucr (Δ-dim⁺-≤ f) -Δ-dim⁺-≤ (keep⁺ f) = Nat.s≤s (Δ-dim⁺-≤ f) - -Δ-dim⁻-≤ : ∀ {m n} → (f : Δ-Hom⁻ m n) → n Nat.≤ m -Δ-dim⁻-≤ done⁻ = Nat.0≤x -Δ-dim⁻-≤ (crush⁻ f) = Nat.≤-sucr (Δ-dim⁻-≤ f) -Δ-dim⁻-≤ (keep⁻ f) = Nat.s≤s (Δ-dim⁻-≤ f) -``` - -Moreover, if a semi/demisimplicial map contains a face/degeneracy, -then we know it must *strictly* increase/decrease the dimension. - -```agda -has-face⁺ : ∀ {m n} → Δ-Hom⁺ m n → Type -has-face⁺ done⁺ = ⊥ -has-face⁺ (shift⁺ f) = ⊤ -has-face⁺ (keep⁺ f) = has-face⁺ f - -has-degeneracy⁻ : ∀ {m n} → Δ-Hom⁻ m n → Type -has-degeneracy⁻ done⁻ = ⊥ -has-degeneracy⁻ (crush⁻ f) = ⊤ -has-degeneracy⁻ (keep⁻ f) = has-degeneracy⁻ f - - -Δ-dim⁺-< : ∀ {m n} → (f : Δ-Hom⁺ m n) → has-face⁺ f → m Nat.< n -Δ-dim⁺-< (shift⁺ f) p = Nat.s≤s (Δ-dim⁺-≤ f) -Δ-dim⁺-< (keep⁺ f) p = Nat.s≤s (Δ-dim⁺-< f p) - -Δ-dim⁻-< : ∀ {m n} → (f : Δ-Hom⁻ m n) → has-degeneracy⁻ f → n Nat.< m -Δ-dim⁻-< (crush⁻ f) p = Nat.s≤s (Δ-dim⁻-≤ f) -Δ-dim⁻-< (keep⁻ f) p = Nat.s≤s (Δ-dim⁻-< f p) -``` - -```agda -is-id⁺ : ∀ {m n} → Δ-Hom⁺ m n → Type -is-id⁺ done⁺ = ⊤ -is-id⁺ (shift⁺ f) = ⊥ -is-id⁺ (keep⁺ f) = is-id⁺ f - -is-id⁻ : ∀ {m n} → Δ-Hom⁻ m n → Type -is-id⁻ done⁻ = ⊤ -is-id⁻ (crush⁻ f) = ⊥ -is-id⁻ (keep⁻ f) = is-id⁻ f -``` - -Note that these dimension raising/lowering properties immediately imply -that the (augmented) demi/semi simplex categories are categories. - -```agda -Δₐ⁺-is-category : is-category Δₐ⁺ -Δₐ⁺-is-category = set-identity-system (λ _ _ → Δₐ⁺-iso-is-prop) λ f → - Nat.≤-antisym (Δ-dim⁺-≤ (Δₐ⁺.to f)) (Δ-dim⁺-≤ (Δₐ⁺.from f)) - -Δₐ⁺-is-gaunt : is-gaunt Δₐ⁺ -Δₐ⁺-is-gaunt .is-gaunt.has-category = Δₐ⁺-is-category -Δₐ⁺-is-gaunt .is-gaunt.has-strict = Nat.Nat-is-set -``` - ## Decidable equality diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md index 1eb447db0..b30831eed 100644 --- a/src/Cat/Instances/Simplex.lagda.md +++ b/src/Cat/Instances/Simplex.lagda.md @@ -4,30 +4,28 @@ description: | --- diff --git a/src/Data/Fin/Properties.lagda.md b/src/Data/Fin/Properties.lagda.md index aff176447..7c7282780 100644 --- a/src/Data/Fin/Properties.lagda.md +++ b/src/Data/Fin/Properties.lagda.md @@ -1,9 +1,8 @@ These normal forms are relatively straightforward to encode in Agda: -descending chains of face maps can be defined via an indexed inductive, -where `shift⁺`{.Agda} postcomposes the nth face map, and `keep⁺`{.Agda} keeps -the value of 'n' fixed. We call these maps **semisimplicial**, and the -resulting category will be denoted $\Delta^{+}$ +ascending chains of face maps can be defined via an indexed inductive, +where `shift⁺`{.Agda} postcomposes the 0th face map, and `keep⁺`{.Agda} +shifts up the index of every face map by 1. We call these maps **semisimplicial**, +and the resulting category will be denoted $\Delta_{a}^{+}$ ```agda data Δ-Hom⁺ : Nat → Nat → Type where @@ -97,10 +101,17 @@ data Δ-Hom⁺ : Nat → Nat → Type where keep⁺ : ∀ {m n} → Δ-Hom⁺ m n → Δ-Hom⁺ (suc m) (suc n) ``` +For instance, the map $\delta_{0} \circ \delta_{2} : [2] \to [4]$ +would be written as `shift⁺ (keep⁺ (keep⁺ (shift⁺ done⁺)))`{.Agda}: the +first `shift⁺`{.Agda} denotes the postcomposition of the 0th face maps, +and the 2 `keep⁺`{.Agda} constructors bump up the index of the next +face map by 2. This means that the final `shift⁺`{.Agda} denotes the 4th +face map! + Descending chains of degeneracies are defined in a similar fashion, where -where `crush⁻`{.Agda} precomposes the nth degeneracy map. We will call +where `crush⁻`{.Agda} precomposes the 0th degeneracy map. We will call these maps **demisimplicial**, and the category they form will be denoted -$\Delta^{-}.$ +$\Delta_{a}^{-}$. ```agda data Δ-Hom⁻ : Nat → Nat → Type where @@ -109,9 +120,17 @@ data Δ-Hom⁻ : Nat → Nat → Type where keep⁻ : ∀ {m n} → Δ-Hom⁻ m n → Δ-Hom⁻ (suc m) (suc n) ``` -Morphisms in $\Delta$ consist of a pair of composable semi and demisimplicial -maps. Note that we allow both `m` and `n` to be 0; this allows us to share -code between the simplex and augmented simplex category. +As an example, the map $\sigma_{2} \circ \sigma_{0} : [5] \to [3]$ would +be written as `crush⁻ (keep⁻ (keep⁻ (crush⁻ (keep⁻ done⁻))))`{.Agda}. Here, +the outermost `crush⁻` constructor denotes the precomposition by $\sigma_{0}$. +Next, the two `keep⁻`{.Agda} constructors bump the index of the next face +map we encounter up by 2, so the final `crush⁻` constructor denotes the +2nd degeneracy map. + +Finally, a **simplicial map** consist of an ascending chain of face maps +and a descending chain of degeneracies that factor through the same object. +We will refer to this object as the *image* of the map. These maps will form +the **augmented simplicial category**, which is denoted via $\Delta_{a}$. ```agda record Δ-Hom (m n : Nat) : Type where @@ -125,6 +144,14 @@ record Δ-Hom (m n : Nat) : Type where open Δ-Hom ``` +Note that we allow $m$ and $n$ to be 0 for all of our classes of maps; +this is useful for algebraic applications, as $0$ plays the role of the +empty context. However, $0$ can be problematic for homotopical applications, +so it is useful to consider categories of simplicial maps between non-zero +naturals. This category is known as the **simplex category**, and is denoted +by $\Delta$. Moreover, there are also non-augmented versions of semi and +demisimplex categories, which are denoted by $\Delta^{+}$ and $\Delta^{-}$, resp. + -We will denote each of these interpretations with `⟦ f ⟧ i` to avoid +We will denote each of these interpretations as `⟦ f ⟧ i` to avoid too much syntactic overhead. + -Note that semisimplicial maps always encode inflationary functions. +Now that we have our interpretations, we can start to charaterize their +behaviour. First, note that semisimplicial maps always encode inflationary +functions. ```agda Δ-hom⁺-incr @@ -611,7 +645,7 @@ Semisimplicial maps are not just monotonic; they are *strictly* monotonic! Nat.s≤s (Δ-hom⁺-pres-< f⁺ (Nat.≤-peel i -These follow by some more brutal inductions that we will -shield the innocent reader from. +These follow by some more brutal inductions. ```agda @@ -773,7 +805,7 @@ directly from these lemmas. (Δ-hom-uniquep⁻ (f .hom⁺) (g .hom⁺) (f .hom⁻) (g .hom⁻) p) ``` -Injectivity the interpretaion of semi and demisimplicial maps follow +Injectivity the interpretation of semi and demisimplicial maps follow neatly as corollaries. ```agda