Simple(r?) simplices
This post is a literate Agda file, where I try to define a category Δ of finite ordinals and monotone maps. Reed Mullanix wrote a post "Simple Simplices" around year and half ago about the topic suggesting an option.
That option, called Δ⇒ is implemented in agda-categories package in Categories.Category.Instance.Simplex module.
Reed asks for a decomposition:
decompose : (Fin m → Fin n) → (m Δ⇒ n)I think I got it.
#Agda setup
module 2022-10-08-simplex whereimport Data.Nat as ℕ
open ℕ using (ℕ; zero; suc; z≤n; s≤s; _∸_)
open import Data.Nat.Properties using (≤-refl; ≤-trans)
open import Data.Fin using (Fin; zero; suc; _≤_; _<_; toℕ)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; map)
open import Data.Fin.Properties using (suc-injective; toℕ<n)
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; cong; sym; trans)
open Relation.Binary.PropositionalEquality.≡-Reasoning
variable
n m p : ℕ#Monotone maps
Reed mentions two options for implementing simplex category
- Define Δ as the category of finite ordinals and monotone maps.
- Define Δ as a free category generated by face and degeneracy maps, quotient by the simplicial identities.
Second one is just awful.
I assume the first option goes something like:
First we define the isMonotone predicate on Fin n → Fin m functions.
isMonotone : (Fin n → Fin m) → Set
isMonotone f = ∀ i j → i ≤ j → f i ≤ f jThen a monotone function is a function together with a proof it is monotone
Monotone : ℕ → ℕ → Set
Monotone n m = Σ (Fin n → Fin m) isMonotoneAnd because it's a function in (ordinary) Agda we need to define an equality:
_≐_ : Monotone n m → Monotone n m → Set
(f , _) ≐ (g , _) = ∀ i → f i ≡ g iThe pointwise equality works well, and we don't actually care about isMonotone proof. (Though I think it can be shown that it is hProp. so this is justified).
Reed mentions that this formulation is nice, except that we want to be able to define simplicial sets by how they act on the face and degeneracy maps, not some random monotonic map!
I actually don't know anything about face and boundary maps, but I trust others on that. (E.g. nLab also says that all morphism are generated by face and degeneracy maps)
Reed then proceed to define a third variant, which resembles free category definition, yet he doesn't quotient by simplicial identities, but instead he defines equality using the semantics (i.e. pointwise on a function "applying" his description to finite ordinal).
#Fourth formulation
... but there is fourth (?) option to encode monotone maps.
And it is very simple! (It does resemble thinnings I wrote recently above, more on them below).
data Mono : ℕ → ℕ → Set where
base : Mono zero zero
skip : Mono n m → Mono n (suc m)
edge : Mono n (suc m) → Mono (suc n) (suc m)The base and skip constructors are similar as in thinnings, but edge as different then keep. Where keep always introduced a new "output", edge requires there to be an element and maps new input to that same element.
So if we have a Mono which looks like:
We can add a new edge which goes to already existing output with edge:
It took some time to get this right.
keep as in thinnings can be define as first adding a new output with skip and then connecting an edge there:
pattern keep f = edge (skip f)We can define identity morphism and composition:
id : Mono n n
id {zero} = base
id {suc n} = keep id
-- I'm rebel, using ⨟ for the composition
_⨟_ : Mono n m → Mono m p → Mono n p
base ⨟ g = g
skip f ⨟ skip g = skip (skip f ⨟ g)
skip f ⨟ edge g = f ⨟ g
edge f ⨟ skip g = skip (edge f ⨟ g)
edge f ⨟ edge g = edge (f ⨟ edge g)I leave as an exercise to prove that category laws are satisfied.
Next we can define the semantics, i.e. how Mono maps finite ordinals: The definition is simple, encoding the graphical intuition from above.
apply : Mono n m → Fin n → Fin m
apply (skip f) i = suc (apply f i)
apply (edge f) zero = zero
apply (edge f) (suc i) = apply f iWe can show that apply, id and ⨟ work together as expected.
apply-id : (i : Fin n) → apply id i ≡ i
apply-id zero = refl
apply-id (suc i) = cong suc (apply-id i)
apply-⨟ : (f : Mono n m) (g : Mono m p) (i : Fin n)
→ apply g (apply f i) ≡ apply (f ⨟ g) i
apply-⨟ (skip f) (skip g) i = cong suc (apply-⨟ (skip f) g i)
apply-⨟ (skip f) (edge g) i = apply-⨟ f g i
apply-⨟ (edge f) (skip g) i = cong suc (apply-⨟ (edge f) g i)
apply-⨟ (edge f) (edge g) zero = refl
apply-⨟ (edge f) (edge g) (suc i) = apply-⨟ f (edge g) iMono has a very nice property: it uniquely represents a monotone map In other words, if there are two Mono n m, but for all i : Fin n, they act the same, then f and g are propositionally equal:
apply-inj : (f g : Mono n m) → (∀ i → apply f i ≡ apply g i) → f ≡ g
apply-inj base base p = refl
apply-inj (skip f) (skip g) p =
cong skip (apply-inj f g λ i → suc-injective (p i))
apply-inj (skip f) (edge g) p with p zero
... | ()
apply-inj (edge f) (skip g) p with p zero
... | ()
apply-inj (edge f) (edge g) p = cong edge (apply-inj f g λ i → p (suc i) )As a sanity check, apply f is indeed monotone:
isMonotone-apply : (f : Mono n m) → isMonotone (apply f)
isMonotone-apply (skip f) i j i≤j = s≤s (isMonotone-apply f i j i≤j)
isMonotone-apply (edge f) zero j 0≤j = z≤n
isMonotone-apply (edge f) (suc i) (suc j) (s≤s i≤j) = isMonotone-apply f i j i≤jCombining the previous, we can map from Mono (data) to Monotone (Agda function).
Mono→Monotone : Mono n m → Monotone n m
Mono→Monotone f = apply f , isMonotone-apply f#From Agda function to data
Because the Mono definition is so simple, we should try to convert back. The code in this section can be improved, but for now we only need the final result.
First we define "subtraction" and "addition" of finite ordinals. The ∸ is monus on natural numbers (i.e. safe subtraction, defaulting to zero). In the same vein, lower doesn't require i ≤ j proof.
-- kind of j - i, no i ≤ j requirement, "monus"
lower : (i j : Fin (suc m)) → Fin (suc (m ∸ toℕ i))
lower zero j = j
lower {m = suc m} (suc i) zero = zero -- extra case, here i≤j
lower {m = suc m} (suc i) (suc j) = lower i j
raise : (i : Fin (suc m)) → Fin (suc (m ∸ toℕ i)) → Fin (suc m)
raise zero j = j
raise {m = suc m} (suc i) j = suc (raise i j)We can show that raise and lower cancel out, here we need j ≤ i proof. (I noticed that I'm not consistent with i and j variables, but hopefully you get along).
raise∘lower≡id : (i j : Fin (suc m)) (j≤i : j ≤ i) → i ≡ raise j (lower j i)
raise∘lower≡id i zero j≤i = refl
raise∘lower≡id {m = suc m} (suc i) (suc j) (s≤s j≤i) =
cong suc (raise∘lower≡id i j j≤i)Then we need a handful of lemmas.
lower for fixed k is monotone:
isMonotone-lower : ∀ (k : Fin (suc m)) → isMonotone (lower k)
isMonotone-lower zero i j i≤j = i≤j
isMonotone-lower {m = suc m} (suc k) zero j z≤0 = z≤n -- redundant case
isMonotone-lower {m = suc m} (suc k) (suc i) (suc j) (s≤s i≤j) = isMonotone-lower k i j i≤jWe can raise the Mono, so we can commute raise and apply
raise-mono' : ∀ p → Mono n (suc (m ∸ p)) → Mono n (suc m)
raise-mono' zero f = f
raise-mono' {m = zero} (suc p) f = f
raise-mono' {m = suc m} (suc p) f = skip (raise-mono' p f)
raise-mono : ∀ (k : Fin (suc m)) → Mono n (suc (m ∸ toℕ k)) → Mono n (suc m)
raise-mono k = raise-mono' (toℕ k)Then the idea is to define Monotone to Mono conversion by looking at f zero input, and trimming f using lower.
For the lack of better name I call this new function next:
next-f : (f : Fin (suc n) → Fin (suc m)) → isMonotone f
→ Fin n → Fin (suc (m ∸ toℕ (f zero)))
next-f f f-mono i = lower (f zero) (f (suc i))And next-f f is monotone if f is:
next-mono : (f : Fin (suc n) → Fin (suc m)) (f-mono : isMonotone f)
→ isMonotone (next-f f f-mono)
next-mono f f-mono i j i≤j = isMonotone-lower
(f zero)
(f (suc i))
(f (suc j))
(f-mono (suc i) (suc j) (s≤s i≤j))
next : (f : Monotone (suc n) (suc m))
→ Monotone n (suc (m ∸ toℕ (proj₁ f zero)))
next (f , f-mono) = next-f f f-mono , next-mono f f-monoNow we have (almost) all the ingredients to define Monotone→Mono function:
absurd : Mono zero n
absurd {zero} = base
absurd {suc n} = skip absurd
Monotone→Mono' : (f : Fin n → Fin m) → isMonotone f → Mono n m
Monotone→Mono' {zero} f f-mono = absurd
Monotone→Mono' {suc n} {zero} f f-mono with f zero
... | ()
Monotone→Mono' {suc n} {suc m} f f-mono = raise-mono (f zero)
(edge (Monotone→Mono' (next-f f f-mono) (next-mono f f-mono)))And Monotone→Mono just packages that:
Monotone→Mono : Monotone n m → Mono n m
Monotone→Mono (f , f-mono) = Monotone→Mono' f f-mono#Monotone ↔ Mono isomorphism
Monotone→Mono and Mono→Monotone are each others inverse.
First two lemmas, showing that raise and apply "commute" in a special case we need:
raise-edge-apply-zero : (j : Fin (suc m))
→ (f : Mono n (suc (m ∸ toℕ j)))
→ j ≡ apply (raise-mono j (edge f)) zero
raise-edge-apply-zero zero f = refl
raise-edge-apply-zero {m = suc m} (suc j) f =
cong suc (raise-edge-apply-zero j f)
raise-edge-apply-suc : (j : Fin (suc m))
→ (i : Fin n)
→ (f : Mono n (suc (m ∸ toℕ j)))
→ raise j (apply f i)
≡ apply (raise-mono j (edge f)) (suc i)
raise-edge-apply-suc zero i f = refl
raise-edge-apply-suc {m = suc m} (suc j) i f =
cong suc (raise-edge-apply-suc j i f)Using which we can show that apply ∘ Monotone→Mono is the identity function: (Agda proofs are wide, layout of my blog looks horrible with those, I'm sorry).
apply-Monotone→Mono : (f : Monotone n m)
→ (i : Fin n)
→ proj₁ f i ≡ apply (Monotone→Mono f) i
apply-Monotone→Mono {suc n} {zero} f i with proj₁ f zero
... | ()
apply-Monotone→Mono {suc n} {suc m} f zero = begin
proj₁ f zero ≡⟨ raise-edge-apply-zero (proj₁ f zero) (Monotone→Mono (next f)) ⟩
apply (Monotone→Mono f) zero ∎
apply-Monotone→Mono {suc n} {suc m} f (suc i) = begin
proj₁ f (suc i) ≡⟨ raise∘lower≡id (proj₁ f (suc i)) (proj₁ f zero) (proj₂ f zero (suc i) z≤n) ⟩
raise (proj₁ f zero) (lower (proj₁ f zero) (proj₁ f (suc i))) ≡⟨ cong (raise (proj₁ f zero)) (apply-Monotone→Mono (next f) i) ⟩
raise (proj₁ f zero) (apply (Monotone→Mono (next f)) i) ≡⟨ raise-edge-apply-suc (proj₁ f zero) i _ ⟩
apply (Monotone→Mono f) (suc i) ∎And that is the same as saying that we can convert Monotone to Mono and back, and we get what we started with (in ≐ sense):
Monotone→Mono→Monotone : (f : Monotone n m)
→ f ≐ Mono→Monotone (Monotone→Mono f)
Monotone→Mono→Monotone = apply-Monotone→MonoThe other direction, i.e. starting with Mono is simple to show as well using apply-inj lemma, which is the benefit of Mono having unique representation:
Monotone→Mono→Mono : (f : Mono n m)
→ f ≡ Monotone→Mono (Mono→Monotone f)
Monotone→Mono→Mono f = apply-inj
f
(Monotone→Mono (Mono→Monotone f))
(apply-Monotone→Mono (Mono→Monotone f))In this section we have shown that Mono and Monotone types are isomorphic. Great news!
#Interlude: Thinnings and contractions
Recall thinnings:
data Thin : ℕ → ℕ → Set where
baseₜ : Thin zero zero
skipₜ : Thin n m → Thin n (suc m)
keepₜ : Thin n m → Thin (suc n) (suc m)
applyₜ : Thin n m → Fin n → Fin m
applyₜ (skipₜ f) i = suc (applyₜ f i)
applyₜ (keepₜ f) zero = zero
applyₜ (keepₜ f) (suc i) = suc (applyₜ f i)These are strictly monotone functions:
isStrictlyMonotone : (Fin n → Fin m) → Set
isStrictlyMonotone f = ∀ i j → i < j → f i < f j
isStrictlyMonotone-applyₜ : (f : Thin n m) → isStrictlyMonotone (applyₜ f)
isStrictlyMonotone-applyₜ (skipₜ f) i j i<j = s≤s (isStrictlyMonotone-applyₜ f i j i<j)
isStrictlyMonotone-applyₜ (keepₜ f) zero (suc j) (s≤s i<j) = s≤s z≤n
isStrictlyMonotone-applyₜ (keepₜ f) (suc i) (suc j) (s≤s i<j) = s≤s (isStrictlyMonotone-applyₜ f i j i<j)Similarly: unique representation
applyₜ-inj : (f g : Thin n m) → (∀ i → applyₜ f i ≡ applyₜ g i) → f ≡ g
applyₜ-inj baseₜ baseₜ p = refl
applyₜ-inj (skipₜ f) (skipₜ g) p =
cong skipₜ (applyₜ-inj f g λ i → suc-injective (p i))
applyₜ-inj (skipₜ f) (keepₜ g) p with p zero
... | ()
applyₜ-inj (keepₜ f) (skipₜ g) p with p zero
... | ()
applyₜ-inj (keepₜ f) (keepₜ g) p =
cong keepₜ (applyₜ-inj f g λ i → suc-injective (p (suc i)))But applyₜ f maps are also injective, i.e. map different Fin ns to to different Fin ms:
applyₜ-inj₂ : (f : Thin n m) (i j : Fin n) → applyₜ f i ≡ applyₜ f j → i ≡ j
applyₜ-inj₂ (skipₜ f) i j p = applyₜ-inj₂ f i j (suc-injective p)
applyₜ-inj₂ (keepₜ f) zero zero p = refl
applyₜ-inj₂ (keepₜ f) (suc i) (suc j) p = cong suc (applyₜ-inj₂ f i j (suc-injective p))Thinnings can be converted to Mono:
Thin→Mono : Thin n m → Mono n m
Thin→Mono baseₜ = base
Thin→Mono (skipₜ f) = skip (Thin→Mono f)
Thin→Mono (keepₜ f) = keep (Thin→Mono f)Thins are injective monotonic maps. Can we represent the surjective ones? Yes! This look very similar:
data Cntr : ℕ → ℕ → Set where
baseₖ : Cntr zero zero
edgeₖ : Cntr n (suc m) → Cntr (suc n) (suc m)
keepₖ : Cntr n m → Cntr (suc n) (suc m)
edgeₖ' : Cntr (suc n) m → Cntr (suc (suc n)) m
edgeₖ' (edgeₖ f) = edgeₖ (edgeₖ f)
edgeₖ' (keepₖ f) = edgeₖ (keepₖ f)
applyₖ : Cntr n m → Fin n → Fin m
applyₖ (edgeₖ f) zero = zero
applyₖ (edgeₖ f) (suc i) = applyₖ f i
applyₖ (keepₖ f) zero = zero
applyₖ (keepₖ f) (suc i) = suc (applyₖ f i)
isMonotone-applyₖ : (f : Cntr n m) → isMonotone (applyₖ f)
isMonotone-applyₖ (edgeₖ f) zero j 0≤j = z≤n
isMonotone-applyₖ (edgeₖ f) (suc i) (suc j) (s≤s i≤j) = isMonotone-applyₖ f i j i≤j
isMonotone-applyₖ (keepₖ f) zero j 0≤j = z≤n
isMonotone-applyₖ (keepₖ f) (suc i) (suc j) (s≤s i≤j) = s≤s (isMonotone-applyₖ f i j i≤j)
applyₖ-surjective : (f : Cntr n m) (j : Fin m) → Σ (Fin n) λ i → applyₖ f i ≡ j
applyₖ-surjective (edgeₖ f) j with applyₖ-surjective f j
... | i , p = suc i , p
applyₖ-surjective (keepₖ f) zero = zero , refl
applyₖ-surjective (keepₖ f) (suc j) with applyₖ-surjective f j
... | i , p = suc i , cong suc p
Cntr→Mono : Cntr n m → Mono n m
Cntr→Mono baseₖ = base
Cntr→Mono (edgeₖ f) = edge (Cntr→Mono f)
Cntr→Mono (keepₖ f) = keep (Cntr→Mono f)We can show that Mono can be decomposed into composition of Cntr and Thin.
We can define the type and smart constructors:
Cntr×Thin : ℕ → ℕ → Set
Cntr×Thin n m = Σ ℕ λ p → Cntr n p × Thin p m
baseₖₜ : Cntr×Thin zero zero
baseₖₜ = 0 , baseₖ , baseₜ
skipₖₜ : Cntr×Thin n m → Cntr×Thin n (suc m)
skipₖₜ (p , f , g) = p , f , skipₜ g
edgeₖₜ : Cntr×Thin n (suc m) → Cntr×Thin (suc n) (suc m)
edgeₖₜ (p , f , skipₜ g) = suc p , keepₖ f , keepₜ g
edgeₖₜ (p , f , keepₜ g) = p , edgeₖ f , keepₜ gThen conversion from Mono is trivial to define:
Mono→Cntr×Thin : (f : Mono n m) → Cntr×Thin n m
Mono→Cntr×Thin base = baseₖₜ
Mono→Cntr×Thin (skip f) = skipₖₜ (Mono→Cntr×Thin f)
Mono→Cntr×Thin (edge f) = edgeₖₜ (Mono→Cntr×Thin f)Other direction isn't tricky either:
Cntr×Thin→Mono : Cntr×Thin n m → Mono n m
Cntr×Thin→Mono (_ , f , g) = Cntr→Mono f ⨟ Thin→Mono gWe can show that starting from Mono we can convert to a pair of Cntr and Thin, and if we convert back, we get what we started with:
skip-⨟ : (f : Mono n m) (g : Mono m p) → f ⨟ skip g ≡ skip (f ⨟ g)
skip-⨟ base g = refl
skip-⨟ (skip f) g = refl
skip-⨟ (edge f) g = refl
skip-pres : (f : Cntr×Thin n m) → Cntr×Thin→Mono (skipₖₜ f) ≡ skip (Cntr×Thin→Mono f)
skip-pres (p , f , g) = skip-⨟ (Cntr→Mono f) (Thin→Mono g)
edge-pres : (f : Cntr×Thin n (suc m)) → Cntr×Thin→Mono (edgeₖₜ f) ≡ edge (Cntr×Thin→Mono f)
edge-pres (p , f , skipₜ g) = refl
edge-pres (suc p , f , keepₜ g) = refl
Mono→CT→Mono : (f : Mono n m) → Cntr×Thin→Mono (Mono→Cntr×Thin f) ≡ f
Mono→CT→Mono base = refl
Mono→CT→Mono (skip f) = trans (skip-pres (Mono→Cntr×Thin f)) (cong skip (Mono→CT→Mono f))
Mono→CT→Mono (edge f) = trans (edge-pres (Mono→Cntr×Thin f)) (cong edge (Mono→CT→Mono f))This is an example of factoring a function into a composition of a surjective function followed by an injective one.
#Isomorphism with Reed's formulation
Reed's "Simple Simplices" blog post ended with a challenge writing
decompose : (Fin m → Fin n) → (m Δ⇒ n)function.
As we can convert Monotone to Mono, maybe we can get close?
Let's try.
open import Categories.Category.Instance.SimplexThe other direction, from Δ⇒ to Mono can be defined in systematic way. We define faceₘ and degenₘ and show that they behave like face and degen maps:
faceₘ : Fin (suc n) → Mono n (suc n)
faceₘ zero = skip id
faceₘ {n = suc n} (suc i) = keep (faceₘ i)
apply-faceₘ : (i : Fin (suc n)) (j : Fin n) → face i j ≡ apply (faceₘ i) j
apply-faceₘ zero j = cong suc (sym (apply-id j))
apply-faceₘ (suc i) zero = refl
apply-faceₘ (suc i) (suc j) = cong suc (apply-faceₘ i j)
degenₘ : Fin n → Mono (suc n) n
degenₘ zero = edge id
degenₘ (suc i) = keep (degenₘ i)
apply-degenₘ : (i : Fin n) (j : Fin (suc n)) → degen i j ≡ apply (degenₘ i) j
apply-degenₘ {suc n} zero zero = refl
apply-degenₘ {suc n} zero (suc j) = sym (apply-id j)
apply-degenₘ {suc n} (suc i) zero = refl
apply-degenₘ {suc n} (suc i) (suc j) = cong suc (apply-degenₘ i j)That is enough to define Δ→Mono map. As we already showed that identity and composition respect apply, We can show that so does respect Δ→Mono.
Δ→Mono : n Δ⇒ m → Mono n m
Δ→Mono ε = id
Δ→Mono (δ i) = faceₘ i
Δ→Mono (σ j) = degenₘ j
Δ→Mono (f ⊚ g) = Δ→Mono g ⨟ Δ→Mono f
apply-Δ→Mono : (f : n Δ⇒ m) (i : Fin n) → apply (Δ→Mono f) i ≡ ⟦ f ⟧ i
apply-Δ→Mono ε j = apply-id j
apply-Δ→Mono (δ i) j = sym (apply-faceₘ i j)
apply-Δ→Mono (σ i) j = sym (apply-degenₘ i j)
apply-Δ→Mono (f ⊚ g) j = begin
apply (Δ→Mono (f ⊚ g)) j ≡⟨ sym (apply-⨟ (Δ→Mono g) (Δ→Mono f) j) ⟩
apply (Δ→Mono f) (apply (Δ→Mono g) j) ≡⟨ cong (apply (Δ→Mono f)) (apply-Δ→Mono g j) ⟩
apply (Δ→Mono f) (⟦ g ⟧ j) ≡⟨ apply-Δ→Mono f (⟦ g ⟧ j) ⟩
⟦ f ⊚ g ⟧ j ∎The actual direction we are interested in is similar. We define smart constructors, and then proceed by structural induction.
First smart constructor is (maybe surprisingly) keepₚ:
Note: it doesn't make Δ⇒ any bigger, it still has the same structure and as many face and degen maps.
keepₚ : n Δ⇒ m → suc n Δ⇒ suc m
keepₚ ε = ε
keepₚ (δ i) = δ (suc i)
keepₚ (σ j) = σ (suc j)
keepₚ (f ⊚ g) = keepₚ f ⊚ keepₚ g
keepₚ-apply-zero : (f : n Δ⇒ m) → ⟦ keepₚ f ⟧ zero ≡ zero
keepₚ-apply-zero ε = refl
keepₚ-apply-zero (δ i) = refl
keepₚ-apply-zero (σ j) = refl
keepₚ-apply-zero (f ⊚ g) = trans (cong ⟦ keepₚ f ⟧ (keepₚ-apply-zero g)) (keepₚ-apply-zero f)
keepₚ-apply-suc : (f : n Δ⇒ m) (i : Fin n) → ⟦ keepₚ f ⟧ (suc i) ≡ suc (⟦ f ⟧ i)
keepₚ-apply-suc ε j = refl
keepₚ-apply-suc (δ i) j = refl
keepₚ-apply-suc (σ i) j = refl
keepₚ-apply-suc (f ⊚ g) j = trans (cong ⟦ keepₚ f ⟧ (keepₚ-apply-suc g j)) (keepₚ-apply-suc f (⟦ g ⟧ j) )Base case is simple:
baseₚ : zero Δ⇒ zero
baseₚ = εSkip is using face map:
skipₚ : n Δ⇒ m → n Δ⇒ suc m
skipₚ f = δ zero ⊚ f
skipₚ-apply : (f : n Δ⇒ m) (i : Fin n) → ⟦ skipₚ f ⟧ i ≡ suc (⟦ f ⟧ i)
skipₚ-apply f i = reflAnd edge is using degen map:
edgeₚ : n Δ⇒ suc m → suc n Δ⇒ suc m
edgeₚ f = σ zero ⊚ keepₚ f
edgeₚ-apply-zero : (f : n Δ⇒ suc m) → ⟦ edgeₚ f ⟧ zero ≡ zero
edgeₚ-apply-zero f = cong (degen zero) (keepₚ-apply-zero f)
edgeₚ-apply-suc : (f : n Δ⇒ suc m) (i : Fin n) → ⟦ edgeₚ f ⟧ (suc i) ≡ ⟦ f ⟧ i
edgeₚ-apply-suc f i = cong (degen zero) (keepₚ-apply-suc f i)Conversion from Mono to Δ⇒ is then easy when you have the pieces. The size of Δ⇒ is n face maps and m degen maps, even for identity map. Thus it's not minimal in any sense, but it isn't enormous either.
Mono→Δ : Mono n m → n Δ⇒ m
Mono→Δ base = baseₚ
Mono→Δ (skip f) = skipₚ (Mono→Δ f)
Mono→Δ (edge f) = edgeₚ (Mono→Δ f)Finally we can show that Mono→Δ and Δ→Mono for an isomorphism:
apply-Mono→Δ : (f : Mono n m) (i : Fin n) → ⟦ Mono→Δ f ⟧ i ≡ apply f i
apply-Mono→Δ (skip f) i = trans (skipₚ-apply (Mono→Δ f) i) (cong suc (apply-Mono→Δ f i))
apply-Mono→Δ (edge f) zero = edgeₚ-apply-zero (Mono→Δ f)
apply-Mono→Δ (edge f) (suc i) = trans (edgeₚ-apply-suc (Mono→Δ f) i) (apply-Mono→Δ f i)
Mono→Δ→Mono : (f : Mono n m) → Δ→Mono (Mono→Δ f) ≡ f
Mono→Δ→Mono f = apply-inj (Δ→Mono (Mono→Δ f)) f λ i → trans (apply-Δ→Mono (Mono→Δ f) i) (apply-Mono→Δ f i)
Δ→Mono→Δ' : (f : n Δ⇒ m) (i : Fin n) → ⟦ Mono→Δ (Δ→Mono f) ⟧ i ≡ ⟦ f ⟧ i
Δ→Mono→Δ' f i = trans (apply-Mono→Δ (Δ→Mono f) i) (apply-Δ→Mono f i)
Δ→Mono→Δ : (f : n Δ⇒ m) → Mono→Δ (Δ→Mono f) ≗ f
Δ→Mono→Δ f = Δ-eq λ {i} → Δ→Mono→Δ' f iUsing this result, and iso between Mono and Monotone we can define conversion from Monotone to Δ⇒:
Monotone→Δ : Monotone n m → n Δ⇒ m
Monotone→Δ f = Mono→Δ (Monotone→Mono f)
Monotone→Δ-correct : (f : Monotone n m) (i : Fin n)
→ proj₁ f i ≡ ⟦ Monotone→Δ f ⟧ i
Monotone→Δ-correct f i = begin
proj₁ f i ≡⟨ apply-Monotone→Mono f i ⟩
apply (Monotone→Mono f) i ≡⟨ sym (apply-Mono→Δ (Monotone→Mono f) i) ⟩
⟦ Monotone→Δ f ⟧ i ∎The Monotone→Δ is almost the decompose Reed was asking about. We need to know that argument is also monotonic to do the conversion. I think it's possible to define
postulate
monotonise : (Fin m → Fin n) → Monotone m nsuch that it is involutive on monotonic maps:
postulate
monotonise-inv : (f : Monotone n m) → f ≐ monotonise (proj₁ f)But if we have monotonise, then we can define
decompose : (Fin n → Fin m) → n Δ⇒ m
decompose f = Monotone→Δ (monotonise f)#Decompose
First the maximum function, and few lemmas:
infix 5 _∨_
_∨_ : Fin n → Fin n → Fin n
zero ∨ j = j
suc i ∨ zero = suc i
suc i ∨ suc j = suc (i ∨ j)
i≤j∨i : (i j : Fin n) → i ≤ j ∨ i
i≤j∨i zero j = z≤n
i≤j∨i (suc i) zero = ≤-refl
i≤j∨i (suc i) (suc j) = s≤s (i≤j∨i i j)
i≤i∨j : (i j : Fin n) → i ≤ i ∨ j
i≤i∨j zero j = z≤n
i≤i∨j (suc i) zero = ≤-refl
i≤i∨j (suc i) (suc j) = s≤s (i≤i∨j i j)
i≤j→i∨k≤i∨k : (i j k : Fin n) → i ≤ j → i ∨ k ≤ j ∨ k
i≤j→i∨k≤i∨k zero j k 0≤j = i≤j∨i k j
i≤j→i∨k≤i∨k (suc i) (suc j) zero i≤j = i≤j
i≤j→i∨k≤i∨k (suc i) (suc j) (suc k) (s≤s i≤j) = s≤s (i≤j→i∨k≤i∨k i j k i≤j)
i≤j→j≡j∨i : (i j : Fin n) → i ≤ j → j ≡ j ∨ i
i≤j→j≡j∨i zero zero 0≤0 = refl
i≤j→j≡j∨i zero (suc j) i<j = refl
i≤j→j≡j∨i (suc i) (suc j) (s≤s i≤j) = cong suc (i≤j→j≡j∨i i j i≤j)Then we can write an algorithm to make arbitrary f monotone:
The idea is to raise the floor for larger inputs:
monotonise-f' : (Fin (suc n) → Fin m) → (Fin n → Fin m)
monotonise-f' f k = f (suc k) ∨ f zero
monotonise-f : (Fin n → Fin m) → (Fin n → Fin m)
monotonise-f f zero = f zero
monotonise-f f (suc i) = monotonise-f (monotonise-f' f) iThe monotonised f is greater then just f:
monotonise-f-≤ : (f : Fin n → Fin m) (i j : Fin n)
→ i ≤ j
→ f i ≤ monotonise-f f j
monotonise-f-≤ f zero zero i≤j = ≤-refl
monotonise-f-≤ {n = suc (suc n)} f zero (suc j) i≤1+j = ≤-trans
(i≤j∨i (f zero) (f (suc zero)))
(monotonise-f-≤ (monotonise-f' f) zero j z≤n)
monotonise-f-≤ f (suc i) (suc j) (s≤s i≤j) = ≤-trans
(i≤i∨j (f (suc i)) (f zero))
(monotonise-f-≤ (monotonise-f' f) i j i≤j)And the result is indeed monotone:
monotonise-mono : (f : Fin n → Fin m) → isMonotone (monotonise-f f)
monotonise-mono f zero zero 0≤0 = ≤-refl
monotonise-mono f zero (suc j) 0≤j = monotonise-f-≤ f zero (suc j) z≤n
monotonise-mono f (suc i) (suc j) (s≤s i≤j) = monotonise-mono (monotonise-f' f) i j i≤jSo we can convert an arbitrary function to Monotone n m:
monotonise : (Fin n → Fin m) → Monotone n m
monotonise f = monotonise-f f , monotonise-mono fFinally we can prove that monotonise is "involutive" when applied
monotonise-f'-mono : (f : Fin (suc n) → Fin m)
→ isMonotone f
→ isMonotone (monotonise-f' f)
monotonise-f'-mono f f-mono i j i≤j = i≤j→i∨k≤i∨k
(f (suc i))
(f (suc j))
(f zero)
(f-mono (suc i) (suc j) (s≤s i≤j))
monotonise-inv' : (f : Fin n → Fin m) → isMonotone f → ∀ i → f i ≡ monotonise-f f i
monotonise-inv' f f-mono zero = refl
monotonise-inv' f f-mono (suc i) = begin
f (suc i) ≡⟨ i≤j→j≡j∨i (f zero) (f (suc i)) (f-mono zero (suc i) z≤n) ⟩
monotonise-f' f i ≡⟨ monotonise-inv' (monotonise-f' f) (monotonise-f'-mono f f-mono) i ⟩
monotonise-f (monotonise-f' f) i ∎
monotonise-inv : (f : Monotone n m) → f ≐ monotonise (proj₁ f)
monotonise-inv (f , f-mono) = monotonise-inv' f f-monoAnd finally we can define decompose!
decompose : (Fin n → Fin m) → n Δ⇒ m
decompose f = Monotone→Δ (monotonise f)- 2025-02-13 – PHOAS to de Bruijn conversion
- 2025-02-11 – NbE PHOAS
- 2024-06-24 – hashable arch native
- 2024-05-28 – cabal fields
- 2024-04-21 – A note about coercions
This work is licensed under a “CC BY SA 4.0” license.