module Size where
open import Prelude public
open import ThinSemiCategory public
open import WellFoundedRelations public
record Size (κ : Set) : Set₁ where
infixr 6 _⊔ˢ_
field
{{thin}} : Thin κ
Oˢ : κ
_⊔ˢ_ : κ → κ → κ
<⊔ˢl : {i j : κ} → i < i ⊔ˢ j
<⊔ˢr : {i j : κ} → j < i ⊔ˢ j
<iswf : wf.iswf {A = κ} _<_
↑ˢ : κ → κ
↑ˢ i = i ⊔ˢ i
<↑ˢ : {i : κ} → i < ↑ˢ i
<↑ˢ = <⊔ˢl
<ᵇ⊔ˢ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 #-}
<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)))