||| Provides definitions of proof-relevance and type universes.
module Obs.Universe

import Data.Bool
import Data.Bool.Decidable
import Data.Nat
import Data.Nat.Order.Properties
import Data.So

import Decidable.Equality

import Text.PrettyPrint.Prettyprinter

%default total

-- Definition ------------------------------------------------------------------

||| Proof relevance of terms
public export
data Relevance = Irrelevant | Relevant

%name Relevance r, r'

||| Type universes.
public export
data Universe : Type where
  ||| Impredicative universe of strict propositions.
  Prop : Universe
  ||| Predicative hierarchy of universes.
  Set  : Nat -> Universe

%name Universe s, s', s'', s'''

||| Converts universes to naturals as a helper for writing implementations.
public export
toNat : Universe -> Nat
toNat Prop = 0
toNat (Set i) = S i

-- Interfaces ------------------------------------------------------------------

public export
Eq Relevance where
  Irrelevant == Irrelevant = True
  Relevant == Relevant = True
  _ == _ = False

export
Uninhabited (Irrelevant = Relevant) where uninhabited Refl impossible

export
Uninhabited (Relevant = Irrelevant) where uninhabited Refl impossible

export
DecEq Relevance where
  decEq Irrelevant Irrelevant = Yes Refl
  decEq Irrelevant Relevant = No absurd
  decEq Relevant Irrelevant = No absurd
  decEq Relevant Relevant = Yes Refl

public export
Eq Universe where
  (==) = (==) `on` toNat

public export
Ord Universe where
  compare = compare `on` toNat
  (<) = lt `on` toNat
  (>) = gt `on` toNat
  (<=) = lte `on` toNat
  (>=) = gte `on` toNat

  min Prop s' = Prop
  min (Set _) Prop = Prop
  min (Set i) (Set j) = Set (minimum i j)

  max Prop s' = s'
  max (Set i) s' = Set (maximum i (pred $ toNat s'))

export
Uninhabited (Prop = Set i) where uninhabited Refl impossible

export
Uninhabited (Set i = Prop) where uninhabited Refl impossible

export
Injective Set where
  injective Refl = Refl

public export
DecEq Universe where
  decEq Prop Prop = Yes Refl
  decEq Prop (Set _) = No absurd
  decEq (Set _) Prop = No absurd
  decEq (Set i) (Set j) = decEqCong $ decEq i j

export
Show Universe where
  showPrec d Prop = "Prop"
  showPrec d (Set 0) = "Set"
  showPrec d (Set (S i)) = showParens (d >= App) $ "Set \{show (S i)}"

export
Pretty Universe where
  prettyPrec d Prop = pretty "Prop"
  prettyPrec d (Set 0) = pretty "Set"
  prettyPrec d (Set (S i)) = parenthesise (d >= App) $ pretty "Set \{show (S i)}"

-- Operations ------------------------------------------------------------------

infixr 5 ~>

||| Computes the proof-relevance of a pair.
public export
pair : (fst, snd : Relevance) -> Relevance
pair Irrelevant = id
pair Relevant = const Relevant

||| Computes the proof-relevance of a function.
public export
function : (dom, cod : Relevance) -> Relevance
function = const id

||| Gets the proof-relevance of values in a universe.
public export
relevance : Universe -> Relevance
relevance Prop = Irrelevant
relevance (Set k) = Relevant

||| True if values in `s` are proof-irrelevant.
public export
isIrrelevant : (s : Universe) -> Bool
isIrrelevant = (Irrelevant ==) . relevance

||| True if values in `s` are proof-relevant.
public export
isRelevant : (s : Universe) -> Bool
isRelevant = (Relevant ==) . relevance

||| Returns the smallest universe containing `s`
||| @ s the universe to contain
public export
succ : (s : Universe) -> Universe
succ = Set . toNat

||| The universe of a dependent product.
||| @ dom the domain universe
||| @ cod the codomain universe
public export
(~>) : (dom, cod : Universe) -> Universe
dom ~> Prop    = Prop
dom ~> (Set k) = max (Set k) dom

-- Views -----------------------------------------------------------------------

namespace Predicates
  public export
  data IsIrrelevant : Universe -> Type where
    Prop : IsIrrelevant Prop

  public export
  data IsRelevant : Universe -> Type where
    Set : IsRelevant (Set k)

  export
  Uninhabited (IsIrrelevant (Set k)) where
    uninhabited _ impossible

  export
  Uninhabited (IsRelevant Prop) where
    uninhabited _ impossible

  export
  isIrrelevant : (s : Universe) -> Dec (IsIrrelevant s)
  isIrrelevant Prop = Yes Prop
  isIrrelevant (Set k) = No absurd

  export
  isRelevant : (s : Universe) -> Dec (IsRelevant s)
  isRelevant Prop = No absurd
  isRelevant (Set k) = Yes Set

-- Properties ------------------------------------------------------------------

export
pairRelevantRight : (fst : Relevance) -> pair fst Relevant = Relevant
pairRelevantRight Irrelevant = Refl
pairRelevantRight Relevant = Refl

succContains : (s : Universe) -> So (s < succ s)
succContains Prop = Oh
succContains (Set k) = eqToSo $ LteIslte k k reflexive

succLeast : (s, s' : Universe) -> So (s < s') -> So (succ s <= s')
succLeast s s' prf = prf

irrelevantReflection : (s : Universe) -> Reflects (IsIrrelevant s) (isIrrelevant s)
irrelevantReflection Prop = RTrue Prop
irrelevantReflection (Set k) = RFalse absurd

relevantReflection : (s : Universe) -> Reflects (IsRelevant s) (isRelevant s)
relevantReflection Prop = RFalse absurd
relevantReflection (Set k) = RTrue Set

export
forgetIsIrrelevant : IsIrrelevant s -> relevance s = Irrelevant
forgetIsIrrelevant Prop = Refl

export
forgetIsRelevant : IsRelevant s -> relevance s = Relevant
forgetIsRelevant Set = Refl

export
pairRelevance : (s, s' : Universe) -> relevance (max s s') = pair (relevance s) (relevance s')
pairRelevance Prop s' = Refl
pairRelevance (Set k) s' = Refl

export
functionRelevance : (s, s' : Universe) ->
  relevance (s ~> s') = function (relevance s) (relevance s')
functionRelevance s Prop = Refl
functionRelevance s (Set k) = Refl