caledon-3.1.0.0: examples/universe.ncc

#include "../prelude/combinators.ncc"

fixity pre 1 ♢
fixity lambda Π 
fixity lambda lam 


{-
for the moment, circularly defined types are allowed!  this violates consistency.  
If a dependency analysis is done, and types are checked in order, this will become safe!
-}

{- 
the implicit argument is pretty much always intialized to ty
tm basically says
t in tm S T has type T where T has sort S.
-}
unsound tm : {S : tm ty} tm S → prop
   | ty  = tm ty
   | ♢   = tm ty -> tm ty
   | Π   = [T : tm ty] (tm T → tm T) → tm $ ♢  T
   | raise = {T : tm ty} tm T → tm $ ♢  T
   | lam = [T : tm ty][F : tm T → tm T] tm {S = ♢ T} (Π A : T . F A)

defn isTm : {Kind : tm ty} {Ty : tm Kind} tm Ty -> prop
   | hasValue = [S : tm ty][T : tm S][V : tm T] isTm V

query whattype0 = isTm { Kind = ty } { Ty = ♢ ty } ( Π A : ty . A)
query whattype1 = isTm (lam A : ty . A)