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.

Filter by
Sorted by
Tagged with
20 votes
1 answer
245 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 ...
user avatar
11 votes
0 answers
153 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 ,...
user avatar
  • 2,246
13 votes
6 answers
951 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 ...
user avatar
  • 4,136
18 votes
2 answers
359 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 ...
user avatar
  • 419
13 votes
2 answers
606 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/...
user avatar
  • 141
7 votes
0 answers
98 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 ...
user avatar
10 votes
1 answer
171 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 ...
user avatar
8 votes
1 answer
179 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 ...
user avatar
  • 2,246
3 votes
0 answers
76 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 ...
user avatar
  • 2,246
18 votes
0 answers
188 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 ...
user avatar
  • 928
20 votes
2 answers
442 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 ...
user avatar
  • 2,246