I was lately again thinking about thinnings.
Thinnings are a weaker form of renamings, which we use in well-scoped or well-typed implementations of programming languages. (Their proper name is order-preserving embeddings, mathematicians may know them as morphism in augmented simplex category Δ₊)
There is one well known and used implementation implementation for them. It's simple to use and write proofs about. However it's not super great. Especially it's not great in Haskell, as it cannot be given Category instance. (Though you almost never need thinnings in Haskell, so the reason is a bit moot).
I'll show two other implementations, and show that they are equivalent, using Cubical Agda to state the equivalences. Before we dive in, Agda module prologue:
{-# OPTIONS --cubical --safe #-}
module 2022-09-30-thinnings where
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Nat
open import Cubical.Data.Empty
open import Cubical.Data.Sigma
open import Cubical.Relation.NullaryI will show only a well-scoped thinnings. So the context are simply natural numbers. As there are plenty of them, let us define few common variables.
Orthodox thinnings
For the sake of this post, I call well known thinnings orthodox, and use ₒ subscript to indicate that.
data _⊑ₒ_ : ℕ → ℕ → Type where
nilₒ : zero ⊑ₒ zero
skipₒ : n ⊑ₒ m → n ⊑ₒ suc m
keepₒ : n ⊑ₒ m → suc n ⊑ₒ suc m
Orth = _⊑ₒ_An example thinning is like
Which would look like:
\begin{tikzpicture} \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (A) at (0,0.00) {}; \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (B) at (0,0.50) {}; \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (C) at (0,1.00) {}; \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (D) at (0,2.00) {}; \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (E) at (0,3.00) {}; \node[anchor=east] at (A) {$0$}; \node[anchor=east] at (B) {$1$}; \node[anchor=east] at (C) {$2$}; \node[anchor=east] at (D) {$3$}; \node[anchor=east] at (E) {$4$}; \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (X) at (2,0.00) {}; \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (Y) at (2,0.50) {}; \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (Z) at (2,1.00) {}; \node[circle, draw, inner sep=0pt, minimum width=4pt] (U) at (2,1.50) {}; \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (V) at (2,2.00) {}; \node[circle, draw, inner sep=0pt, minimum width=4pt] (W) at (2,2.50) {}; \node[circle, draw, fill=black, inner sep=0pt, minimum width=4pt] (Q) at (2,3.00) {}; \node[anchor=west] at (X) {$0$}; \node[anchor=west] at (Y) {$1$}; \node[anchor=west] at (Z) {$2$}; \node[anchor=west] at (U) {$3$}; \node[anchor=west] at (V) {$4$}; \node[anchor=west] at (W) {$5$}; \node[anchor=west] at (Q) {$6$}; \draw[-] (A) -- (X); \draw[-] (B) -- (Y); \draw[-] (C) -- (Z); \draw[-] (D) -- (V); \draw[-] (E) -- (Q); \end{tikzpicture}
We can define identity thinning:
Note how it pattern matches on the size (of the context). That what makes it impossible to defined Category instance in Haskell.
We can also define composition, and weakening on top of the context
_⦂ₒ_ : n ⊑ₒ m → m ⊑ₒ p → n ⊑ₒ p
δ₁ ⦂ₒ nilₒ = δ₁
δ₁ ⦂ₒ skipₒ δ₂ = skipₒ (δ₁ ⦂ₒ δ₂)
keepₒ δ₁ ⦂ₒ keepₒ δ₂ = keepₒ (δ₁ ⦂ₒ δ₂)
skipₒ δ₁ ⦂ₒ keepₒ δ₂ = skipₒ (δ₁ ⦂ₒ δ₂)
wkₒ : n ⊑ₒ suc n
wkₒ = skipₒ idₒAs said, the proofs about this formulation are simple. Plenty of equalities hold definitionally:
Separate thinning
As mentioned in previous section the orthodox thinning is not very efficient. For example when implementing normalization by evaluation (NbE) we run into problems. There we need identity thinning when evaluating every application, so we will pay a price proportional to the size of the current context!
In his work Andras Kovacs makes a variant swapping nilₒ for idₒ. However then thinnings won't have unique representation anymore and proofs become more inconvenient to write.
We can make a special case for identity thinning without sacrificing unique representation for the cost of slightly more complicated definition. We just need to consider identity thinning and non-identity ones separately.
data _⊏ₛ_ : ℕ → ℕ → Type where
wkₛ : n ⊏ₛ suc n
keepₛ : n ⊏ₛ m → suc n ⊏ₛ suc m
skipₛ : n ⊏ₛ m → n ⊏ₛ suc m
data _⊑ₙ_ : ℕ → ℕ → Type where
idₙ : n ⊑ₙ n
strict : n ⊏ₛ m → n ⊑ₙ m
Strict = _⊏ₛ_
NonStr = _⊑ₙ_We can implement most operations without much problems. Note that also wkₙ has a small, context-size independent, representation.
nilₙ : zero ⊑ₙ zero
nilₙ = idₙ
wkₙ : ∀ {n} → n ⊑ₙ suc n
wkₙ = strict wkₛ
skipₙ : n ⊑ₙ m → n ⊑ₙ suc m
skipₙ idₙ = wkₙ
skipₙ (strict x) = strict (skipₛ x)
keepₙ : n ⊑ₙ m → suc n ⊑ₙ suc m
keepₙ idₙ = idₙ
keepₙ (strict δ) = strict (keepₛ δ)
keep-id≡idₙ : keepₙ idₙ ≡ idₙ {suc n}
keep-id≡idₙ = reflComposition is a bit more complicated then for orthodox variant, but not considerably:
_⦂ₛ_ : n ⊏ₛ m → m ⊏ₛ p → n ⊏ₛ p
δ₁ ⦂ₛ wkₛ = skipₛ δ₁
δ₁ ⦂ₛ skipₛ δ₂ = skipₛ (δ₁ ⦂ₛ δ₂)
wkₛ ⦂ₛ keepₛ δ₂ = skipₛ δ₂
keepₛ δ₁ ⦂ₛ keepₛ δ₂ = keepₛ (δ₁ ⦂ₛ δ₂)
skipₛ δ₁ ⦂ₛ keepₛ δ₂ = skipₛ (δ₁ ⦂ₛ δ₂)
_⦂ₙ_ : n ⊑ₙ m → m ⊑ₙ p → n ⊑ₙ p
δ₁ ⦂ₙ idₙ = δ₁
idₙ ⦂ₙ strict δ₂ = strict δ₂
strict δ₁ ⦂ₙ strict δ₂ = strict (δ₁ ⦂ₛ δ₂)Are these orthodox and this thinning the same?
Are ⊑ₒ and ⊑ₙ the same? We can construct an isomorphism between them to answer that question positively.
Orth→NonStr : n ⊑ₒ m → n ⊑ₙ m
Orth→NonStr nilₒ = nilₙ
Orth→NonStr (keepₒ δ) = keepₙ (Orth→NonStr δ)
Orth→NonStr (skipₒ δ) = skipₙ (Orth→NonStr δ)
Strict→Orth : n ⊏ₛ m → n ⊑ₒ m
Strict→Orth wkₛ = wkₒ
Strict→Orth (keepₛ δ) = keepₒ (Strict→Orth δ)
Strict→Orth (skipₛ δ) = skipₒ (Strict→Orth δ)
NonStr→Orth : n ⊑ₙ m → n ⊑ₒ m
NonStr→Orth idₙ = idₒ
NonStr→Orth (strict δ) = Strict→Orth δIt is not enough to define conversion functions we also need to show that they cancel out. Luckily this is not difficult, we need few auxiliary homomorphism lemmas.
NonStr→Orth-keepₒ : (δ : n ⊑ₙ m) → NonStr→Orth (keepₙ δ) ≡ keepₒ (NonStr→Orth δ)
NonStr→Orth-skipₒ : (δ : n ⊑ₙ m) → NonStr→Orth (skipₙ δ) ≡ skipₒ (NonStr→Orth δ)
Orth→NonStr-id≡id : ∀ n → Orth→NonStr idₒ ≡ idₙ {n}NonStr→Orth-keepₒ idₙ = refl
NonStr→Orth-keepₒ (strict _) = refl
NonStr→Orth-skipₒ idₙ = refl
NonStr→Orth-skipₒ (strict _) = refl
Orth→NonStr-id≡id zero = refl
Orth→NonStr-id≡id (suc n) = cong keepₙ (Orth→NonStr-id≡id n)And finally we can show that Orth→NonStr NonStr→Orth are each others inverses.
Orth→NonStr→Orth : (δ : n ⊑ₒ m) → NonStr→Orth (Orth→NonStr δ) ≡ δ
Strict→Orth→NonStr : (δ : n ⊏ₛ m) → Orth→NonStr (Strict→Orth δ) ≡ strict δ
NonStr→Orth→NonStr : (δ : n ⊑ₙ m) → Orth→NonStr (NonStr→Orth δ) ≡ δOrth→NonStr→Orth nilₒ = refl
Orth→NonStr→Orth (keepₒ δ) = NonStr→Orth-keepₒ (Orth→NonStr δ) ∙ cong keepₒ (Orth→NonStr→Orth δ)
Orth→NonStr→Orth (skipₒ δ) = NonStr→Orth-skipₒ (Orth→NonStr δ) ∙ cong skipₒ (Orth→NonStr→Orth δ)
Strict→Orth→NonStr wkₛ = cong skipₙ (Orth→NonStr-id≡id _)
Strict→Orth→NonStr (keepₛ δ) = cong keepₙ (Strict→Orth→NonStr δ)
Strict→Orth→NonStr (skipₛ δ) = cong skipₙ (Strict→Orth→NonStr δ)
NonStr→Orth→NonStr idₙ = Orth→NonStr-id≡id _
NonStr→Orth→NonStr (strict δ) = Strict→Orth→NonStr δIn Cubical Agda we can promote the above isomorphism to an equality.
Orth≡NonStr-pointwise : (n ⊑ₒ m) ≡ (n ⊑ₙ m)
Orth≡NonStr-pointwise = isoToPath
(iso Orth→NonStr NonStr→Orth NonStr→Orth→NonStr Orth→NonStr→Orth)
Orth≡NonStr : Orth ≡ NonStr
Orth≡NonStr i n m = Orth≡NonStr-pointwise {n} {m} iBut are they still the same?
Even the types are the same, are the operations we defined on them the same? We still need to show that the operations give the same results.
I'll define a simplified "category operations" type, with an identity and a composition:
CatOps : (ℕ → ℕ → Type) → Type
CatOps _↝_
= (∀ {n} → n ↝ n) -- identity
× (∀ {n m p} → n ↝ m → m ↝ p → n ↝ p ) -- compositionOrthodox category ops are:
And NonStr ops are:
And we can show transport orthodox ops along Orth≡NonStr to get other variant
The goal is to show that all these are equal.
First We can construct a path between two CatOps NonStr structures,
For identity part we need identity homomorphism:
Orth→NonStr-id : Orth→NonStr idₒ ≡ idₙ {n}
Orth→NonStr-id {zero} = refl
Orth→NonStr-id {suc n} = cong keepₙ (Orth→NonStr-id {n})Then we can extract the transported identity, and show it is the same as idₙ:
idₙₜ : n ⊑ₙ n
idₙₜ = fst CatOps-NonStrₜ
idₙₜ≡idₙ : idₙₜ ≡ idₙ {n}
idₙₜ≡idₙ = transportRefl (Orth→NonStr idₒ) ∙ Orth→NonStr-idThe composition is slightly more complicated.
skip-⦂ₙ : (δ₁ : n ⊑ₙ m) → (δ₂ : m ⊑ₙ p)
→ skipₙ (δ₁ ⦂ₙ δ₂) ≡ (δ₁ ⦂ₙ skipₙ δ₂)
skip-⦂ₙ idₙ idₙ = refl
skip-⦂ₙ (strict _) idₙ = refl
skip-⦂ₙ idₙ (strict _) = refl
skip-⦂ₙ (strict _) (strict _) = refl
skip-keep-⦂ₙ : (δ₁ : n ⊑ₙ m) (δ₂ : m ⊑ₙ p)
→ skipₙ (δ₁ ⦂ₙ δ₂) ≡ (skipₙ δ₁ ⦂ₙ keepₙ δ₂)
skip-keep-⦂ₙ δ₁ idₙ = refl
skip-keep-⦂ₙ idₙ (strict _) = refl
skip-keep-⦂ₙ (strict _) (strict _) = refl
keep-keep-⦂ₙ : (δ₁ : n ⊑ₙ m) (δ₂ : m ⊑ₙ p)
→ keepₙ (δ₁ ⦂ₙ δ₂) ≡ (keepₙ δ₁ ⦂ₙ keepₙ δ₂)
keep-keep-⦂ₙ δ₁ idₙ = refl
keep-keep-⦂ₙ idₙ (strict x) = refl
keep-keep-⦂ₙ (strict _) (strict _) = reflWe can show that Orth→NonStr preserves composition.
Orth→NonStr-⦂ : (δ₁ : n ⊑ₒ m) (δ₂ : m ⊑ₒ p)
→ Orth→NonStr (δ₁ ⦂ₒ δ₂) ≡ Orth→NonStr δ₁ ⦂ₙ Orth→NonStr δ₂
Orth→NonStr-⦂ δ₁ nilₒ = refl
Orth→NonStr-⦂ δ₁ (skipₒ δ₂) = cong skipₙ (Orth→NonStr-⦂ δ₁ δ₂) ∙ skip-⦂ₙ (Orth→NonStr δ₁) (Orth→NonStr δ₂)
Orth→NonStr-⦂ (skipₒ δ₁) (keepₒ δ₂) = cong skipₙ (Orth→NonStr-⦂ δ₁ δ₂) ∙ skip-keep-⦂ₙ (Orth→NonStr δ₁) (Orth→NonStr δ₂)
Orth→NonStr-⦂ (keepₒ δ₁) (keepₒ δ₂) = cong keepₙ (Orth→NonStr-⦂ δ₁ δ₂) ∙ keep-keep-⦂ₙ (Orth→NonStr δ₁) (Orth→NonStr δ₂)Using the above fact, we can show that and are pointwise equal. The proof looks complicated, but is pretty straightforward in the end.
_⦂ₙₜ_ : n ⊑ₙ m → m ⊑ₙ p → n ⊑ₙ p
_⦂ₙₜ_ = snd CatOps-NonStrₜ
⦂ₙₜ≡⦂ₙ : (δ₁ : n ⊑ₙ m) (δ₂ : m ⊑ₙ p) → δ₁ ⦂ₙₜ δ₂ ≡ δ₁ ⦂ₙ δ₂
⦂ₙₜ≡⦂ₙ {n} {m} {p} δ₁ δ₂ =
transport refl expr₁ ≡⟨ transportRefl expr₁ ⟩
expr₁ ≡⟨ expr₁≡expr₂ ⟩
expr₂ ≡⟨ Orth→NonStr-⦂ (NonStr→Orth δ₁) (NonStr→Orth δ₂) ⟩
expr₃ ≡⟨ (λ i → NonStr→Orth→NonStr δ₁ i ⦂ₙ
NonStr→Orth→NonStr δ₂ i) ⟩
δ₁ ⦂ₙ δ₂ ∎
where
expr₁ = Orth→NonStr (NonStr→Orth (transport refl δ₁) ⦂ₒ
NonStr→Orth (transport refl δ₂))
expr₂ = Orth→NonStr (NonStr→Orth δ₁ ⦂ₒ NonStr→Orth δ₂)
expr₃ = Orth→NonStr (NonStr→Orth δ₁) ⦂ₙ Orth→NonStr (NonStr→Orth δ₂)
expr₁≡expr₂ : expr₁ ≡ expr₂
expr₁≡expr₂ i = Orth→NonStr (NonStr→Orth (transportRefl δ₁ i) ⦂ₒ
NonStr→Orth (transportRefl δ₂ i))And finally we can state that first equality:
CatOps-NonStr≡ : CatOps-NonStrₜ ≡ CatOps-NonStr
CatOps-NonStr≡ i = idₙₜ≡idₙ i , λ δ₁ δ₂ → ⦂ₙₜ≡⦂ₙ δ₁ δ₂ iand the quality we actually wanted to say, that CatOps-Orth and CatOps-NonStr are equal (if we equate their types by Orth≡NonStr)!!!
CatOps-Orth≡NonStr : (λ i → CatOps (Orth≡NonStr i))
[ CatOps-Orth ≡ CatOps-NonStr ]
CatOps-Orth≡NonStr = toPathP CatOps-NonStr≡Higher-inductive type
Cubical Agda also supports higher inductive types (HITs), i.e. types with additional equalities. We can formalize Andras better performing thinning as a HIT, by throwing in an additional equality. Agda will then ensure that we always respect it.
data _⊑ₕ_ : ℕ → ℕ → Type where
idₕ : n ⊑ₕ n
keepₕ : n ⊑ₕ m → suc n ⊑ₕ suc m
skipₕ : n ⊑ₕ m → n ⊑ₕ suc m
-- it is what it says: keep idₕ ≡ idₕ
keep-id≡idₕ : ∀ n → keepₕ (idₕ {n = n}) ≡ idₕ {n = suc n}
HIT = _⊑ₕ_Composition for HIT-thinning looks very similar to the orthodox version...
_⦂ₕ_ : n ⊑ₕ m → m ⊑ₕ p → n ⊑ₕ p
δ₁ ⦂ₕ idₕ = δ₁
δ₁ ⦂ₕ skipₕ δ₂ = skipₕ (δ₁ ⦂ₕ δ₂)
idₕ ⦂ₕ keepₕ δ₂ = keepₕ δ₂
keepₕ δ₁ ⦂ₕ keepₕ δ₂ = keepₕ (δ₁ ⦂ₕ δ₂)
skipₕ δ₁ ⦂ₕ keepₕ δ₂ = skipₕ (δ₁ ⦂ₕ δ₂)... except that we have extra cases which deal with an extra equality we threw in.
We have to show that equations are consistent with keep-id≡idₕ equality. The goals may be obfuscated, but relatively easy to fill.
keep-id≡idₕ n i ⦂ₕ keepₕ δ₂ = goal i
where
lemma : ∀ {n m} → (δ : HIT n m) → idₕ ⦂ₕ δ ≡ δ
lemma idₕ = refl
lemma (keepₕ δ) = refl
lemma (skipₕ δ) = cong skipₕ (lemma δ)
lemma (keep-id≡idₕ n i) j = keep-id≡idₕ n i
goal : keepₕ (idₕ ⦂ₕ δ₂) ≡ keepₕ δ₂
goal i = keepₕ (lemma δ₂ i)
idₕ ⦂ₕ keep-id≡idₕ n i = keep-id≡idₕ n i
keepₕ δ₁ ⦂ₕ keep-id≡idₕ n i = keepₕ δ₁
skipₕ δ₁ ⦂ₕ keep-id≡idₕ n i = skipₕ δ₁
keep-id≡idₕ .n i ⦂ₕ keep-id≡idₕ n j = goal i j
where
goal : Square refl (keep-id≡idₕ n) refl (keep-id≡idₕ n)
goal i j = keep-id≡idₕ n (i ∧ j)We can try to prove that the HIT variant is the same as orthodox one. The conversion functions are extremely simple, because the data-type is almost the same:
Orth→HIT : n ⊑ₒ m → n ⊑ₕ m
Orth→HIT nilₒ = idₕ
Orth→HIT (keepₒ δ) = keepₕ (Orth→HIT δ)
Orth→HIT (skipₒ δ) = skipₕ (Orth→HIT δ)
HIT→Orth : n ⊑ₕ m → n ⊑ₒ m
HIT→Orth idₕ = idₒ
HIT→Orth (keepₕ δ) = keepₒ (HIT→Orth δ)
HIT→Orth (skipₕ δ) = skipₒ (HIT→Orth δ)
HIT→Orth (keep-id≡idₕ n i) = keep-id≡idₒ {n} iConverting orthodox representation to HIT and back doesn't change the thinning. The proof is straightforward structural induction.
Orth→HIT→Orth : (δ : Orth n m) → HIT→Orth (Orth→HIT δ) ≡ δ
Orth→HIT→Orth nilₒ = refl
Orth→HIT→Orth (keepₒ δ) = cong keepₒ (Orth→HIT→Orth δ)
Orth→HIT→Orth (skipₒ δ) = cong skipₒ (Orth→HIT→Orth δ)On the other hand the opposite direction is tricky.
Easy part is to show that Orth→HIT preserves the identity, that will show that idₕ roundtrips.
Orth→HIT-id : ∀ n → Orth→HIT idₒ ≡ idₕ {n}
Orth→HIT-id zero = refl
Orth→HIT-id (suc n) = cong keepₕ (Orth→HIT-id n) ∙ keep-id≡idₕ nWe also have to show that keep-id≡idₕ roundtrips. This is considerably more challenging. Luckily if you squint enough (and are familiar with cubical library), you notice the pattern:
lemma : ∀ n → Square
(cong keepₕ (Orth→HIT-id n))
(cong keepₕ (Orth→HIT-id n) ∙ keep-id≡idₕ n)
(refl {x = keepₕ (Orth→HIT idₒ)})
(keep-id≡idₕ n)
lemma n = compPath-filler
{x = keepₕ (Orth→HIT idₒ)}
(cong keepₕ (Orth→HIT-id n))
(keep-id≡idₕ n)(In general, proving the equalities about equalities in Cubical Agda, i.e. filling squares and cubes feels to be black magic).
Using these lemmas we can finish the equality proof:
HIT→Orth→HIT : (δ : HIT n m) → Orth→HIT (HIT→Orth δ) ≡ δ
HIT→Orth→HIT idₕ = Orth→HIT-id _
HIT→Orth→HIT (keepₕ δ) = cong keepₕ (HIT→Orth→HIT δ)
HIT→Orth→HIT (skipₕ δ) = cong skipₕ (HIT→Orth→HIT δ)
HIT→Orth→HIT (keep-id≡idₕ n i) j = lemma n i j
Orth≡HIT-pointwise : n ⊑ₒ m ≡ n ⊑ₕ m
Orth≡HIT-pointwise =
isoToPath (iso Orth→HIT HIT→Orth HIT→Orth→HIT Orth→HIT→Orth)
Orth≡HIT : Orth ≡ HIT
Orth≡HIT i n m = Orth≡HIT-pointwise {n} {m} iAnd we can show that this thinning identity and composition behave as the orthodox one. The identity homomorphism we have already proven, composition is trivial as the HIT structure resembles the structure orthodox thinning:
Orth→HIT-⦂ : ∀ {n m p} (δ₁ : Orth n m) (δ₂ : Orth m p)
→ Orth→HIT (δ₁ ⦂ₒ δ₂) ≡ Orth→HIT δ₁ ⦂ₕ Orth→HIT δ₂
Orth→HIT-⦂ δ₁ nilₒ = refl
Orth→HIT-⦂ δ₁ (skipₒ δ₂) = cong skipₕ (Orth→HIT-⦂ δ₁ δ₂)
Orth→HIT-⦂ (keepₒ δ₁) (keepₒ δ₂) = cong keepₕ (Orth→HIT-⦂ δ₁ δ₂)
Orth→HIT-⦂ (skipₒ δ₁) (keepₒ δ₂) = cong skipₕ (Orth→HIT-⦂ δ₁ δ₂)Then we can repeat what we did with previous thinning.
CatOps-HIT : CatOps HIT
CatOps-HIT = idₕ , _⦂ₕ_
CatOps-HITₜ : CatOps HIT
CatOps-HITₜ = subst CatOps Orth≡HIT CatOps-OrthIdentities are equal:
idₕₜ : n ⊑ₕ n
idₕₜ = fst CatOps-HITₜ
idₕₜ≡idₕ : idₕₜ ≡ idₕ {n}
idₕₜ≡idₕ = transportRefl (Orth→HIT idₒ) ∙ Orth→HIT-id _and composition (literally the same code as in previous section, it can be automated but it's not worth for a blog post)
_⦂ₕₜ_ : n ⊑ₕ m → m ⊑ₕ p → n ⊑ₕ p
_⦂ₕₜ_ = snd CatOps-HITₜ
⦂ₕₜ≡⦂ₕ : (δ₁ : n ⊑ₕ m) (δ₂ : m ⊑ₕ p) → δ₁ ⦂ₕₜ δ₂ ≡ δ₁ ⦂ₕ δ₂
⦂ₕₜ≡⦂ₕ {n} {m} {p} δ₁ δ₂ =
transport refl expr₁ ≡⟨ transportRefl expr₁ ⟩
expr₁ ≡⟨ expr₁≡expr₂ ⟩
expr₂ ≡⟨ Orth→HIT-⦂ (HIT→Orth δ₁) (HIT→Orth δ₂) ⟩
expr₃ ≡⟨ (λ i → HIT→Orth→HIT δ₁ i ⦂ₕ HIT→Orth→HIT δ₂ i) ⟩
δ₁ ⦂ₕ δ₂ ∎
where
expr₁ = Orth→HIT (HIT→Orth (transport refl δ₁) ⦂ₒ
HIT→Orth (transport refl δ₂))
expr₂ = Orth→HIT (HIT→Orth δ₁ ⦂ₒ HIT→Orth δ₂)
expr₃ = Orth→HIT (HIT→Orth δ₁) ⦂ₕ Orth→HIT (HIT→Orth δ₂)
expr₁≡expr₂ : expr₁ ≡ expr₂
expr₁≡expr₂ i = Orth→HIT (HIT→Orth (transportRefl δ₁ i) ⦂ₒ
HIT→Orth (transportRefl δ₂ i))And the equalities of CatOps:
CatOps-HIT≡ : CatOps-HITₜ ≡ CatOps-HIT
CatOps-HIT≡ i = idₕₜ≡idₕ i , λ δ₁ δ₂ → ⦂ₕₜ≡⦂ₕ δ₁ δ₂ i
CatOps-Orth≡HIT : (λ i → CatOps (Orth≡HIT i)) [ CatOps-Orth ≡ CatOps-HIT ]
CatOps-Orth≡HIT = toPathP CatOps-HIT≡Conclusion
We have seen three definitions of thinnings. Orthodox one, one with identity constructor yet unique representation and variant using additional equality. Using Cubical Agda we verified that these three definitions are equal, and their identity and composition behave the same.
What we can learn from it?
Well. It is morally correct to define
data Thin n m where
ThinId :: Thin n n
ThinSkip :: Thin n m -> Thin n (S m)
ThinKeep :: Thin n m -> Thin (S n) (S m)as long as you pay attention to not differentiate between ThinKeep ThinId and ThinId, you are safe. GHC won't point you if you wrote something inconsistent.
For example checking whether the thinning is an identity:
is not correct, but will be accepted by GHC. (Won't be by Cubical Agda).
But if you don't trust yourself, you can go for slightly more complicated
data Thin n m where
ThinId :: Thin n n
Thin' :: Thin' n m -> Thin n m
data Thin' n m where
ThinWk :: Thin' n (S n)
ThinSkip :: Thin' n m -> Thin' n (S m)
ThinKeep :: Thin' n m -> Thin' (S n) (S m)In either case you will be able to write Category instance:
which is not possible with an orthodox thinning definition.
Extras
open import Cubical.Data.Nat.Order
-- thinnings can be converted to less-than-or-equal-to relation:
⊑ₕ→≤ : n ⊑ₕ m → n ≤ m
⊑ₕ→≤ idₕ = 0 , refl
⊑ₕ→≤ (keepₕ δ) with ⊑ₕ→≤ δ
... | n , p = n , +-suc n _ ∙ cong suc p
⊑ₕ→≤ (skipₕ δ) with ⊑ₕ→≤ δ
... | n , p = suc n , cong suc p
⊑ₕ→≤ (keep-id≡idₕ n i) = lemma' i where
lemma' : ⊑ₕ→≤ (keepₕ idₕ) ≡ ⊑ₕ→≤ (idₕ {suc n})
lemma' = Σ≡Prop (λ m → isSetℕ (m + suc n) (suc n)) (refl {x = 0})
-- Then we can check whether thinning is an identity.
-- Agda forces us to not cheat.
-- (Well, and also → Dec (n ≡ m))
isThinId : n ⊑ₕ m → Dec (n ≡ m)
isThinId idₕ = yes refl
isThinId (keepₕ δ) with isThinId δ
... | yes p = yes (cong suc p)
... | no ¬p = no λ p → ¬p (injSuc p)
isThinId {n} {m} (skipₕ δ) with ⊑ₕ→≤ δ
... | (r , p) = no λ q → ¬m+n<m {m = n} {n = 0}
(r , (r + suc (n + 0) ≡⟨ +-suc r (n + 0) ⟩
suc (r + (n + 0)) ≡⟨ cong (λ x → suc (r + x)) (+-zero n) ⟩
suc (r + n) ≡⟨ cong suc p ⟩
suc _ ≡⟨ sym q ⟩
n ∎))
isThinId (keep-id≡idₕ n i) = yes (λ _ → suc n)
-- Same for orthodox
⊑ₒ→≤ : n ⊑ₒ m → n ≤ m
⊑ₒ→≤ nilₒ = 0 , refl
⊑ₒ→≤ (skipₒ δ) with ⊑ₒ→≤ δ
... | n , p = suc n , cong suc p
⊑ₒ→≤ (keepₒ δ) with ⊑ₒ→≤ δ
... | n , p = n , +-suc n _ ∙ cong suc p
-- if indices match, δ is idₒ
⊥-elim : {A : Type} → ⊥ → A
⊥-elim ()
idₒ-unique : (δ : n ⊑ₒ n) → δ ≡ idₒ
idₒ-unique nilₒ = refl
idₒ-unique (skipₒ δ) = ⊥-elim (¬m<m (⊑ₒ→≤ δ))
idₒ-unique (keepₒ δ) = cong keepₒ (idₒ-unique δ)
-- or idₕ, for which direct proof is trickier.
idₕ-unique : (δ : n ⊑ₕ n) → δ ≡ idₕ
idₕ-unique {n} = subst {A = Σ _ CatOps}
(λ { (_⊑_ , (id , _⦂_)) → (δ : n ⊑ n) → δ ≡ id})
(λ i → Orth≡HIT i , CatOps-Orth≡HIT i)
idₒ-uniqueMore extras
The most important operation thinning support is their action on variables.
Using each of the variants let us define the action:
thinₒ : n ⊑ₒ m → Var n → Var m
thinₒ nilₒ ()
thinₒ (skipₒ δ) x = vs (thinₒ δ x)
thinₒ (keepₒ δ) vz = vz
thinₒ (keepₒ δ) (vs x) = vs (thinₒ δ x)
thinₛ : n ⊏ₛ m → Var n → Var m
thinₛ wkₛ x = vs x
thinₛ (skipₛ δ) x = vs (thinₛ δ x)
thinₛ (keepₛ δ) vz = vz
thinₛ (keepₛ δ) (vs x) = vs (thinₛ δ x)
thinₙ : n ⊑ₙ m → Var n → Var m
thinₙ idₙ x = x
thinₙ (strict δ) x = thinₛ δ xIt's worth noticing that HIT forces to take into account the keep≡id≡idₕ equality, so we cannot do silly stuff in keepₕ cases.
thinₕ : n ⊑ₕ m → Var n → Var m
thinₕ idₕ x = x
thinₕ (skipₕ δ) x = vs (thinₕ δ x)
thinₕ (keepₕ δ) vz = vz
thinₕ (keepₕ δ) (vs x) = vs (thinₕ δ x)
thinₕ (keep-id≡idₕ n i) vz = vz
thinₕ (keep-id≡idₕ n i) (vs x) = vs xLet us prove that these definitions are compatible. First we need a simple lemma, that thinₒ idₒ is an identity function.
thin-idₒ : (x : Var n) → thinₒ idₒ x ≡ x
thin-idₒ {suc n} vz = refl
thin-idₒ {suc n} (vs x) = cong vs (thin-idₒ x)Action : ℕ → ℕ → (ℕ → ℕ → Type) → Type
Action n m _⊑_ = n ⊑ m → Var n → Var m
thinₙₜ : n ⊑ₙ m → Var n → Var m
thinₙₜ {n} {m} = subst (Action n m) Orth≡NonStr thinₒ
Strict→Orth-thin : (δ : n ⊏ₛ m) (x : Var n) → thinₒ (Strict→Orth δ) x ≡ thinₛ δ x
Strict→Orth-thin wkₛ x = cong vs (thin-idₒ x)
Strict→Orth-thin (skipₛ δ) x = cong vs (Strict→Orth-thin δ x)
Strict→Orth-thin (keepₛ δ) vz = refl
Strict→Orth-thin (keepₛ δ) (vs x) = cong vs (Strict→Orth-thin δ x)
NonStr→Orth-thin : (δ : n ⊑ₙ m) (x : Var n) → thinₒ (NonStr→Orth δ) x ≡ thinₙ δ x
NonStr→Orth-thin idₙ x = thin-idₒ x
NonStr→Orth-thin (strict δ) x = Strict→Orth-thin δ x
thinₙₜ≡thinₙ-pointwise : (δ : n ⊑ₙ m) (x : Var n) → thinₙₜ δ x ≡ thinₙ δ x
thinₙₜ≡thinₙ-pointwise {n} {m} δ x
= transportRefl (thinₒ (NonStr→Orth (transp (λ i → n ⊑ₙ m) i0 δ)) (transp (λ j → Var n) i0 x))
∙ cong₂ thinₒ (cong NonStr→Orth (transportRefl δ)) (transportRefl x)
∙ NonStr→Orth-thin δ x
thinₙₜ≡thinₙ : (thinₙₜ {n} {m}) ≡ thinₙ
thinₙₜ≡thinₙ i δ x = thinₙₜ≡thinₙ-pointwise δ x i
thinₒ≡thinₙ : (λ i → Action n m (Orth≡NonStr i)) [ thinₒ ≡ thinₙ ]
thinₒ≡thinₙ = toPathP thinₙₜ≡thinₙThe HIT version is not much trickier, if any.
thinₕₜ : n ⊑ₕ m → Var n → Var m
thinₕₜ {n} {m} = subst (Action n m) Orth≡HIT thinₒ
HIT→Orth-thin : (δ : n ⊑ₕ m) (x : Var n) → thinₒ (HIT→Orth δ) x ≡ thinₕ δ x
HIT→Orth-thin idₕ x = thin-idₒ x
HIT→Orth-thin (skipₕ δ) x = cong vs (HIT→Orth-thin δ x)
HIT→Orth-thin (keepₕ δ) vz = refl
HIT→Orth-thin (keepₕ δ) (vs x) = cong vs (HIT→Orth-thin δ x)
HIT→Orth-thin (keep-id≡idₕ n i) vz = refl
HIT→Orth-thin (keep-id≡idₕ n i) (vs x) = cong vs (thin-idₒ x)
thinₕₜ≡thinₕ-pointwise : (δ : n ⊑ₕ m) (x : Var n) → thinₕₜ δ x ≡ thinₕ δ x
thinₕₜ≡thinₕ-pointwise {n} {m} δ x
= transportRefl (thinₒ (HIT→Orth (transp (λ i → n ⊑ₕ m) i0 δ)) (transp (λ j → Var n) i0 x))
∙ cong₂ thinₒ (cong HIT→Orth (transportRefl δ)) (transportRefl x)
∙ HIT→Orth-thin δ x
thinₕₜ≡thinₕ : (thinₕₜ {n} {m}) ≡ thinₕ
thinₕₜ≡thinₕ i δ x = thinₕₜ≡thinₕ-pointwise δ x i
thinₒ≡thinₕ : (λ i → Action n m (Orth≡HIT i)) [ thinₒ ≡ thinₕ ]
thinₒ≡thinₕ = toPathP thinₕₜ≡thinₕAt the end we have three variants of thinnings with identity and composition, and which act on variables the same way.
Now, if we prove properties of these operations, e.g. identity laws, composition associativity, or that composition and action commute, it would be enough to prove these for the orthodox implementation, then we can simply transport the proofs.
In other words, whatever we prove about one structure will hold for two others, like idₕ-unique in previous section.
Some proofs are simple:
but we can get them through the equality anyway:
thin-idₕ' : (x : Var n) → thinₕ idₕ x ≡ x
thin-idₕ' {n} x = subst
{A = Σ _ (λ _⊑_ → Action n n _⊑_ × (n ⊑ n))} -- structure
(λ { (_⊑_ , thin , id) → thin id x ≡ x }) -- motif
(λ i → Orth≡HIT i , thinₒ≡thinₕ i , CatOps-Orth≡HIT i .fst) -- proof that structures are equal
(thin-idₒ x) -- proof to transport
?
?
type with extra information about names bound by definitions. As usual, let 
denote a generic context, that is, a finite mapping from variable names to their types. Then we extend the 
and produces global bindings for some names whose types are recorded in 
as an abbreviation for 
.) So, for example, 
, but rather something like 
, representing the fact that although 
.
. But should the context associated to a command type always contain polytypes, or only when the command type is itself a polytype? In other words, how do we deal with the associated contexts in the monotypes that show up during type inference? And what would it mean to unify two command types with their contexts (and would that ever even be necessary)? I hope it’s actually simple and I just need to think about it some more, but I haven’t wrapped my brain around it yet.
alternatives for the 2 choices of each of 
unknowns (prior to composing). This uses 
which we write as 
and so 
, 
and 
.
but we can rescale at any time.)
