This tool implements some basic Category theory in the form of a diagram with the intention to help to visualize and understand the concepts in Category theory. In the current state it is possible to prove some simple facts, such as AxB≃BxA, Ax1≃A.
An interactable version of the tool is available here.
A category consists of a collection of objects (visualized as circles), and a collection of morphisms (visualized as arrows from one object to another).
Each morphism has a domain and a codomain. A morphism f with domain A and codomain B is denoted as: f: A -> B.
Each object A has a corresponding identity morphism idₐ (sometimes denoted simply id or 1).
Morphisms f and g can be composed together if the codomain of f is the same as the domain of g (i.e. f: A -> B, g: B -> C). Their composition is g ∘ f: A -> C. The category is closed under composition (i.e. composing two morphisms yields another morphism in the same category).
Axioms:
- Identity:
f ∘ id = f,id ∘ f = f - Associativity:
f ∘ (g ∘ h)=(f ∘ g) ∘ h=f ∘ g ∘ h
Some morphisms are unique (visualized by a red dashed arrow) (see terminal/initial objects for an example), which means that any morphism with the same domain and codomain is equal to the unique morphism (i.e. is the same morphism), and it can be removed/merged with the unique morphism.
Some morphisms are unique only under an extra constraint (see product for an example). That means if a morphism has the same domain and codomain and at the same time satisfies the constraint, then it is equal to the unique morphism, and it can be removed/merged with the unique morphism.
A terminal object (denoted as 1) is such an object that for all objects in the category there exists a unique morphism from that object to the terminal object (i.e. any morphism from that object to the terminal object is the same).
An initial object (denoted as 0) is such an object that for all objects in the category there exists a unique morphism from the initial object to that object (the opposite of terminal object).
Two object are called isomorphic if and only if there exists a morphism from both objects to each other and the morphisms are inverse, i.e. their composition in any order equals identity.
Isomorphism is represented as a red connection (not an arrow) with a special symbol in the middle between two objects:
A product AxB of two objects A and B has two morphisms: π₁: AxB -> A, π₂: AxB -> B
- and for all objects C with morphisms:
f: C -> A,g: C -> B - there exists a morphism
m: C -> AxB - such that the triangles commute:
π₁ ∘ m = f,π₂ ∘ m = gand m is unique under that constraint (i.e. if there exists another morphism m' such thatπ₁ ∘ m' = f,π₂ ∘ m' = gthenm = m')
The window is split into three areas (left to right): rules, facts, and goal.
Each rule is built from a sequence of constraints, which can be: for all and exists. For example, the identity rule can be represented by the following sentence: For all objects there exists a morphism coming from that object back to itself.
When applying a rule, possible input selections are highlighted.
The rules are color coded in the following way:
- Blue - input; has to be selected by the user
- Red - output
- Purple - inferred from context
- Cyan - forall
- Green - exists
For example the terminal object rule can be read as:
- there exists a terminal object 1
- such that for all objects A <- input
- there exists a unique (indicated by a dashed line) morphism from A to 1 <- output
Facts can be used together with the rules to infer new facts. To apply a rule, first click on the rule, then select the objects/morphisms that the rule expects (possible options are highlighted).
Rules can also be used on the goal to constraint it. For example, to prove that there exists a morphism from A to B, it is sufficient to prove that there exist some object X together with two morphisms A->X, X->B.
For example, the picture below means that the goal is prove that objects A and Ax1 (the product of A and the terminal object 1) are isomorphic)
Both keyboard+mouse and touchscreen are supported. Hopefully, the controls are intuitive, but anyway here is the list of possible actions:
- Moving objects/morphisms
- Drag with LMB
- Drag with one finger
- Moving camera
- Drag with RMB
- Ctrl + drag with LMB
- Drag from an empty place with one finger (not possible in the rule section)
- Drag with two fingers
- Zooming the camera
- Ctrl + scroll the mouse wheel
- Touch with two fingers and control the distance between them
- Selecting a rule
- Left click or touch any point inside the rule
- Selecting an object/morphism
- Left click or touch the object/morphism
- Scrolling the rules
- Scroll the mouse wheel
- Drag with one finger in the rule area
- Undo last action
- Ctrl + Z
- left click or tap the undo button
- Redo (a.k.a undo last undo)
- Ctrl + ⇧ Shift + Z
- Left click or tap the redo button
- Cancel rule selection
- Esc