mirror of
https://github.com/boris-marinov/category-theory-illustrated.git
synced 2024-07-07 07:16:18 +03:00
stuff
This commit is contained in:
Boris Marinov
parent
fd2d8d861d
commit
55883b12bd
|
|
@ -70,7 +70,7 @@ Category theory embodies all these aspects of mathematics, so I think a very goo
|
|||
Who is this book for
|
||||
====
|
||||
|
||||
So, who is this book for? If we rephrase this question as "Who *should* read this book", then the answer is nobody. Indeed, if you think in terms of "should", mathematics (or at least the type of mathematics that is reviewed here) won't help you much, although it is falsely advertised as a solution to many problems.
|
||||
So, who is this book for? Some people would phrase the question as "Who *should* read this book", but if you ask it this way, then the answer is nobody. Indeed, if you think in terms of "should", mathematics (or at least the type of mathematics that is reviewed here) won't help you much, although it is falsely advertised as a solution to many problems (it is, in fact, something much more).
|
||||
|
||||
Let's take an example --- many people claim that Einstein's theories of relativity are essential for GPS to work properly, as, due to relativistic effects, the clocks on GPS satellites tick faster than identical clocks on the ground.
|
||||
|
||||
|
|
@ -96,7 +96,9 @@ Although I am not an expert in special relativity, I suspect that the way this c
|
|||
|
||||
In other words, we can solve problems without any advanced math, or with no math at all, as evidenced by the fact that the Egyptians were able to build the pyramids without even knowing Euclidean geometry. And with that I am not claiming that math is so insignificant, that it is not even good enough to serve as a tool for building stuff. Quite the contrary, I think that math is much more than just a simple tool. Thinking itself is mathematical. So going through any math textbook (and of course especially this one) would help you in ways that are much more vital than finding solutions to "complex" problems.
|
||||
|
||||
And so "Who is this book for" is not to be read as who should, but who *can* read it. Then the answer is "anyone with some time and dedication to learn category theory".
|
||||
Some people say that we don’t use maths in our daily life. But, if true, that is only because other people have solved all hard problems for us and the solutions are encoded on the tools that we use, however not knowing math means that you will be forever a consumer, bound to use those existing tools and solutions and thinking patterns, not being able to do many things on your own.
|
||||
|
||||
And so "Who is this book for" is not to be read as who should, but who *can* read it. Then the answer is "everyone".
|
||||
|
||||
About category theory
|
||||
===
|
||||
|
|
|
|||
|
|
@ -142,7 +142,7 @@ You can think of $ID_{G}$ as a function which represents the set $G$ in the real
|
|||
Functions and Subsets
|
||||
---
|
||||
|
||||
For each set and subset, no matter what they represent, we can define the function that maps each element of the subset to itself:
|
||||
For each set and subset, no matter what they represent, we can define a function (called the *image* of the subset) that maps each element of the subset to itself:
|
||||
|
||||
|
||||
|
||||
|
|
@ -409,9 +409,9 @@ And in computer science, if we have functions that convert an object of type $A$
|
|||
Equivalence relations
|
||||
---
|
||||
|
||||
What does it mean for two things to be equivalent? The question sounds quite philosophical, but there is actually is a formal way to answer it, i.e., there is a mathematical concept that captures the concept of equality in a rather elegant way — the concept of an *equivalence relation*.
|
||||
What does it mean for two things to be equivalent? The question sounds quite philosophical, but there is actually is a formal way to answer it, i.e., there is a mathematical concept that captures the concept of equality in a rather elegant way &mdash: the concept of an *equivalence relation*.
|
||||
|
||||
So what is an equivalence relation? We already know what a relation is — it is a connection between two sets (an example of which is function). But when is a relation an equivalence relation? Well, according the definition it is when it follows three laws, which correspond to three intuitive ideas about equality. Let's review them.
|
||||
So what is an equivalence relation? We already know what a relation is --- it is a connection between two sets (an example of which is function). But when is a relation an equivalence relation? Well, according the definition it is when it follows three laws, which correspond to three intuitive ideas about equality. Let's review them.
|
||||
|
||||
Reflexivity
|
||||
---
|
||||
|
|
@ -425,7 +425,7 @@ This simple principle translates to the equally simple law of *reflexivity*: for
|
|||
Transitivity
|
||||
---
|
||||
|
||||
The second idea that defines the concept of equivalence is the idea that things that are equal to another thing must also equal between themselves.
|
||||
According to the Christian theology of the Holly Trinity, the Jesus' Father is God, Jesus is God, and the Holy Spirit is also God, however, the Father is not the same person as Jesus (neither is Jesus the Holly Spirit). If this seems weird to you, that's because it breaks the second law of equivalence relations, transitivity. Transitivity is the idea that things that are both equal to a third thing must also equal between themselves.
|
||||
|
||||
|
||||
|
||||
|
|
@ -435,6 +435,7 @@ Note that we don't need to define what happens in similar situations that involv
|
|||
|
||||
Symmetry
|
||||
---
|
||||
|
||||
If one thing is equal to another, the reverse is also true, i.e, the other thing is also equal to the first one. This idea is called *symmetry*. Symmetry is probably the most characteristic property of the equivalence relation, which is not true for almost any other relation.
|
||||
|
||||
|
||||
|
|
|
|||
190
_chapters/01_set/square.svg.2023_11_22_14_29_41.1.svg
Normal file
190
_chapters/01_set/square.svg.2023_11_22_14_29_41.1.svg
Normal file
|
|
@ -0,0 +1,190 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 359"
|
||||
version="1.1"
|
||||
id="svg16"
|
||||
sodipodi:docname="square.svg"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs16" />
|
||||
<sodipodi:namedview
|
||||
id="namedview16"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="137.8"
|
||||
cy="159.89999"
|
||||
r="114.9"
|
||||
id="circle1" />
|
||||
<circle
|
||||
fill="#e6e7e8"
|
||||
stroke="#808285"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="127.1"
|
||||
cy="147"
|
||||
r="114.9"
|
||||
id="circle2" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="435.29999"
|
||||
cy="164.7"
|
||||
r="114.9"
|
||||
id="circle3" />
|
||||
<circle
|
||||
fill="#e6e7e8"
|
||||
stroke="#808285"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="424.5"
|
||||
cy="151.7"
|
||||
r="114.9"
|
||||
id="circle4" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="415.70001"
|
||||
cy="80.699997"
|
||||
r="24.6"
|
||||
id="circle5" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 424.9,80.1 c 0,4.1 -0.7,7.1 -2.1,9.1 -1.4,1.9 -3.5,2.9 -6.3,2.9 -2.8,0 -4.9,-1 -6.3,-3 -1.4,-2 -2.1,-5 -2.1,-8.9 0,-4.1 0.7,-7.2 2.1,-9.1 1.4,-1.9 3.5,-2.9 6.3,-2.9 2.8,0 4.9,1 6.3,3 1.4,1.9 2.1,4.9 2.1,8.9 z m -10.6,0 c 0,2.6 0.2,4.5 0.5,5.4 0.3,1 0.9,1.5 1.7,1.5 0.8,0 1.3,-0.5 1.7,-1.5 0.3,-1 0.5,-2.8 0.5,-5.4 0,-2.6 -0.2,-4.4 -0.5,-5.4 -0.3,-1 -0.9,-1.6 -1.7,-1.6 -0.8,0 -1.3,0.5 -1.7,1.5 -0.3,1 -0.5,2.9 -0.5,5.5 z"
|
||||
id="path5" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="371.39999"
|
||||
cy="133.60001"
|
||||
r="24.6"
|
||||
id="circle6" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 376.6,143.7 h -6.4 v -12.3 c 0,-1.5 0,-2.9 0.1,-4.1 -0.4,0.5 -0.9,1 -1.5,1.5 l -2.6,2.2 -3.3,-4 8,-6.5 h 5.7 z"
|
||||
id="path6" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="490.5"
|
||||
cy="134.60001"
|
||||
r="24.6"
|
||||
id="circle7" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 498.6,144.7 h -16.9 v -4.1 l 5.7,-5.8 c 1.6,-1.7 2.7,-2.9 3.2,-3.5 0.5,-0.6 0.8,-1.2 1,-1.6 0.2,-0.4 0.3,-0.9 0.3,-1.4 0,-0.6 -0.2,-1.1 -0.6,-1.4 -0.4,-0.4 -0.9,-0.5 -1.7,-0.5 -0.7,0 -1.5,0.2 -2.2,0.6 -0.7,0.4 -1.6,1 -2.5,1.9 l -3.5,-4.1 c 1.2,-1.1 2.2,-1.8 3,-2.3 0.8,-0.5 1.7,-0.8 2.7,-1.1 1,-0.3 2,-0.4 3.2,-0.4 1.5,0 2.9,0.3 4,0.8 1.1,0.5 2.1,1.3 2.8,2.3 0.7,1 1,2.1 1,3.3 0,0.9 -0.1,1.8 -0.3,2.5 -0.2,0.8 -0.6,1.5 -1.1,2.3 -0.5,0.8 -1.1,1.5 -1.9,2.4 -0.8,0.8 -2.5,2.4 -5.1,4.7 v 0.2 h 8.8 v 5.2 z"
|
||||
id="path7" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="475.70001"
|
||||
cy="213.2"
|
||||
r="24.6"
|
||||
id="circle8" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 483,205 c 0,1.4 -0.4,2.7 -1.3,3.7 -0.9,1 -2.2,1.8 -3.8,2.3 v 0.1 c 3.9,0.5 5.8,2.3 5.8,5.5 0,2.2 -0.9,3.9 -2.6,5.1 -1.7,1.2 -4.1,1.9 -7.2,1.9 -1.3,0 -2.4,-0.1 -3.5,-0.3 -1.1,-0.2 -2.2,-0.5 -3.5,-1 v -5.2 c 1,0.5 2.1,0.9 3.1,1.2 1,0.3 2,0.4 2.9,0.4 1.4,0 2.4,-0.2 3,-0.6 0.6,-0.4 0.9,-1 0.9,-1.8 0,-0.6 -0.2,-1.1 -0.5,-1.5 -0.3,-0.4 -0.9,-0.6 -1.6,-0.8 -0.7,-0.2 -1.7,-0.3 -2.9,-0.3 h -1.4 V 209 h 1.5 c 3.2,0 4.8,-0.8 4.8,-2.5 0,-0.6 -0.2,-1.1 -0.7,-1.4 -0.5,-0.3 -1.1,-0.4 -1.9,-0.4 -1.5,0 -3,0.5 -4.6,1.5 l -2.6,-4.2 c 1.2,-0.9 2.5,-1.5 3.8,-1.8 1.3,-0.4 2.8,-0.5 4.4,-0.5 2.4,0 4.3,0.5 5.7,1.4 1.5,0.9 2.2,2.2 2.2,3.9 z"
|
||||
id="path8" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="379.39999"
|
||||
cy="215.89999"
|
||||
r="24.6"
|
||||
id="circle9" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 388.2,221.5 h -2.6 v 4.5 h -6.2 v -4.5 h -9.3 v -4.6 l 9.7,-14.2 h 5.8 v 14.1 h 2.6 z m -8.8,-4.7 v -2.7 c 0,-0.5 0,-1.2 0.1,-2.1 0,-0.9 0.1,-1.3 0.1,-1.4 h -0.2 c -0.4,0.8 -0.8,1.6 -1.2,2.3 l -2.6,3.8 h 3.8 z"
|
||||
id="path9" />
|
||||
<path
|
||||
fill="#6d6e71"
|
||||
d="m 223.5,135.4 c 0,0 0.3,-0.4 0.8,-1.1 0.3,-0.4 0.5,-0.8 0.9,-1.4 0.4,-0.5 0.9,-1.1 1.4,-1.8 2.1,-2.6 5.5,-6.1 10.2,-9.8 4.6,-3.7 10.5,-7.4 17.1,-10.7 6.6,-3.3 14,-6.1 21.6,-8.1 7.6,-2 15.5,-3 22.8,-3.1 7.4,-0.1 14.2,0.8 19.9,2.2 0.4,0.1 0.7,0.2 1.1,0.2 0.3,0.1 0.7,0.2 1,0.3 0.7,0.2 1.3,0.4 2,0.6 0.6,0.2 1.3,0.4 1.9,0.6 0.6,0.2 1.2,0.4 1.7,0.7 1.1,0.4 2.2,0.8 3.1,1.2 0.9,0.4 1.8,0.8 2.6,1.2 0.7,0.3 1.1,0.5 1.1,0.5 l -5.1,10.4 c 7.5,-1.2 15.9,-0.8 24.4,1.3 -2.5,-8.4 -6.6,-17 -12.7,-24.9 l -5.1,10.4 -1.2,-0.6 c -0.8,-0.4 -1.7,-0.8 -2.7,-1.2 -1,-0.4 -2.1,-0.8 -3.3,-1.3 -0.6,-0.2 -1.2,-0.4 -1.8,-0.7 -0.6,-0.2 -1.3,-0.4 -1.9,-0.6 l -2.1,-0.6 c -0.4,-0.1 -0.7,-0.2 -1.1,-0.3 -0.4,-0.1 -0.7,-0.2 -1.1,-0.3 -5.9,-1.5 -13.1,-2.4 -20.7,-2.3 -7.6,0.1 -15.7,1.2 -23.6,3.2 -7.8,2.1 -15.5,4.9 -22.3,8.4 -6.8,3.4 -12.8,7.3 -17.6,11.1 -4.8,3.8 -8.4,7.5 -10.7,10.3 -0.6,0.7 -1.1,1.4 -1.5,1.9 -0.4,0.6 -0.7,1.1 -1,1.5 -0.5,0.8 -0.8,1.3 -0.8,1.3 z M 153,183.6 c 0,0 0.5,0.7 1.5,1.9 0.5,0.6 1.1,1.4 1.8,2.3 0.3,0.5 0.7,0.9 1.1,1.5 0.4,0.5 0.9,1 1.4,1.6 1,1.1 2.1,2.3 3.2,3.6 1.2,1.3 2.7,2.6 4.1,4 3,2.8 6.7,5.7 10.9,8.5 0.5,0.4 1.1,0.7 1.6,1 0.6,0.3 1.1,0.6 1.7,1 1.2,0.6 2.3,1.4 3.5,1.9 2.5,1.1 5,2.4 7.8,3.3 0.7,0.2 1.4,0.5 2.1,0.7 0.3,0.1 0.7,0.3 1,0.4 l 1.1,0.3 c 1.4,0.4 2.9,0.8 4.4,1.2 l 4.5,0.9 c 0.8,0.1 1.5,0.3 2.3,0.4 0.8,0.1 1.6,0.2 2.3,0.3 l 2.4,0.3 1.2,0.1 h 1.2 c 1.6,0.1 3.2,0.1 4.8,0.2 3.2,-0.1 6.5,-0.1 9.8,-0.5 3.3,-0.2 6.6,-0.8 9.9,-1.3 3.3,-0.7 6.6,-1.3 9.8,-2.2 3.3,-0.8 6.4,-1.8 9.6,-2.8 1.6,-0.5 3.1,-1.1 4.7,-1.7 l 2.3,-0.8 2.3,-0.9 4.5,-1.8 c 1.5,-0.7 3,-1.3 4.4,-2 3,-1.3 5.8,-2.7 8.6,-4.1 11.2,-5.6 21.1,-11.7 29.4,-17.2 8.3,-5.5 15,-10.5 19.6,-14 l 1.2,-0.9 7,9.2 c 3.6,-8.2 6.8,-16.5 9.7,-24.7 -8.7,1.5 -17.2,2.9 -25.7,3.9 l 7,9.2 -1.2,0.9 c -4.6,3.5 -11.2,8.4 -19.4,13.8 -8.2,5.4 -18.1,11.5 -29.1,17 -2.8,1.3 -5.6,2.8 -8.5,4 -1.4,0.6 -2.9,1.3 -4.4,1.9 l -4.5,1.8 c -0.7,0.3 -1.5,0.6 -2.3,0.9 l -2.3,0.8 c -1.5,0.5 -3.1,1.1 -4.6,1.6 -3.1,1 -6.2,2 -9.4,2.8 -3.1,0.9 -6.4,1.5 -9.5,2.2 -3.2,0.5 -6.4,1.1 -9.6,1.3 -3.2,0.4 -6.4,0.4 -9.5,0.5 -1.6,-0.1 -3.1,-0.1 -4.7,-0.2 h -1.2 l -1.1,-0.1 c -0.8,-0.1 -1.5,-0.2 -2.3,-0.3 -0.8,-0.1 -1.5,-0.2 -2.3,-0.2 -0.7,-0.1 -1.5,-0.3 -2.2,-0.4 -1.5,-0.3 -2.9,-0.5 -4.3,-0.8 -1.4,-0.4 -2.8,-0.8 -4.2,-1.1 l -1,-0.3 c -0.3,-0.1 -0.7,-0.2 -1,-0.4 -0.7,-0.2 -1.3,-0.5 -2,-0.7 -2.7,-0.9 -5.1,-2.1 -7.4,-3.2 -1.2,-0.5 -2.3,-1.3 -3.4,-1.9 -0.5,-0.3 -1.1,-0.6 -1.6,-0.9 -0.5,-0.3 -1.1,-0.6 -1.6,-1 -4.1,-2.7 -7.6,-5.4 -10.5,-8.1 -1.4,-1.4 -2.8,-2.6 -4,-3.9 -1.1,-1.3 -2.2,-2.5 -3.1,-3.5 -0.5,-0.5 -0.9,-1 -1.3,-1.5 -0.4,-0.5 -0.7,-1 -1.1,-1.4 -0.7,-0.9 -1.2,-1.6 -1.7,-2.2 -0.9,-1.2 -1.4,-1.9 -1.4,-1.9 z"
|
||||
id="path10" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="205.89999"
|
||||
cy="153.10001"
|
||||
r="24.6"
|
||||
id="circle10" />
|
||||
<g
|
||||
fill="#808285"
|
||||
id="g11">
|
||||
<path
|
||||
d="m 192.1,156.9 v -5 h 9 v 5 z m 24.7,6.3 h -6.4 v -12.3 c 0,-1.5 0,-2.9 0.1,-4.1 -0.4,0.5 -0.9,1 -1.5,1.5 l -2.6,2.2 -3.3,-4 8,-6.5 h 5.7 z"
|
||||
id="path11" />
|
||||
</g>
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="145.3"
|
||||
cy="168.7"
|
||||
r="24.6"
|
||||
id="circle11" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 150.5,178.7 h -6.4 v -12.3 c 0,-1.5 0,-2.9 0.1,-4.1 -0.4,0.5 -0.9,1 -1.5,1.5 l -2.6,2.2 -3.3,-4 8,-6.5 h 5.7 z"
|
||||
id="path12" />
|
||||
<path
|
||||
fill="#6d6e71"
|
||||
d="m 166.7,69.4 c 0,0 0.7,-0.6 2,-1.6 1.3,-1 3.2,-2.7 5.9,-4.4 0.7,-0.4 1.3,-0.9 2.1,-1.4 0.7,-0.5 1.5,-1 2.3,-1.5 1.6,-1 3.4,-2.1 5.3,-3.2 1.9,-1 4,-2.1 6.2,-3.3 2.2,-1.1 4.6,-2.2 7.1,-3.3 9.9,-4.4 22.1,-8.5 35.4,-11.6 3.3,-0.8 6.7,-1.5 10.2,-2.1 1.7,-0.4 3.5,-0.6 5.2,-0.9 1.8,-0.3 3.5,-0.6 5.3,-0.8 1.8,-0.2 3.6,-0.5 5.4,-0.7 l 2.7,-0.3 2.7,-0.3 c 1.8,-0.2 3.6,-0.4 5.4,-0.5 l 5.5,-0.4 c 29.1,-2 58.4,1.3 79.4,7.4 10.5,3 18.8,6.5 24.5,9.4 0.9,0.5 1.4,0.7 1.4,0.7 l -5.7,10 c 7.9,-0.8 16.2,-0.7 24.8,1.4 -2.5,-8.4 -7,-16.8 -12.5,-24.6 l -5.4,10.2 c 0,0 -0.5,-0.3 -1.4,-0.8 -5.8,-2.9 -14.4,-6.6 -25.1,-9.6 -21.3,-6.2 -51,-9.5 -80.4,-7.5 l -5.5,0.4 c -1.8,0.2 -3.7,0.4 -5.5,0.5 l -2.7,0.3 -2.7,0.3 c -1.8,0.2 -3.6,0.5 -5.4,0.7 -1.8,0.2 -3.6,0.6 -5.4,0.9 -1.8,0.3 -3.5,0.5 -5.3,0.9 -3.5,0.7 -6.9,1.3 -10.3,2.2 -13.5,3.1 -25.8,7.2 -35.9,11.8 -2.5,1.2 -4.9,2.3 -7.2,3.4 -2.2,1.2 -4.4,2.3 -6.3,3.4 -1.9,1.2 -3.7,2.3 -5.4,3.3 l -2.4,1.5 -2.1,1.5 c -2.7,1.8 -4.7,3.5 -6,4.5 -1.4,1.1 -2.1,1.7 -2.1,1.7 z"
|
||||
id="path13" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="151.7"
|
||||
cy="84.400002"
|
||||
r="24.6"
|
||||
id="circle13" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 160.9,83.8 c 0,4.1 -0.7,7.1 -2.1,9.1 -1.4,1.9 -3.5,2.9 -6.3,2.9 -2.8,0 -4.9,-1 -6.3,-3 -1.4,-2 -2.1,-5 -2.1,-8.9 0,-4.1 0.7,-7.2 2.1,-9.1 1.4,-1.9 3.5,-2.9 6.3,-2.9 2.8,0 4.9,1 6.3,3 1.4,1.9 2.1,4.9 2.1,8.9 z m -10.6,0 c 0,2.6 0.2,4.5 0.5,5.4 0.3,1 0.9,1.5 1.7,1.5 0.8,0 1.3,-0.5 1.7,-1.5 0.3,-1 0.5,-2.8 0.5,-5.4 0,-2.6 -0.2,-4.4 -0.5,-5.4 -0.3,-1 -0.9,-1.6 -1.7,-1.6 -0.8,0 -1.3,0.5 -1.7,1.5 -0.3,1 -0.5,2.9 -0.5,5.5 z"
|
||||
id="path14" />
|
||||
<path
|
||||
fill="#6d6e71"
|
||||
d="m 122.1,246.4 c 0,0 0.6,0.8 1.7,2.2 1.2,1.4 2.7,3.6 5.1,6.1 0.6,0.6 1.2,1.3 1.8,2 0.3,0.3 0.7,0.7 1,1.1 0.4,0.3 0.7,0.7 1.1,1 1.5,1.4 3.1,2.9 5,4.5 0.9,0.7 1.9,1.5 2.9,2.3 l 1.5,1.2 c 0.3,0.2 0.5,0.4 0.8,0.6 0.3,0.2 0.6,0.4 0.8,0.6 1.1,0.7 2.3,1.5 3.4,2.3 l 1.8,1.2 c 0.6,0.4 1.3,0.7 1.9,1.1 1.3,0.7 2.6,1.4 3.9,2.2 0.7,0.4 1.4,0.7 2.1,1 0.7,0.3 1.4,0.7 2.1,1 0.7,0.3 1.4,0.7 2.2,1 0.7,0.3 1.5,0.7 2.2,1 1.5,0.6 3.1,1.2 4.6,1.8 1.5,0.6 3.2,1.1 4.8,1.6 0.8,0.3 1.6,0.5 2.5,0.8 0.8,0.3 1.7,0.5 2.5,0.7 1.7,0.4 3.4,0.8 5.2,1.3 0.9,0.2 1.8,0.4 2.6,0.6 0.9,0.2 1.8,0.3 2.7,0.5 3.6,0.8 7.3,1.1 11,1.6 1.9,0.2 3.7,0.3 5.6,0.5 0.9,0.1 1.9,0.1 2.8,0.2 1,0 1.9,0.1 2.9,0.1 7.6,0.4 15.4,0 23.1,-0.6 l 5.8,-0.6 c 1.9,-0.2 3.8,-0.5 5.7,-0.8 3.8,-0.5 7.6,-1.3 11.4,-2 1.9,-0.3 3.7,-0.8 5.6,-1.2 1.8,-0.4 3.7,-0.8 5.5,-1.3 3.6,-1 7.2,-1.9 10.6,-3 13.9,-4.2 26.5,-9.5 36.9,-14.7 10.4,-5.2 18.6,-10.3 24.3,-14 0.9,-0.6 1.3,-0.9 1.3,-0.9 l 6.5,9.6 3.1,-6.1 2.8,-6.2 1.3,-3.1 1.2,-3.1 2.4,-6.2 -6.5,1 -3.2,0.5 -3.2,0.3 -6.3,0.6 -6.3,0.3 6.5,9.6 c 0,0 -0.5,0.3 -1.3,0.9 -5.6,3.6 -13.7,8.7 -24,13.8 -10.3,5.1 -22.7,10.3 -36.4,14.5 -3.4,1.1 -6.9,2 -10.5,3 -1.8,0.5 -3.6,0.9 -5.4,1.3 -1.8,0.4 -3.6,0.9 -5.5,1.2 -3.7,0.7 -7.4,1.4 -11.2,1.9 -1.9,0.3 -3.8,0.6 -5.7,0.8 l -5.7,0.6 c -7.6,0.6 -15.2,1 -22.7,0.6 -0.9,0 -1.9,-0.1 -2.8,-0.1 -0.9,-0.1 -1.9,-0.1 -2.8,-0.2 -1.9,-0.2 -3.7,-0.3 -5.5,-0.5 -3.6,-0.5 -7.3,-0.9 -10.7,-1.6 -0.9,-0.2 -1.7,-0.3 -2.6,-0.5 -0.9,-0.2 -1.7,-0.3 -2.6,-0.5 -1.7,-0.4 -3.4,-0.8 -5,-1.2 -0.8,-0.2 -1.7,-0.4 -2.5,-0.7 -0.8,-0.3 -1.6,-0.5 -2.4,-0.8 -1.6,-0.5 -3.2,-0.9 -4.7,-1.6 -1.5,-0.6 -3,-1.2 -4.5,-1.7 -0.7,-0.3 -1.5,-0.6 -2.2,-0.9 -0.7,-0.3 -1.4,-0.7 -2.1,-1 -0.7,-0.3 -1.4,-0.6 -2.1,-1 -0.7,-0.3 -1.4,-0.6 -2,-1 -1.3,-0.7 -2.6,-1.4 -3.8,-2.1 -9.9,-5.6 -16.9,-12.1 -21.3,-17 -2.3,-2.4 -3.8,-4.5 -4.9,-5.9 -1.1,-1.4 -1.7,-2.1 -1.7,-2.1 z"
|
||||
id="path15" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="105.9"
|
||||
cy="227.7"
|
||||
r="24.6"
|
||||
id="circle15" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="M 114,237.8 H 97.1 v -4.1 l 5.7,-5.8 c 1.6,-1.7 2.7,-2.9 3.2,-3.5 0.5,-0.6 0.8,-1.2 1,-1.6 0.2,-0.4 0.3,-0.9 0.3,-1.4 0,-0.6 -0.2,-1.1 -0.6,-1.4 -0.4,-0.4 -0.9,-0.5 -1.7,-0.5 -0.7,0 -1.5,0.2 -2.2,0.6 -0.7,0.4 -1.6,1 -2.5,1.9 l -3.5,-4.1 c 1.2,-1.1 2.2,-1.8 3,-2.3 0.8,-0.5 1.7,-0.8 2.7,-1.1 1,-0.3 2,-0.4 3.2,-0.4 1.5,0 2.9,0.3 4,0.8 1.1,0.5 2.1,1.3 2.8,2.3 0.7,1 1,2.1 1,3.3 0,0.9 -0.1,1.8 -0.3,2.5 -0.2,0.8 -0.6,1.5 -1.1,2.3 -0.5,0.8 -1.1,1.5 -1.9,2.4 -0.8,0.8 -2.5,2.4 -5.1,4.7 v 0.2 h 8.8 v 5.2 z"
|
||||
id="path16" />
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 12 KiB |
|
|
@ -270,7 +270,7 @@ We mentioned order isomorphisms several times already so this is about time to e
|
|||
|
||||
|
||||
|
||||
> An order isomorphism is essentially an isomorphism between the orders' underlying sets (invertible function). However, besides their underlying sets, orders also have the arrows that connect them, so there is one more condition: in order for an invertible function to constitute an order isomorphism it has to *respect those arrows*, in other words it should be *order preserving*. More specifically, applying this function (let's call it $F$) to any two elements in one set ($a$ and $b$) should result in two elements that have the same corresponding order in the other set (so $a ≤ b$ if and only if $F(a) ≤ F(b)$).
|
||||
> An order isomorphism is essentially an isomorphism between the orders' underlying sets (invertible function). However, besides their underlying sets, orders also have the arrows that connect them, so there is one more condition: in order for an invertible function to constitute an order isomorphism, it has to *respect those arrows*, in other words it should be *order preserving*. More specifically, applying this function (let's call it $F$) to any two elements in one set ($a$ and $b$) should result in two elements that have the same corresponding order in the other set (so $a ≤ b$ if and only if $F(a) ≤ F(b)$).
|
||||
Birkhoff's representation theorem
|
||||
---
|
||||
|
||||
|
|
|
|||
|
|
@ -71,7 +71,7 @@ Tautologies
|
|||
|
||||
We often cannot tell whether a given composite proposition is true or false without knowing the values of the propositions that compose it. However, with propositions such as *modus ponens* we can: modus ponens is *always true*, regardless of whether the propositions that form it are true or false. If we want to be fancy, we can also say that it is *true in all models of the logical system*, a model being a set of real-world premises are taken to be signified by our propositions.
|
||||
|
||||
For example, our previous example will not stop being true if we substitute "Socrates" with any other name, nor if we substitute "mortal" for any other quality that humans possess.
|
||||
For example, our previous example will not stop being true if we *substitute* "Socrates" with any other name, nor if we substitute "mortal" for any other quality that humans possess.
|
||||
|
||||
|
||||
|
||||
|
|
@ -85,11 +85,13 @@ Here are some more complex (less boring) tautologies (the symbol $¬$ means "not
|
|||
|
||||
|
||||
|
||||
We will learn how to determine which propositions are a tautologies shortly, but first let's see why is this important at all i.e. what are tautologies good for: tautologies are useful because they are the basis of *axiom schemas*/*rules of inference*. And *axiom schemas* or *rules of inference* serve as starting point from which we can generate other true logical statements by means of substitution.
|
||||
We will learn how to determine which propositions are a tautologies shortly, but first let's see why is this important at all i.e. what are tautologies good for.
|
||||
|
||||
Axiom schemas/Rules of inference
|
||||
---
|
||||
|
||||
Tautologies are useful because they are the basis of *axiom schemas*/*rules of inference*. And *axiom schemas* or *rules of inference* serve as starting point from which we can generate other true logical statements by means of substitution.
|
||||
|
||||
Realizing that the colors of the balls in modus ponens are superficial, we may want to represent the general structure of modus ponens that all of its variations share.
|
||||
|
||||
|
||||
|
|
@ -100,7 +102,7 @@ Note that the propositions that we plug into the schema don't have to be primary
|
|||
|
||||
|
||||
|
||||
*Axiom schemas* and *rules of inference* are almost the same thing except they allow us to actually distill the conclusion from the premises. For example in the case above, we can use modus ponens as a rule of inference to proves that $a \lor b$ is true.
|
||||
*Axiom schemas* and *rules of inference* are almost the same thing except that rules of inference allow us to actually distill the conclusion from the premises. For example in the case above, we can use modus ponens as a rule of inference to proves that $a \lor b$ is true.
|
||||
|
||||
All axiom schemas can be easily applied as rules of inference and the other way around.
|
||||
|
||||
|
|
|
|||
|
|
@ -1,54 +1,72 @@
|
|||
---
|
||||
layout: default
|
||||
title: Types
|
||||
---
|
||||
|
||||
In the last "category overview" chapter in the book, we will talk about, in my opinion, the most interesting category of all --- the category of **types**.
|
||||
In the last "category overview" chapter in the book, we will talk about, in my opinion, the most interesting category of all --- the category of *types*.
|
||||
|
||||
This might be disappointing, if you expected to learn about as many *new* categories as possible (for which you don't even suspect that they are categories till the unexpected reveal), as we've been giving examples with the category of types in programming languages ever since the first chapter, so we already know that they form a category, and *how* they form it. You have also heard about the Curry-Howard correspondence, that connects types and logic, which we will be discussing in depth
|
||||
This might be disappointing, if you expected to learn about as many *new* categories as possible (for which you don't even suspect that they are categories till the unexpected reveal), as we've been giving examples with the category of types in a given programming language ever since the first chapter, so we already know that they form a category, and *how* they form it. You have also heard about the Curry-Howard correspondence, that connects types and logic.
|
||||
|
||||
However, types are not just about programming languages --- they are an alternative to sets (and categories) as the foundational language of mathematics. More so, they are as powerful tool as any of those formalisms.
|
||||
|
||||
Sets and types
|
||||
Sets, Types and Russell's paradox
|
||||
===
|
||||
|
||||
Most books about category theory (and mathematics in general) begin with sets. The reason for this is simply because *sets are simple to understand*, at least when we are operating on the conceptual level that is customary for introductory materials --- when we draw a circle around a few things, everyone knows what we are talking about.
|
||||
So, here we are back at sets. Most books about category theory (and mathematics in general) begin with sets. The reason for this is simply because *sets are simple to understand*, at least when we are operating on the conceptual level that is customary for introductory materials --- when we draw a circle around a few things, everyone knows what we are talking about.
|
||||
|
||||
|
||||
|
||||
However, this initial understanding of sets is *too simple* --- it leads to a bunch of paradoxes, the most famous of which is Russell's paradox.
|
||||
|
||||
Russell's paradox
|
||||
---
|
||||
|
||||
Type theory and set theory are also related historically, the first version of type theory was developed by Bertrand Russell in response to a paradox that he found in the first version of set theory (usually called *naive* set theory). This paradox is called *Russel's paradox*.
|
||||
|
||||
Russel's paradox arises due to the very same characteristics of set theory that makes it so simple - the idea that everything is a set that contains other sets. The core of the paradox, is that (unlike a type), a set can contain itself.
|
||||
|
||||
|
||||
|
||||
Unlike the set above, most sets that we discussed (like the empty set and singleton sets) do not contain themselves.
|
||||
Most sets that we discussed (like the empty set and singleton sets) do not contain themselves.
|
||||
|
||||
|
||||
|
||||
In order to understand Russell's paradox we will try to visualize *the set of all sets that do not contain themselves*. In the original set notation we can define this set to be such that it contains all sets $x$ such that $x$ is not a member of $x$), or $\{x \mid x ∉ x \}$
|
||||
However, since in set theory everything is a set and the elements of sets are again sets, a set can contain a*set can contain itself*.
|
||||
|
||||
|
||||
|
||||
This is root cause of Russel's paradox. In order to understand it, we will try to visualize *the set of all sets that do not contain themselves*. In the original set notation we can define this set to be such that it contains all sets $x$ such that $x$ is not a member of $x$), or $\{x \mid x ∉ x \}$
|
||||
|
||||
|
||||
|
||||
If we look at the definition, we recognize that the set that we just defined does not contain itself and therefore it belongs there as well.
|
||||
However, there is something wrong with this picture --- if we look at the definition, we recognize that the set that we just defined does not contain itself and therefore it belongs there as well.
|
||||
|
||||
|
||||
|
||||
Hmm, something is not quite right with this diagram as well --- because of the new adjustments that we made, our set now *contains itself*. And removing it from the set would just bring us back to the previous situation. So, this is Russell's paradox.
|
||||
Hmm, something is not quite right here either --- because of the new adjustments that we made, our set now *contains itself*. And removing it from the set would just take us back to where we started. This is Russell's paradox.
|
||||
|
||||
Resolving the paradox --- ZFC
|
||||
Resolving the paradox in set theory
|
||||
---
|
||||
|
||||
Russel's paradox completely changed the game of set theory, as averting it requires that we impose certain restrictions to the ways in which you can define sets. i.e. we can no longer allow sets to be generated freely.
|
||||
We may deem Russell's paradox unimportant at first, our initial reaction being something like
|
||||
|
||||
And, while doing so is possible, (the new paradox-free “version” of set theory by Zermelo and Fraenkel is still in use today) the result is not simple.
|
||||
> "Wait, can't we *just* add some rules that say that you cannot draw the set that contains itself?"
|
||||
|
||||
Resolving the paradox --- Types
|
||||
This was exactly what the mathematicians Ernst Zermelo and Abraham Fraenkel set out to do (no pun intended), by defining the *Zermelo–Fraenkel set theory*, or *ZFC* (the *C* at the end is a separate story). ZFC was a success, and it is still in use today, however it compromises one of the best features that sets have, namely their *simplicity*.
|
||||
|
||||
Why? The original formulation of set theory was based on just one (rather vague) rule/axiom: "Given a property P, there exists a set of all objects that have this property" i.e. any bunch of objects can be put to a set.
|
||||
|
||||
|
||||
|
||||
In contrast, ZFC is defined by a larger number of (more restrictive) axioms, such as the *axiom of pairing*, which states that given any two sets, there exist a set which contains them as elements.
|
||||
|
||||
|
||||
|
||||
...or *the axiom of union*, stating that if you have two sets you also have the set that contains all their elements.
|
||||
|
||||
|
||||
|
||||
There are a total of about 8 such axioms (depending on the flavour of the theory), curated in a way that allows us to construct all sets that are interesting, without being able to construct sets that lead to a contradiction.
|
||||
|
||||
Resolving the paradox with type theory
|
||||
---
|
||||
|
||||
While Zermelo was rushing amend the theory of sets to avert Russell's paradox, Russell himself took a different route and decided to developed an entirely new mathematical theory that is like set theory, but which is much more strict and rigid.
|
||||
While Zermelo and Fraenkel were working on refining axioms of set theory in order to avert Russell's paradox, Russell himself took a different route and decided to ditch sets altogether, and develop an entirely new mathematical theory that is free of paradoxes by design. He called it *the theory of types* (or *type theory*).
|
||||
|
||||
Like set theory, type theory is based on the concept of an objects that are categorized as "belonging" to some other entities. In *set theory*, these entities are *sets* and the concept --- *membership* (*denoted $a \in A$) --- the object $a$ is an element of the set $A$ and in *type theory*, these entitities are, *types* and the concept is **, denoted $a : A$ --- the object $a$ is an $A$.
|
||||
Type theory is not entirely different from set theory, as the concepts of *types* and *terms* are clearly looks reminiscent of the concepts of *sets* and *elements*
|
||||
|
||||
|Theory |Set theory| Type Theory|
|
||||
|------ | ---------| --------|
|
||||
|
|
@ -56,19 +74,240 @@ Like set theory, type theory is based on the concept of an objects that are cate
|
|||
|Belongs to a | Set | Type |
|
||||
|Notation | $a \in A$ | $a : A$ |
|
||||
|
||||
The big difference is that in type theory *a term can only belong to one type*. i.e. the type of each term is an intruistic property of the term.
|
||||
The biggest difference, between the two, when it comes to *structure* is that terms are bound to their types.
|
||||
|
||||
In this respect, type theory can be seen as a more restrictive version of set theory --- all types are sets, but not all sets are types.
|
||||
So, while in set theory, one element can be a member of many sets
|
||||
|
||||
|
||||
|
||||
In type theory, a term can have only one type. (note that the red ball in the small circle is different from the red ball in the bigger circle)
|
||||
|
||||
|
||||
|
||||
For this reason, types, by definition cannot contain themselves. So this settles Russell's paradox. However, the concept is very weird --- we are basically saying that if you have the type `Human` that contains all humans and the type `Mathematician` that contains all mathematicians, than the mathematician Jencel is a different object than the human Jencel.
|
||||
|
||||
<!--comic(and no, I am not implying that mathematicians aren't human). -->
|
||||
|
||||
It only starts to make some sense once we realize that we can always convert the more general version of the value to the more specific one, using the image function that we learned about in the first chapter.
|
||||
|
||||
|
||||
|
||||
As you would see shortly, the concept of types has to do a lot with the concept of functions.
|
||||
|
||||
What are types
|
||||
===
|
||||
|
||||
> "Every propositional function φ(x)—so it is contended—has, in addition to its range of truth, a range of significance, i.e. a range within which x must lie if φ(x) is to be a proposition at all, whether true or false. This is the first point in the theory of types; the second point is that ranges of significance form types, i.e. if x belongs to the range of significance of φ(x), then there is a class of objects, the *type* of x, all of which must also belong to the range of significance of φ(x)" --- Bertrand Russell - Principles of Mathematics
|
||||
|
||||
So let's set all these things aside (haha, this time it was on purpose) and see how do we define a type theory in its own right.
|
||||
|
||||
We say *a* type theory, because (time for a long disclaimer) there are not one, but many different (albeit related) formulations of type theory that are, confusingly, called type *theories* (and less confusingly, *type systems*), such as *Simply-typed lambda calculus* or *Intuitionistic type theory*, so it makes sense to speak about *a* type theory. <!--comic: Dr. Smisloff --- I think they are not confused enough --> At the same time, "type theory" (uncountable) refers to the whole field of study of type theories, just like category theory is the study of categories. Moreover, (take a deep breath) you can sometimes think of the different type systems as "different versions of type theory" and so, when people talk about a given set of features that are common to all type systems, they sometimes use the term "type theory" to refer to any random type system that has these features.
|
||||
|
||||
But back to our subject (however you call it).
|
||||
|
||||
After discovering his paradox, Russell started searching for a new way to define all collections of objects that are *interesting*, without accidentally defining collections that lead us ashtray, (and without having to make up a multitude of additional axioms, a-la ZFC). He devised a system that fits all these criteria, based on a revolutionary new idea... which is basically the same idea that is at the heart of category theory (I don't know why he never got credit for being a category theory pioneer): The *interesting* collections, the ones that we want to talk about in the first place, are the *collections that are the source and target of functions*.
|
||||
|
||||
Building types
|
||||
===
|
||||
|
||||
We saw that type theory is not so different from set theory when it comes to *structure that it produces*, as all types are sets (although not all sets are types) and all functions are still functions. However, type theory is very different from set theory when it comes to *how does this structure come about*.
|
||||
|
||||
In set theory, we start by building all sets and elements. Even we can say (as the existence of all sets is just a result of the axioms) that all sets and their elements are already there at the beginning, floating around and waiting to be explored.
|
||||
|
||||
|
||||
|
||||
Then, with the sets already in place, we start defining functions between them.
|
||||
|
||||
|
||||
|
||||
In type theory, we start with a blank sheet [digram ommitted] and we start defining functions, only *through the functions* do the types come to be. More specifically, we start by defining a functions that ouput things from nothing thus defining the sets that we want to study (like for example the numbers, the booleans etc).
|
||||
|
||||
Next we define functions again, but
|
||||
|
||||
|
||||
|
||||
Because a term can only belong to one type, in type theory, the natural number 1 is denoted as $1: \mathbb{N}$) and it is an entirely separate object from the integer 1 (denoted or $1: \mathbb{Z}$)
|
||||
|
||||
|
||||
|
||||
|
||||
In programming
|
||||
----
|
||||
|
||||
> "In general, we can think of data as defined by some collection of selectors and constructors, together with specified conditions that these procedures must fulfill in order to be a valid representation." --- Harold Abelson, Gerald Jay Sussman, Julie Sussman - Structure and Interpretation of Computer Programs
|
||||
|
||||
So, we already have some idea of what a type is: a type is a collection of terms, that is the source and target of *functions*. This definition may seem a bit vague, but it is trivial when we look at how types are defined in computer programming.
|
||||
|
||||
```
|
||||
class MyType<A> {
|
||||
|
||||
a: A;
|
||||
constructor(a) {
|
||||
this.a = a;
|
||||
}
|
||||
|
||||
getA() {
|
||||
return this.a;
|
||||
}
|
||||
|
||||
}
|
||||
```
|
||||
|
||||
It is obvious, even when viewed through the lense of traditional imperative languages, that the definition of a type consists of the definitions of *a bunch of functions*. However, not just any random collection of functions would suffice -- there are 3 special kinds of functions that have to be defined in order for a type to work.
|
||||
|
||||
First off, a type has to have a *definition* which specifies what it is. Note that this is not a function between values, but a function between types --- a *type-level function*. In programming, we call these types of functions *generic types*, but they are functions nevertheless --- we supply some types and get a definition of the new type.
|
||||
|
||||
```
|
||||
class MyType<A> {
|
||||
a: A;
|
||||
```
|
||||
|
||||
(For non-generic types, the rule would correspond to a type-level function with no arguments, which would correspond to a (non-generic) type.)
|
||||
|
||||
Next up, a type has to have at least one *constructor* which allows us to produce a value/term of that type. The constructor is a "normal" value-level function.
|
||||
|
||||
```
|
||||
constructor(a) {
|
||||
this.a = a;
|
||||
}
|
||||
```
|
||||
|
||||
Finally, a type has to have at least one *method* in order to be useful --- we don't want to construct types just for the sake of constructing new types.
|
||||
|
||||
Methods are functions that allow us to do something with a value of that type, once we constructed it.
|
||||
|
||||
```
|
||||
getA() {
|
||||
return this.a;
|
||||
}
|
||||
```
|
||||
|
||||
(There are also methods that mutate the type's properties, but we don't talk about these in functional programming.)
|
||||
|
||||
In Category Theory
|
||||
---
|
||||
|
||||
Now, let's see the categorical perspective of what are we taling about. We already know that a type corresponds to an *object* in the category of types, and a categorical object has to have at three kinds of morphisms in order for the object to play a role in the category, which correspond to the three types of functions in programming.
|
||||
|
||||
Firstly, a categorical object has to have a morphism that defines it. This one is more special, as it is not an ordinary morphism in the object's category, but we will discuss what exactly it is later (it is connected to the idea of a universal property.)
|
||||
|
||||
Secondly, a categorical object has to have at least one morphism coming *to* it, from some other object in the category. In other words, it has to be the *target* of at least one arrow.
|
||||
|
||||
And thirdly, it has to have morphisms from it to some other objects. Has to be the *source* of at least one arrow.
|
||||
|
||||
In type theory
|
||||
---
|
||||
|
||||
We will now see how these type-creating functions look like in type theory.
|
||||
|
||||
|
||||
The functions that define a type are called *typing rules* and each of them has a name.
|
||||
|
||||
|
||||
For this, we need to get to know the formal language that is used for defining them, called *natural deduction*.
|
||||
|
||||
$$\frac
|
||||
{A \; \mathrm{type}}
|
||||
{MyType \; A \; \mathrm{type}}
|
||||
$$
|
||||
|
||||
$$\frac
|
||||
{a : A}
|
||||
{mytype\;a : MyType \; A}
|
||||
$$
|
||||
|
||||
$$\frac
|
||||
{mytype\;a : MyType \; A}
|
||||
{a : A}
|
||||
$$
|
||||
|
||||
|
||||
Typing rules and the principle of substitution
|
||||
===
|
||||
|
||||
So, why do we call morphisms in type theory *rules*? To understand that, we have to understand the principle that is underneath all of type theory --- the principle of substitution.
|
||||
|
||||
We already saw that functions in type theory and set theory look identical ---
|
||||
|
||||
|
||||
|
||||
|
||||
However, in set theory, sets are just assumed to exist, as for example the set of colors, as any other set is just assumed to exist.
|
||||
|
||||
And type theory, functions are build.
|
||||
|
||||
|
||||
These ways, type theory holds, is nothing more than the process of *substituting* one value with another, according to a finite number of rules.
|
||||
|
||||
This principle is also underneat the way axiom schemas are used in logic, but it is actually much more general than that. It is also the principle behind algrebra in general e.g. the rules of addition are nothing but rules that define when can you substitute a value to another.
|
||||
|
||||
But wait, are substitution rules really powerful enough to represent all functions? How would we go about in representing types that have an infinite number of terms (such as the natural numbers), and functions between them (such as the `sum` function).
|
||||
|
||||
|
||||
Type theory and logic
|
||||
---
|
||||
|
||||
Type theory and computation
|
||||
---
|
||||
|
||||
|
||||
The product type
|
||||
===
|
||||
|
||||
> "In general, we can think of data as defined by some collection of selectors and constructors, together with specified conditions that these procedures must fulfill in order to be a valid representation." --- Hal Abelson Jerry Sussman and Julie Sussman, SICP
|
||||
|
||||
Type formation rules
|
||||
---
|
||||
|
||||
When we define a new type we firstly want to *provide a type definition* show what the type should look like. This is known as the *type-formation rule*.
|
||||
|
||||
$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \times B \; \mathrm{type}}$$
|
||||
|
||||
Term introduction rules
|
||||
---
|
||||
|
||||
OK, now that we have the definition of the type, we would typically want a way to create values from that type or, in other words we would need *constructors*.
|
||||
|
||||
```
|
||||
constructor(a, b) {
|
||||
this.a = a;
|
||||
this.b = b;
|
||||
}
|
||||
```
|
||||
|
||||
In type-theoretic terms, we would call constructor a *term introduction rule*, (*term* being the type-theoretic word for value).
|
||||
|
||||
|
||||
Introduction rules for product types:
|
||||
|
||||
$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma\vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash (x, y):A \times B}$$
|
||||
|
||||
Term elimination rules
|
||||
---
|
||||
|
||||
$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, z:A \times B \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, z:A \times B \vdash \pi_2(z):B}$$
|
||||
|
||||
Computation rule
|
||||
---
|
||||
|
||||
$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma\vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \beta_{\times 1}(x, y):\pi_1((x, y)) =_A x} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \beta_{\times 2}(x, y):\pi_2((x, y)) =_{B} y}$$
|
||||
|
||||
Uniqueness rules
|
||||
---
|
||||
|
||||
$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, z:A \times B \vdash \eta_{\times}(z):z =_{A \times B} (\pi_1(z), \pi_2(z))}$$
|
||||
|
||||
This may seem weird at first, e.g., when we create a subtype for example, as in the type-theoretic example of our constructing the set of all balls with warm colors, we end up with two instances of all objects that are members of both types, but it actually makes sense after we get used to it. After all, we can always convert the more general version of the value to the more specific one, using the function that exist between each set and its subset.
|
||||
|
||||
|
||||
Types as mathematical foundation
|
||||
====
|
||||
===
|
||||
|
||||
Types and computation
|
||||
===
|
||||
|
||||
Types and logic
|
||||
===
|
||||
|
||||
|
||||
Numbers as types
|
||||
===
|
||||
|
|
|
|||
319
_chapters/06_type/int_nat_type.svg
Normal file
319
_chapters/06_type/int_nat_type.svg
Normal file
|
|
@ -0,0 +1,319 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 300"
|
||||
version="1.1"
|
||||
id="svg9"
|
||||
sodipodi:docname="int_nat_type.svg"
|
||||
inkscape:version="1.3 (1:1.3+202307231459+0e150ed6c4)"
|
||||
width="595.29999"
|
||||
height="300"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs9" />
|
||||
<sodipodi:namedview
|
||||
id="namedview9"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1"
|
||||
showgrid="false"
|
||||
inkscape:zoom="1.14805"
|
||||
inkscape:cx="265.23235"
|
||||
inkscape:cy="116.28413"
|
||||
inkscape:window-width="1080"
|
||||
inkscape:window-height="1864"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="0"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg9" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
cx="433.15701"
|
||||
cy="150.95799"
|
||||
r="128.93355"
|
||||
id="circle1"
|
||||
style="stroke-width:6.75045;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="423.03134"
|
||||
cy="143.53252"
|
||||
r="127.69597"
|
||||
id="circle2"
|
||||
style="fill:#e2e3db;stroke-width:6.75045;stroke-miterlimit:10" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
cx="142.93198"
|
||||
cy="157.88959"
|
||||
r="95.558693"
|
||||
id="circle1-3"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="135.42737"
|
||||
cy="152.38623"
|
||||
r="94.641464"
|
||||
id="circle2-6"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<g
|
||||
id="g2"
|
||||
transform="translate(222.13958,-133.07686)">
|
||||
<path
|
||||
d="m 197.09695,390.8976 16.09375,-25.25391 h -4.57031 l -16.09375,25.25391 z m -6.66016,-27.20703 h 25.29297 v 1.95312 l -16.09375,25.25391 h 16.54297 v 1.95312 h -26.19141 v -1.95312 l 16.09375,-25.25391 h -15.64453 z"
|
||||
id="text1-3"
|
||||
style="font-size:40px;line-height:1.25;font-family:'Mell Display 0.6';-inkscape-font-specification:'Mell Display 0.6, ';word-spacing:0px;fill:#ffffff"
|
||||
aria-label="ℤ" />
|
||||
<path
|
||||
d="m 195.21495,389.82813 16.09375,-25.25391 h -4.57031 l -16.09375,25.25391 z m -6.66016,-27.20703 h 25.29297 v 1.95312 l -16.09375,25.25391 h 16.54297 v 1.95312 h -26.19141 v -1.95312 l 16.09375,-25.25391 h -15.64453 z"
|
||||
id="text1"
|
||||
style="font-size:40px;line-height:1.25;font-family:'Mell Display 0.6';-inkscape-font-specification:'Mell Display 0.6, ';word-spacing:0px;fill:#4d4d4d"
|
||||
aria-label="ℤ" />
|
||||
</g>
|
||||
<g
|
||||
id="g1"
|
||||
transform="translate(21.915558,-139.76279)">
|
||||
<path
|
||||
d="m 124.27316,376.32518 -14.57031,-25.25391 h -4.64843 l 14.57031,25.25391 z m -21.75781,-27.20703 h 8.28125 l 14.0625,24.39453 v -24.39453 h 1.95313 v 29.16016 h -8.28125 l -14.0625,-24.39454 v 24.39454 h -1.95313 z"
|
||||
id="text2-6"
|
||||
style="font-size:40px;line-height:1.25;font-family:'Mell Display 0.6';-inkscape-font-specification:'Mell Display 0.6, ';word-spacing:0px;fill:#ffffff"
|
||||
aria-label="ℕ" />
|
||||
<path
|
||||
d="M 122.39116,375.25571 107.82085,350.0018 h -4.64843 l 14.57031,25.25391 z m -21.75781,-27.20703 h 8.28125 l 14.0625,24.39453 v -24.39453 h 1.95313 v 29.16016 h -8.28125 l -14.0625,-24.39454 v 24.39454 h -1.95313 z"
|
||||
id="text2"
|
||||
style="font-size:40px;line-height:1.25;font-family:'Mell Display 0.6';-inkscape-font-specification:'Mell Display 0.6, ';word-spacing:0px;fill:#4d4d4d"
|
||||
aria-label="ℕ" />
|
||||
</g>
|
||||
<g
|
||||
id="g5"
|
||||
transform="translate(-247.59768,249.40423)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="345.37347"
|
||||
cy="-141.91046"
|
||||
r="24.6"
|
||||
id="circle5-3" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 354.57346,-142.51047 c 0,4.1 -0.7,7.1 -2.1,9.1 -1.4,1.9 -3.5,2.9 -6.3,2.9 -2.8,0 -4.9,-1 -6.3,-3 -1.4,-2 -2.1,-5 -2.1,-8.9 0,-4.1 0.7,-7.2 2.1,-9.1 1.4,-1.9 3.5,-2.9 6.3,-2.9 2.8,0 4.9,1 6.3,3 1.4,1.9 2.1,4.9 2.1,8.9 z m -10.6,0 c 0,2.6 0.2,4.5 0.5,5.4 0.3,1 0.9,1.5 1.7,1.5 0.8,0 1.3,-0.5 1.7,-1.5 0.3,-1 0.5,-2.8 0.5,-5.4 0,-2.6 -0.2,-4.4 -0.5,-5.4 -0.3,-1 -0.9,-1.6 -1.7,-1.6 -0.8,0 -1.3,0.5 -1.7,1.5 -0.3,1 -0.5,2.9 -0.5,5.5 z"
|
||||
id="path5" />
|
||||
</g>
|
||||
<g
|
||||
id="g4"
|
||||
transform="translate(-247.59768,249.40423)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="420.17346"
|
||||
cy="-88.010475"
|
||||
r="24.6"
|
||||
id="circle7-6" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 428.27346,-77.910475 h -16.9 v -4.1 l 5.7,-5.8 c 1.6,-1.7 2.7,-2.9 3.2,-3.5 0.5,-0.6 0.8,-1.2 1,-1.6 0.2,-0.4 0.3,-0.9 0.3,-1.4 0,-0.6 -0.2,-1.1 -0.6,-1.4 -0.4,-0.4 -0.9,-0.5 -1.7,-0.5 -0.7,0 -1.5,0.2 -2.2,0.6 -0.7,0.4 -1.6,1 -2.5,1.9 l -3.5,-4.1 c 1.2,-1.1 2.2,-1.8 3,-2.299995 0.8,-0.5 1.7,-0.8 2.7,-1.1 1,-0.3 2,-0.4 3.2,-0.4 1.5,0 2.9,0.3 4,0.8 1.1,0.5 2.1,1.299995 2.8,2.299995 0.7,1 1,2.1 1,3.3 0,0.9 -0.1,1.8 -0.3,2.5 -0.2,0.8 -0.6,1.5 -1.1,2.3 -0.5,0.8 -1.1,1.5 -1.9,2.4 -0.8,0.8 -2.5,2.4 -5.1,4.7 v 0.2 h 8.8 v 5.2 z"
|
||||
id="path7" />
|
||||
</g>
|
||||
<g
|
||||
id="g7"
|
||||
transform="translate(-241.28262,114.18854)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="405.37347"
|
||||
cy="-9.4104691"
|
||||
r="24.6"
|
||||
id="circle8-7" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 412.67346,-17.610475 c 0,1.4 -0.4,2.7 -1.3,3.7 -0.9,1 -2.2,1.8 -3.8,2.3 v 0.1 c 3.9,0.5 5.8,2.3 5.8,5.5 0,2.2 -0.9,3.9 -2.6,5.10000002 -1.7,1.2 -4.1,1.9 -7.2,1.9 -1.3,0 -2.4,-0.1 -3.5,-0.3 -1.1,-0.2 -2.2,-0.5 -3.5,-1 V -5.510475 c 1,0.5 2.1,0.9 3.1,1.2 1,0.3 2,0.4 2.9,0.4 1.4,0 2.4,-0.2 3,-0.6 0.6,-0.4 0.9,-1 0.9,-1.8 0,-0.6 -0.2,-1.1 -0.5,-1.5 -0.3,-0.4 -0.9,-0.6 -1.6,-0.8 -0.7,-0.2 -1.7,-0.3 -2.9,-0.3 h -1.4 v -4.7 h 1.5 c 3.2,0 4.8,-0.8 4.8,-2.5 0,-0.6 -0.2,-1.1 -0.7,-1.4 -0.5,-0.3 -1.1,-0.4 -1.9,-0.4 -1.5,0 -3,0.5 -4.6,1.5 l -2.6,-4.2 c 1.2,-0.9 2.5,-1.5 3.8,-1.8 1.3,-0.4 2.8,-0.5 4.4,-0.5 2.4,0 4.3,0.5 5.7,1.4 1.5,0.9 2.2,2.2 2.2,3.9 z"
|
||||
id="path8" />
|
||||
</g>
|
||||
<g
|
||||
id="g8"
|
||||
transform="translate(-116.78688,254.92104)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="217.85574"
|
||||
cy="-75.016609"
|
||||
r="24.6"
|
||||
id="circle9-5"
|
||||
style="stroke:#658cc6;stroke-opacity:1" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 223.26623,-65.519029 h -6.4 v -12.3 c 0,-1.5 0,-2.9 0.1,-4.1 -0.4,0.5 -0.9,1 -1.5,1.5 l -2.6,2.2 -3.3,-4 8,-6.5 h 5.7 z"
|
||||
id="path6" />
|
||||
</g>
|
||||
<g
|
||||
id="g8-1"
|
||||
transform="translate(132.49114,191.77672)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="217.85574"
|
||||
cy="-75.016609"
|
||||
r="24.6"
|
||||
id="circle9-5-5"
|
||||
style="stroke:#658cc6;stroke-opacity:1" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 223.26623,-65.519029 h -6.4 v -12.3 c 0,-1.5 0,-2.9 0.1,-4.1 -0.4,0.5 -0.9,1 -1.5,1.5 l -2.6,2.2 -3.3,-4 8,-6.5 h 5.7 z"
|
||||
id="path6-5" />
|
||||
</g>
|
||||
<g
|
||||
id="g5-8"
|
||||
transform="translate(46.369064,206.92898)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="345.37347"
|
||||
cy="-141.91046"
|
||||
r="24.6"
|
||||
id="circle5-3-4" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 354.57346,-142.51047 c 0,4.1 -0.7,7.1 -2.1,9.1 -1.4,1.9 -3.5,2.9 -6.3,2.9 -2.8,0 -4.9,-1 -6.3,-3 -1.4,-2 -2.1,-5 -2.1,-8.9 0,-4.1 0.7,-7.2 2.1,-9.1 1.4,-1.9 3.5,-2.9 6.3,-2.9 2.8,0 4.9,1 6.3,3 1.4,1.9 2.1,4.9 2.1,8.9 z m -10.6,0 c 0,2.6 0.2,4.5 0.5,5.4 0.3,1 0.9,1.5 1.7,1.5 0.8,0 1.3,-0.5 1.7,-1.5 0.3,-1 0.5,-2.8 0.5,-5.4 0,-2.6 -0.2,-4.4 -0.5,-5.4 -0.3,-1 -0.9,-1.6 -1.7,-1.6 -0.8,0 -1.3,0.5 -1.7,1.5 -0.3,1 -0.5,2.9 -0.5,5.5 z"
|
||||
id="path5-5" />
|
||||
</g>
|
||||
<g
|
||||
id="g4-0"
|
||||
transform="translate(72.741912,199.5013)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="420.17346"
|
||||
cy="-88.010475"
|
||||
r="24.6"
|
||||
id="circle7-6-3" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 428.27346,-77.910475 h -16.9 v -4.1 l 5.7,-5.8 c 1.6,-1.7 2.7,-2.9 3.2,-3.5 0.5,-0.6 0.8,-1.2 1,-1.6 0.2,-0.4 0.3,-0.9 0.3,-1.4 0,-0.6 -0.2,-1.1 -0.6,-1.4 -0.4,-0.4 -0.9,-0.5 -1.7,-0.5 -0.7,0 -1.5,0.2 -2.2,0.6 -0.7,0.4 -1.6,1 -2.5,1.9 l -3.5,-4.1 c 1.2,-1.1 2.2,-1.8 3,-2.299995 0.8,-0.5 1.7,-0.8 2.7,-1.1 1,-0.3 2,-0.4 3.2,-0.4 1.5,0 2.9,0.3 4,0.8 1.1,0.5 2.1,1.299995 2.8,2.299995 0.7,1 1,2.1 1,3.3 0,0.9 -0.1,1.8 -0.3,2.5 -0.2,0.8 -0.6,1.5 -1.1,2.3 -0.5,0.8 -1.1,1.5 -1.9,2.4 -0.8,0.8 -2.5,2.4 -5.1,4.7 v 0.2 h 8.8 v 5.2 z"
|
||||
id="path7-6" />
|
||||
</g>
|
||||
<g
|
||||
id="g7-1"
|
||||
transform="translate(52.684124,71.713293)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="405.37347"
|
||||
cy="-9.4104691"
|
||||
r="24.6"
|
||||
id="circle8-7-0" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 412.67346,-17.610475 c 0,1.4 -0.4,2.7 -1.3,3.7 -0.9,1 -2.2,1.8 -3.8,2.3 v 0.1 c 3.9,0.5 5.8,2.3 5.8,5.5 0,2.2 -0.9,3.9 -2.6,5.10000002 -1.7,1.2 -4.1,1.9 -7.2,1.9 -1.3,0 -2.4,-0.1 -3.5,-0.3 -1.1,-0.2 -2.2,-0.5 -3.5,-1 V -5.510475 c 1,0.5 2.1,0.9 3.1,1.2 1,0.3 2,0.4 2.9,0.4 1.4,0 2.4,-0.2 3,-0.6 0.6,-0.4 0.9,-1 0.9,-1.8 0,-0.6 -0.2,-1.1 -0.5,-1.5 -0.3,-0.4 -0.9,-0.6 -1.6,-0.8 -0.7,-0.2 -1.7,-0.3 -2.9,-0.3 h -1.4 v -4.7 h 1.5 c 3.2,0 4.8,-0.8 4.8,-2.5 0,-0.6 -0.2,-1.1 -0.7,-1.4 -0.5,-0.3 -1.1,-0.4 -1.9,-0.4 -1.5,0 -3,0.5 -4.6,1.5 l -2.6,-4.2 c 1.2,-0.9 2.5,-1.5 3.8,-1.8 1.3,-0.4 2.8,-0.5 4.4,-0.5 2.4,0 4.3,0.5 5.7,1.4 1.5,0.9 2.2,2.2 2.2,3.9 z"
|
||||
id="path8-6" />
|
||||
</g>
|
||||
<g
|
||||
id="g8-3"
|
||||
transform="translate(120.34436,177.15497)" />
|
||||
<g
|
||||
id="g5-9"
|
||||
transform="translate(82.387522,272.49398)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="345.37347"
|
||||
cy="-141.91046"
|
||||
r="24.6"
|
||||
id="circle5-3-2" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 354.57346,-142.51047 c 0,4.1 -0.7,7.1 -2.1,9.1 -1.4,1.9 -3.5,2.9 -6.3,2.9 -2.8,0 -4.9,-1 -6.3,-3 -1.4,-2 -2.1,-5 -2.1,-8.9 0,-4.1 0.7,-7.2 2.1,-9.1 1.4,-1.9 3.5,-2.9 6.3,-2.9 2.8,0 4.9,1 6.3,3 1.4,1.9 2.1,4.9 2.1,8.9 z m -10.6,0 c 0,2.6 0.2,4.5 0.5,5.4 0.3,1 0.9,1.5 1.7,1.5 0.8,0 1.3,-0.5 1.7,-1.5 0.3,-1 0.5,-2.8 0.5,-5.4 0,-2.6 -0.2,-4.4 -0.5,-5.4 -0.3,-1 -0.9,-1.6 -1.7,-1.6 -0.8,0 -1.3,0.5 -1.7,1.5 -0.3,1 -0.5,2.9 -0.5,5.5 z"
|
||||
id="path5-2" />
|
||||
</g>
|
||||
<g
|
||||
id="g4-8"
|
||||
transform="translate(22.86063,276.67226)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="420.17346"
|
||||
cy="-88.010475"
|
||||
r="24.6"
|
||||
id="circle7-6-9" />
|
||||
<path
|
||||
d="m 405.56747,-86.516948 v -5 h 9 v 5 z"
|
||||
id="path1"
|
||||
style="fill:#808285;fill-opacity:1" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 436.44629,-77.260596 h -16.9 v -4.1 l 5.7,-5.8 c 1.6,-1.7 2.7,-2.9 3.2,-3.5 0.5,-0.6 0.8,-1.2 1,-1.6 0.2,-0.4 0.3,-0.9 0.3,-1.4 0,-0.6 -0.2,-1.1 -0.6,-1.4 -0.4,-0.4 -0.9,-0.5 -1.7,-0.5 -0.7,0 -1.5,0.2 -2.2,0.6 -0.7,0.4 -1.6,1 -2.5,1.9 l -3.5,-4.1 c 1.2,-1.1 2.2,-1.8 3,-2.299995 0.8,-0.5 1.7,-0.799999 2.7,-1.099999 1,-0.3 2,-0.4 3.2,-0.4 1.5,0 2.9,0.3 4,0.8 1.1,0.499999 2.1,1.299994 2.8,2.299994 0.7,1 1,2.1 1,3.3 0,0.9 -0.1,1.8 -0.3,2.5 -0.2,0.8 -0.6,1.5 -1.1,2.3 -0.5,0.8 -1.1,1.5 -1.9,2.4 -0.8,0.8 -2.5,2.4 -5.1,4.7 v 0.2 h 8.8 v 5.2 z"
|
||||
id="path7-7" />
|
||||
</g>
|
||||
<g
|
||||
id="g7-3"
|
||||
transform="translate(99.474922,182.87191)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="405.37347"
|
||||
cy="-9.4104691"
|
||||
r="24.6"
|
||||
id="circle8-7-6" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 416.94531,-16.496153 c 0,1.4 -0.4,2.7 -1.3,3.7 -0.9,1 -2.2,1.8 -3.8,2.3 v 0.1 c 3.9,0.4999996 5.8,2.2999996 5.8,5.4999996 0,2.2 -0.9,3.89999996 -2.6,5.09999998 -1.7,1.20000002 -4.1,1.90000002 -7.2,1.90000002 -1.3,0 -2.4,-0.1 -3.5,-0.3 -1.1,-0.2 -2.2,-0.5 -3.5,-1.00000002 V -4.3961534 c 1,0.5 2.1,0.9 3.1,1.2 1,0.3 2,0.4 2.9,0.4 1.4,0 2.4,-0.2 3,-0.6 0.6,-0.4 0.9,-1 0.9,-1.8 0,-0.6 -0.2,-1.1 -0.5,-1.5 -0.3,-0.4 -0.9,-0.6 -1.6,-0.8 -0.7,-0.2 -1.7,-0.3 -2.9,-0.3 h -1.4 v -4.6999996 h 1.5 c 3.2,0 4.8,-0.8 4.8,-2.5 0,-0.6 -0.2,-1.1 -0.7,-1.4 -0.5,-0.3 -1.1,-0.4 -1.9,-0.4 -1.5,0 -3,0.5 -4.6,1.5 l -2.6,-4.2 c 1.2,-0.9 2.5,-1.5 3.8,-1.8 1.3,-0.4 2.8,-0.5 4.4,-0.5 2.4,0 4.3,0.5 5.7,1.4 1.5,0.9 2.2,2.2 2.2,3.9 z"
|
||||
id="path8-1" />
|
||||
<path
|
||||
d="m 389.29319,-7.9868579 v -5.0000001 h 9 v 5.0000001 z"
|
||||
id="path1-4"
|
||||
style="fill:#808285;fill-opacity:1"
|
||||
inkscape:transform-center-x="-20.153059"
|
||||
inkscape:transform-center-y="1.1151722" />
|
||||
</g>
|
||||
<g
|
||||
id="g3"
|
||||
transform="translate(212.00135,245.97395)">
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="135.57346"
|
||||
cy="-69.510475"
|
||||
r="24.6"
|
||||
id="circle10" />
|
||||
<g
|
||||
fill="#808285"
|
||||
id="g11"
|
||||
transform="translate(-70.326542,-222.61047)">
|
||||
<path
|
||||
d="m 192.1,156.9 v -5 h 9 v 5 z m 24.7,6.3 h -6.4 v -12.3 c 0,-1.5 0,-2.9 0.1,-4.1 -0.4,0.5 -0.9,1 -1.5,1.5 l -2.6,2.2 -3.3,-4 8,-6.5 h 5.7 z"
|
||||
id="path11"
|
||||
sodipodi:nodetypes="cccccccsccccccc" />
|
||||
</g>
|
||||
</g>
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 13 KiB |
169
_chapters/06_type/int_nat_type.svg.2023_11_22_14_29_41.0.svg
Normal file
169
_chapters/06_type/int_nat_type.svg.2023_11_22_14_29_41.0.svg
Normal file
|
|
@ -0,0 +1,169 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 300"
|
||||
version="1.1"
|
||||
id="svg9"
|
||||
sodipodi:docname="int_nat_type.svg"
|
||||
inkscape:version="1.3 (1:1.3+202307231459+0e150ed6c4)"
|
||||
width="595.29999"
|
||||
height="300"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs9" />
|
||||
<sodipodi:namedview
|
||||
id="namedview9"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1"
|
||||
showgrid="false"
|
||||
inkscape:zoom="0.79127337"
|
||||
inkscape:cx="218.63493"
|
||||
inkscape:cy="360.81083"
|
||||
inkscape:window-width="1080"
|
||||
inkscape:window-height="1864"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="0"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg9" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="255.50369"
|
||||
cy="-90.912781"
|
||||
r="24.6"
|
||||
id="circle9-5" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
cx="426.80408"
|
||||
cy="146.5955"
|
||||
r="128.93355"
|
||||
id="circle1"
|
||||
style="stroke-width:6.75045;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="416.67841"
|
||||
cy="139.17003"
|
||||
r="127.69597"
|
||||
id="circle2"
|
||||
style="stroke-width:6.75045;stroke-miterlimit:10;fill:#e2e3db" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
cx="136.57906"
|
||||
cy="153.5271"
|
||||
r="95.558693"
|
||||
id="circle1-3"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="129.07445"
|
||||
cy="148.02374"
|
||||
r="94.641464"
|
||||
id="circle2-6"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="300.01419"
|
||||
cy="-144.41519"
|
||||
r="24.6"
|
||||
id="circle5-3" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 309.21418,-145.01519 c 0,4.1 -0.7,7.1 -2.1,9.1 -1.4,1.9 -3.5,2.9 -6.3,2.9 -2.8,0 -4.9,-1 -6.3,-3 -1.4,-2 -2.1,-5 -2.1,-8.9 0,-4.1 0.7,-7.2 2.1,-9.1 1.4,-1.9 3.5,-2.9 6.3,-2.9 2.8,0 4.9,1 6.3,3 1.4,1.9 2.1,4.9 2.1,8.9 z m -10.6,0 c 0,2.6 0.2,4.5 0.5,5.4 0.3,1 0.9,1.5 1.7,1.5 0.8,0 1.3,-0.5 1.7,-1.5 0.3,-1 0.5,-2.8 0.5,-5.4 0,-2.6 -0.2,-4.4 -0.5,-5.4 -0.3,-1 -0.9,-1.6 -1.7,-1.6 -0.8,0 -1.3,0.5 -1.7,1.5 -0.3,1 -0.5,2.9 -0.5,5.5 z"
|
||||
id="path5" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 260.91418,-81.415186 h -6.4 v -12.3 c 0,-1.5 0,-2.9 0.1,-4.1 -0.4,0.5 -0.9,1 -1.5,1.5 l -2.6,2.2 -3.3,-4 8,-6.500004 h 5.7 z"
|
||||
id="path6" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="374.81418"
|
||||
cy="-90.515182"
|
||||
r="24.6"
|
||||
id="circle7-6" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 382.91418,-80.415186 h -16.9 v -4.1 l 5.7,-5.8 c 1.6,-1.7 2.7,-2.9 3.2,-3.5 0.5,-0.6 0.8,-1.2 1,-1.6 0.2,-0.4 0.3,-0.9 0.3,-1.4 0,-0.6 -0.2,-1.1 -0.6,-1.4 -0.4,-0.4 -0.9,-0.5 -1.7,-0.5 -0.7,0 -1.5,0.2 -2.2,0.6 -0.7,0.4 -1.6,1 -2.5,1.9 l -3.5,-4.100004 c 1.2,-1.1 2.2,-1.8 3,-2.3 0.8,-0.5 1.7,-0.8 2.7,-1.1 1,-0.3 2,-0.4 3.2,-0.4 1.5,0 2.9,0.3 4,0.8 1.1,0.5 2.1,1.3 2.8,2.3 0.7,1 1,2.100004 1,3.300004 0,0.9 -0.1,1.8 -0.3,2.5 -0.2,0.8 -0.6,1.5 -1.1,2.3 -0.5,0.8 -1.1,1.5 -1.9,2.4 -0.8,0.8 -2.5,2.4 -5.1,4.7 v 0.2 h 8.8 v 5.2 z"
|
||||
id="path7" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="360.01419"
|
||||
cy="-11.91519"
|
||||
r="24.6"
|
||||
id="circle8-7" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 367.31418,-20.115186 c 0,1.4 -0.4,2.7 -1.3,3.7 -0.9,1 -2.2,1.8 -3.8,2.3 v 0.1 c 3.9,0.5 5.8,2.3 5.8,5.4999996 0,2.2 -0.9,3.9 -2.6,5.1 -1.7,1.2 -4.1,1.9 -7.2,1.9 -1.3,0 -2.4,-0.1 -3.5,-0.3 -1.1,-0.2 -2.2,-0.5 -3.5,-1 v -5.2 c 1,0.5 2.1,0.9 3.1,1.2 1,0.3 2,0.4 2.9,0.4 1.4,0 2.4,-0.2 3,-0.6 0.6,-0.4 0.9,-1 0.9,-1.8 0,-0.6 -0.2,-1.1 -0.5,-1.4999996 -0.3,-0.4 -0.9,-0.6 -1.6,-0.8 -0.7,-0.2 -1.7,-0.3 -2.9,-0.3 h -1.4 v -4.7 h 1.5 c 3.2,0 4.8,-0.8 4.8,-2.5 0,-0.6 -0.2,-1.1 -0.7,-1.4 -0.5,-0.3 -1.1,-0.4 -1.9,-0.4 -1.5,0 -3,0.5 -4.6,1.5 l -2.6,-4.2 c 1.2,-0.9 2.5,-1.5 3.8,-1.8 1.3,-0.4 2.8,-0.5 4.4,-0.5 2.4,0 4.3,0.5 5.7,1.4 1.5,0.9 2.2,2.2 2.2,3.9 z"
|
||||
id="path8" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="263.71417"
|
||||
cy="-9.2151928"
|
||||
r="24.6"
|
||||
id="circle9" />
|
||||
<path
|
||||
fill="#808285"
|
||||
d="m 272.51418,-3.6151864 h -2.6 v 4.49999997 h -6.2 V -3.6151864 h -9.3 v -4.6 l 9.7,-14.1999996 h 5.8 v 14.0999996 h 2.6 z m -8.8,-4.7 v -2.6999996 c 0,-0.5 0,-1.2 0.1,-2.1 0,-0.9 0.1,-1.3 0.1,-1.4 h -0.2 c -0.4,0.8 -0.8,1.6 -1.2,2.3 l -2.6,3.7999996 h 3.8 z"
|
||||
id="path9" />
|
||||
<circle
|
||||
fill="#ffffff"
|
||||
stroke="#939598"
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
cx="90.21418"
|
||||
cy="-72.015182"
|
||||
r="24.6"
|
||||
id="circle10" />
|
||||
<g
|
||||
fill="#808285"
|
||||
id="g11"
|
||||
transform="translate(-115.68582,-225.11519)">
|
||||
<path
|
||||
d="m 192.1,156.9 v -5 h 9 v 5 z m 24.7,6.3 h -6.4 v -12.3 c 0,-1.5 0,-2.9 0.1,-4.1 -0.4,0.5 -0.9,1 -1.5,1.5 l -2.6,2.2 -3.3,-4 8,-6.5 h 5.7 z"
|
||||
id="path11" />
|
||||
</g>
|
||||
<text
|
||||
xml:space="preserve"
|
||||
style="font-size:40px;line-height:1.25;font-family:'Mell Display 0.6';-inkscape-font-specification:'Mell Display 0.6, ';word-spacing:0px"
|
||||
x="172.46959"
|
||||
y="-114.79131"
|
||||
id="text1"><tspan
|
||||
sodipodi:role="line"
|
||||
id="tspan1"
|
||||
x="172.46959"
|
||||
y="-114.79131">ℤ</tspan></text>
|
||||
<text
|
||||
xml:space="preserve"
|
||||
style="font-size:40px;line-height:1.25;font-family:'Mell Display 0.6';-inkscape-font-specification:'Mell Display 0.6, ';word-spacing:0px"
|
||||
x="82.927071"
|
||||
y="-129.36371"
|
||||
id="text2"><tspan
|
||||
sodipodi:role="line"
|
||||
id="tspan2"
|
||||
x="82.927071"
|
||||
y="-129.36371">ℕ</tspan></text>
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 6.0 KiB |
113
_chapters/06_type/naive_sets.svg
Normal file
113
_chapters/06_type/naive_sets.svg
Normal file
|
|
@ -0,0 +1,113 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 359"
|
||||
version="1.1"
|
||||
id="svg9"
|
||||
sodipodi:docname="naive_sets.svg"
|
||||
inkscape:version="1.3 (1:1.3+202307231459+0e150ed6c4)"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs9" />
|
||||
<sodipodi:namedview
|
||||
id="namedview9"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1"
|
||||
showgrid="false"
|
||||
inkscape:zoom="1.5159794"
|
||||
inkscape:cx="297.82727"
|
||||
inkscape:cy="179.09215"
|
||||
inkscape:window-width="1080"
|
||||
inkscape:window-height="1864"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="0"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg9" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="275.24869"
|
||||
cy="236.51604"
|
||||
r="113.5"
|
||||
id="circle2"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="252.94789"
|
||||
cy="297.09973"
|
||||
r="38.982136"
|
||||
id="circle2-5"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:4.92927;stroke-miterlimit:10;stroke-dasharray:none" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="382.85217"
|
||||
cy="202.68269"
|
||||
r="113.5"
|
||||
id="circle2-3"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="234.00404"
|
||||
cy="132.97266"
|
||||
r="113.5"
|
||||
id="circle2-3-6"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:6;stroke-miterlimit:10" />
|
||||
<g
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
id="g8"
|
||||
transform="translate(11.533391,32.07755)">
|
||||
<circle
|
||||
fill="#fce600"
|
||||
stroke="#ffdd00"
|
||||
cx="242.07047"
|
||||
cy="264.15356"
|
||||
r="24.6"
|
||||
id="circle3" />
|
||||
<circle
|
||||
fill="#39bced"
|
||||
stroke="#008dd2"
|
||||
cx="244.8"
|
||||
cy="53.900002"
|
||||
r="24.6"
|
||||
id="circle4" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="220.2"
|
||||
cy="149.10001"
|
||||
r="24.6"
|
||||
id="circle5" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="322.29999"
|
||||
cy="214.7"
|
||||
r="24.6"
|
||||
id="circle6" />
|
||||
<circle
|
||||
fill="#8967ac"
|
||||
stroke="#651c5f"
|
||||
cx="420"
|
||||
cy="224.5"
|
||||
r="24.6"
|
||||
id="circle7" />
|
||||
<circle
|
||||
fill="#54b948"
|
||||
stroke="#00873a"
|
||||
cx="293.38333"
|
||||
cy="139.38791"
|
||||
r="24.6"
|
||||
id="circle8" />
|
||||
</g>
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 2.8 KiB |
|
Before Width: | Height: | Size: 26 KiB After Width: | Height: | Size: 26 KiB |
|
Before Width: | Height: | Size: 82 KiB After Width: | Height: | Size: 82 KiB |
|
Before Width: | Height: | Size: 7.7 KiB After Width: | Height: | Size: 7.7 KiB |
107
_chapters/06_type/set_subset.svg
Normal file
107
_chapters/06_type/set_subset.svg
Normal file
|
|
@ -0,0 +1,107 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 300"
|
||||
version="1.1"
|
||||
id="svg9"
|
||||
sodipodi:docname="set_subset.svg"
|
||||
inkscape:version="1.3 (1:1.3+202307231459+0e150ed6c4)"
|
||||
width="595.29999"
|
||||
height="300"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs9" />
|
||||
<sodipodi:namedview
|
||||
id="namedview9"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1"
|
||||
showgrid="false"
|
||||
inkscape:zoom="1.4913712"
|
||||
inkscape:cx="297.37733"
|
||||
inkscape:cy="233.67756"
|
||||
inkscape:window-width="1080"
|
||||
inkscape:window-height="1864"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="0"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg9" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
cx="300.52634"
|
||||
cy="151.34262"
|
||||
r="128.93355"
|
||||
id="circle1"
|
||||
style="stroke-width:6.75045;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="290.40067"
|
||||
cy="143.91714"
|
||||
r="127.69597"
|
||||
id="circle2"
|
||||
style="fill:#e2e3db;stroke-width:6.75045;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#39bced"
|
||||
stroke="#008dd2"
|
||||
cx="288.28903"
|
||||
cy="46.661957"
|
||||
r="20.5126"
|
||||
id="circle4"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="263.8793"
|
||||
cy="163.34995"
|
||||
r="83.773407"
|
||||
id="circle2-6"
|
||||
style="stroke-width:4.42855;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#8967ac"
|
||||
stroke="#651c5f"
|
||||
cx="381.5545"
|
||||
cy="145.5983"
|
||||
r="20.5126"
|
||||
id="circle7"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#54b948"
|
||||
stroke="#00873a"
|
||||
cx="352.37918"
|
||||
cy="84.860786"
|
||||
r="20.5126"
|
||||
id="circle8"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#fce600"
|
||||
stroke="#ffdd00"
|
||||
cx="265.59259"
|
||||
cy="203.60463"
|
||||
r="20.5126"
|
||||
id="circle3-0"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="233.97963"
|
||||
cy="120.16159"
|
||||
r="20.5126"
|
||||
id="circle5-6"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="307.10605"
|
||||
cy="154.84302"
|
||||
r="20.5126"
|
||||
id="circle6-2"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 2.7 KiB |
105
_chapters/06_type/sets.svg
Normal file
105
_chapters/06_type/sets.svg
Normal file
|
|
@ -0,0 +1,105 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 359"
|
||||
version="1.1"
|
||||
id="svg9"
|
||||
sodipodi:docname="sets.svg"
|
||||
inkscape:version="1.3 (1:1.3+202307231459+0e150ed6c4)"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs9" />
|
||||
<sodipodi:namedview
|
||||
id="namedview9"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1"
|
||||
showgrid="false"
|
||||
inkscape:zoom="0.7357635"
|
||||
inkscape:cx="297.64999"
|
||||
inkscape:cy="180.08504"
|
||||
inkscape:window-width="1080"
|
||||
inkscape:window-height="1864"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="0"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg9" />
|
||||
<switch
|
||||
id="switch9">
|
||||
<g
|
||||
id="g9">
|
||||
<g
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
id="g2">
|
||||
<circle
|
||||
opacity=".14"
|
||||
stroke="#000"
|
||||
cx="265.4"
|
||||
cy="214.7"
|
||||
r="114.6"
|
||||
id="circle1" />
|
||||
<circle
|
||||
fill="#E9E5CC"
|
||||
stroke="#808285"
|
||||
cx="256.4"
|
||||
cy="208.1"
|
||||
r="113.5"
|
||||
id="circle2" />
|
||||
</g>
|
||||
<g
|
||||
stroke-width="6"
|
||||
stroke-miterlimit="10"
|
||||
id="g8">
|
||||
<circle
|
||||
fill="#FCE600"
|
||||
stroke="#FD0"
|
||||
cx="261.2"
|
||||
cy="257.4"
|
||||
r="24.6"
|
||||
id="circle3" />
|
||||
<circle
|
||||
fill="#39BCED"
|
||||
stroke="#008DD2"
|
||||
cx="244.8"
|
||||
cy="53.9"
|
||||
r="24.6"
|
||||
id="circle4" />
|
||||
<circle
|
||||
fill="#D71920"
|
||||
stroke="#BE1E2D"
|
||||
cx="220.2"
|
||||
cy="149.1"
|
||||
r="24.6"
|
||||
id="circle5" />
|
||||
<circle
|
||||
fill="#F58235"
|
||||
stroke="#E76524"
|
||||
cx="322.3"
|
||||
cy="214.7"
|
||||
r="24.6"
|
||||
id="circle6" />
|
||||
<circle
|
||||
fill="#8967AC"
|
||||
stroke="#651C5F"
|
||||
cx="420"
|
||||
cy="224.5"
|
||||
r="24.6"
|
||||
id="circle7" />
|
||||
<circle
|
||||
fill="#54B948"
|
||||
stroke="#00873A"
|
||||
cx="365.4"
|
||||
cy="103.1"
|
||||
r="24.6"
|
||||
id="circle8" />
|
||||
</g>
|
||||
</g>
|
||||
</switch>
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 2.5 KiB |
|
Before Width: | Height: | Size: 26 KiB After Width: | Height: | Size: 26 KiB |
139
_chapters/06_type/type_subtype.svg
Normal file
139
_chapters/06_type/type_subtype.svg
Normal file
|
|
@ -0,0 +1,139 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 300"
|
||||
version="1.1"
|
||||
id="svg9"
|
||||
sodipodi:docname="type_subtype.svg"
|
||||
inkscape:version="1.3 (1:1.3+202307231459+0e150ed6c4)"
|
||||
width="595.29999"
|
||||
height="300"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs9" />
|
||||
<sodipodi:namedview
|
||||
id="namedview9"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1"
|
||||
showgrid="false"
|
||||
inkscape:zoom="1.4913712"
|
||||
inkscape:cx="297.04208"
|
||||
inkscape:cy="233.67757"
|
||||
inkscape:window-width="1080"
|
||||
inkscape:window-height="1864"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="0"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg9" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
cx="426.80408"
|
||||
cy="146.5955"
|
||||
r="128.93355"
|
||||
id="circle1"
|
||||
style="stroke-width:6.75045;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="416.67841"
|
||||
cy="139.17003"
|
||||
r="127.69597"
|
||||
id="circle2"
|
||||
style="stroke-width:6.75045;stroke-miterlimit:10;fill:#e2e3db" />
|
||||
<circle
|
||||
fill="#fce600"
|
||||
stroke="#ffdd00"
|
||||
cx="385.19333"
|
||||
cy="211.92174"
|
||||
r="20.5126"
|
||||
id="circle3"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#39bced"
|
||||
stroke="#008dd2"
|
||||
cx="390.83389"
|
||||
cy="62.502029"
|
||||
r="20.5126"
|
||||
id="circle4"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="351.00568"
|
||||
cy="121.61627"
|
||||
r="20.5126"
|
||||
id="circle5"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="436.14127"
|
||||
cy="176.31653"
|
||||
r="20.5126"
|
||||
id="circle6"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
cx="136.57906"
|
||||
cy="153.5271"
|
||||
r="95.558693"
|
||||
id="circle1-3"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="129.07445"
|
||||
cy="148.02374"
|
||||
r="94.641464"
|
||||
id="circle2-6"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#fce600"
|
||||
stroke="#ffdd00"
|
||||
cx="133.07692"
|
||||
cy="189.13232"
|
||||
r="20.5126"
|
||||
id="circle3-0"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="98.889244"
|
||||
cy="98.826874"
|
||||
r="20.5126"
|
||||
id="circle5-6"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="184.02486"
|
||||
cy="153.5271"
|
||||
r="20.5126"
|
||||
id="circle6-2"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#8967ac"
|
||||
stroke="#651c5f"
|
||||
cx="507.83224"
|
||||
cy="140.85118"
|
||||
r="20.5126"
|
||||
id="circle7"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#54b948"
|
||||
stroke="#00873a"
|
||||
cx="472.08002"
|
||||
cy="83.259377"
|
||||
r="20.5126"
|
||||
id="circle8"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 3.4 KiB |
207
_chapters/06_type/type_subtype_function.svg
Normal file
207
_chapters/06_type/type_subtype_function.svg
Normal file
|
|
@ -0,0 +1,207 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 300"
|
||||
version="1.1"
|
||||
id="svg9"
|
||||
sodipodi:docname="type_subtype_function.svg"
|
||||
inkscape:version="1.3 (1:1.3+202307231459+0e150ed6c4)"
|
||||
width="595.29999"
|
||||
height="300"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs9" />
|
||||
<sodipodi:namedview
|
||||
id="namedview9"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1"
|
||||
showgrid="false"
|
||||
inkscape:zoom="1.4913712"
|
||||
inkscape:cx="297.37733"
|
||||
inkscape:cy="233.67756"
|
||||
inkscape:window-width="1080"
|
||||
inkscape:window-height="1864"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="0"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="g25985-4-8-8" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
cx="429.78027"
|
||||
cy="150.19801"
|
||||
r="128.93355"
|
||||
id="circle1"
|
||||
style="stroke-width:6.75045;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="419.6546"
|
||||
cy="142.77254"
|
||||
r="127.69597"
|
||||
id="circle2"
|
||||
style="fill:#e2e3db;stroke-width:6.75045;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#fce600"
|
||||
stroke="#ffdd00"
|
||||
cx="388.16953"
|
||||
cy="215.52423"
|
||||
r="20.5126"
|
||||
id="circle3"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#39bced"
|
||||
stroke="#008dd2"
|
||||
cx="393.81009"
|
||||
cy="66.10453"
|
||||
r="20.5126"
|
||||
id="circle4"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="353.98187"
|
||||
cy="125.21877"
|
||||
r="20.5126"
|
||||
id="circle5"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="439.11746"
|
||||
cy="179.91904"
|
||||
r="20.5126"
|
||||
id="circle6"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
opacity="0.14"
|
||||
stroke="#000000"
|
||||
cx="139.55527"
|
||||
cy="157.12961"
|
||||
r="95.558693"
|
||||
id="circle1-3"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="132.05066"
|
||||
cy="151.62625"
|
||||
r="94.641464"
|
||||
id="circle2-6"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#8967ac"
|
||||
stroke="#651c5f"
|
||||
cx="510.80844"
|
||||
cy="144.45369"
|
||||
r="20.5126"
|
||||
id="circle7"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#54b948"
|
||||
stroke="#00873a"
|
||||
cx="475.05621"
|
||||
cy="86.861877"
|
||||
r="20.5126"
|
||||
id="circle8"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<g
|
||||
style="display:inline;fill:#dddddd;stroke:#4d4d4d;stroke-width:6.389;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||
id="g1482-7-0-7-1-1-7-3-5-2-8-4-8-3"
|
||||
transform="matrix(0.13805666,0.04096437,-0.07153662,0.24568081,448.76267,-4.6780015)"
|
||||
inkscape:transform-center-x="103.33557"
|
||||
inkscape:transform-center-y="-11.630887">
|
||||
<g
|
||||
id="g25985-4-8-8"
|
||||
style="stroke:#4d4d4d;stroke-opacity:1"
|
||||
transform="translate(7.7655222,14.986479)">
|
||||
<path
|
||||
inkscape:connector-curvature="0"
|
||||
style="fill:#838383;fill-opacity:1;stroke:#4d4d4d;stroke-width:30.0282;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1"
|
||||
d="m -609.36914,524.31037 14.41784,-35.42618 36.64345,26.90294 z"
|
||||
id="path3233-5-4-8-4-4-1-3-3-6"
|
||||
inkscape:transform-center-x="0.9901113"
|
||||
inkscape:transform-center-y="2.1216647" />
|
||||
<path
|
||||
style="fill:none;stroke:#4d4d4d;stroke-width:9.11185;stroke-opacity:1;paint-order:markers fill stroke"
|
||||
inkscape:connector-curvature="0"
|
||||
id="path1480-1-3-3-3-9-1-6-0-7-2-0-1-0"
|
||||
d="M -2144.6367,791.15053 C -1767.2979,508.0558 -1016.0331,384.05419 -539.57256,520.80751"
|
||||
sodipodi:nodetypes="cc" />
|
||||
</g>
|
||||
</g>
|
||||
<g
|
||||
style="display:inline;fill:#dddddd;stroke:#4d4d4d;stroke-width:6.389;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||
id="g1482-7-0-7-1-1-7-3-5-2-8-4-8-3-1"
|
||||
transform="matrix(0.14320665,-0.01515179,-0.0256242,-0.25459762,452.88276,351.50697)"
|
||||
inkscape:transform-center-x="-28.411412"
|
||||
inkscape:transform-center-y="5.4915379">
|
||||
<g
|
||||
id="g25985-4-8-8-8"
|
||||
style="stroke:#4d4d4d;stroke-opacity:1"
|
||||
transform="translate(7.7655222,14.986479)">
|
||||
<path
|
||||
inkscape:connector-curvature="0"
|
||||
style="fill:#838383;fill-opacity:1;stroke:#4d4d4d;stroke-width:30.0282;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1"
|
||||
d="m -609.36914,524.31037 14.41784,-35.42618 36.64345,26.90294 z"
|
||||
id="path3233-5-4-8-4-4-1-3-3-6-7"
|
||||
inkscape:transform-center-x="0.9901113"
|
||||
inkscape:transform-center-y="2.1216647" />
|
||||
<path
|
||||
style="fill:none;stroke:#4d4d4d;stroke-width:9.11185;stroke-opacity:1;paint-order:markers fill stroke"
|
||||
inkscape:connector-curvature="0"
|
||||
id="path1480-1-3-3-3-9-1-6-0-7-2-0-1-0-9"
|
||||
d="M -2125.0849,747.3062 C -1670.8412,503.43984 -1107.8315,440.06102 -539.57256,520.80751"
|
||||
sodipodi:nodetypes="cc" />
|
||||
</g>
|
||||
<g
|
||||
id="g25985-4-8-8-8-0"
|
||||
style="display:inline;fill:#dddddd;stroke:#4d4d4d;stroke-width:6.389;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||
transform="matrix(0.99614115,-0.05233641,0.16524513,0.99519196,293.19153,134.76036)">
|
||||
<path
|
||||
inkscape:connector-curvature="0"
|
||||
style="fill:#838383;fill-opacity:1;stroke:#4d4d4d;stroke-width:30.0282;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1"
|
||||
d="m -609.36914,524.31037 14.41784,-35.42618 36.64345,26.90294 z"
|
||||
id="path3233-5-4-8-4-4-1-3-3-6-7-2"
|
||||
inkscape:transform-center-x="0.9901113"
|
||||
inkscape:transform-center-y="2.1216647" />
|
||||
<path
|
||||
style="fill:none;stroke:#4d4d4d;stroke-width:9.11185;stroke-opacity:1;paint-order:markers fill stroke"
|
||||
inkscape:connector-curvature="0"
|
||||
id="path1480-1-3-3-3-9-1-6-0-7-2-0-1-0-9-3"
|
||||
d="M -2077.0136,622.92034 C -1665.132,483.28607 -1107.8315,440.06102 -539.57256,520.80751"
|
||||
sodipodi:nodetypes="cc" />
|
||||
</g>
|
||||
</g>
|
||||
<circle
|
||||
fill="#fce600"
|
||||
stroke="#ffdd00"
|
||||
cx="136.05313"
|
||||
cy="192.73482"
|
||||
r="20.5126"
|
||||
id="circle3-0"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="101.86546"
|
||||
cy="102.42937"
|
||||
r="20.5126"
|
||||
id="circle5-6"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="187.00107"
|
||||
cy="157.12961"
|
||||
r="20.5126"
|
||||
id="circle6-2"
|
||||
style="stroke-width:5.00307;stroke-miterlimit:10" />
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 7.0 KiB |
178
_chapters/06_type/zfc_pairing.svg
Normal file
178
_chapters/06_type/zfc_pairing.svg
Normal file
|
|
@ -0,0 +1,178 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 300"
|
||||
version="1.1"
|
||||
id="svg9"
|
||||
sodipodi:docname="zfc_pairing.svg"
|
||||
inkscape:version="1.3 (1:1.3+202307231459+0e150ed6c4)"
|
||||
width="595.29999"
|
||||
height="300"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs9" />
|
||||
<sodipodi:namedview
|
||||
id="namedview9"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1"
|
||||
showgrid="false"
|
||||
inkscape:zoom="1.5159794"
|
||||
inkscape:cx="283.3152"
|
||||
inkscape:cy="179.09215"
|
||||
inkscape:window-width="1080"
|
||||
inkscape:window-height="1864"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="0"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg9" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="459.24136"
|
||||
cy="144.80049"
|
||||
r="111.29372"
|
||||
id="circle2"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:5.88337;stroke-miterlimit:10" />
|
||||
<g
|
||||
id="g2"
|
||||
transform="matrix(0.61031809,0,0,0.61031809,46.499398,135.02372)">
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="176.05109"
|
||||
cy="-80.547012"
|
||||
r="83.076897"
|
||||
id="circle2-3-6"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:4.39173;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#39bced"
|
||||
stroke="#008dd2"
|
||||
cx="196.1284"
|
||||
cy="-121.63628"
|
||||
r="24.6"
|
||||
id="circle4"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="159.43069"
|
||||
cy="-50.629074"
|
||||
r="24.6"
|
||||
id="circle5"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
</g>
|
||||
<g
|
||||
id="g1"
|
||||
transform="matrix(0.61031809,0,0,0.61031809,-174.29762,259.67408)">
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="486.37695"
|
||||
cy="-99.171982"
|
||||
r="82.52964"
|
||||
id="circle2-3"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:4.3628;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="456.76855"
|
||||
cy="-92.491066"
|
||||
r="24.6"
|
||||
id="circle6"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#8967ac"
|
||||
stroke="#651c5f"
|
||||
cx="512.26965"
|
||||
cy="-66.375298"
|
||||
r="24.6"
|
||||
id="circle7"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#54b948"
|
||||
stroke="#00873a"
|
||||
cx="503.81094"
|
||||
cy="-140.23228"
|
||||
r="24.6"
|
||||
id="circle8"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
</g>
|
||||
<g
|
||||
id="g2-5"
|
||||
transform="matrix(0.61031809,0,0,0.61031809,400.99938,183.98908)">
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="176.05109"
|
||||
cy="-80.547012"
|
||||
r="83.076897"
|
||||
id="circle2-3-6-6"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:4.39173;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#39bced"
|
||||
stroke="#008dd2"
|
||||
cx="196.1284"
|
||||
cy="-121.63628"
|
||||
r="24.6"
|
||||
id="circle4-2"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="159.43069"
|
||||
cy="-50.629074"
|
||||
r="24.6"
|
||||
id="circle5-9"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
</g>
|
||||
<g
|
||||
id="g3"
|
||||
transform="matrix(0.61031809,0,0,0.61031809,109.15538,222.67422)">
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="486.37695"
|
||||
cy="-99.171982"
|
||||
r="82.52964"
|
||||
id="circle2-3-1"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:4.3628;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="456.76855"
|
||||
cy="-92.491066"
|
||||
r="24.6"
|
||||
id="circle6-2"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#8967ac"
|
||||
stroke="#651c5f"
|
||||
cx="512.26965"
|
||||
cy="-66.375298"
|
||||
r="24.6"
|
||||
id="circle7-7"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#54b948"
|
||||
stroke="#00873a"
|
||||
cx="503.81094"
|
||||
cy="-140.23228"
|
||||
r="24.6"
|
||||
id="circle8-0"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
</g>
|
||||
<path
|
||||
d="m 262.27225,130.5401 c 8.0409,-1.4716 8.3867,-1.86733 18.70165,-2.22543 3.04178,-0.009 10.45591,-0.086 12.21468,0.006 l 1.10794,0.0191 0.5474,-8.07957 c 8.2013,5.0999 15.75577,10.76538 22.43704,17.02514 -8.50178,3.19702 -16.52106,7.22389 -23.84983,11.81016 l 0.76665,-8.70008 -1.108,-0.0191 c -1.75944,-0.0916 -9.08636,-0.0727 -12.07459,0.0277 -9.61357,0.29743 -10.29073,0.76075 -18.19093,2.26464 z"
|
||||
fill="#e90909"
|
||||
stroke-width="0.790915"
|
||||
id="path1881-4"
|
||||
sodipodi:nodetypes="cccccccccccc"
|
||||
style="fill:#333333" />
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 5.0 KiB |
154
_chapters/06_type/zfc_union.svg
Normal file
154
_chapters/06_type/zfc_union.svg
Normal file
|
|
@ -0,0 +1,154 @@
|
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<svg
|
||||
viewBox="0 0 595.3 300"
|
||||
version="1.1"
|
||||
id="svg9"
|
||||
sodipodi:docname="zfc_union.svg"
|
||||
inkscape:version="1.3 (1:1.3+202307231459+0e150ed6c4)"
|
||||
width="595.29999"
|
||||
height="300"
|
||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||
xmlns="http://www.w3.org/2000/svg"
|
||||
xmlns:svg="http://www.w3.org/2000/svg">
|
||||
<defs
|
||||
id="defs9" />
|
||||
<sodipodi:namedview
|
||||
id="namedview9"
|
||||
pagecolor="#ffffff"
|
||||
bordercolor="#666666"
|
||||
borderopacity="1.0"
|
||||
inkscape:showpageshadow="2"
|
||||
inkscape:pageopacity="0.0"
|
||||
inkscape:pagecheckerboard="0"
|
||||
inkscape:deskcolor="#d1d1d1"
|
||||
showgrid="false"
|
||||
inkscape:zoom="1.5159794"
|
||||
inkscape:cx="283.3152"
|
||||
inkscape:cy="179.09215"
|
||||
inkscape:window-width="1080"
|
||||
inkscape:window-height="1864"
|
||||
inkscape:window-x="0"
|
||||
inkscape:window-y="0"
|
||||
inkscape:window-maximized="1"
|
||||
inkscape:current-layer="svg9" />
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="459.24136"
|
||||
cy="144.80049"
|
||||
r="111.29372"
|
||||
id="circle2"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:5.88337;stroke-miterlimit:10" />
|
||||
<g
|
||||
id="g2"
|
||||
transform="matrix(0.61031809,0,0,0.61031809,46.499398,135.02372)">
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="176.05109"
|
||||
cy="-80.547012"
|
||||
r="83.076897"
|
||||
id="circle2-3-6"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:4.39173;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#39bced"
|
||||
stroke="#008dd2"
|
||||
cx="196.1284"
|
||||
cy="-121.63628"
|
||||
r="24.6"
|
||||
id="circle4"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="159.43069"
|
||||
cy="-50.629074"
|
||||
r="24.6"
|
||||
id="circle5"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
</g>
|
||||
<g
|
||||
id="g1"
|
||||
transform="matrix(0.61031809,0,0,0.61031809,-174.29762,259.67408)">
|
||||
<circle
|
||||
fill="#e9e5cc"
|
||||
stroke="#808285"
|
||||
cx="486.37695"
|
||||
cy="-99.171982"
|
||||
r="82.52964"
|
||||
id="circle2-3"
|
||||
style="fill:#e9e5cc;fill-opacity:0.352166;stroke-width:4.3628;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="456.76855"
|
||||
cy="-92.491066"
|
||||
r="24.6"
|
||||
id="circle6"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#8967ac"
|
||||
stroke="#651c5f"
|
||||
cx="512.26965"
|
||||
cy="-66.375298"
|
||||
r="24.6"
|
||||
id="circle7"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#54b948"
|
||||
stroke="#00873a"
|
||||
cx="503.81094"
|
||||
cy="-140.23228"
|
||||
r="24.6"
|
||||
id="circle8"
|
||||
style="stroke-width:6;stroke-miterlimit:10" />
|
||||
</g>
|
||||
<circle
|
||||
fill="#39bced"
|
||||
stroke="#008dd2"
|
||||
cx="525.76331"
|
||||
cy="122.13081"
|
||||
r="15.013825"
|
||||
id="circle4-2"
|
||||
style="stroke-width:3.66191;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#d71920"
|
||||
stroke="#be1e2d"
|
||||
cx="483.95566"
|
||||
cy="168.56242"
|
||||
r="15.013825"
|
||||
id="circle5-9"
|
||||
style="stroke-width:3.66191;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#f58235"
|
||||
stroke="#e76524"
|
||||
cx="419.15674"
|
||||
cy="156.09875"
|
||||
r="15.013825"
|
||||
id="circle6-2"
|
||||
style="stroke-width:3.66191;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#8967ac"
|
||||
stroke="#651c5f"
|
||||
cx="438.11859"
|
||||
cy="214.79829"
|
||||
r="15.013825"
|
||||
id="circle7-7"
|
||||
style="stroke-width:3.66191;stroke-miterlimit:10" />
|
||||
<circle
|
||||
fill="#54b948"
|
||||
stroke="#00873a"
|
||||
cx="445.05377"
|
||||
cy="100.79744"
|
||||
r="15.013825"
|
||||
id="circle8-0"
|
||||
style="stroke-width:3.66191;stroke-miterlimit:10" />
|
||||
<path
|
||||
d="m 262.27225,130.5401 c 8.0409,-1.4716 8.3867,-1.86733 18.70165,-2.22543 3.04178,-0.009 10.45591,-0.086 12.21468,0.006 l 1.10794,0.0191 0.5474,-8.07957 c 8.2013,5.0999 15.75577,10.76538 22.43704,17.02514 -8.50178,3.19702 -16.52106,7.22389 -23.84983,11.81016 l 0.76665,-8.70008 -1.108,-0.0191 c -1.75944,-0.0916 -9.08636,-0.0727 -12.07459,0.0277 -9.61357,0.29743 -10.29073,0.76075 -18.19093,2.26464 z"
|
||||
fill="#e90909"
|
||||
stroke-width="0.790915"
|
||||
id="path1881-4"
|
||||
sodipodi:nodetypes="cccccccccccc"
|
||||
style="fill:#333333" />
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 4.3 KiB |
|
|
@ -146,12 +146,6 @@ There definitely is more to be said about free and forgetful functors, as well a
|
|||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Like equivalence, adjunction is a relationship between two categories. Like equivalence, it is composed of two functors.
|
||||
|
||||
However, unlike equivalence, an adjunction is not symmetric i.e. although the two functors are two way and we
|
||||
|
|
@ -192,8 +186,3 @@ https://github.com/adamnemecek/adjoint/
|
|||
https://chrispenner.ca/posts/adjunction-battleship
|
||||
|
||||
https://graphicallinearalgebra.net/2015/05/19/paths-and-matrices-part-1/
|
||||
|
||||
|
||||
<!--
|
||||
TODO: Formal concept analysis
|
||||
-->
|
||||
|
|
|
|||
|
|
@ -3,8 +3,6 @@ layout: default
|
|||
title: Functors
|
||||
---
|
||||
|
||||
|
||||
|
||||
Functors
|
||||
===
|
||||
|
||||
|
|
@ -155,7 +153,7 @@ Now let's unpack this definition by going through each of its components.
|
|||
Object mapping
|
||||
---
|
||||
|
||||
In the definition above we use the word "mapping" to avoid misusing the word "function" for something that isn't exactly a function. But in this particular case, calling the mapping a function would barely be a misuse --- if we forget about morphisms and treat the source and target categories as sets, the object mapping is nothing but a regular old function.
|
||||
In the definition above, we use the word "mapping" to avoid misusing the word "function" for something that isn't exactly a function. But in this particular case, calling the mapping a function would barely be a misuse --- if we forget about morphisms and treat the source and target categories as sets, the object mapping is nothing but a regular old function.
|
||||
|
||||
|
||||
|
||||
|
|
@ -174,7 +172,7 @@ A more formal definition of a morphism mapping involves the concept of the *homo
|
|||
|
||||
|
||||
|
||||
Note how the concepts of *homomorphism set* and of *underlying set* allowed us to "escape" to set theory when defining categorical concepts and define everything using functions.
|
||||
(Notice how the concepts of *homomorphism set* and of *underlying set* allowed us to "escape" to set theory when defining categorical concepts and define everything using functions.)
|
||||
|
||||
Functor laws
|
||||
---
|
||||
|
|
@ -198,6 +196,17 @@ And these laws conclude the definition of functors --- a simple but, as we will
|
|||
|
||||
To see *why* is it so powerful, let's check some examples.
|
||||
|
||||
Functors in everyday language
|
||||
---
|
||||
|
||||
There is a common figure of speech, that goes like this:
|
||||
|
||||
> If $a$ is like $F a$, then $b$ is like $F b$.
|
||||
|
||||
Or "$a$ is related to $F a$, in the same way as $b$ is related to $F b$," e.g. "If schools are like corporations, then teachers are like bosses".
|
||||
|
||||
This figure of speech is a way to introduce a functor: what are you saying is that there is a certain connection (or category-theory therms a "morphism") between schools and teachers, that is similar to the connection between corporations and bosses i.e. that there is some kind of structure preserving map that connects the category of school-related things, to the category of work-related things in which schools (a) are mapped to corporations (F a) and teacher (b) are mapped to bosses (F b). and the connections between schools and teachers (a -> b) are mapped to the connections between corporations and bosses (F a -> F b).
|
||||
|
||||
Diagrams are functors
|
||||
---
|
||||
|
||||
|
|
|
|||
|
|
@ -219,6 +219,30 @@ Isomorphism is not hard to construct --- given two sets, containing three object
|
|||
But most of these isomorphisms, are just random. In our studies we are only interested in structures that *make sense*. In category theory the abstract notion of making sense is captured by the naturality condition.
|
||||
|
||||
|
||||
|
||||
Limits
|
||||
===
|
||||
|
||||
Products are one example of what is known in category theory as *limits*. A limit is an object that summarizes a structure (also called a diagram) consisting of other objects and morphisms in a way that allows us to later retrieve some of it.
|
||||
|
||||
A limit also has to be unique in the sense that you cannot have two limit objects for the same structure.
|
||||
|
||||
The notion of a limit is strongly related with the notion of a commuting diagrams. This is not obvious when we are examining products because the diagram of products does not have several routes reaching to the same point.
|
||||
|
||||
Limits can be defined formally, just like everything else that we examine, but we won't bother to do that here.
|
||||
|
||||
Products are Limits
|
||||
---
|
||||
|
||||
OK, we said that limits summarize a structure. What is the structure that a product is summarizing? It is a structure that consists of two objects (sets) that are have no connections between them.
|
||||
|
||||
|
||||
|
||||
Why is the product unique when it comes to representing the two objects? Because any other object that also represents them is connected to the product through a morphism (this is known as the *universal property* of limits).
|
||||
|
||||
|
||||
|
||||
|
||||
Natural transformations and associativity
|
||||
===
|
||||
|
||||
|
|
|
|||
|
|
@ -24,13 +24,19 @@ Logic
|
|||
|
||||
Types
|
||||
---
|
||||
[Naive set theory](https://proofwiki.org/wiki/Definition:Frege_Set_Theory)
|
||||
[Sets types categories](../references/sets_types_categories.pdf)
|
||||
|
||||
[Russell - Principles of Mathematics](https://people.umass.edu/klement/pom/pom.html#sec497)
|
||||
|
||||
|
||||
|
||||
[Number theory from first principles](https://explained-from-first-principles.com/number-theory/)
|
||||
|
||||
[The natural numbers game](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
|
||||
|
||||
[Martin Lof lecture notes](https://ncatlab.org/nlab/files/MartinLofIntuitionisticTypeTheory.pdf)
|
||||
|
||||
Functors
|
||||
---
|
||||
|
||||
|
|
@ -59,3 +65,9 @@ etc
|
|||
|
||||
|
||||
[Graphical linear algebra with string diagrams](https://graphicallinearalgebra.net/2015/04/26/adding-part-1-and-mr-fibonacci/)
|
||||
|
||||
|
||||
[First-order categorical logic](https://diagonalargument.com/2019/06/02/first-order-categorical-logic-1/)
|
||||
[Zansi's blog](https://zanzix.github.io/)
|
||||
|
||||
[Baez homotopy](https://math.ucr.edu/home/baez/calgary/homotopy.html)
|
||||
|
|
|
|||
|
|
@ -65,9 +65,29 @@ window.MathJax = {
|
|||
-->
|
||||
</div>
|
||||
</div>
|
||||
|
||||
<div class="footer">
|
||||
<div class="container chapters">
|
||||
<h1>Subscribe for updates</h1>
|
||||
<form
|
||||
action="https://buttondown.email/api/emails/embed-subscribe/abuseofnotation"
|
||||
method="post"
|
||||
target="popupwindow"
|
||||
onsubmit="window.open('https://buttondown.email/abuseofnotation', 'popupwindow')"
|
||||
class="embeddable-buttondown-form"
|
||||
>
|
||||
<input type="email" placeholder="Enter your email" name="email" id="bd-email" class="textfield" />
|
||||
|
||||
<input type="submit" class="read-more" value="Subscribe" />
|
||||
<p>
|
||||
<a href="https://buttondown.email/refer/abuseofnotation" target="_blank">Powered by Buttondown.</a>
|
||||
</p>
|
||||
</form>
|
||||
</div>
|
||||
</div>
|
||||
|
||||
<div class="footer" style="background-color:#39bcedff">
|
||||
<div class="container">
|
||||
|
||||
<h1>Created by Jencel Panic</h1>
|
||||
<p><a target="_blank" href="/">personal blog</a></p>
|
||||
<p><a href="mailto:marinovboris@protonmail.com">email</a></p>
|
||||
|
|
|
|||
20
limit.md
20
limit.md
|
|
@ -1,20 +0,0 @@
|
|||
Limits
|
||||
===
|
||||
|
||||
Products are one example of what is known in category theory as *limits*. A limit is an object that summarizes a structure (also called a diagram) consisting of other objects and morphisms in a way that allows us to later retrieve some of it.
|
||||
|
||||
A limit also has to be unique in the sense that you cannot have two limit objects for the same structure.
|
||||
|
||||
The notion of a limit is strongly related with the notion of a commuting diagrams. This is not obvious when we are examining products because the diagram of products does not have several routes reaching to the same point.
|
||||
|
||||
Limits can be defined formally, just like everything else that we examine, but we won't bother to do that here.
|
||||
|
||||
Products are Limits
|
||||
---
|
||||
|
||||
OK, we said that limits summarize a structure. What is the structure that a product is summarizing? It is a structure that consists of two objects (sets) that are have no connections between them.
|
||||
|
||||
|
||||
|
||||
Why is the product unique when it comes to representing the two objects? Because any other object that also represents them is connected to the product through a morphism (this is known as the *universal property* of limits).
|
||||
|
||||
BIN
references/ok-type-theory.pdf
Normal file
BIN
references/ok-type-theory.pdf
Normal file
Binary file not shown.
Loading…
Reference in New Issue
Block a user