{-# OPTIONS --safe #-}

-- Definition of Fin n in terms of the inductively defined <

module Cubical.Data.Fin.Inductive.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Nat.Order.Inductive
open import Cubical.Data.Empty as 
open import Cubical.Data.Unit

open import Cubical.Relation.Nullary

-- Fin defined using <ᵗ
Fin : (n : )  Type
Fin n = Σ[ m   ] (m <ᵗ n)

fsuc : {n : }  Fin n  Fin (suc n)
fst (fsuc {n = n} (x , p)) = suc x
snd (fsuc {n = suc n} (x , p)) = p

injectSuc : {n : }  Fin n  Fin (suc n)
fst (injectSuc {n = n} (x , p)) = x
snd (injectSuc {n = suc n} (x , p)) = <ᵗ-trans-suc {n = x} p

flast : {m : }  Fin (suc m)
fst (flast {m = m}) = m
snd (flast {m = m}) = <ᵗsucm {m = m}

fzero : {m : }  Fin (suc m)
fzero = 0 , tt

fone :  {m}  Fin (suc (suc m))
fone {m} = suc zero , tt

-- Sums
sumFinGen :  {} {A : Type } {n : }
  (_+_ : A  A  A) (0A : A) (f : Fin n  A)  A
sumFinGen {n = zero} _+_ 0A f = 0A
sumFinGen {n = suc n} _+_ 0A f =
  f flast + (sumFinGen {n = n}) _+_ 0A (f  injectSuc)