Abstract. This paper concerns retracts in simply typed lambda calculus assuming βη-equality. We provide a simple tableau proof system which characterises when a type is a retract of another type and which leads to an exponential decision procedure.
REF gives a proof system which leads to an exponential decision procedure to characterise retraction for Curry types in the λβη-calculus.
Proof Systems for Retracts in Simply Typed Lambda Calculus