SymmetryBook definitions

Here's an example where we use a judgmental equality incorrectly. What should we do instead?

Oct 13 '22 15:10 DanGrayson

Oops, now I see that maybe := is not intended to convey something judgmental!

Maybe we should highlight the difference between the two symbols in a marginal note.

Oct 13 '22 16:10 DanGrayson

If I recall correctly, := is supposed to convey "a path by definition". Properly speaking there is a map rec : ∑(a : A(∙)) (a =_⟲ a) → ∏(x : S¹) A(x), but we simply use "f defined by f(∙) :≡ a and f(⟲) := ℓ" to denote rec(a,ℓ) in our semi-informal writing style.

I'm not in favor of transitioning to have explicit recursors, but we can definitely have explanations in the margin.

Oct 19 '22 18:10 pierrecagne

Thanks!

Oct 19 '22 18:10 DanGrayson

Right. I'll add a note.

Oct 20 '22 13:10 DanGrayson

I've added a note in commit 8cfccd1a809fea51dc6721a2f3b388514be9ee10, and I've added := to the glossary.

Oct 29 '22 23:10 DanGrayson