search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
371 stars 22 forks source link

definitions #157

Closed DanGrayson closed 1 year ago

DanGrayson commented 1 year ago

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

Screen Shot 2022-10-13 at 8 48 02 AM
DanGrayson commented 1 year ago

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.

pierrecagne commented 1 year ago

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.

DanGrayson commented 1 year ago

Thanks!

DanGrayson commented 1 year ago

Right. I'll add a note.

DanGrayson commented 1 year ago

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