Abstract

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.