module Size where

open import Prelude public
open import ThinSemiCategory public
open import WellFoundedRelations public

----------------------------------------------------------------------
-- Types of size
----------------------------------------------------------------------
record Size (κ : Set) : Set₁ where
  infixr  _⊔ˢ_
  field
    -- Types of sizes are thin semi-categories
    {{thin}} :  Thin κ
    -- whose edge relation is directed
    Oˢ   : κ
    _⊔ˢ_ : κ → κ → κ
    <⊔ˢl : {i j : κ} → i < i ⊔ˢ j
    <⊔ˢr : {i j : κ} → j < i ⊔ˢ j
    -- and well-founded
    <iswf : wf.iswf {A = κ} _<_
  -- The derived strict successor operation
  ↑ˢ : κ → κ
  ↑ˢ i = i ⊔ˢ i
  <↑ˢ : {i : κ} → i < ↑ˢ i
  <↑ˢ = <⊔ˢl
  -- For use as instance arguements
  <ᵇ⊔ˢl : {i j : κ} → i <ᵇ i ⊔ˢ j
  <ᵇ⊔ˢl = <inst <⊔ˢl

  <ᵇ⊔ˢr : {i j : κ} → j <ᵇ i ⊔ˢ j
  <ᵇ⊔ˢr = <inst <⊔ˢr

  <ᵇ↑ˢ : {i : κ} → i <ᵇ ↑ˢ i
  <ᵇ↑ˢ = <inst <↑ˢ

open Size {{...}} public

{-# DISPLAY Size._⊔ˢ_ _ i j = i ⊔ˢ j #-}

-- Well-founded induction and recursion for a size
<ind :
  {κ : Set}
  {{_ : Size κ}}
  {n : Level}
  (P : κ → Prop n)
  (p : ∀ i → (∀ᵇ j < i , P j) → P i)
  → --------------------------------
  ∀ i → P i
<ind P p = wf.ind _<_ <iswf P
  (λ i h → p i (λ j {{j<ᵇi}} → h j (<prf j<ᵇi)))

<rec :
  {κ : Set}
  {{_ : Size κ}}
  {n : Level}
  (B : κ → Set n)
  (b : ∀ i → (∏ᵇ j < i , B j) → B i)
  → --------------------------------
  ∀ i → B i
<rec B b = wf.rec _<_ <iswf B
  (λ i h → b i (λ j {{j<ᵇi}} → h j (<prf j<ᵇi)))