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
378 stars 22 forks source link

Introduce the subset notation #174

Closed UlrikBuchholtz closed 1 year ago

UlrikBuchholtz commented 1 year ago

… in Sec. 2.20. Perhaps as an exercise stating the type of commuting triangles with last two legs being subset inclusions is a proposition.

pierrecagne commented 1 year ago

See commit bc6c168258769f157127d95cc7cdc0c9e4d1cd15

If this is satisfying enough, I'll close the issue.

DanGrayson commented 1 year ago

Looks good to me.

marcbezem commented 1 year ago

Why do we restrict to subsets $S_0,S_1$ of $T$, in combination with injections? The type-to-be-proved-a-proposition also depends on $i_0,i_1$. Perhaps only a typo, injection ---> inclusion, which would solve both? Or should we aim for the more general $(S_0,i_0)\subseteq(S_1,i_1)$?

marcbezem commented 1 year ago

Wait, I see that Ulrik above speaks of inclusions. So I will change to inclusions (fst!) and add glossary and index info. This because $\subseteq$ is important and defined in an exercise - hard to find without glossary/index. See 1b9a99e4558c1c5b