caledon-2.0.0.0: examples/universe.ncc

fixity right 0 $
defn $ : {a b:prop} (a -> b) -> a -> b
  as ?\At Bt :prop . \ F . \A . F A  

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
   | lam = [T : tm ty][F : tm T → tm T] tm {S = ♢ T} (Π A : T . F A)
   | raise = {T : tm ty} tm T → tm $ ♢ T

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

query whattype0 = isTm (Π A : ty . A)
query whattype1 = isTm (lam A : ty . A)