An Interpretation of the Fan Theorem in Type Theory
This article presents a formulation of the fan theorem in
Martin-L¨of'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.
Keywords: type theory, fan theorem, inductive bar.
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.