module Model where

open import PrimTypes

data Sort : Set where
  PROP  : Sort
  SET   : Sort

mutual
  data Ty : Sort -> Set where
    `0'   :  Ty PROP
    `1'   :  Ty PROP
    `2'   :  Ty SET
    `Pi'  :  {K : Sort}(S : Ty SET)  (T : [ S ] -> Ty K) -> Ty K
    `Sg'  :  {K : Sort}(S : Ty K)    (T : [ S ] -> Ty K) -> Ty K
    `IMu' :  (S : Ty SET)
             (C : [ S ] -> Ty SET)
             (R : (s : [ S ])(c : [ C s ]) -> Ty SET)
             (n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->
             (s : [ S ]) ->
             Ty SET
    `INu' :  {K : Sort}
             (S : Ty SET)
             (C : [ S ] -> Ty K)
             (R : (s : [ S ])(c : [ C s ]) -> Ty SET)
             (n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->
             (s : [ S ]) ->
             Ty K
    `Prf' :  Ty PROP -> Ty SET

  [_] : {K : Sort} -> Ty K -> Set
  [ `0' ]                = Zero
  [ `1' ]                = One
  [ `2' ]                = Two
  [ `Pi' S T ]           = (s : [ S ]) -> [ T s ]
  [ `Sg' S T ]           = Sg [ S ] \ s -> [ T s ]
  [ `IMu' S C R n s ]    =
   IMu {[ S ]} (record {Comm = \ s -> [ C s ]; Resp = \ s c -> [ R s c ]; next = n}) s
  [ `INu' S C R n s ]    =
   INu {[ S ]} (record {Comm = \ s -> [ C s ]; Resp = \ s c -> [ R s c ]; next = n}) s
  [ `Prf' P ]            = [ P ]

_=>_ : {K : Sort} -> Ty K -> Ty K -> Ty K
_=>_ {SET}   S T = `Pi' S \ _ -> T
_=>_ {PROP}  P Q = `Pi' (`Prf' P) \ _ -> Q

_&_ : {K : Sort} -> Ty K -> Ty K -> Ty K
S & T = `Sg' S \ _ -> T