open import 1Lab.Path.IdentitySystem
open import 1Lab.Function.Embedding
open import 1Lab.HLevel.Closure
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
open import Data.Irr

open import Meta.Idiom

import Data.Nat.Base as Nat

module Data.Fin.Base where

Finite sets🔗

The type $Fin (n)$ is the type with exactly $n$ elements. We define it as a record type, packaging a natural number $k$ with a proof that $k < n .$

record Fin (n : Nat) : Type where
  constructor fin
  field
    lower       : Nat
    ⦃ bounded ⦄ : Irr (lower Nat.< n)

While the type $k < n$ is a homotopy proposition, we would like to enforce that constructions on $Fin (n)$ definitionally do not depend on the given proof. Therefore, we have wrapped it in Irr.

In dependent type theory, it’s common to instead define the finite sets as an inductive family indexed over Nat. However, in cubical type theory, there is a good reason to avoid inductive families: they have subst as an additional constructor, including along constant paths. This makes the normal form of any expression involving substitution in an indexed family, even if the thing being transported is a constructor form, very bad.

Instead, we would like the subst operation on Fin to definitionally commute with the constructors, and (if possible) to definitionally preserve the underlying numeric value. Defining Fin as an indexed type with an irrelevant proof field achieves exactly this. Moreover, if we’re substituting over a loop, even at a neutral number, transport at Fin is definitionally the identity function.

private
  cast : ∀ {m n} → m ≡ n → Fin m → Fin n
  cast p (fin n ⦃ i ⦄) = record
    { lower   = n
    ; bounded = subst (n Nat.<_) p <$> i
    }

  _ : ∀ {m n} {p : m ≡ n} {x : Fin m} → subst Fin p x ≡ cast p x
  _ = refl

  _ : ∀ {m} {p : m ≡ m} {x : Fin m} → subst Fin p x ≡ x
  _ = refl

open Data.Irr using (make-irr) public
open Fin using (lower) public

pattern fzero = fin zero

We can still prove that the definition above is equivalent to an inductive family. In particular, it’s generated by the “constructors” fzero and fsuc.

_ : ∀ {n} → Fin (suc n)
_ = fzero

fsuc : ∀ {n} → Fin n → Fin (suc n)
fsuc (fin n ⦃ x ⦄) = fin (suc n) ⦃ Nat.s≤s <$> x ⦄

from-nat : ∀ (n : Nat) → Fin (suc n)
from-nat zero = fzero
from-nat (suc n) = fsuc (from-nat n)

module _ {m n : Nat} (p : m ≡ n) (x : Fin m) where
  _ : subst (Fin ∘ suc) p (fsuc x) ≡ fsuc (subst Fin p x)
  _ = refl

  _ : subst (Fin ∘ suc) p fzero ≡ fzero
  _ = refl

Viewing elements of a finite set🔗

Agda has good support, through the with abstraction, to pretend that a type is inductively generated. We therefore expose a type Fin-view which allows us to discriminate on whether an element of $Fin (n)$ is fzero or fsuc.

data Fin-view : {n : Nat} → Fin n → Type where
  zero : ∀ {n}             → Fin-view {suc n} fzero
  suc  : ∀ {n} (i : Fin n) → Fin-view {suc n} (fsuc i)

Of course, this family has a section, expressing that any finite number is generated by one of the two “constructors”.

fin-view : ∀ {n} (i : Fin n) → Fin-view i
fin-view {suc n} fzero               = zero
fin-view {suc n} (fin (suc i) ⦃ b ⦄) = suc (fin i ⦃ Nat.≤-peel <$> b ⦄)

fin-view {zero}  (fin _ ⦃ forget i ⦄) = absurd (Nat.¬suc≤0 i)

As a first application, we can prove that Fin 0 is empty:

Fin-absurd : Fin 0 → ⊥
Fin-absurd i with fin-view i
... | ()

We can also define an elimination principle for the family $Fin (-),$ which applies the view at “every level”.

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 i with fin-view i
... | zero  = pfzero
... | suc i = pfsuc i (Fin-elim P pfzero pfsuc i)

fin-ap : ∀ {n : I → Nat} {x : Fin (n i0)} {y : Fin (n i1)} → x .lower ≡ y .lower → PathP (λ i → Fin (n i)) x y
fin-ap {n = n} {fin i ⦃ q ⦄} {fin j ⦃ r ⦄} s k = fin (s k) ⦃ is-prop→pathp (λ k → hlevel {T = Irr (s k Nat.< n k)} 1) q r k ⦄

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} k with fin-view k
... | vzero = inl fzero
strengthen {n = suc n} k with fin-view k
... | zero  = inr fzero
... | suc 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 n with fin-view n
... | zero  = fzero
... | suc 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 p (fin n ⦃ b ⦄) = fin n ⦃ (λ e → Nat.≤-trans e p) <$> b ⦄

As a subset of the natural numbers🔗

We can also view Fin as a subset of the natural numbers.

Fin↪Nat : ∀ {n} → Fin n ↪ Nat
Fin↪Nat .fst = lower
Fin↪Nat .snd = injective→is-embedding (hlevel 2) lower fin-ap

