An Interpretation of the Fan Theorem in Type Theory

Daniel Fridlender

December 1998


This article presents a formulation of the fan theorem in Martin-Löf's type theory. Starting from one of the standard versions of the fan theorem we gradually introduce reformulations leading to a final version which is easy to interpret in type theory. Finally we describe a formal proof of that final version of the fan theorem

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.