open import 1Lab.Path.IdentitySystem open import 1Lab.HLevel.Retracts open import 1Lab.Type.Sigma open import 1Lab.HLevel open import 1Lab.Equiv open import 1Lab.Path open import 1Lab.Type open import Data.Dec.Base open import Data.Sum.Base open import Data.Id.Base import Data.Nat.Base as Nat 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)
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
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)