TY - JOUR AU - Fridlender, Daniel PY - 1998/06/09 Y2 - 2024/03/28 TI - An Interpretation of the Fan Theorem in Type Theory JF - BRICS Report Series JA - BRICS VL - 5 IS - 39 SE - Articles DO - 10.7146/brics.v5i39.19484 UR - https://tidsskrift.dk/brics/article/view/19484 SP - AB - <p>This article presents a formulation of the fan theorem in<br />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.</p><p>Keywords: type theory, fan theorem, inductive bar.</p> ER -