\begin{code}

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

module MLTT.Fin where

open import MLTT.Spartan
open import MLTT.List
open import MLTT.Bool

data Fin : β„• β†’ 𝓀₀ Μ‡ where
 𝟎   : {n : β„•} β†’ Fin (succ n)
 suc : {n : β„•} β†’ Fin n β†’ Fin (succ n)

β„•-to-Fin : (n : β„•) β†’ Fin (succ n)
β„•-to-Fin 0        = 𝟎
β„•-to-Fin (succ n) = suc (β„•-to-Fin n)

pattern 𝟏 = suc 𝟎
pattern 𝟐 = suc 𝟏
pattern πŸ‘ = suc 𝟐
pattern πŸ’ = suc πŸ‘
pattern πŸ“ = suc πŸ’
pattern πŸ” = suc πŸ“
pattern πŸ• = suc πŸ”
pattern πŸ– = suc πŸ•
pattern πŸ— = suc πŸ–

is-nonzero : β„• β†’ 𝓀₀ Μ‡
is-nonzero 0        = 𝟘
is-nonzero (succ n) = πŸ™

Fin-gives-is-nonzero : {n : β„•} β†’ Fin n β†’ is-nonzero n
Fin-gives-is-nonzero 𝟎       = ⋆
Fin-gives-is-nonzero (suc i) = ⋆

Fin-0-is-empty : Β¬ Fin 0
Fin-0-is-empty = Fin-gives-is-nonzero

is-𝟎 : {n : β„•} β†’ Fin n β†’ 𝓀₀ Μ‡
is-𝟎 𝟎       = πŸ™
is-𝟎 (suc _) = 𝟘

𝟎-is-not-suc : {n : β„•} (i : Fin n) β†’ 𝟎 β‰  suc i
𝟎-is-not-suc i p = transport is-𝟎 p ⋆

pred : {n : β„•} β†’ Fin n β†’ Fin (succ n) β†’ Fin n
pred i 𝟎       = i
pred i (suc k) = k

suc-lc : {n : β„•} {i j : Fin n} β†’ suc i ＝ suc j β†’ i ＝ j
suc-lc {n} {i} = ap (pred i)

list-Fin : (n : β„•) β†’ List (Fin n)
list-Fin 0        = []
list-Fin (succ n) = 𝟎 ∷ map suc (list-Fin n)

list-Fin-correct : (n : β„•) (i : Fin n) β†’ member i (list-Fin n)
list-Fin-correct 0        i       = 𝟘-elim (Fin-0-is-empty i)
list-Fin-correct (succ n) 𝟎       = in-head
list-Fin-correct (succ n) (suc i) = in-tail g
 where
  IH : member i (list-Fin n)
  IH = list-Fin-correct n i

  g : member (suc i) (map suc (list-Fin n))
  g = member-map suc i (list-Fin n) IH

Fin-listed : (n : β„•) β†’ listed (Fin n)
Fin-listed n = list-Fin n , list-Fin-correct n

Fin-listed⁺ : (n : β„•) β†’ listed⁺ (Fin (succ n))
Fin-listed⁺ n = 𝟎 , Fin-listed (succ n)

Fin-== : {n : β„•} β†’ Fin n β†’ Fin n β†’ Bool
Fin-== {0}      x       y       = 𝟘-elim (Fin-0-is-empty x)
Fin-== {succ n} (suc x) (suc y) = Fin-== {n} x y
Fin-== {succ n} (suc x) 𝟎       = false
Fin-== {succ n} 𝟎       (suc y) = false
Fin-== {succ n} 𝟎       𝟎       = true

Fin-refl : {n : β„•} (x : Fin n) β†’ (Fin-== x x) ＝ true
Fin-refl {0}      x       = 𝟘-elim (Fin-0-is-empty x)
Fin-refl {succ n} (suc x) = Fin-refl {n} x
Fin-refl {succ n} 𝟎       = refl

module _ {n : β„•} where
 instance
  eqFin : Eq (Fin n)
  _==_    {{eqFin}} = Fin-== {n}
  ==-refl {{eqFin}} = Fin-refl {n}

\end{code}