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)

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 [n][n] is the same type as as {x:x<n}\{ x : x < n \}. This makes sense! Any set with nn elements is equivalent to any other set with nn elements, and a very canonical choice is the first nn values of N\mathbb{N}.

β„•< : 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)