Standard Finite Types Properties

Table of Contents

1 Fin Properties

module Lib.Prop.Fin where

This file states and shows more properties about finite types.

1.1 Packages imports

The imported packages can be accessed via the following links: 

import Lib.Data.Fin
import Lib.Prop.Coprod
import Lib.Prop.Equiv
import Lib.Prop.Nat

1.2 Fin k + l is Fin k + Fin l

The proof is easy by induction on l. 

Fin/Equiv-add-copr (k : Nat) : (l : Nat) → (Equiv (Fin (plus-Nat k l)) (Coprod (Fin k) (Fin l))) = split
  zero → Equiv/sym (Coprod (Fin k) Empty) (Fin k) (Equiv/Equiv-copr-type-empty (Fin k))
  suc l → Equiv/trans (Fin (plus-Nat k (suc l))) (Coprod (Coprod (Fin k) (Fin l)) Unit) (Coprod (Fin k) (Fin (suc l)))
                                                 (Coprod/closed-Equiv (Fin (plus-Nat k l)) (Coprod (Fin k) (Fin l)) Unit Unit
                                                                      (Fin/Equiv-add-copr k l) (Equiv/refl Unit))
                                                 (Coprod/assoc (Fin k) (Fin l) Unit)

1.3 Relation to classical Fin

The classical version of Fin is defined as a Σ-type Σ(x: Nat)x < k for Fin k. There's an equivalence between the classical version of the standard finite type and the classical finite type. 

classical-Fin : Nat → U =
  λk. Σ Nat (λx. Prop/type (lt x k))

First, we define the inclusion map from Fin k to Nat. 

Fin/inclusion' (k : Nat) (f : Fin k → Nat) : Fin (suc k) → Nat = split
  inl x → f x
  inr s → k

Fin/inclusion : (k : Nat) → Fin k → Nat = split
  zero → ex-falso Nat
  suc k → Fin/inclusion' k (Fin/inclusion k)

For any x in Fin k, we obviously have that inclusion(x) < k. 

Fin/inclusion/lt' (k : Nat) (H : (x : Fin k) → Prop/type (lt (Fin/inclusion k x) k))
                     : (x : Fin (suc k)) → Prop/type (lt (Fin/inclusion (suc k) x) (suc k)) = split
  inl x → lt/suc-right (Fin/inclusion k x) k (H x)
  inr s → lt/next k

Fin/inclusion/lt : (k : Nat) → (x : Fin k) → Prop/type (lt (Fin/inclusion k x) k) = split
  zero → λx. ex-falso (Prop/type (lt (Fin/inclusion zero x) zero)) x
  suc k → Fin/inclusion/lt' k (Fin/inclusion/lt k)

Hence, the inclusion function induces a map from Fin k to classical-Fin k. 

classical-Fin/from-Fin (k : Nat) (x : Fin k) : classical-Fin k =
  ( Fin/inclusion k x, Fin/inclusion/lt k x)

We show that there's a map from classical-Fin to Fin. 

Fin/from-classical-Fin' (k : Nat) (x : classical-Fin (suc k)) (f : classical-Fin k → Fin k)
                           : Coprod (Path Nat x.1 k) (neg (Path Nat x.1 k)) → Fin (suc k) = split
  inl _ → inr star
  inr np → inl (f (x.1, le-neq-lt x.1 k x.2 np))

Fin/from-classical-Fin : (k : Nat) (x : classical-Fin k) → Fin k = split
  zero → λx. x.2
  suc k → λx. Fin/from-classical-Fin' k x (Fin/from-classical-Fin k) (Nat/has-decidable-eq x.1 k)

These maps are inverse to each other, as witnessed by the right homotopy: 

