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/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/Antiinjection.lagda.md b/src/1Lab/Function/Antiinjection.lagda.md new file mode 100644 index 000000000..f92ad9ef1 --- /dev/null +++ b/src/1Lab/Function/Antiinjection.lagda.md @@ -0,0 +1,191 @@ +--- +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₁) +``` + +```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 new file mode 100644 index 000000000..89c2e944e --- /dev/null +++ b/src/1Lab/Function/Antisurjection.lagda.md @@ -0,0 +1,145 @@ +--- +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) +``` + +```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) +``` diff --git a/src/1Lab/Function/Embedding.lagda.md b/src/1Lab/Function/Embedding.lagda.md index a7a19a19d..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)) +``` diff --git a/src/1Lab/Function/Surjection.lagda.md b/src/1Lab/Function/Surjection.lagda.md index abf1aa928..06f8c68dc 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,17 @@ 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|axiom-of-choice]]. + + +```agda +split-surjective : (A → B) → Type _ +split-surjective f = ∀ b → fibre f b +``` 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) ``` + + 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/Functor/Concrete.lagda.md b/src/Cat/Functor/Concrete.lagda.md new file mode 100644 index 000000000..e2999e712 --- /dev/null +++ b/src/Cat/Functor/Concrete.lagda.md @@ -0,0 +1,194 @@ +--- +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 +``` +
diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md index 7456e99bf..049ad7811 100644 --- a/src/Cat/Instances/Simplex.lagda.md +++ b/src/Cat/Instances/Simplex.lagda.md @@ -1,10 +1,31 @@ +--- +description: | + The simplex category. +--- @@ -15,55 +36,2065 @@ module Cat.Instances.Simplex where -# The simplex 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. 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. +of non-empty finite ordinals and order-preserving maps. Though +conceptually simple, this definition is difficult to work with, as +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$ + +Face maps $\delta^{n}_{i}$ are meant to be interpreted as injections that skip +the $i$th element of $[n + 1]$, and degeneracies as 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 +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 construct a simplicial diagram. +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$. In simpler +terms, every map can be uniquely factored as a composite of a strictly +increasing sequence of face maps, followed by a decreasing sequence of +degeneracies. + + + +These normal forms are relatively straightforward to encode in Agda: +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 + 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) +``` + +For instance, the map $\delta_{0} \circ \delta_{2} : [2] \to [4]$ +would be written as: + +```agda +private + δ₀∘δ₂ : Δ-Hom⁺ 2 4 + δ₀∘δ₂ = shift⁺ (keep⁺ (keep⁺ (shift⁺ done⁺))) +``` + +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 0th degeneracy map. We will call +these maps **demisimplicial**, and the category they form will be denoted +$\Delta_{a}^{-}$. + +```agda +data Δ-Hom⁻ : Nat → Nat → Type where + done⁻ : Δ-Hom⁻ 0 0 + crush⁻ : ∀ {m n} → Δ-Hom⁻ (suc m) n → Δ-Hom⁻ (suc (suc m)) n + keep⁻ : ∀ {m n} → Δ-Hom⁻ m n → Δ-Hom⁻ (suc m) (suc n) +``` + +As an example, the map $\sigma_{2} \circ \sigma_{0} : [5] \to [3]$ would +be written as: + +```agda +private + σ₂∘σ₀ : Δ-Hom⁻ 5 3 + σ₂∘σ₀ = crush⁻ (keep⁻ (keep⁻ (crush⁻ (keep⁻ done⁻)))) +``` + +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 Δ-map (n m : Nat) : Type where +record Δ-Hom (m n : Nat) : Type where + no-eta-equality + constructor Δ-factor field - map : Fin (suc n) → Fin (suc m) - ascending : (x y : Fin (suc n)) → x ≤ y → map x ≤ map y + {im} : Nat + hom⁺ : Δ-Hom⁺ im n + hom⁻ : Δ-Hom⁻ m im + +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. + + +## Identities and composites + +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 -Δ : Precategory lzero lzero -Δ .Ob = Nat -Δ .Hom n m = Δ-map n m -Δ .Hom-set _ _ = hlevel 2 +id⁺ : ∀ {n} → Δ-Hom⁺ n n +id⁺ {zero} = done⁺ +id⁺ {suc n} = keep⁺ id⁺ + +id⁻ : ∀ {n} → Δ-Hom⁻ n n +id⁻ {zero} = done⁻ +id⁻ {suc n} = keep⁻ id⁻ +``` + +Identity morphisms in $\Delta$ factorize as the identities in $\Delta^{+}$ +and $\Delta^{-}$. + +```agda +idΔ : Δ-Hom n n +idΔ .im = _ +idΔ .hom⁺ = id⁺ +idΔ .hom⁻ = id⁻ +``` + +Composing semisimplicial maps is somewhat tricky, as we need to preserve +the invariant that they form an ascending chain of face maps. To ensure +this, we will need to judiciously apply the simplicial identities to +commute face maps past one another. + +```agda +_∘⁺_ : Δ-Hom⁺ n o → Δ-Hom⁺ m n → Δ-Hom⁺ m o +``` + +First, the base case: composing a semisimplicial map $f$ with the identity +map $[0] \to [0]$ should clearly yield $f$. + +```agda +f ∘⁺ done⁺ = f +``` + +Next, the composite $(\delta_0 \circ f) \circ (\delta_0 \circ g)$ +can be written in normal form by reassociating as +$$ +\delta_0 \circ (f \circ (\delta_0 \circ g)) +$$ +and then recursively normalizing the right-hand side. + +```agda +shift⁺ f ∘⁺ shift⁺ g = shift⁺ (f ∘⁺ shift⁺ g) +``` + +Now for the tricky case: consider the composite $\uparrow f \circ (\delta_0 \circ g)$, +where $\uparrow f$ shifts the index of every face map in $f$ by 1. +This means that we can repeatedly apply the 1st simplicial identity to +commute $\delta_{0}$ past every single face map in $f$ by lowering their +indices by one. This yields the following equality +$$ +\uparrow f \circ (\delta_0 \circ g) = \delta_0 \circ (f \circ g) +$$ +and the right-hand side can be placed into normal form by normalizing +$f \circ g$. + +```agda +keep⁺ f ∘⁺ shift⁺ g = shift⁺ (f ∘⁺ g) +``` + +Luckily, the dual case is much easier: the composite $(\delta_0 \circ f) \circ \uparrow g$ +can directly be reassociated as +$$ +\delta_0 \circ (f \circ \uparrow g) +$$ +We can then recursively normalize the right hand side to obtain a normal form. + +```agda +shift⁺ f ∘⁺ keep⁺ g = shift⁺ (f ∘⁺ keep⁺ g) +``` + +Finally, $\uparrow f \circ \uparrow g = \uparrow (f \circ g)$. + +```agda +keep⁺ f ∘⁺ keep⁺ g = keep⁺ (f ∘⁺ g) +``` + +Composing demisimplicial maps follows a similar process, though it is +slightly trickier. + +```agda +_∘⁻_ : Δ-Hom⁻ n o → Δ-Hom⁻ m n → Δ-Hom⁻ m o +``` + +As before, precomposing $g$ with the identity map $[0] \to [0]$ just yields $g$. + +```agda +done⁻ ∘⁻ g = g +``` + +Next, $(f \circ \sigma_0) \circ (g \circ \sigma_0)$ can be written +in our normal form by reassociating it as +$$ +(f \circ \sigma_0) \circ g) \circ \sigma_0 +$$ +and then recursively normalizing the left-hand side. + +```agda +crush⁻ f ∘⁻ crush⁻ g = crush⁻ (crush⁻ f ∘⁻ g) +``` + +Our first tricky case is when we encounter a composite of the form +$(f \circ \sigma_0) \circ (\uparrow g \circ \sigma_1)$. Every degeneracy +in $\uparrow g$ must have an index of at least $1$, so we can apply +the 2nd simplicial identity to commute the 0th face map past them +by lowering all indices by 1. This yields the following equation +$$ +(f \circ \sigma_0) \circ (\uparrow g \circ \sigma_1) = (f \circ g) \circ \sigma_0 \circ \sigma_0 +$$ +If we recursively normalize $f \circ g$, then the RHS of this equation will +be in normal form! + +```agda +crush⁻ f ∘⁻ keep⁻ (crush⁻ g) = crush⁻ (crush⁻ (f ∘⁻ g)) +``` + +The next tricky case is when we encounter a composite of the form +$(f \circ \sigma_0) \circ (\uparrow \uparrow g)$. We can use a similar +line of reasoning as the previous case to commute $\sigma_0$ past $\uparrow \uparrow g$ +by decrementing all indices by one, yielding the following equation: +$$ +(f \circ \sigma_0) \circ (\uparrow \uparrow g) = (f \circ \uparrow g) \circ \sigma_0 +$$ + +We will take this equation as definitional, and then proceed to recursively +normalize the left-hand side. + +```agda +crush⁻ f ∘⁻ keep⁻ (keep⁻ g) = crush⁻ (f ∘⁻ (keep⁻ g)) +``` + +Mercifully, the final 2 cases are easy. For the first, note that +composites of the form $\uparrow f \circ (g \circ \sigma_0)$ can +be placed into normal form by reassociating and recursively normalizing. +The second case is even easier, as we can rewrite $\uparrow f \circ \uparrow g$ +into $\uparrow (f \circ g)$. + +```agda +keep⁻ f ∘⁻ crush⁻ g = crush⁻ (keep⁻ f ∘⁻ g) +keep⁻ f ∘⁻ keep⁻ g = keep⁻ (f ∘⁻ g) +``` + +Composites of simplicial maps are even more tricky, as we +need to somehow normalize 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 that we need to factor the composite of $f^{-} \circ g^{+}$ +$h^{+} \circ h^{-}$, where $h^{+}$ is semisimplicial and $h^{-}$ is +demisimplicial. Once this is done, we can obtain our final factorization +by pre and post-composing with $g^{-}$ and $f^{+}$, resp. + +For pedagogic purposes, we will define the image and semi/demisimplicial +components of our factorization simultaneously. + +```agda +interleaved mutual + imΔ : Δ-Hom⁻ n o → Δ-Hom⁺ m n → Nat + _∘Δ⁺_ : (f⁻ : Δ-Hom⁻ n o) → (f⁺ : Δ-Hom⁺ m n) → Δ-Hom⁺ (imΔ f⁻ f⁺) o + _∘Δ⁻_ : (f⁻ : Δ-Hom⁻ n o) → (f⁺ : Δ-Hom⁺ m n) → Δ-Hom⁻ m (imΔ f⁻ f⁺) +``` + +If both maps are the identity $[0] \to [0]$, then we can clearly factor +them as identity maps. + +```agda + imΔ done⁻ done⁺ = 0 + done⁻ ∘Δ⁺ done⁺ = done⁺ + done⁻ ∘Δ⁻ done⁺ = done⁻ +``` + +Next, a composite of the form $(f^{-} \circ \sigma_0) \circ (\delta_0 \circ g^{+})$ +is equal to $f^{-} \circ g^{+}$ by the 4th simplicial identity. + +```agda + imΔ (crush⁻ f⁻) (shift⁺ g⁺) = imΔ f⁻ g⁺ + (crush⁻ f⁻) ∘Δ⁺ (shift⁺ g⁺) = f⁻ ∘Δ⁺ g⁺ + (crush⁻ f⁻) ∘Δ⁻ (shift⁺ g⁺) = f⁻ ∘Δ⁻ g⁺ +``` + +We can also apply the 4th simplicial identity to composites of the form +$(f^{-} \circ \sigma_0) \circ (\delta_1 \circ \uparrow g^{+})$. + + +```agda + imΔ (crush⁻ f⁻) (keep⁺ (shift⁺ g⁺)) = imΔ f⁻ (keep⁺ g⁺) + (crush⁻ f⁻) ∘Δ⁺ (keep⁺ (shift⁺ g⁺)) = f⁻ ∘Δ⁺ (keep⁺ g⁺) + (crush⁻ f⁻) ∘Δ⁻ (keep⁺ (shift⁺ g⁺)) = f⁻ ∘Δ⁻ (keep⁺ g⁺) +``` + +The 5th simplicial identity can be applied to composites of the form +$(f^{-} \circ \sigma_0) \circ (\uparrow \uparrow g^{+})$, which allows +us to commute the $\sigma_0$ past $\uparrow \uparrow g^{+}$ by decrementing +the index of every face map in $\uparrow \uparrow g^{+}$. + +```agda + imΔ (crush⁻ f⁻) (keep⁺ (keep⁺ g⁺)) = imΔ f⁻ (keep⁺ g⁺) + (crush⁻ f⁻) ∘Δ⁺ (keep⁺ (keep⁺ g⁺)) = f⁻ ∘Δ⁺ (keep⁺ g⁺) + (crush⁻ f⁻) ∘Δ⁻ (keep⁺ (keep⁺ g⁺)) = crush⁻ (f⁻ ∘Δ⁻ (keep⁺ g⁺)) +``` + +Likewise, the 3rd simplicial identity can be applied to composites +of the form $(\uparrow f^{-}) \circ (\delta_0 \circ g^{+})$. This +Like the other laws, this lets us commute $\delta_0$ past $\uparrow f^{-}$ +by decrementing the index of every face map. + +```agda + imΔ (keep⁻ f) (shift⁺ g⁺) = imΔ f g⁺ + (keep⁻ f⁻) ∘Δ⁺ (shift⁺ g⁺) = shift⁺ (f⁻ ∘Δ⁺ g⁺) + (keep⁻ f⁻) ∘Δ⁻ (shift⁺ g⁺) = f⁻ ∘Δ⁻ g⁺ +``` + +Finally, we can reduce $\uparrow f^{-} \circ \uparrow g{+}$ to $\uparrow (f^{-} \circ g^{+})$. + +```agda + imΔ (keep⁻ f) (keep⁺ g) = suc (imΔ f g) + _∘Δ⁺_ (keep⁻ f⁻) (keep⁺ f⁺) = keep⁺ (f⁻ ∘Δ⁺ f⁺) + _∘Δ⁻_ (keep⁻ f⁻) (keep⁺ f⁺) = keep⁻ (f⁻ ∘Δ⁻ f⁺) +``` + +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 +(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⁻ +``` + +## 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`. This interpretation is +has 2 key properties: + +1. The interpretation is functorial: both $\llbracket id \rrbracket = id$, + and $\llbracket f \circ g \rrbracket = \llbracket f \rrbracket \circ \llbracket g \rrbracket$. +2. The interpretation is injective: if $\llbracket f \rrbracket = \llbracket g \rrbracket$, then $f = g$. + +Together, this ensures that our interpretations form a series [[faithful functors]], +which allows us to lift equations from functions back to equations on their +syntactic presentations. In particular, composition of functions is associative +and unital, so constructing these interpretations 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 as `⟦ f ⟧ i` to avoid +too much syntactic overhead. + + + +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 + : ∀ (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) +``` + +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) +``` + +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) +``` + +Moreover, semisimplicial maps always encode injective functions, and +demisimplicial maps encode *split* surjections. + +```agda +Δ-hom⁺-to-inj + : ∀ {m n} + → (f : Δ-Hom⁺ m n) + → injective ⟦ f ⟧ + +Δ-hom⁻-to-split-surj + : ∀ {m n} + → (f : Δ-Hom⁻ m n) + → split-surjective ⟦ f ⟧ +``` + +
+These both follow directly via induction, so we omit the proofs. + + +```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) +``` +
+ + + +We also remark that semi and demisimplicial maps always encode monotonic functions. + +```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)) +``` -Δ .id .map x = x -Δ .id .ascending x y p = p +This in turn implies that simplicial maps also encode monotonic functions. + +```agda +Δ-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) +``` + +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 +Δ-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)) +``` + + +We also need to show that if a pair of factorizations is semantically +equal, then the semi and demisimplicial components are syntactically equal. + +```agda +Δ-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⁻ +``` + +
+These follow by some more brutal inductions. + + +```agda +Δ-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)) +Δ-hom-unique⁻ (keep⁺ f⁺) (keep⁺ g⁺) (keep⁻ f⁻) (keep⁻ g⁻) p = + ap keep⁻ (Δ-hom-unique⁻ f⁺ g⁺ f⁻ g⁻ (fsuc-inj ⊙ p ⊙ fsuc)) +``` +
+ + + +Injectivity of the interpretation of simplicial maps follows +directly from these lemmas. + +```agda +Δ-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 interpretation 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) +``` + + + +### 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) → ⟦ f ∘⁺ g ⟧ i ≡ ⟦ f ⟧ (⟦ g ⟧ i) +Δ-hom⁻-∘ + : (f : Δ-Hom⁻ n o) (g : Δ-Hom⁻ m n) + → ∀ (i : Fin m) → ⟦ f ∘⁻ g ⟧ i ≡ ⟦ f ⟧ (⟦ g ⟧ i) +``` + +
+The proofs are not particularly difficult; they both +consist of some (rather large) case bashes. + + +```agda +Δ-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) +``` +
+ +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. + +```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 +Δ-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) +``` +
+ +Luckily, that was our last big induction, and we can get our final functoriality +lemma by piecing together previous results! + +```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 2 +Δₐ⁺-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 2 +Δₐ⁻-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 2 +Δₐ-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 2 +Δ⁺-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 2 +Δ⁻-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 2 +Δ-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 Δ +``` + +## 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 +interesting maps. We begin by constructing more familiar versions of +face and degeneracy map that are parameterized by some $i$. + +```agda +δ⁺ : 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) +``` + +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 +¡Δ .im = 0 +¡Δ .hom⁺ = ¡⁺ +¡Δ .hom⁻ = done⁻ +``` + +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 = ext λ i → fabsurd i + +¡Δ-unique : (f : Δ-Hom 0 n) → f ≡ ¡Δ +¡Δ-unique f = ext λ i → fabsurd i +``` + + + +Likewise, $1$ is a terminal object in the (demi) simplex category. + +```agda +!⁻ : Δ-Hom⁻ (suc n) 1 +!⁻ {n = zero} = id⁻ +!⁻ {n = suc n} = crush⁻ !⁻ + +!Δ : Δ-Hom (suc n) 1 +!Δ .im = 1 +!Δ .hom⁺ = id⁺ +!Δ .hom⁻ = !⁻ +``` + +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 +!Δₐ : Δ-Hom n 1 +!Δₐ {n = zero} = ¡Δ +!Δₐ {n = suc n} = !Δ +``` + +We can use the same semantic strategy to prove that these maps are +unique. + +```agda +!⁻-unique : (f : Δ-Hom⁻ (suc n) 1) → f ≡ !⁻ +!⁻-unique f = ext λ i → Finite-one-is-prop (⟦ f ⟧ i) (⟦ !⁻ ⟧ i) + +!Δ-unique : (f : Δ-Hom (suc n) 1) → f ≡ !Δ +!Δ-unique f = ext λ i → Finite-one-is-prop (⟦ f ⟧ i) (⟦ !Δ ⟧ i) + +!Δₐ-unique : (f : Δ-Hom n 1) → f ≡ !Δₐ +!Δₐ-unique {n = zero} = ¡Δ-unique +!Δₐ-unique {n = suc n} = !Δ-unique +``` + + + +## Decidable equality + + + +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 .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) +``` +
+ +Equality is not the only thing we can decide: recall that +a map $f$ is an equivalence if and only if it does not contain +any `shift⁺`{.Agda} or `crush⁻`{.Agda} constructors. The latter is +a purely syntactic condition, which makes it easily decidable! + +```agda +has-shift?⁺ + : ∀ (f⁺ : Δ-Hom⁺ m n) + → Dec (has-shift⁺ f⁺) +has-shift?⁺ done⁺ = no λ ff → ff +has-shift?⁺ (shift⁺ f⁺) = yes tt +has-shift?⁺ (keep⁺ f⁺) = has-shift?⁺ f⁺ + +has-crush?⁻ + : ∀ (f⁻ : Δ-Hom⁻ m n) + → Dec (has-crush⁻ f⁻) +has-crush?⁻ done⁻ = no λ ff → ff +has-crush?⁻ (crush⁻ f⁻) = yes tt +has-crush?⁻ (keep⁻ f⁻) = has-crush?⁻ f⁻ +``` + +This gives us an efficient way to check if a (semi/demi) simplicial +map is an equivalence. + +```agda +Δ-hom⁺-equiv? + : ∀ (f⁺ : Δ-Hom⁺ m n) + → Dec (is-equiv ⟦ f⁺ ⟧) + +Δ-hom⁻-equiv? + : ∀ (f⁻ : Δ-Hom⁻ m n) + → Dec (is-equiv ⟦ f⁻ ⟧) + +Δ-hom-equiv? + : ∀ (f : Δ-Hom m n) + → Dec (is-equiv ⟦ f ⟧) +``` + +
+The actual decidability proofs are just stitching together +previous results, and are not particularly interesting. + +```agda +Δ-hom⁺-equiv? f⁺ = + Dec-map + (no-shift⁺→is-equiv f⁺) + (is-equiv→no-shift⁺ f⁺) + (not? (has-shift?⁺ f⁺)) -Δ ._∘_ f g .map x = f .map (g .map x) -Δ ._∘_ f g .ascending x y p = f .ascending _ _ (g .ascending _ _ p) +Δ-hom⁻-equiv? f⁻ = + Dec-map + (no-crush⁻→is-equiv f⁻) + (is-equiv→no-crush⁻ f⁻) + (not? (has-crush?⁻ f⁻)) -Δ .idr f = Δ-map-path λ x → refl -Δ .idl f = Δ-map-path λ x → refl -Δ .assoc f g h = Δ-map-path λ x → refl +Δ-hom-equiv? f = + Dec-map + (rec! (no-shift+no-crush→is-equiv f)) + (is-equiv→no-shift+no-crush f) + (Dec-× ⦃ not? (has-shift?⁺ (f .hom⁺)) ⦄ ⦃ not? (has-crush?⁻ (f .hom⁻)) ⦄) ``` +
diff --git a/src/Cat/Morphism/Factorisation.lagda.md b/src/Cat/Morphism/Factorisation.lagda.md index 96ad84c5b..8322024ac 100644 --- a/src/Cat/Morphism/Factorisation.lagda.md +++ b/src/Cat/Morphism/Factorisation.lagda.md @@ -89,12 +89,10 @@ if, and only if, we have $f \ortho g$ for every $f \in E$. @@ -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/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 ``` diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md index d1c24c44b..1db65f062 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,18 @@ 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..7c7282780 100644 --- a/src/Data/Fin/Properties.lagda.md +++ b/src/Data/Fin/Properties.lagda.md @@ -1,5 +1,7 @@ + + + + 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 f47d58b8a..fdafe1c4e 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 @@ -142,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 @@ -227,3 +239,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},