module Data.Fin.Closure where
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)) ββ