open import 1Lab.Prelude

open import Data.Fin.Base
open import Data.Sum

module Data.Fin.Closure where

private variable
  β„“ : Level
  A B C : Type β„“
  k l m n : Nat

Closure of finite setsπŸ”—

In this module, we prove that the finite sets are closed under β€œtypal arithmetic”: The initial and terminal objects are finite (they have 1 and 0 elements respectively), products of finite sets are finite, coproducts of finite sets are finite, and functions between finite sets are finite. Moreover, these operations all correspond to arithmetic operations on the natural number indices: etc.

Zero, one, successorsπŸ”—

The finite set is an initial object, and the finite set is a terminal object:

Finite-zero-is-initial : Fin 0 ≃ βŠ₯
Finite-zero-is-initial .fst ()
Finite-zero-is-initial .snd .is-eqv ()

Finite-one-is-contr : is-contr (Fin 1)
Finite-one-is-contr .centre = fzero
Finite-one-is-contr .paths fzero = refl

The successor operation on indices corresponds to taking coproducts with the unit set.

Finite-successor : Fin (suc n) ≃ (⊀ ⊎ Fin n)
Finite-successor {n} = Iso→Equiv (f , iso g rinv linv) where
  f : Fin (suc n) β†’ ⊀ ⊎ Fin n
  f fzero = inl tt
  f (fsuc x) = inr x

  g : ⊀ ⊎ Fin n β†’ Fin (suc n)
  g (inr x) = fsuc x
  g (inl _) = fzero

  rinv : is-right-inverse g f
  rinv (inr _) = refl
  rinv (inl _) = refl

  linv : is-left-inverse g f
  linv fzero = refl
  linv (fsuc x) = refl

We can also phrase this equivalence in a particularly strong way, which applies to dependent types over finite successor types:

Fin-suc-Ξ 
  : βˆ€ {β„“} {n} {A : Fin (suc n) β†’ Type β„“}
  β†’ (βˆ€ x β†’ A x) ≃ (A fzero Γ— (βˆ€ x β†’ A (fsuc x)))
Fin-suc-Π = Iso→Equiv λ where
  .fst f β†’ f fzero , (Ξ» x β†’ f (fsuc x))

  .snd .is-iso.inv (z , f) fzero    β†’ z
  .snd .is-iso.inv (z , f) (fsuc x) β†’ f x

  .snd .is-iso.rinv x β†’ refl

  .snd .is-iso.linv k i fzero    β†’ k fzero
  .snd .is-iso.linv k i (fsuc n) β†’ k (fsuc n)

Fin-suc-Ξ£
  : βˆ€ {β„“} {n} {A : Fin (suc n) β†’ Type β„“}
  β†’ Ξ£ (Fin (suc n)) A ≃ (A fzero ⊎ Ξ£ (Fin n) (A ∘ fsuc))
Fin-suc-Σ = Iso→Equiv λ where
  .fst (fzero , a) β†’ inl a
  .fst (fsuc x , a) β†’ inr (x , a)

  .snd .is-iso.inv (inl a) β†’ fzero , a
  .snd .is-iso.inv (inr (x , a)) β†’ fsuc x , a

  .snd .is-iso.rinv (inl _) β†’ refl
  .snd .is-iso.rinv (inr _) β†’ refl

  .snd .is-iso.linv (fzero , a) β†’ refl
  .snd .is-iso.linv (fsuc x , a) β†’ refl

AdditionπŸ”—

For binary coproducts, we prove the correspondence with addition in steps, to make the proof clearer:

Finite-coproduct : (Fin n ⊎ Fin m) ≃ Fin (n + m)
Finite-coproduct {zero} {m}  =
  (Fin 0 ⊎ Fin m) β‰ƒβŸ¨ ⊎-apl Finite-zero-is-initial βŸ©β‰ƒ
  (βŠ₯ ⊎ Fin m)     β‰ƒβŸ¨ ⊎-zerol βŸ©β‰ƒ
  Fin m           β‰ƒβˆŽ
