Category of contexts and context-renamings

contexts.lagda.md

{-# OPTIONS --without-K #-}

open import foundation.functions using (_∘_)
open import foundation.identity-types using (refl; ap) renaming (Id to _≡_)

Contexts

We think of contexts as snoc lists of types

infixl 28 _,_
data Ctx (A : Set) : Set where
  ε : Ctx A
  _,_ : Ctx A → A → Ctx A

DeBruijn Indices

Contexts have the notion of a membership denoted with ∈:

infix 26 _∈_
data _∈_ {U : Set} (A : U) : Ctx U → Set where
  zero : {Γ : Ctx U} → A ∈ (Γ , A)
  suc : {Γ : Ctx U} {B : U} → (A ∈ Γ) → (A ∈ Γ , B)

The constructor zero refers to the type of the topmost-bound variable in the context, while suc adds a new bound variable and thus increases the index of the original variable by one. This encodes exactly deBruijn indices to assign a type for every bound variable in scope with a clean nameless representation.

Context Renaming

We also give contexts the notion of a sublist relation ⊆:

infix 27 _⊆_
data _⊆_ {U : Set} : Ctx U → Ctx U → Set where
  ε-refl : ε ⊆ ε
  lift : {Γ Δ : Ctx U} {A : U} → Γ ⊆ Δ → (Γ , A) ⊆ (Δ , A)
  weak : {Γ Δ : Ctx U} {A : U} → Γ ⊆ Δ → Γ ⊆ (Δ , A)

• The empty list is a sublist of itself.
• Adding the same element to sublists keeps them sublists.
• Adding an element to the containing list keeps it containing the sublist.

This relation implies a renaming of every variable in the domain to a new variable in the codomain, which can also be interpreted as a var-to-var substitution.

Context Renamings Form a Category

By starting from ε-refl and repeatedly applying lift we can show reflexivity of ⊆ for contexts of any size:

id : {U : Set} {Γ : Ctx U} → Γ ⊆ Γ
id {Γ = ε} = ε-refl
id {Γ = Γ , A} = lift id

which allows us to define singleton weakening

wk : {U : Set} (A : U) {Γ : Ctx U} → Γ ⊆ Γ , A
wk A = weak id

We can also show transitivity by defining a composition operation

infix 26 _⨟_
_⨟_ : {U : Set} {Γ Δ Φ : Ctx U} → Γ ⊆ Δ → Δ ⊆ Φ → Γ ⊆ Φ
ε-refl ⨟ q = q
lift p ⨟ lift q = lift (p ⨟ q)
weak p ⨟ lift q = weak (p ⨟ q)
lift p ⨟ weak q = weak (lift p ⨟ q)
weak p ⨟ weak q = weak (weak p ⨟ q)

These definitions indeed form a category

id-⨟ : {U : Set} {Γ Δ : Ctx U} (p : Γ ⊆ Δ) → id ⨟ p ≡ p
id-⨟ ε-refl = refl
id-⨟ (lift p) = ap lift (id-⨟ p)
id-⨟ {Γ = ε} (weak p) = refl
id-⨟ {Γ = Γ , x} (weak p) = ap weak (id-⨟ p)

⨟-id : {U : Set} {Γ Δ : Ctx U} (p : Γ ⊆ Δ) → p ⨟ id ≡ p
⨟-id ε-refl = refl
⨟-id (lift p) = ap lift (⨟-id p)
⨟-id (weak p) = ap weak (⨟-id p)

⨟-assoc : {U : Set} {Γ Δ Φ Ω : Ctx U} (p : Γ ⊆ Δ) (q : Δ ⊆ Φ) (r : Φ ⊆ Ω) →
  (p ⨟ q) ⨟ r ≡ p ⨟ (q ⨟ r)
⨟-assoc ε-refl q r = refl
⨟-assoc (lift p) (lift q) (lift r) = ap lift (⨟-assoc p q r)
⨟-assoc (lift p) (lift q) (weak r) = ap weak (⨟-assoc (lift p) (lift q) r)
⨟-assoc (lift p) (weak q) (lift r) = ap weak (⨟-assoc (lift p) q r)
⨟-assoc (lift p) (weak q) (weak r) = ap weak (⨟-assoc (lift p) (weak q) r)
⨟-assoc (weak p) (lift q) (lift r) = ap weak (⨟-assoc p q r)
⨟-assoc (weak p) (lift q) (weak r) = ap weak (⨟-assoc (weak p) (lift q) r)
⨟-assoc (weak p) (weak q) (lift r) = ap weak (⨟-assoc (weak p) q r)
⨟-assoc (weak p) (weak q) (weak r) = ap weak (⨟-assoc (weak p) (weak q) r)

Presheaf Structure

The partial application A∈_ for any fixed A : U is a mapping Ctx U → Set, which happens to be a functor from the category Ctx U we just formed to Set (aka presheaf over (Ctx U)ᵒᵖ). That functor maps a context Γ : Ctx U to a Set A ∈ Γ which represents the membership of A in Γ (witnessed by the deBruijn index of A). The functor needs to send a morphism Γ ⊆ Δ to some function A ∈ Γ → A ∈ Δ. Indeed, Γ ⊆ Δ means that every variable that appears in Γ also appears somewhere in Δ. So given a variable of type A at some index in Γ, we can also find its index in Δ with the following function:

reindex : {U : Set} {A : U} {Γ Δ : Ctx U} →
  Γ ⊆ Δ → A ∈ Γ → A ∈ Δ
reindex (lift p) zero = zero
reindex (lift p) (suc i) = suc (reindex p i)
reindex (weak p) i = suc (reindex p i)

and this definition satisfies the functor laws:

reindex-id : {U : Set} {A : U} {Γ : Ctx U} (i : A ∈ Γ) →
  reindex id i ≡ i
reindex-id zero = refl
reindex-id (suc i) = ap suc (reindex-id i)

reindex-⨟ : {U : Set} {A : U} {Γ Δ Φ : Ctx U} (p : Γ ⊆ Δ) (q : Δ ⊆ Φ) (i : A ∈ Γ) →
  reindex q (reindex p i) ≡ reindex (p ⨟ q) i
reindex-⨟ (lift p) (lift q) zero = refl
reindex-⨟ (lift p) (lift q) (suc i) = ap suc (reindex-⨟ p q i)
reindex-⨟ (lift p) (weak q) i = ap suc (reindex-⨟ (lift p) q i)
reindex-⨟ (weak p) (lift q) i = ap suc (reindex-⨟ p q i)
reindex-⨟ (weak p) (weak q) i = ap suc (reindex-⨟ (weak p) q i)