Skip to main content

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
4 votes
1 answer
209 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 ...
Chris Henson's user avatar
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 ...
Julius Hamilton's user avatar
0 votes
0 answers
40 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 ...
Julius Hamilton's user avatar
1 vote
2 answers
279 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 ...
TomR's user avatar
  • 133
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 ...
Julius Hamilton's user avatar
4 votes
2 answers
316 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 ...
Joey Eremondi's user avatar
1 vote
1 answer
110 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 ...
Julius Hamilton's user avatar
1 vote
1 answer
84 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 ...
Russoul's user avatar
  • 345
4 votes
1 answer
457 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 ...
Trebor's user avatar
  • 3,967
3 votes
1 answer
149 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 ...
Nico's user avatar
  • 722
9 votes
1 answer
176 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 ...
Nico's user avatar
  • 722
11 votes
1 answer
282 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 ...
Dario's user avatar
  • 213
1 vote
1 answer
101 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 ...
Trebor's user avatar
  • 3,967
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 ...
Ms. Molly Stewart-Gallus's user avatar
20 votes
1 answer
309 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 ...
Kevin Buzzard's user avatar
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 ,...
Trebor's user avatar
  • 3,967
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 ...
ice1000's user avatar
  • 6,186
18 votes
2 answers
552 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 ...
Ende Jin's user avatar
  • 429
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/...
Anqur's user avatar
  • 301
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 ...
Ms. Molly Stewart-Gallus's user avatar
11 votes
1 answer
205 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 ...
Ms. Molly Stewart-Gallus's user avatar
10 votes
1 answer
285 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 ...
Trebor's user avatar
  • 3,967
5 votes
0 answers
94 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 ...
Trebor's user avatar
  • 3,967
20 votes
0 answers
273 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 ...
Wojowu's user avatar
  • 1,058
27 votes
2 answers
819 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 ...
Trebor's user avatar
  • 3,967