We record a particularly simple construction on top of Lumsdaine's local universes that allows for a Coquand-style universe of propositions with propositional extensionality to be interpreted in a category with subobject classifiers.

翻译：我们在Lumsdaine局部宇宙的基础上记录了一种特别简单的构造，该构造允许将具有命题外延性的Coquand风格命题宇宙解释为具有子对象分类器的范畴中。