Questions tagged [ct.category-theory]

Questions in category theory

Filter by
Sorted by
Tagged with
0
votes
0answers
42 views

Functor Image example in Roman’s CT book

In his book, An Introduction to the Language of Category Theory,Steven Roman provide us with the following diagram: Then, he states: Note that in this example, the object part of F is not injective, ...
8
votes
0answers
142 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 ...
1
vote
0answers
94 views

Kleisli-like category for applicatives?

I am wondering if there is a good way to complete the following analogy: monad : Kleisli category :: applicative functor : ?? That is, a given monad T on a ...
3
votes
1answer
84 views

Relating functors to relational functors with the parametricity translation

$\newcommand{\Type}{\text{Type}}\newcommand{\id}{\text{id}}\newcommand{\map}{\text{map}}$ In attempting to answer the question: Rigorous proof that parametric polymorphism implies naturality using ...
3
votes
0answers
94 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 ...
8
votes
1answer
122 views

"Interesting" categories whose internal logic is a dependent-linear type theory

Dependent-linear type theories may be a functional programmer's dream, but is it categorically interesting, i.e. is it the internal language of an "interesting" category? By "...
14
votes
2answers
1k views

Proof relevance vs. proof irrelevance

I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance. Jacques Carette wrote a Proof-relevant Category Theory in Agda library. But ...
6
votes
1answer
124 views

Given a domain, how do we build a language whose denotation is the domain?

Say we have an arbitrary domain $D$ with a countable basis $B$. Now, how do i build a "language" whose "denotation" lives in the domain? My understanding is that Dana Scott ...
-2
votes
1answer
77 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$ ...
0
votes
0answers
78 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 ...
6
votes
0answers
150 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
5
votes
2answers
209 views

Categorical equivalent of higher order logic

From Simply typed lambda calculus and higher order logic, I get the impression that HOL is STLC + equality + equality axioms. I was wondering if there is a particular kind of category modelling this.
7
votes
2answers
202 views

Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

It is well known that any CCC (cartesian closed category) is a model of the simply-typed $\lambda$-calculus. It is less well known that System F admits a categorical model, but it is also well studied ...
-1
votes
1answer
111 views

Are all computable functions monoidal from a category theory POV? [closed]

I have been studying some category theory only to understand the "why" behind the various categorical constructs we use ("borrow") in the world of functional programming. One of ...
5
votes
0answers
151 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 ...
2
votes
0answers
281 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 ...
6
votes
2answers
540 views

What category are Tagless Final Algebras final In?

The Haskell and Scala community have been very enamored recently with what they call tagless final 'pattern' of programming. These are referenced as dual to initial free algebras, so I was wondering ...
14
votes
2answers
2k views

Category-theoretic treatment of diffs, patches and merging?

Is there a category of patches that looks roughly like this: The objects are strings in some base alphabet The morphisms are edit scripts ("diffs" or "patches") between the strings I'm interested in ...
8
votes
1answer
144 views

Understanding the Beck-Chevalley Condition

I've been reading through Bart Jacobs' "Categorical Logic and Type Theory", and lemma 1.8.9 has me stumped. The lemma is stated as follows: Let $p : \mathbb E \to \mathbb B$ and $q : \mathbb D \to \...
7
votes
2answers
893 views

What logic correponds via Curry-Howard to a Monad?

According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural ...
3
votes
0answers
102 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 ...
10
votes
0answers
150 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 ...
4
votes
2answers
565 views

What does the category of RDF models look like in Institution Theory?

The Question in short Here is the question in its pure form. Details of my reasoning can be found below. The RDF1.1 spec semantics defines a model to consist of a set IR of objects and IP of ...
2
votes
1answer
70 views

Does an initial algebra for a class have to belong to the class itself?

In the context of algebraic data types, a concept of initial algebras is usually defined, e.g., in the following way: An algebra $S$ is initial in a class $C$ of algebras iff for every $A\in C$ ...
7
votes
2answers
248 views

The chromatic number of a graph as a functor

I was fooling around with some concept and was wondering if this viewpoint is explored at all. Let INJ-GRAPH be the subcategory of graphs (with morphisms as homomorphisms) whose morphisms consist only ...
4
votes
1answer
143 views

What are values relative to Hask?

