This is a short story written with help from ChatGPT, about the intuition behind counter-examples to Leibniz' first principle. This is generally believe to be true among logicians, but the equality as it is expressed in Leibniz' first principle is just an assumption about equality and not a proof of equality.
x=y → ∀F(Fx ↔ Fy) Leibniz' first principle
In short, Leibniz' first principle does not hold for all operators in mathematics, because not all operators are congruent by normal equality.
It is not possible to reason about proofs of equality directly in logic (this is not about terms of types as proofs, but about "actual proofs"). There is a weaker statement of tautological equality that is used to provide this intuition.
If x=y
is taken as "tautological equality", then the principle holds, but since tautological equality can be assumed, this does not prove that all properties are the same in the strong sense, but only a weak sense (up to provability within the language).
Now, it is important to remember that this counter-example is relative to the theory of Path Semantics. In the theory of Path Semantics, reasoning with symbolic indistinction (what would be considered actual numerical sameness) is not considered safe, only symbolic distinction. This is why it gets so complex, as there is no way to access the "actual" proof directly.
In Path Semantics, the actual counter-example to Leibniz' first principle is the qubit operator ~
which has tautological congruence. This is not part of the short story and takes a lot more background knowledge to understand. For those interested, one can read about the classical model of path semantical qubit here:
The Pocket-Prover library contains an implementation of the classical model: https://crates.io/crates/pocket_prover
The constructive model is more complex and uses a higher order logic with propositional exponentials (HOOO EP). You can try out an implementation using Rust: https://crates.io/crates/prop
Provability logic is inconsistent together with HOOO EP, so you can not use one to talk about the other. HOOO EP has an associated modal logic, but Löb's theorem is false in this model.
Maybe you can talk to Eric Weiser, who kindly provided me a proof in Lean 3: https://github.com/advancedresearch/path_semantics/blob/master/papers-wip/semiconjugates-as-satisfied-models-of-total-normal-paths.pdf
The experts in dependent types I know, think Path Semantics might help provide a better foundation or understanding in the future, or perhaps languages with some new features. We don't know yet, because it takes a lot of work to get there. I don't have the impression that they are thinking about Path Semantics, since there is already a lot to do in dependent types.
The reason I worked with Kent Palmer, was because unlike in dependent types, it is easier to see the connection between Path Semantics and Continental Philosophy. Currently, there is a divide between Analytic Philosophy and Continental Philosophy and Kent Palmer is interested in bridging these two.