Questions tagged [category-theory]
Categories are structures containing objects and arrows between them. Many mathematical structures can be viewed as objects of a category, with structure preserving morphisms as arrows. Reformulating properties of mathematical objects in the general language of category can help one see connections between seemingly different areas of mathematics.
4
questions
4
votes
1
answer
229
views
Are there proof assistants whose core uses category theory?
I have seen many examples of working with categories inside a proof assistant, even some proof assistants like rzk created in part with this as a motivating purpose. Given trinitarianism, it seems at ...
- 153
0
votes
0
answers
51
views
Analysis of proof that for a category which is also a poset, every diagram commutes
A poset may be defined as a set (axioms of ZFC go here to define "set") and a binary relation (which is taken as a primitive notion in first-order logic), which meets these conditions:
$a R ...
0
votes
0
answers
42
views
Create an olog for Wikipedia policy
I really want to try my hand at formalizing some kind of conceptual argument as an olog, after David Spivak.
There are so many unknowns at the same time that I would really appreciate external ...
1
vote
2
answers
283
views
Formalization of a model of ∞-category in a proof assistant
I am aware of similar question in MO whose comment nicely lists zoo of possible models and only such models can be formalized. But I have not found any implementation so far which I could use or ...
- 133