According to ncatlab's page on category theory and haskell, "we can identify a subset of Haskell called Hask that is often used to identify concepts used in basic category theory. One considers ...
3
votes
2answers
257 views

Moggi's computational metalanguage

In Notions of Computation and Monads Moggi models the notion of a computation of type $A$, $TA$, using a monad $T$. Among other things this ensures the $T\eta$ rule: $$\frac{x: A \vdash a:TB}{x:A \...
17
votes
0answers
224 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 ...
6
votes
1answer
156 views

Can all structurally recursive functions be written without explicit recursion using a catamorphism/fold?

In particular, I am thinking of a function which involves conditionals changing the recursive behavior and multiple F-algebras. ...
6
votes
1answer
240 views

Algebraic account of Gaussian elimination?

For fun, I've been looking at the interpretation of linear logic in terms of finite-dimensional vector spaces, and ran into an interesting question about the interpretation of double-negation-...
6
votes
2answers
371 views

Explicit set of types and terms in MLTT

Whenever I read a presentation of MLTT, especially in the context of the correspondence of MLTT with LCCCs (eg. Seely's paper), they say "the type constructors/formation rules are..." and then list a ...
2
votes
0answers
79 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 ?
8
votes
2answers
1k views

What kind of theoretical object corresponds to a C++ concept?

I am lacking a background in theoretical computer science but I would have liked to understand to what kind of theoretical objects C++ concepts corresponds to. Basically, C++ concepts allow to define ...
5
votes
1answer
193 views

Does the Category of CPOs have omega^op limits?

In "Domains and Lambdi Calculi" by Amadio and Curien, in the section on solving recursive domain equations (section 7), they give sufficient conditions on a cpo-enriched category so that the category ...
22
votes
1answer
2k views

Is there a relationship between relational algebra/calculus and category theory?

I am aware of at least two different theoretical approaches for understanding relational databases: Codd's relational algebra/calculus, and category theory. Is there any relationship between these ...
17
votes
1answer
844 views

Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

Many theorems and "paradoxes" - Cantor's diagonalization, undecidability of hatling, undeciability of Kolmogorov complexity, Gödel Incompleteness, Chaitin Incompleteness, Russell's paradox, etc. -...
4
votes
0answers
112 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 ...
11
votes
1answer
305 views

Why Reflexive Graphs for Parametricity?

Looking at models of parametric polymorphism, I am curious why are reflexive graph categories are used? In particular, why do they not include relational composition? In looking at the models, they ...
12
votes
0answers
213 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 ...
18
votes
3answers
1k views

"The" category of Turing machines?

Disclaimer: I know very little about complexity theory. I'm sorry but there is really no way to ask this question without being (terribly) concise: What should be the morphisms in "the" category ...
1
vote
0answers
53 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
votes
2answers
460 views

Implementing "Internal" Languages

One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured ...
8
votes
1answer
305 views

A bicartesian closed category of strict complete partial orders (Hask)

It seems to be well-known that programming languages can't have sums, products and nontermination together. Q1. Is this true? Below (or in the above link I gave) is a partial argument. However, ...
17
votes
2answers
2k views

Status quo of category theory and monads in theoretical computer science research?

Background. I am a bachelor student who is interested in research related to category theory, monads and Haskell, and I want to find a topic for my bachelor’s thesis in that area. I have looked at ...
1
vote
0answers
83 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 ...
4
votes
0answers
321 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 ...
2
votes
1answer
262 views

How can I formalize key value stores with set theory? [closed]

I'm currently developing a simple key-value NoSQL store and want to build its formal model. I'm interested in knowing if there some work about formalization of key-value stores outside of category ...
3
votes
1answer
250 views

What are the morphisms of Adj(C,T) - the category whose objects are the adjunctions of a given monad?

The Wikipedia page for Monad says just that for a monad $(T,\eta,\mu)$ we can define the category of all adjunctions that define the monad: Let $\textbf{Adj}(C,T)$ be the category whose objects ...
13
votes
2answers
573 views

Category theory and parsers --- references wanted

Since I'm interested in parsers (mainly in parser expression grammars), I'm wondering if there's some work that gives a categorical treatment of parsing. Any reference on applications of category ...
2
votes
0answers
86 views

How to derive a monoid's append from category theory [closed]

As I understand, a monoid $M$ is just a special kind of category; it has only one object and its morphisms can be composed through a composition operation. In principle, if $a$ is the object of the ...