Martin Escardo, sometime between 2014 and 2021

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Fin.Properties where

open import UF.Subsingletons

open import Factorial.PlusOneLC
open import Fin.Type
open import MLTT.Spartan
open import MLTT.Unit-Properties
open import UF.Equiv

\end{code}

The largest element of Fin (succ n) is ⟪ n ⟫ (TODO: formulate and prove this).

\begin{code}

⟪_⟫ : (n : )  Fin (succ n)
 0       = fzero
 succ n  = fsucc  n 

Fin0-is-empty : is-empty (Fin 0)
Fin0-is-empty i = i

Fin1-is-singleton : is-singleton (Fin 1)
Fin1-is-singleton = 𝟎 , γ
 where
  γ : (i : Fin 1)  𝟎  i
  γ 𝟎 = refl

Fin0-is-prop : is-prop (Fin 0)
Fin0-is-prop i = 𝟘-elim i

Fin1-is-prop : is-prop (Fin 1)
Fin1-is-prop 𝟎 𝟎 = refl

positive-not-𝟎 : {n : } {x : Fin n}  fsucc x  𝟎
positive-not-𝟎 {0}      {x} p = 𝟘-elim x
positive-not-𝟎 {succ n} {x} p = 𝟙-is-not-𝟘 (g p)
 where
  f : Fin (succ (succ n))  𝓤₀ ̇
  f 𝟎       = 𝟘
  f (suc x) = 𝟙

  g : suc x  𝟎  𝟙  𝟘
  g = ap f

when-Fin-is-prop : (n : )  is-prop (Fin n)  (n  0) + (n  1)
when-Fin-is-prop 0               i = inl refl
when-Fin-is-prop 1               i = inr refl
when-Fin-is-prop (succ (succ n)) i = 𝟘-elim (positive-not-𝟎 (i 𝟏 𝟎))

when-Fin-is-singleton : (n : )  is-singleton (Fin n)  n  1
when-Fin-is-singleton 0               ()
when-Fin-is-singleton (succ 0)        _           = refl
when-Fin-is-singleton (succ (succ n)) (𝟎 , c)     = 𝟘-elim (positive-not-𝟎 ((c 𝟏)⁻¹))
when-Fin-is-singleton (succ (succ n)) (suc k , c) = 𝟘-elim (positive-not-𝟎 (c 𝟎))

\end{code}

The left cancellability of Fin uses the construction +𝟙-cancellable
defined in the module PlusOneLC.lagda.

\begin{code}

Fin-lc : (m n : )  Fin m  Fin n  m  n
Fin-lc 0           0       p = refl
Fin-lc (succ m)    0       p = 𝟘-elim ( p  𝟎)
Fin-lc 0          (succ n) p = 𝟘-elim ( p ⌝⁻¹ 𝟎)
Fin-lc (succ m)   (succ n) p = ap succ r
 where
  IH : Fin m  Fin n  m  n
  IH = Fin-lc m n

  remark : Fin m + 𝟙  Fin n + 𝟙
  remark = p

  q : Fin m  Fin n
  q = +𝟙-cancellable p

  r : m  n
  r = IH q

\end{code}

Notice that Fin is an example of a map that is left-cancellable but
not an embedding in the sense of univalent mathematics.