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

Which maps are constant? #99

Open marcbezem opened 3 years ago

marcbezem commented 3 years ago

We currently have "constant map, which is one of the form x |→ b". The "of the form" seems to refer to the definition. Would the degree 0 function, which happens to be constant, also be "a constant map"? Somewhat related, Exercise 3.3.3 does (after some changes) not longer directly apply to the degree 0 function. This should be fixed, either in the exercise or in the statement about the degree 0 function.

DanGrayson commented 3 years ago

Probably the "degree 0 map" is defined as the constant map to the basepoint.

By the way, another possible definition for a constant function f would be one with an identification with one of the form x |-> b. Then it would be a mathematical definition.

marcbezem commented 3 years ago

Actually, Exercise 3.3.3 (2) seems wrong now: how to prove that all fibers are sets?

marcbezem commented 3 years ago

@DanGrayson the text suggests δ_0 is defined by circle induction to be constant, so definitionally different from the "constant map".

DanGrayson commented 3 years ago

I found the definition finally in 3.6.3. And you are right -- it's not a "constant map". But it can be identified with one.

UlrikBuchholtz commented 3 years ago

I've tweaked the definition of constant maps (to what was intended): a map equal to one of the form …

As for Ex. 3.3.3(2): It is solvable as stated. To avoid spoilers, I won't write the solution here in public, but I'll email you one if necessary :)

marcbezem commented 3 years ago

@DanGrayson sorry for lettting you search, will add "degree" to the index @UlrikBuchholtz thanks, and this is the second time I stumble over Ex. 3.3.3 (2). Will try harder, or search for your previous answer :-)

Still, Ex. 3.3.3 does not directly apply to the degree 0 function, factoring through type 1 doesn't give the negative result.

marcbezem commented 3 years ago

In some cases one wants the definitional variant of constancy, for example here: "transport in a constant type family is the identity". Not sure there are such cases in the book now, though.