The following file shows the usefulness of Yarrow (as opposed to Coq etc): the file proves the inconsistency of the Pure Type System S with rules
 * : square
 (*,*), (square, *), (*,square,*)

So in this PTS, if A is a type, the A->* : *, so predicate types are types again (and not kinds). This is a variant of the cube system lambdaP2, which has polymorphism and type dependency. So S is "just" lambdaP2, where the predicate domains are types and not kinds. The first lines of the file declare the PTS S.



system (*,#),
       (*:#),
       ((#,*),(*,*),(*,#,*))

var B : *

def V := @ A:*. ((A -> *) -> A -> *) -> A -> *
def U := V -> *
def sb := \z:V. \A:*. \r: (A -> *) -> A -> *.\a:A . r (z A r) a
def le:= \i:U -> *.\x:U.
  x (\A:*. \r: (A -> *) -> A -> *.\a:A  . i (\ v:V . sb v A r a))
def induct := \i:(U -> *). @ x:U. (le i x) -> (i x)
def WF := \ z:V . (induct (z U le))
def I:=  \x:U. (@ i:U -> *. ((le i x) -> (i (\ v:V . sb v U le x)))) -> B

Prove Omega : @ i:U -> *. induct i -> (i WF)
Intro i, y
Apply y
Unfold le
Unfold WF
Unfold induct
Intro x,H0
Apply y
Apply H0
Exit

Prove lemma1 : induct I
Unfold induct
Intro x,p
Unfold I
Intro q
Apply q I
Exact p
Intro i, H
Apply q On \y:U. i (\v:V. sb v U le y)
Apply H
Exit

Prove lemma2 : (@i:U->*. induct i -> i WF)->B
Intro x
Apply x I lemma1
Intro i,H0
Apply x
Unfold induct
Apply H0
Exit

Prove paradox : B
exact lemma2 Omega
Exit