Definability of finite sum types in Martin-Löf's type theories

• 1 December 1983
• journal article
• Published by Elsevier in Indagationes Mathematicae
• Vol. 86  (4) , 475-481
• https://doi.org/10.1016/s1385-7258(83)80024-9

Abstract

Keywords

• TYPE THEORY