module Data.Fin.Base where
Finite Setsπ
The type Fin is the type of size n
.
These are defined as an inductive family over Nat, such that
Fin 0
has 0 elements, Fin 1
has 1 element, and
so on.
Another way to view Fin is that
itβs the type of numbers less than some upper bound. For instance,
fsuc fzero
is of type Fin 3
, but will
not typecheck as a Fin 1
!
data Fin : Nat β Type where fzero : β {n} β Fin (suc n) fsuc : β {n} β Fin n β Fin (suc n)
Keeping with the perspective of Fin as a type of bounded natural numbers, we provide conversion functions going back and forth.
from-nat : β (n : Nat) β Fin (suc n) from-nat zero = fzero from-nat (suc n) = fsuc (from-nat n) to-nat : β {n : Nat} β Fin n β Nat to-nat fzero = zero to-nat (fsuc i) = suc (to-nat i)
A note of caution: because of some β¨technical reasonsβ¨ cubical agda cannot handle transports over indexed inductive types very well. Instead, we define a function cast that computes on the indices of Fin, rather than on the path.
cast : β {m n} β m β‘ n β Fin m β Fin n cast {suc m} {zero} p fzero = absurd (Nat.zeroβ suc (sym p)) cast {suc m} {suc n} p fzero = fzero cast {suc m} {zero} p (fsuc i) = absurd (Nat.zeroβ suc (sym p)) cast {suc m} {suc n} p (fsuc i) = fsuc (cast (Nat.suc-inj p) i)
cast-is-equiv : β {m n} (p : m β‘ n) β is-equiv (cast p) cast-is-equiv = J (Ξ» _ p β is-equiv (cast p)) cast-refl-is-equiv where idβ‘cast-refl : β {n} β id β‘ cast (Ξ» _ β n) idβ‘cast-refl {zero} i () idβ‘cast-refl {suc n} i fzero = fzero idβ‘cast-refl {suc n} i (fsuc x) = fsuc (idβ‘cast-refl {n} i x) cast-refl-is-equiv : β {n} β is-equiv (cast (Ξ» i β n)) cast-refl-is-equiv = subst is-equiv idβ‘cast-refl id-equiv
Next, we move on to one of the most useful functions for Fin: strength
. This allows us
to (possibly) strengthen the upper bound on some Fin n
.
strengthen : β {n} β Fin (suc n) β Fin (suc n) β Fin n strengthen {n = zero} fzero = inl fzero strengthen {n = suc n} fzero = inr fzero strengthen {n = suc n} (fsuc i) = β-map fsuc fsuc (strengthen i)
On the other hand, weaken does
the opposite: it relaxes the upper bound on some Fin n
,
allowing us to regard it as a Fin (suc n)
.
weaken : β {n} β Fin n β Fin (suc n) weaken fzero = fzero weaken (fsuc i) = fsuc (weaken i)
We can also relax the upper bounds if m β€ n
.
inject : β {m n} β m Nat.β€ n β Fin m β Fin n inject {_} {suc n} le fzero = fzero inject {_} {suc n} (Nat.sβ€s le) (fsuc i) = fsuc (inject le i)
Discretenessπ
The proof here mirrors the one found in Data.Nat.Base
, just with some
slight tweaks required to handle the indexing.
We begin by showing that one can distinguish zero from successor:
fzeroβ fsuc : β {n} {i : Fin n} β Β¬ fzero β‘ fsuc i fzeroβ fsuc {n = n} path = subst distinguish path tt where distinguish : Fin (suc n) β Type distinguish fzero = β€ 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 is well
typed!
fsuc-inj : β {n} {i j : Fin n} β fsuc i β‘ fsuc j β i β‘ j fsuc-inj {n = suc n} p = ap pred p where pred : Fin (suc (suc n)) β Fin (suc n) pred fzero = fzero pred (fsuc i) = i
Finally, we pull everything together to show that Fin is Discrete. This is not exactly a shock (after all, Nat is discrete), but itβs useful nonetheless!
Discreteα΅’-Fin : β {n} β Discreteα΅’ (Fin n) Discreteα΅’-Fin fzero fzero = yes reflα΅’ Discreteα΅’-Fin fzero (fsuc j) = no Ξ» () Discreteα΅’-Fin (fsuc i) fzero = no Ξ» () Discreteα΅’-Fin (fsuc i) (fsuc j) with Discreteα΅’-Fin i j ... | yes reflα΅’ = yes reflα΅’ ... | no Β¬iβ‘j = no Ξ» { reflα΅’ β Β¬iβ‘j reflα΅’ } Discrete-Fin : β {n} β Discrete (Fin n) Discrete-Fin = Discreteα΅’βdiscrete Discreteα΅’-Fin
Hedbergβs theorem implies that Fin is a set, i.e., it only has trivial paths.
Fin-is-set : β {n} β is-set (Fin n) Fin-is-set = Discreteβis-set Discrete-Fin instance H-Level-Fin : β {n k} β H-Level (Fin n) (2 + k) H-Level-Fin = basic-instance 2 Fin-is-set
instance Number-Fin : β {n} β Number (Fin n) Number-Fin {n} .Number.Constraint k = k Nat.< n Number-Fin {n} .Number.fromNat k {{e}} = go k n e where go : β k n β k Nat.< n β Fin n go zero (suc n) e = fzero go (suc k) (suc n) (Nat.sβ€s e) = fsuc (go k n e) open import Data.Nat.Base using (0β€x ; sβ€sβ²) public Fin-elim : β {β} (P : β {n} β Fin n β Type β) β (β {n} β P {suc n} fzero) β (β {i} (j : Fin i) β P j β P (fsuc j)) β β {n} (i : Fin n) β P i Fin-elim P pfzero pfsuc fzero = pfzero Fin-elim P pfzero pfsuc (fsuc x) = pfsuc x (Fin-elim P pfzero pfsuc x)
Orderingπ
Keeping with the view that Fin represents
the type of bounded natural numbers, we can re-use the ordering on Nat to induce an ordering on Fin. This lets us repurpose any lemmas on β€
to also operate on
Fin.
_β€_ : β {n} β Fin n β Fin n β Type i β€ j = to-nat i Nat.β€ to-nat j infix 3 _β€_ _<_ : β {n} β Fin n β Fin n β Type i < j = to-nat i Nat.< to-nat j infix 3 _<_
Next, we define a pair of functions squish and
skip, which are the building blocks for
all monotone functions between Fin.
squish i
takes a j : Fin (suc n)
to a
Fin n
by mapping both i
and i+1
to i
. Its counterpart skip i
takes some
j : Fin n
to a Fin (suc n)
by skipping over
i
instead.
squish : β {n} β Fin n β Fin (suc n) β Fin n squish fzero fzero = fzero squish fzero (fsuc j) = j squish (fsuc i) fzero = fzero squish (fsuc i) (fsuc j) = fsuc (squish i j) skip : β {n} β Fin (suc n) β Fin n β Fin (suc n) skip fzero j = fsuc j skip (fsuc i) fzero = fzero skip (fsuc i) (fsuc j) = fsuc (skip i j)
As a subsetπ
While Fin is very conveniently defined as an indexed family of types, it can also be defined as a subset of the natural numbers: Namely, the finite ordinal is the same type as as . This makes sense! Any set with elements is equivalent to any other set with elements, and a very canonical choice is the first values of .
β< : Nat β Type β< x = Ξ£[ n β Nat ] (n Nat.< x) from-β< : β {n} β β< n β Fin n from-β< {n = suc n} (zero , q) = fzero from-β< {n = suc n} (suc p , Nat.sβ€s q) = fsuc (from-β< (p , q)) to-β< : β {n} β Fin n β β< n to-β< x = to-nat x , p x where p : β {n} (x : Fin n) β suc (to-nat x) Nat.β€ n p {n = suc n} fzero = Nat.sβ€s Nat.0β€x p {n = suc n} (fsuc x) = Nat.sβ€s (p x)
Arithmeticπ
weaken-β€ : β {m n} β m Nat.β€ n β Fin m β Fin n weaken-β€ {suc m} {suc n} mβ€n fzero = fzero weaken-β€ {suc m} {suc n} (Nat.sβ€s mβ€n) (fsuc i) = fsuc (weaken-β€ mβ€n i) fshift : β {n} (m : Nat) β Fin n β Fin (m + n) fshift zero i = i fshift (suc m) i = fsuc (fshift m i) opposite : β {n} β Fin n β Fin n opposite {n = suc n} fzero = from-nat n opposite {n = suc n} (fsuc i) = weaken (opposite i)