------------------------------------------------------------------------
-- Universe-level⁻
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
open import Graded.Modality
open import Graded.Mode

module Definition.Typed.Decidable.Internal.Universe-level
  {a} {M : Set a} {𝕄 : Modality M}
  (TR : Type-restrictions 𝕄)
  where

open import Definition.Untyped M
open import Definition.Untyped.Sup TR

open import Definition.Typed TR
open import Definition.Typed.Inversion TR
open import Definition.Typed.Properties.Admissible.Level TR
open import Definition.Typed.Properties.Well-formed TR
open import Definition.Typed.Reasoning.Level TR
open import Definition.Typed.Well-formed TR

open import Tools.Function
open import Tools.Nat as N
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Relation

private variable
  n : Nat
  Ξ“ : Cons _ _

------------------------------------------------------------------------
-- The type

-- Universe-level without the top-most element.

data Universe-level⁻ : Set where
  0ᡘ+ Ο‰α΅˜+ : (m : Nat) β†’ Universe-level⁻

private variable
  β„“ ℓ₁ β„“β‚‚ : Universe-level⁻

opaque

  -- The semantics of Universe-level⁻.

  ⌜_⌝⁻ : Universe-level⁻ β†’ Lvl n
  ⌜ 0ᡘ+ m ⌝⁻ = level (β†“α΅˜ m)
  ⌜ Ο‰α΅˜+ m ⌝⁻ = Ο‰α΅˜+ m

------------------------------------------------------------------------
-- _β‰Ÿ_

-- Equality is decidable for Universe-level⁻.

_β‰Ÿβ»_ : (ℓ₁ β„“β‚‚ : Universe-level⁻) β†’ Dec (ℓ₁ PE.≑ β„“β‚‚)
0ᡘ+ m₁ β‰Ÿβ» 0ᡘ+ mβ‚‚ =
  Dec-map (PE.cong 0ᡘ+ , (Ξ» { PE.refl β†’ PE.refl })) (m₁ N.β‰Ÿ mβ‚‚)
0ᡘ+ _  β‰Ÿβ» Ο‰α΅˜+ _  = no (Ξ» ())
Ο‰α΅˜+ _  β‰Ÿβ» 0ᡘ+ _  = no (Ξ» ())
Ο‰α΅˜+ m₁ β‰Ÿβ» Ο‰α΅˜+ mβ‚‚ =
  Dec-map (PE.cong Ο‰α΅˜+ , (Ξ» { PE.refl β†’ PE.refl })) (m₁ N.β‰Ÿ mβ‚‚)

------------------------------------------------------------------------
-- 1+⁻

-- A successor operation for Universe-level⁻.

1+⁻ : Universe-level⁻ β†’ Universe-level⁻
1+⁻ (0ᡘ+ m) = 0ᡘ+ (1+ m)
1+⁻ (Ο‰α΅˜+ m) = Ο‰α΅˜+ (1+ m)

opaque
  unfolding ⌜_⌝⁻ β†“α΅˜_

  -- ⌜_⌝⁻ commutes with 1+⁻/1ᡘ+ (for well-formed levels).

  ⊒⌜1+β»βŒβ»β‰‘ :
    Ξ“ ⊒ ⌜ β„“ ⌝⁻ ∷Level β†’
    Ξ“ ⊒ ⌜ 1+⁻ β„“ ⌝⁻ ≑ 1ᡘ+ ⌜ β„“ ⌝⁻ ∷Level
  ⊒⌜1+β»βŒβ»β‰‘ {β„“ = 0ᡘ+ _} βŠ’β„“ = refl-βŠ’β‰‘βˆ·L (⊒1ᡘ+ βŠ’β„“)
  ⊒⌜1+β»βŒβ»β‰‘ {β„“ = Ο‰α΅˜+ _} βŠ’β„“ = refl-βŠ’β‰‘βˆ·L (⊒1ᡘ+ βŠ’β„“)

------------------------------------------------------------------------
-- _βŠ”β»_

-- Max for Universe-level⁻.

infixl 6 _βŠ”β»_

_βŠ”β»_ : (_ _ : Universe-level⁻) β†’ Universe-level⁻
0ᡘ+ m βŠ”β» 0ᡘ+ n = 0ᡘ+ (m βŠ” n)
0ᡘ+ _ βŠ”β» Ο‰α΅˜+ n = Ο‰α΅˜+ n
Ο‰α΅˜+ m βŠ”β» 0ᡘ+ _ = Ο‰α΅˜+ m
Ο‰α΅˜+ m βŠ”β» Ο‰α΅˜+ n = Ο‰α΅˜+ (m βŠ” n)