Finite-coproduct {suc n} {m} =
  (Fin (suc n) ⊎ Fin m) β‰ƒβŸ¨ ⊎-apl Finite-successor βŸ©β‰ƒ
  ((⊀ ⊎ Fin n) ⊎ Fin m) β‰ƒβŸ¨ ⊎-assoc βŸ©β‰ƒ
  (⊀ ⊎ (Fin n ⊎ Fin m)) β‰ƒβŸ¨ ⊎-apr (Finite-coproduct {n} {m}) βŸ©β‰ƒ
  (⊀ ⊎ Fin (n + m))     β‰ƒβŸ¨ Finite-successor e⁻¹ βŸ©β‰ƒ
  Fin (suc (n + m))     β‰ƒβˆŽ

SumsπŸ”—

We also have a correspondence between β€œcoproducts” and β€œaddition” in the iterated case: If you have a family of finite types (represented by a map to their cardinalities), the dependent sum of that family is equivalent to the iterated binary sum of the cardinalities:

sum : βˆ€ n β†’ (Fin n β†’ Nat) β†’ Nat
sum zero f = zero
sum (suc n) f = f fzero + sum n (f ∘ fsuc)

Finite-sum : (B : Fin n β†’ Nat) β†’ Ξ£ (Fin _) (Fin ∘ B) ≃ Fin (sum n B)
Finite-sum {zero} B .fst ()
Finite-sum {zero} B .snd .is-eqv ()
Finite-sum {suc n} B =
  Ξ£ (Fin (suc n)) (Fin ∘ B)              β‰ƒβŸ¨ Fin-suc-Ξ£ βŸ©β‰ƒ
  Fin (B 0) ⊎ Ξ£ (Fin n) (Fin ∘ B ∘ fsuc) β‰ƒβŸ¨ ⊎-apr (Finite-sum (B ∘ fsuc)) βŸ©β‰ƒ
  Fin (B 0) ⊎ Fin (sum n (B ∘ fsuc))     β‰ƒβŸ¨ Finite-coproduct βŸ©β‰ƒ
  Fin (sum (suc n) B)                    β‰ƒβˆŽ

MultiplicationπŸ”—

Recall (from middle school) that the product is the same thing as summing together copies of the number Correspondingly, we can use the theorem above for general sums to establish the case of binary products:

Finite-multiply : (Fin n Γ— Fin m) ≃ Fin (n * m)
Finite-multiply {n} {m} =
  (Fin n Γ— Fin m)       β‰ƒβŸ¨ Finite-sum (Ξ» _ β†’ m) βŸ©β‰ƒ
  Fin (sum n (Ξ» _ β†’ m)) β‰ƒβŸ¨ cast (sum≑* n m) , cast-is-equiv _ βŸ©β‰ƒ
  Fin (n * m)           β‰ƒβˆŽ
  where
    sum≑* : βˆ€ n m β†’ sum n (Ξ» _ β†’ m) ≑ n * m
    sum≑* zero m = refl
    sum≑* (suc n) m = ap (m +_) (sum≑* n m)

ProductsπŸ”—

Similarly to the case for sums, the cardinality of a dependent product of finite sets is the product of the cardinalities:

product : βˆ€ n β†’ (Fin n β†’ Nat) β†’ Nat
product zero f = 1
product (suc n) f = f fzero * product n (f ∘ fsuc)

Finite-product : (B : Fin n β†’ Nat) β†’ (βˆ€ x β†’ Fin (B x)) ≃ Fin (product n B)
Finite-product {zero} B .fst _ = fzero
Finite-product {zero} B .snd = is-iso→is-equiv λ where
  .is-iso.inv _ ()
  .is-iso.rinv fzero β†’ refl
  .is-iso.linv _ β†’ funext Ξ» ()
Finite-product {suc n} B =
  (βˆ€ x β†’ Fin (B x))                          β‰ƒβŸ¨ Fin-suc-Ξ  βŸ©β‰ƒ
  Fin (B fzero) Γ— (βˆ€ x β†’ Fin (B (fsuc x)))   β‰ƒβŸ¨ Ξ£-ap-snd (Ξ» _ β†’ Finite-product (B ∘ fsuc)) βŸ©β‰ƒ
  Fin (B fzero) Γ— Fin (product n (B ∘ fsuc)) β‰ƒβŸ¨ Finite-multiply βŸ©β‰ƒ
  Fin (B fzero * product n (B ∘ fsuc))       β‰ƒβˆŽ