Post #1809091

Here is an ``interesting'' question I have in type theory, and it has to do with Leibniz equality. In type theory, we can formalize a version of Leibniz equality principle on sets as a type ``` Leq(A, a, b) ≡ ∏ (P : A → hProp), P a = P b ``` where `A : hSet`. I.e. two things are equal if no proposition can distinguish them. Thus we 'explain' equality in an hSet in terms of hProp-predicates. In case `A : hSet`, the defined Leibniz equality coincides with the usual equality. Since both types in this case are propositions, it is easy to show the logical bi-implication. What I am interested in is if this generalizes to higher type? Suppose `A : n-Type`, and we define ``` Leq_n(A, a, b) ≡ ∏ (P : A → (n-1)-Type), P a = P b ``` what can we say in relation to the actual equality? We can still have a logical bi-implication, but I am not sure if the types are going to be isomorphic. Can anyone (dis)prove me?