diff --git a/examples/typetheory/Donkey.gf b/examples/typetheory/Donkey.gf
new file mode 100644
index 000000000..5ed296e30
--- /dev/null
+++ b/examples/typetheory/Donkey.gf
@@ -0,0 +1,52 @@
+abstract Donkey = Types ** {
+
+cat 
+  S ; 
+  CN ;
+  NP Set ;
+  V2 Set Set ;
+  V  Set ;
+
+data
+  PredV2 : ({A,B} : Set) -> V2 A B -> NP A -> NP B -> S ;
+  PredV  : ({A} : Set)   -> V A -> NP A -> S ;
+  If     : (A : S) -> (El (iS A) -> S) -> S ;
+  An     : (A : CN) -> NP (iCN A) ;
+  The    : (A : CN)   -> El (iCN A) -> NP (iCN A) ;
+  Pron   : ({A} : CN) -> El (iCN A) -> NP (iCN A) ;
+
+  Man, Donkey : CN ;
+  Own, Beat : V2 (iCN Man) (iCN Donkey) ;
+  Walk, Talk : V (iCN Man) ;
+
+fun
+  iS  : S -> Set ;
+  iCN : CN -> Set ;
+  iNP : ({A} : Set) -> NP A -> (El A -> Set) -> Set ;
+  iV2 : ({A,B} : Set) -> V2 A B -> (El A -> El B -> Set) ;
+  iV  : ({A} : Set) -> V A -> (El A -> Set) ;
+
+def
+  iS (PredV2 A B F Q R) = iNP A Q (\x -> iNP B R (\y -> iV2 A B F x y)) ;
+  iS (PredV A F Q) = iNP A Q (iV A F) ;
+  iS (If A B) = Pi (iS A) (\x -> iS (B x)) ;
+  iNP _ (An A) F = Sigma (iCN A) F ;
+  iNP _ (Pron _ x) F = F x ;
+  iNP _ (The _ x) F = F x ;
+
+-- for the lexicon
+
+data
+  Man', Donkey' : Set ;
+  Own', Beat' : El Man' -> El Donkey' -> Set ;
+  Walk', Talk' : El Man' -> Set ;
+
+def
+  iCN Man = Man' ;
+  iCN Donkey = Donkey' ;
+  iV2 _ _ Beat = Beat' ;
+  iV2 _ _ Own = Own' ;
+  iV _ Walk = Walk' ;
+  iV _ Talk = Talk' ;
+
+}
\ No newline at end of file
diff --git a/examples/typetheory/DonkeyEng.gf b/examples/typetheory/DonkeyEng.gf
new file mode 100644
index 000000000..ec80285f0
--- /dev/null
+++ b/examples/typetheory/DonkeyEng.gf
@@ -0,0 +1,36 @@
+concrete DonkeyEng of Donkey = TypesSymb ** open Prelude in {
+
+lincat 
+  S  = SS ; 
+  CN = SS ** {g : Gender} ;
+  NP = SS ;
+  V2 = SS ;
+  V  = SS ;
+
+param Gender = Masc | Fem | Neutr ;
+
+lin
+  PredV2 _ _ F x y = ss (x.s ++ F.s ++ y.s) ;
+  PredV _ F x = ss (x.s ++ F.s) ;
+  If A B = ss ("if" ++ A.s ++ B.s) ;
+  An A = ss ("a" ++ A.s) ;
+  The A _ = ss ("the" ++ A.s) ;
+  Pron A _ = ss (case A.g of {Masc => "he" ; Fem => "she" ; Neutr => "it"}) ;
+
+  Man = {s = "man" ; g = Masc} ;
+  Donkey = {s = "donkey" ; g = Neutr} ;
+  Own = ss "owns" ;
+  Beat = ss "beats" ;
+  Walk = ss "walks" ;
+  Talk = ss "talks" ;
+
+-- for the lexicon
+
+lin
+  Man' = ss "man'" ;
+  Donkey' = ss "donkey'" ;
+  Own' = apply "own'" ;
+  Beat' = apply "beat'" ;
+  Walk' = apply "walk'" ;
+  Talk' = apply "talk'" ;
+}
\ No newline at end of file
diff --git a/examples/typetheory/README b/examples/typetheory/README
new file mode 100644
index 000000000..0ed6df0d7
--- /dev/null
+++ b/examples/typetheory/README
@@ -0,0 +1,58 @@
+13/9/2011 by AR
+
+Main files
+
+  Types.gf     -- Martin-Löf's "Intuitionistic Type Theory" (book 1984)
+  TypesSymb.gf -- concrete syntax close to the notation of the book
+
+Experimental extension
+
+  Donkey.gf    -- sentences about men and donkeys, with Montague semantics in Types
+  DonkeyEng.gf -- quick and dirty English concrete syntax
+
+Example 1: the formula for the "donkey sentence", 
+"if a number is equal to a number, it is equal to it"
+The parser restores implicit arguments, and linearizing the formula back returns it with
+Greek letters (which could also be used in the input):
+ 
+  > import TypesSymb.gf
+
+  Types> p -tr -cat=Set "( Pi z : ( Sigma x : N ) ( Sigma y : N ) I ( N , x , y ) ) I ( N , p ( z ) , p ( q ( z ) ) )" | l -unlexcode
+
+  Pi 
+    (Sigma Nat (\x -> 
+      Sigma Nat (\y -> Id Nat x y))) 
+    (\z -> 
+      Id Nat 
+        (p {Nat} {\_1 -> Sigma Nat (\v2 -> Id Nat _1 v2)} 
+           z) 
+        (p {Nat} {\_1 -> Id Nat (p Nat (\v2 -> Sigma Nat (\v3 -> Id Nat v2 v3)) z) _1} (
+           q {Nat} {\_1 -> Sigma Nat (\v2 -> Id Nat _1 v2)} 
+             z)))
+
+  (Π z : (Σ x : N)(Σ y : N)I (N , x , y))I (N , p (z), p (q (z)))
+
+
+Example 2: parse and interpret a sentence, also showing the nice formula.
+
+  > import DonkeyEng.gf
+
+  Donkey> p -cat=S -tr "a man owns a donkey " | pt -transfer=iS -tr | l -unlexcode
+  PredV2 {Man'} {Donkey'} Own (An Man) (An Donkey)
+
+  Sigma Man' (\v0 -> Sigma Donkey' (\v1 -> Own' v0 v1))
+
+  (Σ v0 : man')(Σ v1 : donkey')own' (v0 , v1)
+
+
+Example 3: (to be revisited) parse of "the donkey sentence" fails, but should succeed
+
+  Donkey> p -cat=S "if a man owns a donkey he beats it"
+  The parsing is successful but the type checking failed with error(s):
+    Couldn't match expected type NP Man'
+           against inferred type NP (iCN Donkey)
+    In the expression: Pron {Donkey} ?13
+  
+  Donkey> p -cat=S "if a man owns a donkey the man beats the donkey"
+  The sentence is not complete
+
diff --git a/examples/typetheory/Types.gf b/examples/typetheory/Types.gf
index 3a477e437..394a617d3 100644
--- a/examples/typetheory/Types.gf
+++ b/examples/typetheory/Types.gf
@@ -4,9 +4,17 @@ abstract Types = {
 
 -- categories
 cat 
+  Judgement ;
   Set ; 
   El Set ;
 
+flags startcat = Judgement ;
+
+-- forms of judgement
+data
+  JSet   : Set -> Judgement ;
+  JElSet : (A : Set) -> El A -> Judgement ;
+
 -- basic forms of sets
 data
   Plus   : Set -> Set -> Set ;
@@ -17,14 +25,14 @@ data
   Id     : (A : Set) -> (a,b : El A) -> Set ;
 
 -- defined forms of sets
-fun Impl : Set -> Set -> Set ;
-def Impl A B = Pi A (\x -> B) ;
+fun Funct : Set -> Set -> Set ;
+def Funct A B = Pi A (\x -> B) ;
 
-fun Conj : Set -> Set -> Set ;
-def Conj A B = Sigma A (\x -> B) ;
+fun Prod : Set -> Set -> Set ;
+def Prod A B = Sigma A (\x -> B) ;
 
 fun Neg : Set -> Set ;
-def Neg A = Impl A Falsum ;
+def Neg A = Funct A Falsum ;
 
 -- constructors
 
@@ -82,7 +90,7 @@ def
   Rec _ Zero d _ = d ;
   Rec C (Succ x) d e = e x (Rec C x d e) ;
 
-fun J : (A : Set) -> (a,b : El A) -> (C : (x,y : El A) -> El (Id A x y) -> Set) -> 
+fun J : (A : Set) -> (C : (x,y : El A) -> El (Id A x y) -> Set) -> (a,b : El A) -> 
           (c : El (Id A a b)) -> 
           (d : (x : El A) -> El (C x x (r A x))) ->
             El (C a b c) ;
@@ -108,7 +116,7 @@ def exp2 a = Rec (\x -> Nat) a one (\x,y -> plus y y) ;
 fun fast : El Nat -> El Nat ;  -- fast (Succ x) = exp2 (fast x)
 def fast a = Rec (\x -> Nat) a one (\_ -> exp2) ;
 
-fun test : El Nat ;
-def test = fast (fast two) ;
+fun big : El Nat ;
+def big = fast (fast two) ;
 
 }
\ No newline at end of file
diff --git a/examples/typetheory/TypesSymb.gf b/examples/typetheory/TypesSymb.gf
new file mode 100644
index 000000000..1c0cc5fae
--- /dev/null
+++ b/examples/typetheory/TypesSymb.gf
@@ -0,0 +1,81 @@
+concrete TypesSymb of Types = open Prelude in {
+
+-- Martin-Löf's set theory 1984, the polymorphic notation used in the book
+
+lincat 
+  Judgement = SS ;
+  Set = SS ; 
+  El = SS ;
+
+-- Greek letters; latter alternative for easy input
+
+flags coding = utf8 ;
+
+oper
+  capPi = "Π" | "Pi" ;
+  capSigma = "Σ" | "Sigma" ;
+  smallLambda = "λ" | "lambda" ;
+
+lin
+  JSet A = ss (A.s ++ ":" ++ "set") ;
+  JElSet A a = ss (a.s ++ ":" ++ A.s) ;
+
+  Plus A B = parenss (infixSS "+" A B) ;
+  Pi A B = ss (paren (capPi ++ B.$0 ++ ":" ++ A.s) ++ B.s) ;
+  Sigma A B = ss (paren (capSigma ++ B.$0 ++ ":" ++ A.s) ++ B.s) ;
+  Falsum = ss "_|_" ;
+  Nat = ss "N" ; 
+  Id A a b = apply "I" A a b ;
+
+
+oper
+  apply = overload {
+    apply : Str -> Str -> Str = \f,x -> f ++ paren x ;
+    apply : Str -> SS -> SS = \f,x -> prefixSS f (parenss x) ;
+    apply : Str -> SS -> SS -> SS = \f,x,y -> 
+      prefixSS f (parenss (ss (x.s ++ "," ++ y.s))) ;
+    apply : Str -> SS -> SS -> SS -> SS = \f,x,y,z -> 
+      prefixSS f (parenss (ss (x.s ++ "," ++ y.s ++ "," ++ z.s))) ;
+    apply : Str -> SS -> SS -> SS -> SS -> SS = \f,x,y,z,u -> 
+      prefixSS f (parenss (ss (x.s ++ "," ++ y.s ++ "," ++ z.s ++ "," ++ u.s))) ;
+    } ;
+
+  binder = overload {
+    binder : Str -> Str -> SS = \x,b ->
+      ss (paren x ++ b) ;
+    binder : Str -> Str -> Str -> SS = \x,y,b ->
+      ss (paren x ++ paren y ++ b) ;
+    } ;
+
+lin 
+  Funct A B = parenss (infixSS "->" A B) ;
+  Prod A B = parenss (infixSS "x" A B) ;
+  Neg A    = parenss (prefixSS "~" A) ;
+
+  i _ _ a = apply "i" a ;
+  j _ _ b = apply "j" b ;
+
+  lambda _ _ b = ss (paren (smallLambda ++ b.$0) ++ b.s) ;
+
+  pair _ _ a b = apply [] a b ;
+
+  Zero = ss "0" ;
+  Succ x = apply "s" x ;
+
+  r _ = apply "r" ;
+
+  D _ _ _ c d e = apply "D" c (binder d.$0 d.s) (binder e.$0 e.s) ;
+  app _ _ = apply "app" ;
+  p _ _ = apply "p" ;
+  q _ _ = apply "q" ;
+
+  E _ _ _ c d = apply "E" c (binder d.$0 d.$1 d.s) ;
+
+  R0 _ = apply "R_0" ;
+
+  Rec _ c d e = apply "R" c c (binder e.$0 e.$1 e.s) ;
+
+  J _ _ a b c d = apply "J" a b c (binder d.$0 d.s) ;
+
+}
+