Questions tagged [ct.category-theory]
Questions in category theory
120
questions
3
votes
1
answer
61
views
Is Linear Evaluation Parametric?
Parametric functions satisfy free theorems which state that they take related arguments to related results. This is formalized by the notion of parametric transformation introduced in section 5 of ...
- 93
3
votes
1
answer
122
views
Can the initial algebra of a 2-variable polynomial functor be computed on the diagonal?
Given a polynomial functor $F$, its initial algebra is denoted by $\mu X.F(X)$.
Now, if $F$ is a 2-variable polynomial functor, $Y \mapsto \mu X.F(X,Y)$ turns out to be functorial and we can, again, (...
- 99
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
2
votes
1
answer
213
views
Fixpoint of a functor in the category of embeddings
In Section 5.2 of the text on Domain Theory by S. Abramsky and A. Jung, it is mentioned that:
"Suppose we are given a recursive domain equation $X \cong F(X)$ where the right hand
side defines a ...
- 193
6
votes
0
answers
109
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
1
vote
0
answers
62
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
3
votes
1
answer
87
views
Does ${\bf CPO}$ have $\omega$-colimits?
Does the category ${\bf CPO}$ have $\omega$-colimits? By ${\bf CPO}$ I mean the category that has as objects the $\omega$-complete pointed partial orders and as arrows $\omega$-continuous functions.
- 193
4
votes
2
answers
230
views
Composition with recursion in functions between types
I always understood functions in functional programming to be modeled by morphisms in the category of types, where any powerful function you write in your code is a morphism that is the composition of ...
- 43
3
votes
1
answer
146
views
Exposition of categorical models of type theory from type-theoretic perspective
Are there any formalizations or expositions of categorical models from type theoretic point-of-view? What I have in mind to get a better grasp of categorical models of dependent types, treating ...
- 890
2
votes
0
answers
114
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,638
5
votes
2
answers
182
views
Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories
In Atkey & McBride ICFP 2013, they extend a simple type theory with guarded recursion indexed by clock variables $\triangleright^k$ and a clock quantification $\forall k. A$ that conveniently ...
- 1,638
4
votes
1
answer
133
views
Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?
This question extends my inquiry from a previous post [0].
Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories [1] and Brown and Palsberg's self-interpreter for F-Omega [2] both employ ...
- 81
2
votes
1
answer
78
views
Question about "Free-ness" of Free SCWF
In Category with Family by Castellan et al., they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF.
My ...
- 133
1
vote
1
answer
60
views
Question in relating STLC and Free CCC
In Lambek's Intro to Higher Order Cat Logic, Chapter 1 Section 4 introduces the free construction (upon graph)
My question is, if I want to have STLC + (fake/incomplete) boolean type, how do I have ...
- 133
10
votes
2
answers
556
views
Induction-recursion in models other than $\mathbf{Set}$
It is well-known that various flavors of induction-recursion are consistent*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-...
- 313
0
votes
1
answer
128
views
Why can't opaque optics form a category?
The optics Haskell package is an alternative to the famous lens package.
lens uses a van ...
- 111
10
votes
0
answers
209
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,030
4
votes
3
answers
310
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 ...
- 41
4
votes
2
answers
173
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 ...
- 185
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 ...
7
votes
1
answer
180
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 "...
- 1,155
17
votes
2
answers
2k
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 ...
- 575
6
votes
1
answer
142
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 ...
- 595
-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
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
7
votes
0
answers
230
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
5
votes
2
answers
252
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.
- 919
8
votes
2
answers
312
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,155
-1
votes
1
answer
124
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,255
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 ...
- 919
2
votes
0
answers
529
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
8
votes
2
answers
779
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 ...
- 575
14
votes
2
answers
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 ...
- 584
9
votes
1
answer
204
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 \...
- 323
10
votes
2
answers
1k
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 ...
- 575
3
votes
0
answers
115
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
11
votes
0
answers
205
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.3k
4
votes
2
answers
670
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 ...
- 575
2
votes
1
answer
82
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$ ...
user49685
7
votes
2
answers
292
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 ...
- 173
4
votes
1
answer
179
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 ...
- 433
3
votes
2
answers
309
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 \...
- 443
17
votes
0
answers
268
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,638
6
votes
1
answer
214
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.
...
- 433
6
votes
1
answer
273
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-...
- 32.3k
7
votes
2
answers
414
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 ...
- 173
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
10
votes
2
answers
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 ...
- 307
5
votes
1
answer
294
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 ...
- 1,638
24
votes
1
answer
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 ...
- 503