What is Leibniz equality? What is it for?

[robrix]

I think this implements Leibniz equality, but I don‘t know what it is, or why, or how it works, or why:

let Equal = Declaration<Recur>("Equal", Datatype(.Type) { A in
    Datatype(A, A) { a, b in
        [ "equal": .Argument((A --> .Type) => { f in f[a] --> f[b] }, const(.End)) ]
    }
})

[langston-barrett]

@robrix I don't know anything about Swift or this project, but in logic, Leibniz equality is the principle that two things that are indistinguishable (by propositions) must be identical. Informally "if everything that is true of a is also true of b, then a=b. See https://en.wikipedia.org/wiki/Identity_of_indiscernibles.

[robrix]

@siddharthist: That’s super helpful! Thank you.