Equal signs with fancy marks

One context in which the distinction between "equal by definition" and "equal because we proved it" has a precise mathematical meaning is intensional dependent type theory. This includes formalizing mathematics in a computer proof assistant based on ITT, such as Coq or Agda, but mathematics in ITT can also be done "unformalized" such as in the homotopy type theory book.

As for notation:

• Coq uses $=$ for propositional equality (i.e. "we proved it" equality) and $:=$ for definitional equality (more precisely, for definitions currently being made).

• Agda uses $=$ for definitions being made, and (at least in the standard library) $\equiv$ for propositional equality.

• The HoTT book uses $=$ for propositional equality, $\equiv$ for an equality that holds by definition but is not something currently being defined, and $:\equiv$ for something currently being defined.

  We spent a long time deciding on this; we wanted to use $=$ for "ordinary" equality, and we wanted to use something symmetric like $\equiv$ for equalities-by-previous-definition and something asymmetric like $:=$ for current-definitions so as to indicate visually that the left side is what's being defined. But $:=$ for a current-definition would suggest that it's a propositional equality that results rather than a definitional one, which led us to invent the symbol $:\equiv$. (We then actually ended up using $:=$ later for a "propositional equality being currently defined to hold", which happens under some versions of higher inductive types.)

In a slightly different direction, $\overset{\mbox{(2.3)}}{\ge}$ (the overset should be in a smaller font using \tiny, but for some reason that wouldn't render here) is a nice way to indicate that the inequality uses $(2.3)$ - this is especially convenient with a long string of inequalities in display-math where it's otherwise hard work to figure out which inequality uses which previous calculation.