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.
25
questions
27
votes
2
answers
863
views
What is Artin gluing, and how is it useful in proving meta-theoretic properties?
I came across this notion in several places, especially in recent papers that establish important meta-theoretic properties of type theories like CuTT. The entry in nLab focuses on the geometric ...
4
votes
1
answer
231
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 ...
- 9,732
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 ...
19
votes
2
answers
1k
views
What are "fibration/cofibration" in type theory and what are their intuitions?
I keep seeing these phrasing in some proof assistants/elaborators and their issues/internal discussions (e.g. Github search results in cooltt), that seems not that related to the actual proofs/...
- 296
1
vote
2
answers
285
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 ...
- 665
10
votes
1
answer
289
views
What is realignment and is it useful in non-univalent theories?
From my rough understanding, an (external/internal) realignment property says that given a type $A$, a proposition $p : \Omega$, and a partial isomorph $B : p \to \sum_{A'} A' \cong A$, we can extend ...
- 4,025
1
vote
1
answer
112
views
Formal proof of “functional” / purposive law
I am really interested in exploring if (legal) laws can be proven to be self-consistent using a formal programming language / proof assistant, and modeling the laws using category theory, perhaps ...
- 2,220
4
votes
2
answers
320
views
Reasoning about CwFs in a proof assistant
I've been chatting with folks on Mastodon about this but the perspective there is markedly Agda-focused, so I thought I'd ask here for some broader opinions.
What tools/libraries are there for ...
2
votes
0
answers
81
views
Formally verified email or communication?
This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway.
I would like to consider the simplest possible formally verified ...
1
vote
1
answer
85
views
Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator
In Category Theory the Natural Numbers object ℕ has the universal mapping-out property that tells us how to build arrows out of ℕ into an arbitrary object A. But it doesn't say that every arrow ...
- 4,025
5
votes
1
answer
469
views
Semantics of type theory
There are many tools regarding the semantics of type theory. On one hand, we may organize the structure of substitutions explicitly, resulting in notions such as CwFs, CwAs, natural models, display ...
- 516
3
votes
1
answer
152
views
Stacks versus universes
This is a vague question, and I apologize in advance for it. I do not need a definite answer, I am happy to just get some general ideas.
An elementary topos can model higher order logic over a ...
- 2,336
9
votes
1
answer
179
views
Interpretation of dependent types: Coherence
I have trouble understanding precisely how dependent type theories are intepreted in categories (in the most simple case, for example in a locally cartesian closed category). I know that a type in ...
- 3,200
11
votes
1
answer
288
views
Seven Trees in One, or How to formalize the Semiring of Types?
This is somewhat conceptual beginner's question about proof assistants.
I've been re-reading the famous Seven Trees in One / Objects of categories as complex numbers. The gist: The type $T$ of binary ...
- 2,022