An Interpretation of the Fan Theorem in Type Theory

Authors

  • Daniel Fridlender

DOI:

https://doi.org/10.7146/brics.v5i39.19484

Abstract

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.

Downloads

Published

1998-06-09

How to Cite

Fridlender, D. (1998). An Interpretation of the Fan Theorem in Type Theory. BRICS Report Series, 5(39). https://doi.org/10.7146/brics.v5i39.19484