论文部分内容阅读
The paper discusses semantics ofencodings in logical frameworks where equalities in object calculi arerepresented by families of types as the case in ELF.The notion of Leibniz equality in a category is introduced. Twomorphisms in a category are Leibniz equal if they are seen so by aninternal category. The usual categorical properties are then relativizedto r-properties by requiring mediating morphisms to be unique up to someLeibniz equality. Using these terminologies, it is shown, by an example,that the term model of the encoding of an adequately represented objectcalculus is r-isomorphic to the term model of the object language.