{-# OPTIONS --safe #-}
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 : (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
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)