================================================================================
P9611   M.P.A. Sellink
        "On the conservativity of Leibniz Equality"


We embed a first order theory with equality in the Pure Type System
lambda-MON2 that is a subsystem of the well-known type system lambda-PRED2.
The embedding is based on the Curry-Howard isomorphism, i.e., implication 
and universal quantification coincide with arrow types and product types.
Formulas of the form t1 == t2 are treated as Leibniz equalities. That is,
t1 == t2 is identified with the second order formula ALL P. P(t1) --> P(t2), 
which contains only implications and universal quantifications and can hence 
be embedded straightforwardly. We give a syntactic proof --- based on 
enriching typed lambda-calculus with extra reduction steps --- for the 
equivalence between derivability in the logic and inhabitance in lambda-MON2.  
Familiarity with Pure Type Systems [Bar92] is assumed.


[Bar92] H.P. Barendregt.  Lambda calculi with types. In S. Abramsky, 
        D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic 
        in Computer Science, volume 2, pages 117--309. Oxford
        Science Publications, 1992.