The Standard Finite Type

1. Standard finite types

1 Standard finite types

module Lib.Data.Fin where

This file defines the standard finite types as done in [1, Def. 7.3.2] by recursion over the natural numbers.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Lib.Data.Decidability
import Lib.Data.Nat
import Lib.Prop.Coprod
import Lib.Prop.Unit

1.2 Definition

Fin : Nat → U = split
  zero → Empty
  suc k → Coprod (Fin k) Unit

1.3 Some elements of `Fin`, inclusion functions

zero-Fin : (k : Nat) → Fin (suc k) = split
  zero → inr star
  suc k' → inl (zero-Fin k')

Left and right inclusion functions.

Fin/i/left (k : Nat) (x : Fin k) : Fin (suc k) =
  inl x

Fin/i/right (k : Nat) (x : Unit) : Fin (suc k) =
  inr x

1.4 Properties

1.4.1 Observational equality

We build an observational equality Fin/Eq for the type Fin k such that there is a path between x, y : Fin k iff Fin/Eq x y.

Definition

We proceed by induction on k.

If k is 0, we have nothing to do as Fin 0 is Empty.
If k is suc k', then there are 4 cases.
- if x, y are star, then Fin/Eq x y is Unit ;
- if x is star and y is inl y' or x is inl x' and y is star, then Fin/Eq x y is Empty ;
- if x and y are both inl x' and inl y', then Fin/Eq x y is Fin/Eq x' y'.

Fin/Eq (k : Nat) (x : Fin k) (y : Fin k) : U =
  ind-Nat (λk'. Fin k' → Fin k' → U)
          (λx' _. ex-falso U x')
          (λk' r. ind-Coprod (Fin k') (Unit)
                     (λ_. Coprod (Fin k') (Unit) → U)
                     (λx'. ind-Coprod (Fin k') (Unit) (λ_. U) (λy'. r x' y') (λ_. Empty))
                     (λ_. ind-Coprod (Fin k') (Unit) (λ_. U) (λ_. Empty) (λ_. Unit)))
          k x y

Correspondance with Path

We show that, for x, y : Fin k, Fin/Eq x y iff Path (Fin k) x y. First, we show the "if" side. We only need to consider the cases where x, y are either both inl _ or both inr _ as otherwise, Fin/Eq x y is an element from Empty. If both are inl, the induction hypothesis on k suffices to conclude. Otherwise, both elements are star ; that is, x, y can be identified by reflexivity.

Fin/Eq/is-eq (k : Nat) (x y : Fin k) (e : Fin/Eq k x y) : Path (Fin k) x y =
  ind-Nat (λk'. (x' : Fin k') → (y' : Fin k') → Fin/Eq k' x' y' → Path (Fin k') x' y')
          (λx' y' _. ex-falso (Path Empty x' y') x')
          (λk' r. ind-Coprod (Fin k') (Unit)
                             (λx'. (y' : Fin (suc k')) → Fin/Eq (suc k') x' y' → Path (Fin (suc k')) x' y')
                             (λx'. ind-Coprod (Fin k') (Unit) (λy'. Fin/Eq (suc k') (inl x') y' → Path (Fin (suc k')) (inl x') y')
                                              (λy' e'. ap (Fin k') (Fin (suc k')) (Fin/i/left k') x' y' (r x' y' e'))
                                              (λy' e'. ex-falso (Path (Fin (suc k')) (inl x') (inr y')) e'))
                             (λx'. ind-Coprod (Fin k') (Unit) (λy'. Fin/Eq (suc k') (inr x') y' → Path (Fin (suc k')) (inr x') y')
                                              (λy' e'. ex-falso (Path (Fin (suc k')) (inr x') (inl y')) e')
                                              (λy' _. ap Unit (Fin (suc k')) (Fin/i/right k') x' y' (Unit/all-elements-equal x' y'))))
          k x y e

Conversely, we start by showing that Fin/Eq is reflexive by induction on k. If k is 0, there is nothing to do. Otherwise, there are two cases. Either x is inl x' and the induction hypothesis is enough to conclude, either x is inr star and we need to return something of type Unit, that is, we return star.

Fin/Eq/refl (k : Nat) (x : Fin k) : Fin/Eq k x x =
  ind-Nat (λk'. (x' : Fin k') → Fin/Eq k' x' x')
          (λx'. ex-falso (ex-falso U x') x')
          (λk' r x'. ind-Coprod (Fin k') (Unit)
                      (λx''. Fin/Eq (suc k') x'' x'')
                      (λl. r l)
                      (λ_. star) x') k x

Then, we can show the property by path-induction.

Fin/is-path-is-Eq (k : Nat) (x y : Fin k) (p : Path (Fin k) x y) : Fin/Eq k x y =
  J (Fin k) x (λy' _. Fin/Eq k x y')
    (Fin/Eq/refl k x) y p

1.4.2 Decidable equality

Fin k has a decidable equality. Indeed, the equality on Fin k is logically equivalent to Fin/Eq, that is defined as either Empty or Unit, that are decidable (as shown in decidability).

Fin/Eq-decidable (k : Nat) (x y : Fin k) : is-decidable (Fin/Eq k x y) =
  ind-Nat (λk'. (x' : Fin k') → (y' : Fin k') → is-decidable (Fin/Eq k' x' y'))
          (λx' y'. ex-falso (is-decidable (Fin/Eq zero x' y')) x')
          (λk' r. ind-Coprod (Fin k') (Unit)
                             (λx'. (y' : Fin (suc k')) → is-decidable (Fin/Eq (suc k') x' y'))
                             (λx'. ind-Coprod (Fin k') (Unit)
                                              (λy'. is-decidable (Fin/Eq (suc k') (inl x') y'))
                                              (λy'. r x' y')
                                              (λy'. is-decidable/Empty))
                             (λx'. ind-Coprod (Fin k') (Unit)
                                              (λy'. is-decidable (Fin/Eq (suc k') (inr x') y'))
                                              (λy'. is-decidable/Empty)
                                              (λy'. is-decidable/Unit))) k x y

Hence, as Fin/Eq is equivalent to the equality on Fin k, it is also decidable.

Fin/decidable-eq (k : Nat) : has-decidable-equality (Fin k) =
  λx y. Coprod/map (Fin/Eq k x y) (neg (Fin/Eq k x y)) (Path (Fin k) x y) (neg (Path (Fin k) x y))
          (Fin/Eq/is-eq k x y)
          (λf p. f (Fin/is-path-is-Eq k x y p))
          (Fin/Eq-decidable k x y)

1.4.3 `Fin 1` is contractible.

As Fin 1 has only one element, it is contractible.

Fin/fin-one-is-contr-contr : (y : Fin one-Nat) → Path (Fin one-Nat) (inr star) y = split
  inl e → ex-falso (Path (Fin one-Nat) (inr star) (inl e)) e
  inr s → ind-Unit (λz. Path (Fin one-Nat) (inr star) (inr z))
                   (refl (Fin one-Nat) (inr star)) s

Fin/fin-one-is-contr : is-contr (Fin one-Nat) =
  (inr star, Fin/fin-one-is-contr-contr)