Ranta’s view that all substitutions of variables between MLTT contexts in some sense “extend” these contexts, so the MLTT contexts always form a partial order, is not justified. It is well known that the category of MLTT contexts is, generally, locally Cartesian closed but not necessarily a poset. Thus, Domanov’s reading of such general substitutions as mutual interpretations between contexts, which represent their corresponding epistemic agents, is more adequate. The formal analysis offered by Domanov can be improved if this latter viewpoint is developed more systematically than the author does it in his paper.
Translated title of the contributionMARTIN-LöF TYPE THEORY AS A MULTI-AGENT EPISTEMIC FORMAL SYSTEM
Original languageRussian
Pages (from-to)44-47
JournalЭПИСТЕМОЛОГИЯ И ФИЛОСОФИЯ НАУКИ
Volume55
Issue number4
StateAccepted/In press - 2018

    Research areas

  • Constructive Type theory, INTERPRETATIONS OF CONTEXTS, EPISTEMIC AGENT

ID: 35625386