Judgmental and Definitional Equality from a Fregean Perspective

In the literature on constructive type theory the notions of definitional and judgmental equality are sometimes identified and sometimes treated as distinct. These different attitudes can be found also in the work of Martin-Löf, who identified the two notions in discussing the intensional version of type theory in the mid seventies, while he treated them as distinct in his mid-eighties monograph in which constructive type theory is presented in its extensional version. In the present article we investigate the reasons behind these different views starting from Frege’s distinctions between sense and denotation, and between function and object. We highlight some weaknesses in both analyses proposed by Martin-Löf, and we suggest a possible further “Fregean” reading of judgmental equality in the intensional version of constructive type theory.