open import 1Lab.Path.IdentitySystem
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 is the type with exactly elements. We define it as a record type, packaging a natural number with a proof that 

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

While the type is a homotopy proposition, we would like to enforce that constructions on 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 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 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 ⦄

DiscretenessπŸ”—

Since the finite set of size is a subset of the natural numbers, which have decidable equality, it follows that 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 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 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)