\begin{code}
{-# OPTIONS --safe #-}

module Data.Fin where

open import Level
open import Data.Nat
open import Data.Sigma

private
  variable n : ℕ

module DisplayDef where
  open import Data.Empty using (⊥)
  open import Data.Unit  using (⊤)
  open import Data.Sum   using (_⊎_)
\end{code}
%<*fin-display-def>
\begin{code}
  Fin : ℕ → Type
  Fin zero     = ⊥
  Fin (suc n)  = ⊤ ⊎ Fin n
\end{code}
%</fin-display-def>
\begin{code}
data Fin : ℕ → Type where
  zero  : Fin (suc n)
  suc   : Fin n → Fin (suc n)

open import Decidable
open import Data.Bool
open import Path

module DiscreteFin where
  _≡ᴮ_ : Fin n → Fin n → Bool
  zero  ≡ᴮ zero  = true
  suc x ≡ᴮ suc y = x ≡ᴮ y
  _     ≡ᴮ _     = false

  sound : (x y : Fin n) → T (x ≡ᴮ y) → x ≡ y
  sound zero    zero    p = refl
  sound (suc x) (suc y) p = cong suc (sound x y p)

  complete : (x : Fin n) → T (x ≡ᴮ x)
  complete zero    = _
  complete (suc x) = complete x

discreteFin : Discrete (Fin n)
discreteFin = from-bool-eq record { DiscreteFin }

open import HLevels

isSetFin : isSet (Fin n)
isSetFin = Discrete→isSet discreteFin

open import Data.Nat.Order

FinFromℕ : ∀ m n → m < n → Fin n
FinFromℕ zero    (suc n) p = zero
FinFromℕ (suc m) (suc n) p = suc (FinFromℕ m n p)

FinToℕ : Fin n → Σ[ m ⦂ ℕ ] × m < n
FinToℕ zero    = zero , _
FinToℕ (suc x) = let x′ , p = FinToℕ x in suc x′ , p

open import Literals.Number

instance
  numberFin : ∀ {n} → Number (Fin n)
  numberFin {n} = record
    { Constraint = λ m → T (m <ᵇ n)
    ; fromNat    = λ m {{pr}} → FinFromℕ m n pr
    }

open import Data.Unit

_ : Fin 
_ = 

_ : Fin 
_ = 
\end{code}