It can get more complicated. When your logic can talk about equivalence of equivalences of proofs, then you can have two proofs that are equivalent in two ways

It can get more complicated. When your logic can talk about equivalence of equivalences of proofs, then you can have two proofs that are equivalent in two ways that are not equivalent. Or, you could have two proofs that are equivalent in two ways whose equivalence can be proved, but maybe also in more than one way. You can iterate equivalences of equivalences in such a logic and equality becomes a significantly richer concept. The study of such mathematical structures is the study of what is called an (infinity,1)-topos.