\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 πŸ–

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 (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-== {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 {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}