opaque
  unfolding ⌜_⌝⁻ _supα΅˜β‚—_

  -- ⌜_⌝⁻ commutes with _βŠ”β»_/_supα΅˜β‚—_ (for well-formed levels).

  βŠ’βŒœβŠ”β»βŒβ»β‰‘ :
    Ξ“ ⊒ ⌜ ℓ₁ ⌝⁻ ∷Level β†’
    Ξ“ ⊒ ⌜ β„“β‚‚ ⌝⁻ ∷Level β†’
    Ξ“ ⊒ ⌜ ℓ₁ βŠ”β» β„“β‚‚ ⌝⁻ ≑ ⌜ ℓ₁ ⌝⁻ supα΅˜β‚— ⌜ β„“β‚‚ ⌝⁻ ∷Level
  βŠ’βŒœβŠ”β»βŒβ»β‰‘ {ℓ₁ = 0ᡘ+ m₁} {β„“β‚‚ = 0ᡘ+ mβ‚‚} βŠ’β„“β‚ _ =
    level (β†“α΅˜ (m₁ N.βŠ” mβ‚‚))             β‰‘Λ˜βŸ¨ supα΅˜β‚—-β†“α΅˜ (wfLevel βŠ’β„“β‚) ⟩⊒∎
    level (β†“α΅˜ m₁) supα΅˜β‚— level (β†“α΅˜ mβ‚‚)  ∎
  βŠ’βŒœβŠ”β»βŒβ»β‰‘ {ℓ₁ = 0ᡘ+ _} {β„“β‚‚ = Ο‰α΅˜+ mβ‚‚} _ βŠ’β„“β‚‚ =
    Ο‰α΅˜+ mβ‚‚  ∎⟨ uncurry βŠ’Ο‰α΅˜+ (inversion-Ο‰α΅˜+ βŠ’β„“β‚‚) ⟩⊒
  βŠ’βŒœβŠ”β»βŒβ»β‰‘ {ℓ₁ = Ο‰α΅˜+ m₁} {β„“β‚‚ = 0ᡘ+ _} βŠ’β„“β‚ _ =
    Ο‰α΅˜+ m₁  ∎⟨ uncurry βŠ’Ο‰α΅˜+ (inversion-Ο‰α΅˜+ βŠ’β„“β‚) ⟩⊒
  βŠ’βŒœβŠ”β»βŒβ»β‰‘ {ℓ₁ = Ο‰α΅˜+ m₁} {β„“β‚‚ = Ο‰α΅˜+ mβ‚‚} βŠ’β„“β‚ _ =
    Ο‰α΅˜+ (m₁ N.βŠ” mβ‚‚)  ∎⟨ uncurry βŠ’Ο‰α΅˜+ (inversion-Ο‰α΅˜+ βŠ’β„“β‚) ⟩⊒

opaque
  unfolding ⌜_⌝⁻

  -- βŒœΒ β„“β‚Β βŠ”β»Β β„“β‚‚Β βŒβ» is well-formed if βŒœΒ β„“β‚Β βŒβ» and βŒœΒ β„“β‚‚Β βŒβ» are (for the
  -- same context).

  ⊒⌜⌝⁻ :
    Ξ“ ⊒ ⌜ ℓ₁ ⌝⁻ ∷Level β†’
    Ξ“ ⊒ ⌜ β„“β‚‚ ⌝⁻ ∷Level β†’
    Ξ“ ⊒ ⌜ ℓ₁ βŠ”β» β„“β‚‚ ⌝⁻ ∷Level
  ⊒⌜⌝⁻ βŠ’β„“β‚ βŠ’β„“β‚‚ = wf-βŠ’β‰‘βˆ·L (βŠ’βŒœβŠ”β»βŒβ»β‰‘ βŠ’β„“β‚ βŠ’β„“β‚‚) .proj₁

------------------------------------------------------------------------
-- _≀⁻_

opaque

  -- An ordering relation for Universe-level⁻.

  infix 4 _≀⁻_

  _≀⁻_ : Universe-level⁻ β†’ Universe-level⁻ β†’ Set
  ℓ₁ ≀⁻ β„“β‚‚ = ℓ₁ βŠ”β» β„“β‚‚ PE.≑ β„“β‚‚

opaque
  unfolding _≀⁻_

  -- Reflexivity.

  ≀⁻-refl : β„“ ≀⁻ β„“
  ≀⁻-refl {β„“ = 0ᡘ+ _} = PE.cong 0ᡘ+ (N.βŠ”-idem _)
  ≀⁻-refl {β„“ = Ο‰α΅˜+ _} = PE.cong Ο‰α΅˜+ (N.βŠ”-idem _)