Fin-classical-Fin/right-htpy' (k : Nat) (x : classical-Fin (suc k))
                              (IH : (x' : classical-Fin k)
                                   → Path (classical-Fin k) (classical-Fin/from-Fin k (Fin/from-classical-Fin k x')) x')
                                  : (u : Coprod (Path Nat x.1 k) (neg (Path Nat x.1 k)))
                                   → Path (Coprod (Path Nat x.1 k) (neg (Path Nat x.1 k))) (Nat/has-decidable-eq x.1 k) u
                                   → Path (classical-Fin (suc k)) (classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin (suc k) x)) x = split
  inl p →
    λq.
      let r : Path (classical-Fin (suc k))
                   (classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin (suc k) x))
                   (classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin' k x (Fin/from-classical-Fin k) (inl p))) =
            ( ap (Coprod (Path Nat x.1 k) (neg (Path Nat x.1 k))) (classical-Fin (suc k))
                 (λr'. classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin' k x (Fin/from-classical-Fin k) r'))
                 (Nat/has-decidable-eq x.1 k) (inl p) q) in
      SgPath-prop Nat
        ( λz. Prop/type (lt z (suc k)))
        ( λz. Prop/is-prop (lt z (suc k)))
        ( classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin (suc k) x)) x
        ( comp Nat
          ( classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin (suc k) x)).1
          ( classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin' k x (Fin/from-classical-Fin k) (inl p))).1
          ( λi. (r i).1)
          x.1 (inv Nat x.1 k p))
  inr np →
    λp.
      let x' : classical-Fin k = (x.1, le-neq-lt x.1 k x.2 np)
          q : Path (classical-Fin k) (classical-Fin/from-Fin k (Fin/from-classical-Fin k x')) x' = IH x'
          r : Path (Fin (suc k)) (Fin/from-classical-Fin (suc k) x) (inl (Fin/from-classical-Fin k x'))
                    = ap (Coprod (Path Nat x.1 k) (neg (Path Nat x.1 k))) (Fin (suc k))
                         (λu. Fin/from-classical-Fin' k x (Fin/from-classical-Fin k) u)
                         (Nat/has-decidable-eq x.1 k) (inr np) p
          s : Path (classical-Fin (suc k))
                   (classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin (suc k) x))
                   (classical-Fin/from-Fin (suc k) (inl (Fin/from-classical-Fin k x')))
                    = ap (Fin (suc k)) (classical-Fin (suc k)) (classical-Fin/from-Fin (suc k))
                         (Fin/from-classical-Fin (suc k) x) (inl (Fin/from-classical-Fin k x')) r
      in
      SgPath-prop Nat
        ( λz. Prop/type (lt z (suc k)))
        ( λz. Prop/is-prop (lt z (suc k)))
        ( classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin (suc k) x)) x
        ( comp Nat
          ( classical-Fin/from-Fin (suc k) (Fin/from-classical-Fin (suc k) x)).1
          ( classical-Fin/from-Fin (suc k) (inl (Fin/from-classical-Fin k x'))).1
          ( λi. (s i).1)
          x.1 (λi. (q i).1))

Fin-classical-Fin/right-htpy : (k : Nat) → (x : classical-Fin k)
                              → Path (classical-Fin k) (classical-Fin/from-Fin k (Fin/from-classical-Fin k x)) x = split
  zero → λx. ex-falso (Path (classical-Fin zero) (classical-Fin/from-Fin zero (Fin/from-classical-Fin zero x)) x) x.2
  suc k → λx. Fin-classical-Fin/right-htpy' k x (Fin-classical-Fin/right-htpy k)
              ( Nat/has-decidable-eq x.1 k)
              ( refl (Coprod (Path Nat x.1 k) (neg (Path Nat x.1 k))) (Nat/has-decidable-eq x.1 k))

and the left homotopy: 

lock Coprod/Eq/map
Fin-classical-Fin/left-htpy'' (k : Nat) (s : Unit)
                                 : (u : Coprod (Path Nat (classical-Fin/from-Fin (suc k) (inr s)).1 k) (neg (Path Nat (classical-Fin/from-Fin (suc k) (inr s)).1 k)))
                                  → Path (Coprod (Path Nat (classical-Fin/from-Fin (suc k) (inr s)).1 k) (neg (Path Nat (classical-Fin/from-Fin (suc k) (inr s)).1 k)))
                                         (Nat/has-decidable-eq (classical-Fin/from-Fin (suc k) (inr s)).1 k) u
                                  → Path (Fin (suc k)) (Fin/from-classical-Fin (suc k) (classical-Fin/from-Fin (suc k) (inr s))) (inr s) = split
  inl p → λq.
    let x : classical-Fin (suc k) = (classical-Fin/from-Fin (suc k) (inr s)) in
    comp
      ( Fin (suc k))
      ( Fin/from-classical-Fin (suc k) x)
      ( Fin/from-classical-Fin' k x (Fin/from-classical-Fin k) (inl p))
      ( ap (Coprod (Path Nat x.1 k) (neg (Path Nat x.1 k))) (Fin (suc k))
           (Fin/from-classical-Fin' k x (Fin/from-classical-Fin k))
           (Nat/has-decidable-eq x.1 k) (inl p) q)
      ( inr s)
      ( Coprod/Eq/map
        ( Fin k) Unit
        ( inr star)
        ( inr s)
        ( Unit/all-elements-equal star s))
  inr np → λ_.
    ex-falso
      ( Path (Fin (suc k)) (Fin/from-classical-Fin (suc k) (classical-Fin/from-Fin (suc k) (inr s))) (inr s))
      ( np (refl Nat k))

Fin-classical-Fin/left-htpy/inl (k : Nat) (IH : (x : Fin k) → Path (Fin k) (Fin/from-classical-Fin k (classical-Fin/from-Fin k x)) x)
                                (x : Fin k)
                                   : (u : Coprod (Path Nat (classical-Fin/from-Fin (suc k) (inl x)).1 k) (neg (Path Nat (classical-Fin/from-Fin (suc k) (inl x)).1 k)))
                                    → Path (Coprod (Path Nat (classical-Fin/from-Fin (suc k) (inl x)).1 k) (neg (Path Nat (classical-Fin/from-Fin (suc k) (inl x)).1 k)))
                                           (Nat/has-decidable-eq (classical-Fin/from-Fin (suc k) (inl x)).1 k) u
                                    → Path (Fin (suc k)) (Fin/from-classical-Fin (suc k) (classical-Fin/from-Fin (suc k) (inl x))) (inl x) = split
  inl p → λ_.
    let x' : classical-Fin k = (classical-Fin/from-Fin k x) in
    ex-falso
      ( Path (Fin (suc k)) (Fin/from-classical-Fin (suc k) (classical-Fin/from-Fin (suc k) (inl x))) (inl x))
      ( lt-neq x'.1 k x'.2 p)
  inr np → λq.
   let x' : classical-Fin (suc k) = (classical-Fin/from-Fin (suc k) (inl x)) in
    comp-n 
    ( Fin (suc k)) three-Nat
    ( Fin/from-classical-Fin (suc k) x')
    ( Fin/from-classical-Fin' k x' (Fin/from-classical-Fin k) (inr np))
    ( ap (Coprod (Path Nat x'.1 k) (neg (Path Nat x'.1 k))) (Fin (suc k))
         (Fin/from-classical-Fin' k x' (Fin/from-classical-Fin k))
         (Nat/has-decidable-eq x'.1 k) (inr np) q)
    ( inl (Fin/from-classical-Fin k (classical-Fin/from-Fin k x)))
    ( Coprod/Eq/map
      ( Fin k) Unit
      ( Fin/from-classical-Fin' k x' (Fin/from-classical-Fin k) (inr np))
      ( inl (Fin/from-classical-Fin k (classical-Fin/from-Fin k x)))
      ( ap (classical-Fin k) (Fin k) (Fin/from-classical-Fin k)
           (x'.1, le-neq-lt x'.1 k x'.2 np) (classical-Fin/from-Fin k x)
           (SgPath-prop Nat
              ( λn. Prop/type (lt n k))
              ( λn. Prop/is-prop (lt n k))
              ( x'.1, le-neq-lt x'.1 k x'.2 np)
              ( classical-Fin/from-Fin k x)
              ( refl Nat x'.1))))
    ( inl x)
    ( Coprod/Eq/map
      ( Fin k) Unit
      ( inl (Fin/from-classical-Fin k (classical-Fin/from-Fin k x)))
      ( inl x)
      ( IH x))

Fin-classical-Fin/left-htpy' (k : Nat) (IH : (x : Fin k) → Path (Fin k) (Fin/from-classical-Fin k (classical-Fin/from-Fin k x)) x)
                                : (x : Fin (suc k))
                                 → Path (Fin (suc k)) (Fin/from-classical-Fin (suc k) (classical-Fin/from-Fin (suc k) x)) x = split
  inl x →
    Fin-classical-Fin/left-htpy/inl k IH x
    ( Nat/has-decidable-eq (classical-Fin/from-Fin (suc k) (inl x)).1 k)
    ( refl (Coprod (Path Nat (classical-Fin/from-Fin (suc k) (inl x)).1 k) (neg (Path Nat (classical-Fin/from-Fin (suc k) (inl x)).1 k)))
      ( Nat/has-decidable-eq (classical-Fin/from-Fin (suc k) (inl x)).1 k))
  inr s →
    Fin-classical-Fin/left-htpy'' k s
      ( Nat/has-decidable-eq (classical-Fin/from-Fin (suc k) (inr s)).1 k)
      ( refl (Coprod (Path Nat (classical-Fin/from-Fin (suc k) (inr s)).1 k) (neg (Path Nat (classical-Fin/from-Fin (suc k) (inr s)).1 k)))
        ( Nat/has-decidable-eq (classical-Fin/from-Fin (suc k) (inr s)).1 k))

Fin-classical-Fin/left-htpy : (k : Nat) → (x : Fin k)
                             → Path (Fin k) (Fin/from-classical-Fin k (classical-Fin/from-Fin k x)) x = split
  zero → λx. ex-falso (Path Empty (Fin/from-classical-Fin zero (classical-Fin/from-Fin zero x)) x) x
  suc k → Fin-classical-Fin/left-htpy' k (Fin-classical-Fin/left-htpy k)

Equivalence: 

Fin-is-classical-Fin (k : Nat) : Equiv (Fin k) (classical-Fin k) =
  has-inverse/Equiv
    ( Fin k)
    ( classical-Fin k)
    ( classical-Fin/from-Fin k)
    ( Fin/from-classical-Fin k,
      ( Fin-classical-Fin/right-htpy k,
        Fin-classical-Fin/left-htpy k))

classical-Fin-is-Fin (k : Nat) : Equiv (classical-Fin k) (Fin k) =
  has-inverse/Equiv
    ( classical-Fin k)
    ( Fin k)
    ( Fin/from-classical-Fin k)
    ( classical-Fin/from-Fin k,
      ( Fin-classical-Fin/left-htpy k,
        Fin-classical-Fin/right-htpy k))

From this equivalence, we can deduce that Fin k is equivalent to a family indexed over the natural numbers. 

Fin-Nat-family (k : Nat) (P : Fin k → U) : Nat → U =
  λn.
    Σ ( Prop/type (lt n k))
      (λp. P ( Fin/from-classical-Fin k ( n, p)))

Fin-Nat-family/Equiv (k : Nat) (P : Fin k → U) : Equiv (Σ (Fin k) P) (Σ Nat (Fin-Nat-family k P)) =
  Equiv/trans
    ( Σ (Fin k) P)
    ( Σ (classical-Fin k) (λx. P (Fin/from-classical-Fin k x)))
    ( Σ Nat (Fin-Nat-family k P))
    ( Sg/equiv-base'
      ( classical-Fin k)
      ( Fin k) P
      ( classical-Fin-is-Fin k))
    ( Equiv/associative-Sg' Nat
      ( λn. Prop/type (lt n k))
      ( λn p. P (Fin/from-classical-Fin k (n, p))))

Author: Johann Rosain

Created: 2024-07-23 Tue 13:51

Validate