abuseofnotation/category-theory-illustrated
1
1
Fork 0
mirror of https://github.com/abuseofnotation/category-theory-illustrated.git synced 2024-09-11 17:08:54 +03:00
Code Issues Packages Projects Releases Wiki Activity

stuff

Browse Source
This commit is contained in:
Boris Marinov 2021-05-24 15:41:39 +03:00
parent eeca3f8b49
commit 2dfeb28050
8 changed files with 758 additions and 109 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

185
_chapters/05_logic.md
View File

@ -4,32 +4,28 @@ title: Logic
---
Logic
===
==
Now let's talk about one more *seemingly* unrelated topic, just so we can surprise ourselves that it is all connected. This time I will not merely transport you to a different branch of mathematics, but an entirely different discipline, namely *logic*. Or, to be more precise, intuitionistic logic. This discipline may seem to you as detached from what we have been talking about as it possibly can, but it is actually very close.
What is logic
===
Beyond the world that we inhabit and perceive every day there exist the world of *forms*. Although inaccessible to us, this world is the realization of all our ideas and concepts that we use in our everyday thinking. Beyond all the people, there lies the prototypical person, and we are people only insofar as we resemble that person. Beyond all the things in the world that are strong, lies the ultimate concepts of strength, from which all of them borrow. This is a worldview that is due to the Greek philosopher Plato and which is sometimes called "the theory of forms". The discipline of logic represents an effort to think and structure our thoughts in a way that they apply to this world of forms i.e. in a "formal" way.
As such, logic aims to study the *rules* by which knowing one thing leads you to conclude or (*prove*) that some other thing is also true without any regard of what these things are specifically, i.e. by only refering to their form.
Logic aims to study the *rules* by which knowing one thing leads you to conclude or (*prove*) that some other thing is also true without any regard of what these things are specifically, i.e. by only refering to their form.
On top of that, it (logic) tries to organize those rules in what are called *formal systems* - these are collections of rules that have give you the maximum expressive ability without adding anything extra.
What does "prove" mean in this context? Simple - when we are able, using the rules of a given logical system, to transform one set of *propositions* (or "things we know") **A** to another set of proposition **B** (things that we *want* to know) we say that we have proven that **A → B** in that logical system. Note that the word "prove" is a little misleading here, especially when used with the combination of the word *true* (which is misleading even by itself) - you don't prove anything using logic, you merely verify that it follows from a given set of propositions *AND* rules for manipulating those propositions. I think that we are only using this word (prove) because verifying that something follows from a set of axioms and rules is the closest that we have to an actual proof (in the same way in which our world is the closest that we have to Plato's world of forms).
What does "prove" mean in this context? Simple - when we are able, using the rules of a given logical system, to transform one set of *propositions* (or "things we know") **A** to another set of proposition **B** (things that we *want* to know) we say that we have proven that **A → B** in that logical system. Note that the word "prove" is a little misleading here, especially when used with the combination of the word *true* (which is misleading even by itself) - you don't prove anything using logic, you merely verify that it follows from a given set of propositions *AND* rules for manipulating those propositions. I think that we are only using this word (prove) because verifying that something follows from a set of axioms and rules is the closest that we have to an actual proof.
Here I will have to quote Bertrand Russell, and the way he explains this concept, using geometry as an example:
> But since the growth of non-Euclidean Geometry, it has appeared that pure mathematics has no concern with the question whether the axioms and propositions of Euclid hold of actual space or not: this is a question for applied mathematics, to be decided, so far as any decision is possible, by experiment and observation. What pure mathematics asserts is merely that the Euclidean propositions follow from the Euclidean axioms--i.e. it asserts an implication: any space which has such and such properties has also such and such other properties. Thus, as dealt with in pure mathematics, the Euclidean and non-Euclidean Geometries are equally true: in each nothing is affirmed except implications. All propositions as to what actually exists, like the space we live in, belong to experimental or empirical science, not to mathematics; when they belong to applied mathematics, they arise from giving to one or more variables in a proposition of pure mathematics some constant value satisfying the hypothesis, and thus enabling us, for that value of the variable, actually to assert both hypothesis and consequent instead of asserting merely the implication.
> Bertrand Russell, from The Principles of Mathematics (1903)
Try to relate this to Plato's theory of forms.
Logic and mathematics
---
All of the concepts that we studied here are formal concepts, so we can say that we have been doing logic throughout this book. And we would be quite correct - every mathematical theory is logic plus some additional definitions added to it. Part of the reason why *set theory* is so popular as a theory for the foundations of mathematics is that set theory (in particular the Zermelo–Fraenkel flavour of it) adds just one single primitive to the standard axioms of logic which we will see shortly - the binary relation that indicates *set membership* i.e. it is very very close to logic.
All of the concepts that we studied here are formal concepts, so we can say that we have been doing logic throughout this book. And we would be quite correct - every mathematical theory is logic plus some additional definitions added to it. Part of the reason why *set theory* is so popular as a theory for the foundations of mathematics is that set theory (in particular the Zermelo–Fraenkel flavour of it) adds just one single primitive to the standard axioms of logic which we will see shortly - the binary relation that indicates *set membership* i.e. set theory is very very close to logic. Category theory is close to logic too, but in a quite different way (we will see how later.)
Primary propositions
---
@ -43,29 +39,21 @@ In the real-world usages, these propositions would be facts about the world, pro
Composing propositions
---
If we have two or more propositions that are somehow related to one another, we can combine them into one using a logical operator, like "and", "or" "follows". The result would be a new proposition, not unlike the way in which monoid objects are combined into a new monoid object using the monoid operation. Moreover, some logical operations, like **AND** and **OR** do actually form monoids.
If we have two or more propositions that are somehow related to one another, we can combine them into one using a logical operator, like "and", "or" "follows". The result would be a new proposition, not unlike the way in which monoid objects are combined into a new monoid object using the monoid operation. And, some logical operations do form monoids, like the operation **and** with **true** serving as the identity element.
[Logical operations that form monoids](logic_monoid.svg)
![Logical operations that form monoids](logic_monoid.svg)
However logic is not *just* a monoid, as logic involves more than one logical operation so logical propositions can relate to one another in more than one ways (and we are interested in how do they relate).
However logic is not *just* a monoid, as logic studies not one but many logical operations and they ways in which they relate, for example a in logic we might be interested in the distributivity of the **and** and **or** operations.
[The distributivity operation of "and" and "or"](logic_distributivity.svg)
![The distributivity operation of "and" and "or"](logic_distributivity.svg)
One very important note: when looking at the diagram above, we may be inclined to distinguish propositions that are composed of several premises (united with operators) from primary propositions.
Important to note that **∧** is the symbol for **and** and **∨** is the symbol for **or** (although the law is actually valid even if **and** and **or** are flipped).
[Composite and atomic propositions](composite_atomic_contrast.svg)
However in order for our logic to work, we should *not* threat those two types any differently from one another, e.g. **A** is a proposition in the same way as **A ∧ B** or **((A ∧ B) ∨ C)**
In order to represent composite propositions we would have to amend our notation a bit: aside from the single-color balls (which represent the atomic propositions), we would also have some multi-colored ones that represent composite propositions.
[Composite and atomic propositions](composite_atomic_united.svg)
In other words, we can view atomic propositions as composite propositions that have just one value.
When looking at the diagram above, we may be inclined to distinguish propositions that are composed of several premises (united with operators) from "primary" propositions (single-color balls). However in order for our logic to work, we should *not* threat those two types any differently from one another, e.g. **A** is a proposition in the same way as **A ∧ B** or **((A ∧ B) ∨ C)** - wherever one goes, the others might go as well.
![Balls as propositions](balls_propositions.svg)
Threating atomic and composite propositions the same allow us to compose logical propositions with multiple levels of nesting (*recursively* as the computer science people say). Let's take an example with one of the most famous propositions ever - *modus ponens*, which states that if **A** is true and if also **A → B** is true (if **A** implies **B**), then **B** is true as well. On a basic level, it is expressed by two propositions in a "follows" relation in which the proposition that follows **B** atomic, but the proposition from which **B** follows is not - let's call that one **C** and so the proposition becomes **C → B**. But if we go deeper we have to mention that the **C** propositions is itself composed of two propositions in an "and", relationship **A** and let's call it **D** (so **A ∨ D**), where **D** is itself composed of two propositions, this time in a "follows" relationship **A → B**.
As a result of this is that we can compose propositions with multiple levels of nesting (*recursively* as the computer science people say). Let's take an example with one of the most famous propositions ever - *modus ponens*, which states that if **A** is true and if also **A → B** is true (if **A** implies **B**), then **B** is true as well. On a basic level, it is expressed by two propositions in a "follows" relation in which the proposition that follows **B** atomic, but the proposition from which **B** follows is not - let's call that one **C** and so the proposition becomes **C → B**. But if we go deeper we have to mention that the **C** propositions is itself composed of two propositions in an "and", relationship **A** and let's call it **D** (so **A ∨ D**), where **D** is itself composed of two propositions, this time in a "follows" relationship **A → B**.
![Modus ponens](modus_ponens.svg)
@ -74,7 +62,6 @@ Tautologies
As the implicit aim of logic is the search for truth, a very interesting type of propositions are those that are *always true*, regardless of the premises (or *in all models of the system*, if we want to be fancy with the terminology). Ludvig Wittgenstein called such propositions *tautologies* as in "something that repeats itself" and that is a pretty appropriate name - most of them state that something follows from something else where the something and the something else are actually the same thing.
![Identity tautology](tautology_identity.svg)
The the simplest tautology, is one which states that a proposition implies itself (the canonical example of a "All bachelors are unmarried"), but there are some less boring ones, where the connection between the left and the right is not so apparent.
@ -107,36 +94,37 @@ This is how we transform axioms to rules of inference, that help you to build (p
Logical systems
---
Knowing that we can take a tautology and use it by means of substitution to generate tautologies (as well as other propositions), you might ask whether it is possible to compile a small collection of such tautologies, selected in such a way that if we use them as axiom schemas we can generate all other tautologies.
Knowing that we can take a tautology and use it by means of substitution to generate tautologies (as well as other propositions), you might ask whether it is possible to compile a small collection of such tautolkogies, selected in such a way that if we use them as axiom schemas we can generate all other tautologies.
[A minimal collection of Hilbert axioms](min_hilbert.svg)
![A minimal collection of Hilbert axioms](min_hilbert.svg)
You would be happy (although a little annoyed, I imagine) to learn that there exist not only one, but an infinite number of such collections. Those collections are what we call "logical systems" (also "proof systems", or "proof calculi"). There are two main classes of such logical systems, which we will examine later: the first one are the so-called *Hilbert-style* proof systems (also called *Frege-style*) and the other one are the systems of *natural deduction*, the main difference between the two being whether they rely on *axioms* or on *rules of inference* as a methods for proving propositions.
You would be happy (although a little annoyed, I imagine) to learn that there exist not only one, but an infinite number of such collections. Those collections are what we call "logical systems" (also "proof systems", or "proof calculi").
- *Natural deduction* systems consist only of *rules of inference* (they don't have axiom schemas).
- *Hilbert-style* systems, on the other hand rely mainly on *axiom schemas* as means of proving propositions. They do, however, contain one rule of inference, just because otherwise there would be no way to combine the generated propositions - usually that rule is the *modus ponens* rule, that we already saw.
We will see an example of such system, but first let's take a step back and try to formalize the terms that we talked about so far.
But wait, how can we be *sure* that a given system is really capable of deducing all tautologies that exist in the world? We can be sure, because it was proven by a guy called Godel, who is like the greated logician ever, a result known as Godel's completenes theorem. However we won't get into that result right now - in fact let's take a step back and try to formalize the terms that we talked about so far.
The classical perspective
Classical logic
===
The classical formalization of logic is based on a simple observation - each proposition is either true or false i.e. it has just two possible values.
Beyond the world that we inhabit and perceive every day there exist the world of *forms*. Although inaccessible to us, this world is the realization of all our ideas and concepts that we use in our everyday thinking. And this world exist outside of us and our ideas e.g. beyond all the people, there lies the prototypical person, and we are people only insofar as we resemble that person. Beyond all the things in the world that are strong, lies the ultimate concepts of strength, from which all of them borrow. This is a worldview that is due to the Greek philosopher Plato and which is sometimes called "the theory of forms". The discipline of classical logic represents an effort to think and structure our thoughts in a way that they apply to this world of forms i.e. in a "formal" way.
We can view primary propositions as simple functions that return a boolean value and don't take any arguments.
The existence of the world of forms is a comforting thought. It means that even if there are many things that we, people, don't know, the answers to many questions (and are not sure of anything) at least *somewhere out there* there the answer to every question (whether it be affirmitive or negative) exists i.e. that ultimately *each proposition is either true or false*.
We can view logical operators as functions that take a bunch of boolean values and return another boolean value (composite propositions are just the results of the invocation of these functions.)
For this reason, propositions in classical logic can be aptly expressed as functions which output boolean values.
This observation (that propositions can be either true or false) vastly simplifies both the definition of logical operators and the solving of some problems - all you need to do is to ennumerate all possibilities.
- We can view primary propositions as simple functions that return a boolean value and don't take any arguments.
Negation
- We can view logical operators as functions that take a bunch of boolean values and return another boolean value (composite propositions are just the results of the invocation of these functions.)
We will see why this simple and *seemingly* self-evident observation (that propositions can be either true or false) is so important and how it vastly simplifies both the definition of both propositions and logical operators and the solving of some problems - all you need to do is to ennumerate all (two) possibilities.
The *negation* operation
---
Let's begin with the the negation operation, because it is the simplest one, as it is an unary operation, which means it takes just one argument. The negation operation can be represented by this function.
Let's begin with the the negation operation, because it is the simplest one, as it is an unary operation, which means it takes just one argument. It can be represented by this function.
![negation](negation.svg)
Which can be expressed in a sligtly less-fancy way by this table (the header of the second column is read "not p".)
It can also be expressed in a sligtly less-fancy way by this table (the header of the second column is read "not p".)
| p | ¬p |
|---| --- |
@ -148,13 +136,17 @@ Such tables are called *truth tables* and they are ubiquitos in classical logic,
Proving results by truth tables
---
Eventhough axioms and rules of inference are important, each proposition in classical logic can be proved by means of truth tables. Moreover, the fact that a proposition is proven by means of axioms and rules means nothing more than the fact that it can be also proven by truth tables. This is so, because axioms are themselves proven by means of truth tables. In fact, having the definition of the negation operator, we can use it to prove our first proposition, called *double negation elimination*, says that a double negative of a given proposition is equivalent to the proposition itself.
Eventhough axioms and rules of inference are important, each proposition in classical logic can be proved without them, by means of truth tables. Moreover, the fact that a proposition is proven by means of axioms and rules means nothing more than the fact that it can be also proven by truth tables (this is so, because axioms are themselves proven by means of truth tables).
In fact, having the definition of the negation operator, we are in position to prove our first proposition/axiom, called *double negation elimination*. It says that a double negative of a given proposition is equivalent to the proposition itself.
![Double negation elimination formula](double_negation_formula.svg)
If we view logical operators as functions, from and to the set of boolean values, than proving axioms involves composing those functions (using in this case just plain *functional composition*) and observing that theit outputs match. The proof of the formula above is the observation that composing the negation function by itself is equivalent to applying the identity function.
If we view logical operators as functions, from and to the set of boolean values, than proving axioms involves composing those functions (using *functional composition*) and observing that theit outputs match. This would mean that the propositions are *universally valid*, that is they are true for all possible inputs.
![Double negation elimination](double_negation.svg)
More specifically, the proof of the formula above is the observation that composing the negation function by itself is equivalent to applying the identity function.
![Double negation elimination](double_negation_proof.svg)
The equivalent of this in natural language is the fact that saying that I am *not unable* to do X is the same as saying that I am *able* to do it.
@ -165,12 +157,51 @@ Here is the same thing as a truth-table.
| True | False | True |
| False | True | False |
Despite its triviality, this is probably the most controversial result in logic. We will see why later.
Despite its triviality, this proposition is probably the most controversial result in logic, we will see why later.
The **and** and **or** relations
The *implies* operation
---
OK, you know what **and** means and I know what it means, but what about those annoying people that want everything to be formally specified (nudge, nudge). Well we already know how we can satisfy them: we just showing them this truth-table (of course **∧** is the symbol for **and**.)
Let's now look into something less trivial: the "implies" operation, (also known as "entailment"). This operation binds two propositions in a way that the truth of the first one implies the truth of the second one. You can read **p → q** as "if **p** is true, then **q** must also be true. The entailment is a binary one, it is represented by a function from an ordered pair of boolean values, to a boolean value.
![Entailment](entailment.svg)
Here is the truth table.
| p | q | p → q |
|---| --- | --- |
| True | True | True |
| True | False | False |
| False | True | True |
| False | False | True |
Now there are some aspects of this which are non obvious so let's go through every case.
1. If *p* is true and *q* is also true, then **p** does imply **q** - obviously.
2. If *p* is true but *q* is false then **q** does not follow from **p**, cause it would have been true if it did.
3. If *p* is false but *q* is true, then **p** still does imply **q**. What the hell? Consider two factors:
- By saying that *p* implies *q* we don't say that the two are 100% interdependent e.g. the claim that "drinking causes headache" does not mean that drinking is the only source of headaches, and it won't be refuted the fact that you can get headache without drinking.
- The conclusion that *p* implies *q* is reached only if all four cases are satisfied, so this events means nothing by itself.
4. And finally if **p** is false but **q** is false too, then **p** still does imply **q** (just some other day).
It might help you to remember that **p → q** (**p** implies **q**) is true when **-p ∨ q** (either **p** is false or **q** is true.) Because the arguments that truth functions take have just two possible values (**true** and **false**), it is not hard to prove that by enumerating all possible combinations of the arguments.
| p | q | p → q | ¬p | q | ¬p ∨ q |
|---| --- | --- | --- | --- | --- |
| True | True | **True** | False | True | **True** |
| True | False | **False** | False | False | **False** |
| False | True | **True** | True | True | **True** |
| False | False | **True** | True | False | **True** |
You can see that truth tables don't scale well for longer problems. In a sec we will see how we can prove this result of this using some predefined set of axioms. But let's go through the **and** and **or** relations real quick.
The **and** and **or** operations
---
OK, you know what **and** means and I know what it means, but what about those annoying people that want everything to be formally specified (nudge, nudge). Well we already know how we can satisfy them: we just show them this truth-table (in which **∧** is the symbol for **and**.)
| p | q | p ∧ q |
|---| --- | --- |
@ -188,56 +219,56 @@ We can do the same for **or**.
| False | True | True |
| False | False | False |
Some interesting
And we can use as axioms a pair of pretty obvious propositions that we can prove with just looking at the definition of the operations.
Implies relation
- For **and**: **p ∧ q → p** and **p ∧ q → q** "If I am tired and hungry, this means that I am hungry".
- For **or**: **p → p ∨ q** and **p → p ∨ q** "If I have a pen this means that I am either have a pen or a ruler".
Logical systems redux
---
The "implies" relation, also called ("if-then" relation), binds two propositions in a way that the truth of the first one implies the truth of the second one (but not the other way around). You can read **p → q** as "if **p** is true, then **q** must also be true (notice this says nothing about when **p** is false).
After we defined the main logical operators and saw and proved some propositions (which we called tautologies) are universally valid, using truth tables, we are now in position to finish our talk about logical systems which prompted this chapter. If you recall, a logical system is a collection of tautologies and rules that allow us to deduce all other tautologies.
| p | q | p → q |
|---| --- | --- |
| True | True | True |
| True | False | False |
| False | True | True |
| False | False | True |
There are two main classes of such logical systems, the first one are the so-called *Hilbert-style* proof systems (also called *Frege-style*) and the other one are the systems of *natural deduction*, the main difference between the two being whether they rely on *axioms* or on *rules of inference* as a methods for proving propositions.
- *Natural deduction* systems consist only of *rules of inference* (they don't have axiom schemas).
- *Hilbert-style* systems, on the other hand rely mainly on *axiom schemas* as means of proving propositions. They do, however, contain one rule of inference, just because otherwise there would be no way to combine the generated propositions - usually that rule is the *modus ponens* rule, that we already saw.
Proving results
---
With some variations Hilbert-style system consist of the following axioms.
When combining different logical operations into formulas we often want to check what the output would be for different values and whether the formulas are *universally valid*, that is whether they are true for all possible inputs.
![A minimal collection of Hilbert axioms](min_hilbert.svg)
Because the arguments that truth functions take have just two possible values (**true** and **false**), it is not hard to do that by enumerating all possible combinations of the arguments.
And, as an example, we can use those axioms to prove the And let's see an example of a proof using these axioms
For example, here is how we use truth table to prove that **p → q** is the same as **-p ∨ q**.
But wait, how can we be *sure* that a given system is really capable of deducing all tautologies that exist in the world? We can be sure, because it was proven by a guy called Godel, who is like the greated logician ever, a result known as Godel's completenes theorem. However we won't get into that result right now.
| p | q | p → q | -p | q | -p ∨ q |
|---| --- | --- | --- | --- | --- |
| True | True | **True** | False | True | **True** |
| True | False | **False** | False | False | **False** |
| False | True | **True** | True | True | **True** |
| False | False | **True** | True | False | **True** |
The intuinistic perspective
Intuinistic logic
===
Classical logic
> Now this is the story all about how
> Classical logic got flipped, turned upside down
> And I'd like to take a minute, just sit right there
> I'll tell you bout the ideas of a guy called Brouwer
The foundations of classical logic (which was the topic of the last chapter) remained undisputed from its inception untill the 20th century when people tried to really put them to the test by using it as a basis of all mathematics. It was then when came some results like Godel's *other* famous theorem - his *in*completeness theorem was published, stating that formal systems that in formal systems that are able to represent arithmetics, contain some statements that are undecidable, so they cannot be proven to be true, nor false (note that this does not contradict Godel's completeness theorem, as it speaks about arithmetics in particular, while the completeness theorem is about general logic).
In this times, a new philosophical mathematical and logical theory, known as *intuitionism* (also called *constructivism*) was born. If *classical logic* is based on Plato's theory of forms, then intuinism beginned with a philosophical idea originating from Kant and Schopenhauer, that is more or less the exact opposite of what Plato thought - it is the notion that forms are not a thing in itself, but are just subjective ideas that exist only in our minds and the idea that the world as we experience it is largely predetermined of out perceptions of it. Or in the words or L.E.J. Brouwer:
> [...] logic is life in the human brain; it may accompany life outside the brain but it can never guide it by virtue of its own power.
Heyting algebra
Intuinistic logic
===
And since mathematics is a free activity and truth is only in our head, we have no basis to claim that each statements is necessarily *either true or false*, which if you remember is the basis of classical logic and truth-tables.
Follows as an order
---
(you may remember that these kinds of relations are also called "operations").
Or and And as joins and meets
The *negation* operation
---
Not object
The *implies* operation
---
The **and** and **or** operations
---
Formalizing logic with *orders*
===

317
_chapters/05_logic/logic_distributivity.svg Normal file
View File

@ -0,0 +1,317 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<svg
viewBox="0 0 595.3 177"
version="1.1"
id="svg3397"
sodipodi:docname="logic_distributivity.svg"
inkscape:version="1.1-alpha (17bc9184, 2021-03-28)"
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"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:cc="http://creativecommons.org/ns#"
xmlns:dc="http://purl.org/dc/elements/1.1/">
<metadata
id="metadata3403">
<rdf:RDF>
<cc:Work
rdf:about="">
<dc:format>image/svg+xml</dc:format>
<dc:type
rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
</cc:Work>
</rdf:RDF>
</metadata>
<defs
id="defs3401" />
<sodipodi:namedview
pagecolor="#ffffff"
bordercolor="#666666"
borderopacity="1"
objecttolerance="10"
gridtolerance="10"
guidetolerance="10"
inkscape:pageopacity="0"
inkscape:pageshadow="2"
inkscape:window-width="1920"
inkscape:window-height="1035"
id="namedview3399"
showgrid="false"
inkscape:zoom="1.8797245"
inkscape:cx="263.86845"
inkscape:cy="118.9004"
inkscape:window-x="0"
inkscape:window-y="23"
inkscape:window-maximized="0"
inkscape:current-layer="svg3397"
inkscape:document-rotation="0"
inkscape:pagecheckerboard="0" />
<g
id="g8880-3-88"
transform="matrix(0.75024244,0,0,0.75024244,-246.16991,-77.099625)">
<circle
cx="423.45349"
cy="220.3054"
r="73.749413"
id="circle3373-8-7"
style="opacity:0.13;fill:#999999;stroke:#000000;stroke-width:5.2717;stroke-miterlimit:10" />
</g>
<g
id="g8880-3"
transform="matrix(0.75024244,0,0,0.75024244,-109.5405,-74.140609)">
<circle
cx="423.45349"
cy="220.3054"
r="73.749413"
id="circle3373-8"
style="opacity:0.13;fill:#999999;stroke:#000000;stroke-width:5.2717;stroke-miterlimit:10" />
</g>
<g
id="g9442"
transform="matrix(0.75024244,0,0,0.75024244,115.72745,30.94073)"
style="paint-order:fill markers stroke">
<g
id="g2445-3-1"
transform="matrix(2.4458076,0,0,2.2485166,-117.57238,88.039232)"
style="fill:#000000;fill-opacity:0.112903;stroke:none;stroke-width:1.32404;stroke-miterlimit:4;stroke-dasharray:none;paint-order:fill markers stroke" />
</g>
<text
xml:space="preserve"
style="font-style:normal;font-weight:normal;font-size:30.0097px;line-height:1.25;font-family:sans-serif;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.750243"
x="145.6279"
y="-7.5933027"
id="text9288"><tspan
sodipodi:role="line"
id="tspan9286"
x="145.6279"
y="-7.5933027"
style="stroke-width:0.750243" /></text>
<g
id="g8876"
transform="matrix(0.75024244,0,0,0.75024244,-132.42292,-98.0684)">
<circle
cx="414.65698"
cy="258.30109"
r="18.663952"
id="circle3371"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#f58235"
stroke="#e76524"
cx="411.01526"
cy="252.00392"
r="18.663952"
id="circle3385"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g8880"
transform="matrix(0.75024244,0,0,0.75024244,-103.9756,-127.60437)">
<circle
cx="457.06818"
cy="298.73965"
r="18.663952"
id="circle3373"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#8967ac"
stroke="#651c5f"
cx="453.42642"
cy="292.44247"
r="18.663952"
id="circle3387"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g8872"
transform="matrix(0.75024244,0,0,0.75024244,-175.11521,-124.33923)">
<circle
cx="331.20029"
cy="289.40768"
r="18.663952"
id="circle3375-7"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#54b948"
stroke="#00873a"
cx="327.55856"
cy="283.1105"
r="18.663952"
id="circle3389-30"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g1730-53"
transform="matrix(0.44917662,0.02755103,-0.02771664,0.44649302,7.220824,46.657971)"
style="stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none">
<path
style="fill:none;stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 287.69326,71.771896 11.81056,20.289944 9.69072,-21.501284"
id="path1717-2" />
</g>
<g
id="g1730-53-4"
transform="matrix(0.44917662,-0.02755103,-0.02771664,-0.44649302,75.835123,137.08308)"
style="stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none">
<path
style="fill:none;stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 287.69326,71.771896 11.81056,20.289944 9.69072,-21.501284"
id="path1717-2-2" />
</g>
<g
style="display:inline;fill:#dddddd;stroke:#838383;stroke-width:6.389;stroke-miterlimit:10"
id="g1482-7-0-7"
transform="matrix(0.19962538,-0.00371824,0.01929213,0.27843255,234.47022,28.617879)">
<path
style="stroke-width:35.526"
inkscape:connector-curvature="0"
id="path1478-7-9-4"
transform="matrix(0.4768,-0.02932,0.03214,0.42867,147.58,197.367)"
d="m 315.1,101.79 c 10.682,-4.135 21.77,-7.738 33.127,-11.074 -8.518,-8.139 -17.577,-16.01 -27.178,-23.616 -2.04,12.119 -3.103,21.663 -5.949,34.69 z" />
<path
style="stroke-width:10.649;paint-order:markers fill stroke"
inkscape:connector-curvature="0"
id="path1480-1-3-4"
transform="matrix(0.89574,0,0,0.81736,18.384,154.236)"
d="M 256.00808,84.703489 C 283.39188,81.262654 297.41031,82.245264 317.498,86.173"
sodipodi:nodetypes="cc" />
</g>
<g
style="display:inline;fill:#dddddd;stroke:#838383;stroke-width:6.389;stroke-miterlimit:10"
id="g1482-7-0-7-0"
transform="matrix(-0.19962538,-0.00371824,-0.01929213,0.27843255,351.30491,28.007747)">
<path
style="stroke-width:35.526"
inkscape:connector-curvature="0"
id="path1478-7-9-4-3"
transform="matrix(0.4768,-0.02932,0.03214,0.42867,147.58,197.367)"
d="m 315.1,101.79 c 10.682,-4.135 21.77,-7.738 33.127,-11.074 -8.518,-8.139 -17.577,-16.01 -27.178,-23.616 -2.04,12.119 -3.103,21.663 -5.949,34.69 z" />
<path
style="stroke-width:10.649;paint-order:markers fill stroke"
inkscape:connector-curvature="0"
id="path1480-1-3-4-2"
transform="matrix(0.89574,0,0,0.81736,18.384,154.236)"
d="M 256.00808,84.703489 C 283.39188,81.262654 297.41031,82.245264 317.498,86.173"
sodipodi:nodetypes="cc" />
</g>
<g
id="g8880-3-8"
transform="matrix(0.75024244,0,0,0.75024244,56.681214,-74.151178)">
<circle
cx="423.45349"
cy="220.3054"
r="73.749413"
id="circle3373-8-6"
style="opacity:0.13;fill:#999999;stroke:#000000;stroke-width:5.2717;stroke-miterlimit:10" />
</g>
<g
id="g8876-2"
transform="matrix(0.75024244,0,0,0.75024244,234.85387,-98.164326)">
<circle
cx="414.65698"
cy="258.30109"
r="18.663952"
id="circle3371-5"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#f58235"
stroke="#e76524"
cx="411.01526"
cy="252.00392"
r="18.663952"
id="circle3385-1"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g8880-39"
transform="matrix(0.75024244,0,0,0.75024244,62.246123,-127.61492)">
<circle
cx="457.06818"
cy="298.73965"
r="18.663952"
id="circle3373-7"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#8967ac"
stroke="#651c5f"
cx="453.42642"
cy="292.44247"
r="18.663952"
id="circle3387-3"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g8872-7"
transform="matrix(0.75024244,0,0,0.75024244,95.597097,-122.29943)">
<circle
cx="331.20029"
cy="289.40768"
r="18.663952"
id="circle3375-7-5"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#54b948"
stroke="#00873a"
cx="327.55856"
cy="283.1105"
r="18.663952"
id="circle3389-30-0"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g1730-53-2"
transform="matrix(0.44917662,0.02755103,-0.02771664,0.44649302,240.69364,46.647407)"
style="stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none">
<path
style="fill:none;stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 287.69326,71.771896 11.81056,20.289944 9.69072,-21.501284"
id="path1717-2-1" />
</g>
<g
id="g1730-53-4-8"
transform="matrix(0.44917662,-0.02755103,-0.02771664,-0.44649302,312.49525,136.27426)"
style="stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none">
<path
style="fill:none;stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 287.69326,71.771896 11.81056,20.289944 9.69072,-21.501284"
id="path1717-2-2-7" />
</g>
<g
id="g8880-3-8-4"
transform="matrix(0.75024244,0,0,0.75024244,196.34821,-74.812036)">
<circle
cx="423.45349"
cy="220.3054"
r="73.749413"
id="circle3373-8-6-5"
style="opacity:0.13;fill:#999999;stroke:#000000;stroke-width:5.2717;stroke-miterlimit:10" />
</g>
<g
id="g8872-7-3"
transform="matrix(0.75024244,0,0,0.75024244,235.2641,-122.96029)">
<circle
cx="331.20029"
cy="289.40768"
r="18.663952"
id="circle3375-7-5-9"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#54b948"
stroke="#00873a"
cx="327.55856"
cy="283.1105"
r="18.663952"
id="circle3389-30-0-0"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g1730-53-2-5"
transform="matrix(0.44917662,0.02755103,-0.02771664,0.44649302,380.36063,45.986546)"
style="stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none">
<path
style="fill:none;stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 287.69326,71.771896 11.81056,20.289944 9.69072,-21.501284"
id="path1717-2-1-5" />
</g>
</svg>
Side by Side

After

Width:  |  Height:  |  Size: 11 KiB

302
_chapters/05_logic/logic_monoid.svg Normal file
View File

@ -0,0 +1,302 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<svg
viewBox="0 0 595.3 177"
version="1.1"
id="svg3397"
sodipodi:docname="logic_monoid.svg"
inkscape:version="1.1-alpha (17bc9184, 2021-03-28)"
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"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:cc="http://creativecommons.org/ns#"
xmlns:dc="http://purl.org/dc/elements/1.1/">
<metadata
id="metadata3403">
<rdf:RDF>
<cc:Work
rdf:about="">
<dc:format>image/svg+xml</dc:format>
<dc:type
rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
</cc:Work>
</rdf:RDF>
</metadata>
<defs
id="defs3401" />
<sodipodi:namedview
pagecolor="#ffffff"
bordercolor="#666666"
borderopacity="1"
objecttolerance="10"
gridtolerance="10"
guidetolerance="10"
inkscape:pageopacity="0"
inkscape:pageshadow="2"
inkscape:window-width="1920"
inkscape:window-height="1035"
id="namedview3399"
showgrid="false"
inkscape:zoom="1.8797245"
inkscape:cx="302.70393"
inkscape:cy="92.832753"
inkscape:window-x="0"
inkscape:window-y="23"
inkscape:window-maximized="0"
inkscape:current-layer="svg3397"
inkscape:document-rotation="0"
inkscape:pagecheckerboard="0" />
<g
id="g9442"
transform="matrix(0.75024244,0,0,0.75024244,150.30699,18.704894)"
style="paint-order:fill markers stroke">
<g
id="g2445-3-1"
transform="matrix(2.4458076,0,0,2.2485166,-117.57238,88.039232)"
style="fill:#000000;fill-opacity:0.112903;stroke:none;stroke-width:1.32404;stroke-miterlimit:4;stroke-dasharray:none;paint-order:fill markers stroke" />
</g>
<text
xml:space="preserve"
style="font-style:normal;font-weight:normal;font-size:30.0097px;line-height:1.25;font-family:sans-serif;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.750243"
x="180.20743"
y="-19.829138"
id="text9288"><tspan
sodipodi:role="line"
id="tspan9286"
x="180.20743"
y="-19.829138"
style="stroke-width:0.750243" /></text>
<g
id="g8876"
transform="matrix(1.151878,0,0,1.151878,-276.70708,-241.80449)">
<circle
cx="414.65698"
cy="258.30109"
r="18.663952"
id="circle3371"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#f58235"
stroke="#e76524"
cx="411.01526"
cy="252.00392"
r="18.663952"
id="circle3385"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g1730-53-4"
transform="matrix(0.6896393,-0.04230023,-0.04255449,-0.68551906,45.040035,117.23323)"
style="stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none">
<path
style="fill:none;stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 287.69326,71.771896 11.81056,20.289944 9.69072,-21.501284"
id="path1717-2-2" />
</g>
<g
style="display:inline;fill:#dddddd;stroke:#838383;stroke-width:6.389;stroke-miterlimit:10"
id="g1482-7-0-7"
transform="matrix(0.30649304,-0.00570877,0.02962,0.42748892,265.89679,-44.847473)">
<path
style="stroke-width:35.526"
inkscape:connector-curvature="0"
id="path1478-7-9-4"
transform="matrix(0.4768,-0.02932,0.03214,0.42867,147.58,197.367)"
d="m 315.1,101.79 c 10.682,-4.135 21.77,-7.738 33.127,-11.074 -8.518,-8.139 -17.577,-16.01 -27.178,-23.616 -2.04,12.119 -3.103,21.663 -5.949,34.69 z" />
<path
style="stroke-width:10.649;paint-order:markers fill stroke"
inkscape:connector-curvature="0"
id="path1480-1-3-4"
transform="matrix(0.89574,0,0,0.81736,18.384,154.236)"
d="M 256.00808,84.703489 C 283.39188,81.262654 297.41031,82.245264 317.498,86.173"
sodipodi:nodetypes="cc" />
</g>
<g
style="display:inline;fill:#dddddd;stroke:#838383;stroke-width:6.389;stroke-miterlimit:10"
id="g1482-7-0-7-0"
transform="matrix(-0.30649304,-0.00570877,-0.02962,0.42748892,445.27788,-45.784234)">
<path
style="stroke-width:35.526"
inkscape:connector-curvature="0"
id="path1478-7-9-4-3"
transform="matrix(0.4768,-0.02932,0.03214,0.42867,147.58,197.367)"
d="m 315.1,101.79 c 10.682,-4.135 21.77,-7.738 33.127,-11.074 -8.518,-8.139 -17.577,-16.01 -27.178,-23.616 -2.04,12.119 -3.103,21.663 -5.949,34.69 z" />
<path
style="stroke-width:10.649;paint-order:markers fill stroke"
inkscape:connector-curvature="0"
id="path1480-1-3-4-2"
transform="matrix(0.89574,0,0,0.81736,18.384,154.236)"
d="M 256.00808,84.703489 C 283.39188,81.262654 297.41031,82.245264 317.498,86.173"
sodipodi:nodetypes="cc" />
</g>
<g
id="g8876-5"
transform="matrix(1.151878,0,0,1.151878,-59.252332,-242.20228)">
<circle
cx="414.65698"
cy="258.30109"
r="18.663952"
id="circle3371-8"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#f58235"
stroke="#e76524"
cx="411.01526"
cy="252.00392"
r="18.663952"
id="circle3385-3"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g8876-4"
transform="matrix(1.151878,0,0,1.151878,-175.37378,-172.49556)">
<circle
cx="414.65698"
cy="258.30109"
r="18.663952"
id="circle3371-2"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#f58235"
stroke="#e76524"
cx="411.01526"
cy="252.00392"
r="18.663952"
id="circle3385-1"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g1730-53-4-5"
transform="matrix(0.6896393,-0.04230023,-0.04255449,-0.68551906,47.82669,191.3301)"
style="stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none">
<path
style="fill:none;stroke:#808080;stroke-width:5.81758;stroke-linecap:square;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 287.69326,71.771896 11.81056,20.289944 9.69072,-21.501284"
id="path1717-2-2-8" />
</g>
<g
style="display:inline;fill:#dddddd;stroke:#838383;stroke-width:6.389;stroke-miterlimit:10"
id="g1482-7-0-7-6"
transform="matrix(0.30649304,-0.00570877,0.02962,0.42748892,268.68344,29.249398)">
<path
style="stroke-width:35.526"
inkscape:connector-curvature="0"
id="path1478-7-9-4-2"
transform="matrix(0.4768,-0.02932,0.03214,0.42867,147.58,197.367)"
d="m 315.1,101.79 c 10.682,-4.135 21.77,-7.738 33.127,-11.074 -8.518,-8.139 -17.577,-16.01 -27.178,-23.616 -2.04,12.119 -3.103,21.663 -5.949,34.69 z" />
<path
style="stroke-width:10.649;paint-order:markers fill stroke"
inkscape:connector-curvature="0"
id="path1480-1-3-4-5"
transform="matrix(0.89574,0,0,0.81736,18.384,154.236)"
d="M 256.00808,84.703489 C 283.39188,81.262654 297.41031,82.245264 317.498,86.173"
sodipodi:nodetypes="cc" />
</g>
<g
style="display:inline;fill:#dddddd;stroke:#838383;stroke-width:6.389;stroke-miterlimit:10"
id="g1482-7-0-7-0-1"
transform="matrix(-0.30649304,-0.00570877,-0.02962,0.42748892,448.06453,28.312637)">
<path
style="stroke-width:35.526"
inkscape:connector-curvature="0"
id="path1478-7-9-4-3-3"
transform="matrix(0.4768,-0.02932,0.03214,0.42867,147.58,197.367)"
d="m 315.1,101.79 c 10.682,-4.135 21.77,-7.738 33.127,-11.074 -8.518,-8.139 -17.577,-16.01 -27.178,-23.616 -2.04,12.119 -3.103,21.663 -5.949,34.69 z" />
<path
style="stroke-width:10.649;paint-order:markers fill stroke"
inkscape:connector-curvature="0"
id="path1480-1-3-4-2-9"
transform="matrix(0.89574,0,0,0.81736,18.384,154.236)"
d="M 256.00808,84.703489 C 283.39188,81.262654 297.41031,82.245264 317.498,86.173"
sodipodi:nodetypes="cc" />
</g>
<g
id="g8876-5-7"
transform="matrix(1.151878,0,0,1.151878,-56.465682,-168.10541)">
<circle
cx="414.65698"
cy="258.30109"
r="18.663952"
id="circle3371-8-3"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10" />
<circle
fill="#f58235"
stroke="#e76524"
cx="411.01526"
cy="252.00392"
r="18.663952"
id="circle3385-3-7"
style="stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<g
id="g15965-5"
transform="translate(147.04016,-61.901334)">
<circle
cx="330.06189"
cy="260.59518"
r="18.663952"
id="circle3371-2-5-6"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10"
transform="matrix(1.151878,0,0,1.151878,-225.38111,-182.60342)" />
<g
id="g8880-9-7"
transform="matrix(1.151878,0,0,1.151878,-372.15821,-225.29124)"
style="fill:#e6e6e6;stroke:#808080">
<circle
fill="#8967ac"
stroke="#651c5f"
cx="453.42642"
cy="292.44247"
r="18.663952"
id="circle3387-4-9"
style="fill:#e6e6e6;stroke:#808080;stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<text
xml:space="preserve"
style="font-style:normal;font-weight:normal;font-size:15.131px;line-height:1.25;font-family:sans-serif;fill:#666666;fill-opacity:1;stroke:none;stroke-width:0.378275"
x="134.47717"
y="115.7421"
id="text2961-5-4"><tspan
sodipodi:role="line"
id="tspan2959-0-1"
x="134.47717"
y="115.7421"
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15.131px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Bold';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;fill:#666666;stroke-width:0.378275">true</tspan></text>
</g>
<g
id="g15965-5-4"
transform="translate(47.025505,10.449695)">
<circle
cx="330.06189"
cy="260.59518"
r="18.663952"
id="circle3371-2-5-6-8"
style="opacity:0.13;stroke:#000000;stroke-width:4.55218;stroke-miterlimit:10"
transform="matrix(1.151878,0,0,1.151878,-225.38111,-182.60342)" />
<g
id="g8880-9-7-8"
transform="matrix(1.151878,0,0,1.151878,-372.15821,-225.29124)"
style="fill:#e6e6e6;stroke:#808080">
<circle
fill="#8967ac"
stroke="#651c5f"
cx="453.42642"
cy="292.44247"
r="18.663952"
id="circle3387-4-9-7"
style="fill:#e6e6e6;stroke:#808080;stroke-width:4.55218;stroke-miterlimit:10" />
</g>
<text
xml:space="preserve"
style="font-style:normal;font-weight:normal;font-size:15.131px;line-height:1.25;font-family:sans-serif;fill:#666666;fill-opacity:1;stroke:none;stroke-width:0.378275"
x="134.47717"
y="115.7421"
id="text2961-5-4-1"><tspan
sodipodi:role="line"
id="tspan2959-0-1-9"
x="134.47717"
y="115.7421"
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15.131px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Bold';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;fill:#666666;stroke-width:0.378275">true</tspan></text>
</g>
</svg>
Side by Side

After

Width:  |  Height:  |  Size: 12 KiB

8
_layouts/default.html
View File

@ -19,10 +19,10 @@
<div class="prev-next">
{% if page.previous.url %}
<a class="prev" href="{{site.baseurl}}{{page.previous.url}}">&laquo;prev</a>
<a class="button" href="{{site.baseurl}}{{page.previous.url}}">&laquo;prev</a>
{% endif %}
{% if page.next.url %}
<a class="next" href="{{site.baseurl}}{{page.next.url}}">next&raquo;</a>
<a class="button" href="{{site.baseurl}}{{page.next.url}}">next&raquo;</a>
{% endif %}
</div>
@ -30,10 +30,10 @@
<div class="prev-next">
{% if page.previous.url %}
<a class="prev" href="{{site.baseurl}}{{page.previous.url}}">&laquo;prev</a>
<a class="button" href="{{site.baseurl}}{{page.previous.url}}">&laquo;prev</a>
{% endif %}
{% if page.next.url %}
<a class="next" href="{{site.baseurl}}{{page.next.url}}">next&raquo;</a>
<a class="button" href="{{site.baseurl}}{{page.next.url}}">next&raquo;</a>
{% endif %}
</div>
<script type='text/javascript' src='https://ko-fi.com/widgets/CounterWidget.js'></script><script type='text/javascript'>counterwidget.init('K3K539YDO');counterwidget.draw();</script>

8
custom-style.css
View File

@ -1,7 +1,3 @@
img {
width: 100%;
}
body {
font-size: 25px;
font-family: Arial, sans-serif;
@ -30,3 +26,7 @@ h1, h2, h3, h4, h5, h6 {
.footer {
background-color: #8967acff;
}
.button {
background-color: #8967acff;
}

3
index.md
View File

@ -2,4 +2,5 @@
layout: default
title: index
---
![cover](cover.svg)
[![cover.svg](cover.svg)](00)

36
style.css
View File

@ -1,7 +1,6 @@
body {
line-height: 1.5;
margin: 0;
font-size: 20px;
}
@ -48,28 +47,6 @@ blockquote {
color: #666;
}
@font-face {
font-family: 'mell';
src: url('RubikMonoOne.ttf') format('truetype');
font-weight: bold;
font-style: normal;
}
h1, h2, h3, h4, h5, h6 {
font-family: 'mell', cursive;
}
h1 {
font-size: 40px;
}
@ -119,3 +96,16 @@ table tfoot {
font-weight: bold;
border-top: 3px solid blue;
}
img {
width: 100%;
}
.button {
background-color: black;
color: white;
padding: 10px;
text-decoration: none;
}
.icon {
font-size: 26px;
}

8
todo.md
View File

@ -31,3 +31,11 @@ With respect to orders, it states.
Here my intuition thinks it should be "so for any other object P such that Y ≤ P and B ≤ P then we should also have G ≤ P"
Take this comments with a grain of salt, since I am no mathematician and these comments are based on intuition rather than logic.
I think there might be an error in the colors on this page: https://boris-marinov.github.io/category-theory-illustrated/02_category/
https://boris-marinov.github.io/category-theory-illustrated/02_category/product.svg
Shouldn't the orange element from b be red in B x Y?