Oleg's gists — Archive

Simple(r?) simplices

Posted on 2022-10-08 by Oleg Grenrus agda

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
Monotone maps
Fourth formulation
From Agda function to data

Monotone ↔ Mono isomorphism

Interlude: Thinnings and contractions
Isomorphism with Reed's formulation
Decompose

#Agda setup

module 2022-10-08-simplex where

import 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 j

Then a monotone function is a function together with a proof it is monotone

Monotone : ℕ → ℕ → Set
Monotone n m = Σ (Fin n → Fin m) isMonotone

And 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 i

The 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 i

We 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) i

Mono 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≤j

Combining 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≤j

We 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-mono

Now 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→Mono

The 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ₜ g

Then 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 g

We 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.Simplex

The 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 = refl

And 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 i

Using 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 n

such 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) i

The 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≤j

So 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 f

Finally 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-mono

And finally we can define decompose!

decompose : (Fin n → Fin m) → n Δ⇒ m
decompose f = Monotone→Δ (monotonise f)

2024-04-21 – A note about coercions
2024-04-18 – What makes a good compiler warning?
2024-04-12 – Core Inspection
2024-04-01 – Implicit arguments
2024-03-17 – ST with an early exit

This work is licensed under a “CC BY SA 4.0” license.

Oleg's gists — Archive

twitter github email linkedin stackoverflow

Site proudly generated by Hakyll