Questions tagged [ct.category-theory]
Questions in category theory
28
questions with no upvoted or accepted answers
17
votes
0
answers
269
views
Using Dependent Type Theory for Categories that are not LCCC
I have recently been working with polynomial functors and monads based mostly on Gambino-Kock. There they define polynomial functors in a Locally Cartesian Closed Category (LCCC) and extensively use ...
- 1,653
13
votes
0
answers
268
views
Categorical semantics for S5 modal logic?
Does anyone know where I can look to find out what the generally categorical semantics of S5 is?
For S4, the answer is well-known: we want a Cartesian closed category with a product-preserving ...
- 32.4k
11
votes
0
answers
208
views
Do Banach spaces and linear contraction maps form a model of ILL with an exponential?
Recently, I read on the nLab that the category of Banach spaces and linear contractions is small complete, small cocomplete, and monoidal closed.
This means that Banach spaces and short linear maps ...
- 32.4k
10
votes
0
answers
212
views
What is the "standard" lambda-calculus model for bicartesian closed categories?
(I'm familiar with the lambda-calculus, less so with its categorical models.)
It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with ...
- 2,040
8
votes
0
answers
181
views
Equivalence of categories of directed complete posets
I asked this question there: https://math.stackexchange.com/questions/700975/equivalence-of-categories-of-directed-complete-posets.
Since I had no answer, I try here.
In the book ``Domains and Lambda-...
- 181
7
votes
0
answers
234
views
Category theory lambda cube?
If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to?
https://en.m.wikipedia.org/wiki/Lambda_cube
- 163
6
votes
0
answers
111
views
List Functions That Don't Depend on Length
Intuitively, a polymorphic function of type $f : \forall a. [a] \to [a]$ cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or ...
- 93
6
votes
0
answers
273
views
Generalizing Haskell: could we replace Hask with Cat?
N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum.
It is great that Haskell allows us to walk around in the category $Hask$. But ...
- 381
5
votes
0
answers
179
views
On the interpretation of coinduction in type theory
The notion of (co)datatype can be modeled satisfactorily in category theory as fixed-points of polynomial functors. Then, (co)induction principles are derived from initial algebras/terminal ...
- 921
5
votes
0
answers
143
views
Structures admitting directed sums and directed products?
Some structures have a property of closure by a "sum" or "product" operation. Given a family of structures $(S_i)_{i \in I}$, we can then define a new structure denoted by $\sum_{i \in I} S_i$, resp. $...
- 1,292
5
votes
0
answers
236
views
What's the connection between these two categories of games and innocent strategies?
Lately I've been reading a lot about game semantics and in particular the problem of PCF's full abstraction.
I'm trying to understand how the definition from this article relates to the one found in ...
- 151
4
votes
0
answers
116
views
Transferring results on coalgebras in one category to another
Let $F$ and $G$ be endofunctors over categories $C$ and $ D$, respectively. Suppose that there is a forgetful functor $C \to D$ that has a left adjoint. Can we infer properties of $F$-coalgebras ...
- 895
4
votes
0
answers
341
views
Category theory in plain MLTT
I want to define a category in simple MLTT (not in HoTT). I defined it with the help of setoids. I.e. category consists of:
a type of objects with equivalence relation (Obj : Set)
a type of arrows ...
- 1,762
3
votes
0
answers
104
views
CCCs, computational calculi and point-surjectivity
The models of some computational calculi are in a correspondence with Cartesian Closed Categories with an object $U$ that has some relationship to its exponential object $U^U$ e.g. a retraction ...
3
votes
0
answers
116
views
What's the example of natural transformation in 'Type" that is not a parametric function?
Take a type theory of your choice (perhaps System Fω).
Parametric functions are known to be natural transformations in 'Type' category. Yet not every natural transformation in 'Type' is a polymorphic ...
- 1,177
3
votes
0
answers
546
views
Distributive law between monads in Haskell
A distributive law between monads must satisfy laws that are usually given in terms of the units $\eta$ and multiplications $\mu$ of the two monads. Among the four laws there are:
$\mu^S T \circ S l \...
- 381
2
votes
0
answers
57
views
Is the Category of $(* \to)^n *$-kinded types freely generated from the discrete graph with $n$ nodes?
In Introduction to Higher Order Categorical Logic part 1, section 4, Lambek defines an adjunction between $\mathbf{Graph}$, the category of graphs and graph homomorphisms, and the category of ...
2
votes
0
answers
119
views
Why Multiple Clocks in Guarded Dependent Type Theories?
The main purpose of clocks in guarded type theories (originating in Atkey & McBride ICFP 2013) is so that we can define coinductive constructions from guarded recursive definitions.
Semantically ...
- 1,653
2
votes
0
answers
561
views
Can Category Theory help us prove P != NP?
Scott Aaronson, in this funny April Fools’ Day post, introduces a fictionalized $P \neq NP$ Proof and, among other things, he says that the proof make use of
Higher topos theory to solve the biggest ...
- 684
2
votes
0
answers
82
views
Categorical model of binding / first class modules
Binders are explained using presheaves (Pitts/Gabbay A new approach to Abstract Syntax with variable binding)
What is the equivalent (categorical) theory to explain first class modules as in 1ML ?
- 121
2
votes
0
answers
76
views
Composition series and isogeny
I'm not sure this question is appropriate for this site, but it might have some connections with computational algebra.
Consider a fixed "category" $\sf{Cat}$ (in the sense of category theory, but ...
- 1,292
1
vote
0
answers
110
views
Closely related (?) arrows in categories
Let $f: x\to y$ and $f':x' \to y'$ be arrows in a category ${\bf C}$, where $x\cong x'$ and $y\cong y'$. Assume that for all isomorphisms $v: x \to x'$ and $u: y\to y'$, the corresponding diagram ...
- 193
1
vote
0
answers
63
views
Mappings that are not functors in category theory
Let C be a category and let $F$ be a mapping on C. Assume that $F$ is defined for all objects of C. However, on the arrows of C the mapping $F$ does not always behave like a (covariant) functor. For ...
- 11
1
vote
0
answers
55
views
How to read this formula for composition in an asynchronous interaction category?
The paper is available here Interaction Categories and the Foundations of Typed Concurrent Programming Abramsky, Gay, Nagarajan
p.38 composition of two processes $p:A \rightarrow B$, $q:B \rightarrow ...
- 11
1
vote
0
answers
85
views
Categorical way of factoring out points
Major rewrite justifiably asked for:
I'm currently trying to get a categorical way of doing something called the Gelfond-Lifschitz reduct on a set of single-headed Horn clauses. The semantics is the ...
- 191
0
votes
0
answers
29
views
Which family of bicartesian closed functors can define the semantics of simply typed lambda calculus with products and sums
Given any bicartesian closed category $\mathbf{C}$, any natural number $n \geq 0$, and any vector $\boldsymbol{A} \in \mathbf{C}^n$ with $n$ objects $A_1, A_2, … A_n \in \mathbf{C}$, how can I define ...
0
votes
0
answers
87
views
Is this a reader monad?
I'm unsure whether the following three equations constitute a valid instance of a reader/environment monad on the simply-typed lambda calculus, where $\alpha$ is any type (I subscript some terms with ...
- 105
-2
votes
1
answer
81
views
Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs
Suppose we have a set $S$ of constants of the Simply-Typed Lambda Calculus (STLC) various types, and the operation of union $\cup$ which takes two constants and forms their union.
For example, $S$ ...
- 105