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
1
vote
1
answer
107
views
Proving that applicative functors compose
For simplicity, here an applicative functor means (in a proof assistant based on dependent type theory) the Haskellian applicative functor, bundled with its equational laws.
This I can of course brute ...
- 9,195
2
votes
0
answers
70
views
Construction of "free Lawvere theory" on a collection of function symbols
I think I've been able to puzzle out the free Lawvere theory on a collection of function symbols ought to have maps being just tuples of the free monad.
In Coq
...
- 2,868
14
votes
6
answers
1k
views
Is there any example of a dependent product that makes sense in a non-type-theory context?
Dependent products are said to be the right adjoints of reindexing functors according to nlab. However, I can only make sense of this explanation in the context of type theory, where dependent ...
- 2,868
20
votes
1
answer
314
views
Examples of formalisation of abelian categories
The question
I would be interested to hear about examples of formalisation of the theory of abelian categories in theorem provers, and in particular formalisations of things like the zig-zag lemma and ...
- 2,300
10
votes
0
answers
187
views
Is there a proof assistant (or an embedding) for the (co)end calculus?
A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
- 2,846
18
votes
2
answers
562
views
What are the motivations for different variants of categorical models of dependent type?
I am new to the categorical semantics for dependent type theories, so it is surprising for me to see nLab introduces so many variants of categorical models, including comprehension categories, display ...
- 3,200
6
votes
0
answers
114
views
Is every logical theory embeddable in a dependently typed extensional type theory?
In category theory by the Yoneda embedding every category $\mathcal{C}$ is a subcategory of a category of presheafs $[\mathcal{C}^{\text{op}}, \text{Set}]$. Every category of presheafs is a topos and ...
- 2,868
11
votes
1
answer
207
views
Ergonomic use of multicategories in proof assistants
I've been looking at syntactic multicategories for mechanizing some type theory stuff.
But multicategories are pretty messy to work with in a two sorted definition like the usual dependently typed ...
- 3,200
5
votes
0
answers
95
views
What is the relation of $\lambda^\to$ and $\lambda^{\to\times}$ to cartesian closed categories?
I am learning about the categorical semantics of type theory. I've written some preliminary results in Agda. In particular, I partially proved that the contexts and substitutions of simply-typed ...
- 4,025
20
votes
0
answers
275
views
Can we automatically get around set-theoretic difficulties?
One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large ...
- 1,013