Update Quest1.md
This commit is contained in:
parent
e49f5a5717
commit
3e77252ee7
@ -117,9 +117,11 @@ This is called a _sigma type_, which has three interpretations:
|
|||||||
- the total space of the bundle `isEven` over `ℕ`,
|
- the total space of the bundle `isEven` over `ℕ`,
|
||||||
which is the space obtained by putting together all the fibers.
|
which is the space obtained by putting together all the fibers.
|
||||||
Pictorially, it looks like
|
Pictorially, it looks like
|
||||||
|
|
||||||
<img src="images/isEvenBundle.png"
|
<img src="images/isEvenBundle.png"
|
||||||
alt="SigmaTypeOfIsEven"
|
alt="SigmaTypeOfIsEven"
|
||||||
width="500"/>
|
width="500"/>
|
||||||
|
|
||||||
which can also be viewed as the subset of even naturals,
|
which can also be viewed as the subset of even naturals,
|
||||||
since the fibers are either empty or singleton.
|
since the fibers are either empty or singleton.
|
||||||
(It is a _subsingleton bundle_).
|
(It is a _subsingleton bundle_).
|
||||||
|
Loading…
Reference in New Issue
Block a user