Discreteness🔗

Since the finite set of size $n$ is a subset of the natural numbers, which have decidable equality, it follows that $Fin (n)$ also has decidable equality.

instance
  Discrete-Fin : ∀ {n} → Discrete (Fin n)
  Discrete-Fin .decide x y with x .lower ≡? y .lower
  ... | yes p = yes (fin-ap p)
  ... | no ¬p = no λ p → ¬p (ap lower p)

In particular, Hedberg’s theorem shows that $Fin (n)$ is a set.

opaque
  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

However, we can also mimic parts of the proof that Nat itself is discrete, and obtain useful combinators for reasoning with finite sets. For example, the zero element in $Fin (1 + n)$ is never equal to a successor:

fzero≠fsuc : ∀ {n k p} → ¬ Path (Fin (suc n)) fzero (fin (suc k) ⦃ p ⦄)
fzero≠fsuc p = Nat.zero≠suc (ap lower p)

fsuc≠fzero : ∀ {n k p} → ¬ Path (Fin (suc n)) (fin (suc k) ⦃ p ⦄) fzero
fsuc≠fzero p = Nat.suc≠zero (ap lower p)

Moreover, since we can implement a “predecessor” operation, we get that fsuc is an injection.

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 n with fin-view n
  ... | zero  = fzero
  ... | suc i = i

instance
  Number-Fin : ∀ {n} → Number (Fin n)
  Number-Fin {n} .Number.Constraint k = k Nat.< n
  Number-Fin {n} .Number.fromNat k ⦃ e ⦄ = fin k ⦃ forget e ⦄

open import Data.Nat.Base using (0≤x ; s≤s') public

Fin-cases : ∀ {ℓ} {n} {P : Fin (suc n) → Type ℓ} → P 0 → (∀ x → P (fsuc x)) → ∀ x → P x
Fin-cases p0 ps n with fin-view n
... | zero  = p0
... | suc i = ps i

fin-cons  : ∀ {ℓ} {n} {P : Fin (suc n) → Type ℓ} → P 0 → (∀ x → P (fsuc x)) → ∀ x → P x
fin-cons = Fin-cases

fin-nil : ∀ {ℓ} {P : Fin 0 → Type ℓ} → ∀ x → P x
fin-nil x = absurd (Fin-absurd 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 means that any lemmas about the ordering on natural numbers apply immediately to the ordering on standard finite sets.

_≤_ : ∀ {n} → Fin n → Fin n → Type
i ≤ j = i .lower Nat.≤ j .lower
infix 7 _≤_

_<_ : ∀ {n} → Fin n → Fin n → Type
i < j = i .lower Nat.< j .lower
infix 7 _<_

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 n k with fin-view n | fin-view k
... | zero  | zero  = fzero
... | zero  | suc j = j
... | suc i | zero  = fzero
... | suc i | suc j = fsuc (squish i j)

skip : ∀ {n} → Fin (suc n) → Fin n → Fin (suc n)
skip n k with fin-view n
... | zero = fsuc k
... | suc i with fin-view k
... | zero = fzero
... | suc j = fsuc (skip i j)

Arithmetic🔗

split-+ : ∀ {m n} → Fin (m + n) → Fin m ⊎ Fin n
split-+ {m = zero} i = inr i
split-+ {m = suc m} k with fin-view k
... | zero  = inl fzero
... | suc i = ⊎-map fsuc id (split-+ i)

avoid : ∀ {n} (i j : Fin (suc n)) → i ≠ j → Fin n
avoid {n = n} i j i≠j with fin-view i | fin-view j
... | zero  | zero  = absurd (i≠j refl)
... | zero  | suc j = j
avoid {n = suc n} _ _ i≠j | suc i | zero  = fzero
avoid {n = suc n} _ _ i≠j | suc i | suc j = fsuc (avoid i j (i≠j ∘ ap fsuc))

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 = n} i with fin-view i
opposite {n = suc n} _ | zero  = from-nat n
opposite {n = suc n} _ | suc i = weaken (opposite i)

Vector operations🔗

_[_≔_]
  : ∀ {ℓ} {A : Type ℓ} {n}
  → (Fin n → A) → Fin (suc n) → A
  → Fin (suc n) → A
_[_≔_] {n = n} ρ i a j with fin-view i | fin-view j
_[_≔_] {n = n} ρ fzero a fzero             | zero  | zero  = a
_[_≔_] {n = n} ρ fzero a .(fsuc j)         | zero  | suc j = ρ j
_[_≔_] {n = suc n} ρ .(fsuc i) a .fzero    | suc i | zero  = ρ fzero
_[_≔_] {n = suc n} ρ .(fsuc i) a .(fsuc j) | suc i | suc j = ((ρ ∘ fsuc) [ i ≔ a ]) j

delete
  : ∀ {ℓ} {A : Type ℓ} {n}
  → (Fin (suc n) → A) → Fin (suc n)
  → Fin n → A
delete ρ i j = ρ (skip i j)