As of May 31, 2023, we have updated our Code of Conduct.

# Questions tagged [category-theory]

Category theory is used to formalize mathematics and its concepts as a collection of objects and arrows (also called morphisms). Category theory can be used to formalize concepts of other high-level abstractions such as set theory, ring theory, and group theory. (By Steve Awodey)

120 questions
Filter by
Sorted by
Tagged with
1 vote
38 views

### Is, beta reduction in type theory being considered as counit for hom-tensor adjunction in category theory, a denotational or operational semantic?

In the article at nlab about the relation between type theory and category theory, it is said that "beta reduction" in type theory corresponds to "counit for hom-tensor adjunction" in category theory ...
• 611
66 views

### $\beta$ reduction equational equality

In Categories, Types and Structures, authors talk about exponential objects in section 2.3.1. Let $C$ be a Cartesian category, and $a,b \in Ob_C$. The exponent of $a$ and $b$ is an object $b^a$ ...
• 611
1 vote
57 views

### A notion dual to a product type having a given type

Consider this class: class Has record part where extract :: record -> part update :: (part -> part) -> record -> record It captures the notion of ...
• 165
87 views

• 133
201 views

### Formalizing basic category theory in Coq

I'm a total beginner in Coq and I'm trying to implement some category theory stuff as an exercise. I surfed a little among git repos of the many avaible such implementations (HoTT, Awodey's Coq ...
• 311
1 vote
195 views

### How can I formalize key value stores with set theory?

I'm currently developing a simple key-value NoSQL store and want to build its formal model. I found article about key value formalisation with category theory, but I'm interested are there some works ...
75 views

### Exponential Object in a poset [closed]

I have been trying to get to grips with what an exponential object is using a poset as an example. So in the poset... {2, 4, 6, 8, 9, 12, 14, 30, 36, 48, 60, 72, 84} x is related to y iff x is a ...
• 21
1 vote
From page 31 of The algebra of programming : Next, consider the squaring functor $()^2: Fun \leftarrow Fun$ defined by $$A^2 = \{(a, b) | a \in A, b \in B\} \\ f^2(a, b) = (f a, f b)$$ ...