Bool_Polytype : *p = (Data:*) -> Data -> Data -> Data
Bool  : *m   = Monotype Bool_Polytype
True  : Bool = monotype Bool_Polytype (λ(Data:*) (True:Data) (False:Data) -> True)
False : Bool = monotype Bool_Polytype (λ(Data:*) (True:Data) (False:Data) -> False)

and (x:Bool) (y:Bool) : Bool
 = monotype Bool_Polytype
   (λ(Data:*) (True:Data) (False:Data) ->
     polytype Bool_Polytype x Data
      (polytype Bool_Polytype y Data True  False)
      (polytype Bool_Polytype y Data False False)
   )
or (x:Bool) (y:Bool) : Bool
 = monotype Bool_Polytype
   (λ(Data:*) (True:Data) (False:Data) ->
     polytype Bool_Polytype x Data
      (polytype Bool_Polytype y Data True  True)
      (polytype Bool_Polytype y Data True False)
   )
xor (x:Bool) (y:Bool) : Bool
 = monotype Bool_Polytype
   (λ(Data:*) (True:Data) (False:Data) ->
     polytype Bool_Polytype x Data
      (polytype Bool_Polytype y Data False  True)
      (polytype Bool_Polytype y Data True False)
   )
not (x:Bool) : Bool
 = monotype Bool_Polytype
   (λ(Data:*) (True:Data) (False:Data) ->
     polytype Bool_Polytype x Data False True)