Model.Nat

{-# OPTIONS --without-K #-}
module Model.Nat where

open import Model.Size as MS using
  ( Size ; Sizes ; _≤_ ; _<_ ; ≤-IsProp ; nat )
open import Model.Type.Core
open import Util.HoTT.HLevel
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using (Σ-≡⁺)

import Data.Nat.Properties as ℕ

open Size


ℕ≤ : Size → Set
ℕ≤ n = ∃[ m ] (nat m ≤ n)


ℕ≤-IsSet : ∀ {n} → IsSet (ℕ≤ n)
ℕ≤-IsSet = Σ-IsSet ℕ.≡-irrelevant λ m → IsOfHLevel-suc 1 ≤-IsProp


abstract
  ℕ≤-≡⁺ : ∀ {n} {m m′} (m≤n : nat m ≤ n) (m′≤n : nat m′ ≤ n)
    → m ≡ m′
    → (m , m≤n) ≡ (m′ , m′≤n)
  ℕ≤-≡⁺ _ _ m≡m′ = Σ-≡⁺ (m≡m′ , ≤-IsProp _ _)


Nat : ⟦Type⟧ Sizes
Nat = record
  { ObjHSet = λ n → HLevel⁺ (ℕ≤ n) ℕ≤-IsSet
  ; eqHProp = λ { _ (n , _) (m , _) → HLevel⁺ (n ≡ m) ℕ.≡-irrelevant }
  ; eq-refl = λ _ → refl
  }


castℕ≤ : ∀ {n m} → n ≤ m → ℕ≤ n → ℕ≤ m
castℕ≤ n≤m (k , k≤n) = k , go
  where abstract go = MS.≤-trans k≤n n≤m


zero≤ : ∀ n → ℕ≤ n
zero≤ n = 0 , MS.0≤n


suc≤ : ∀ n m → m < n → ℕ≤ m → ℕ≤ n
suc≤ n m m<n (x , x≤m) = suc x , MS.n<m→Sn≤m (MS.≤→<→< x≤m m<n)


caseℕ≤ : ∀ {α} {A : Set α} {n}
  → ℕ≤ n
  → A
  → (∀ m → m < n → ℕ≤ m → A)
  → A
caseℕ≤ (zero , _) z s = z
caseℕ≤ (suc x , Sx≤n) z s = s (nat x) (MS.Sn≤m→n<m Sx≤n) (x , MS.≤-refl)


caseℕ≤-pres : ∀ {α β γ} {A : Set α} {A′ : Set β} {n n′}
  → (R : A → A′ → Set γ)
  → (i : ℕ≤ n) (i′ : ℕ≤ n′)
  → (z : A) (z′ : A′)
  → (s : ∀ m → m < n → ℕ≤ m → A) (s′ : ∀ m → m < n′ → ℕ≤ m → A′)
  → proj₁ i ≡ proj₁ i′
  → R z z′
  → (∀ m m<n m′ m′<n′ j j′
      → proj₁ j ≡ proj₁ j′
      → R (s m m<n j) (s′ m′ m′<n′ j′))
  → R (caseℕ≤ i z s) (caseℕ≤ i′ z′ s′)
caseℕ≤-pres R (zero , _) (_ , _) z z′ s s′ refl zRz′ sRs′ = zRz′
caseℕ≤-pres R (suc i , _) (_ , _) z z′ s s′ refl zRz′ sRs′
  = sRs′ _ _ _ _ _ _ refl