An Interpretation of the Fan Theorem in Type Theory

Daniel Fridlender

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.


Full Text:

PDF


DOI: http://dx.doi.org/10.7146/brics.v5i39.19484
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.
OK


ISSN: 0909-0878 

Hosted by the State and University Library and Aarhus University Library