# NiftyKitty95

less info
reputation
1139
bio website axiomsofchoice.org location age member for 2 years, 5 months seen Apr 12 at 21:13 profile views 1,383

A duck walks into a bar. Animal control is promptly called and the duck is released into a near by park.

# 1,093 Actions

 Apr9 comment What is the shortest way to write the number $1234567890$? I computationally searched many numbers of the form $\left|\left(e·a^{b^c+d}\pm f·g^h\right)-1234567890\right|$ and haven't found anything particularly close to zero. Apr8 comment Do we lose everything, if the natural transformations in a monad are exactly inverse? @GiorgioMossa: Thanks for the example. I guess the question doesn't imply that the relation is generally true - I ask if we require the natural transfomrations (which are a family of endomorphisms) are exact inverses/bijections $\eta=\mu^{-1}$, if then the image of $1_{\bf C}$ (the category itself) and the image of $T$ can be distinguished in any way, apart from objects and arrows having different names. If $\eta=\mu^{-1}$, can $T$ add or remove anything to the objects which wasn't there before (like the Maybe monad in Haskell adds a new value to every type.) Apr8 comment Do we lose everything, if the natural transformations in a monad are exactly inverse? @user21929: Ah, okay I see, the index of $\mu$ doesn't coincide with it's domain then. I've updated the questions, hopefully well typed, with the reverse concatenation which should be non-trivial in general. /// As an example I think of $\text{return}(x):=[x]$ and flatten as join (e.g. $\text{join}([[a,b,c],[e],[f,g]]):=[a,b,c,e,f,g]$), which -coming from the list of lists side- can't be inverse to each other. So then if a monad were defined to require the natural morphism components to be strict inverses, would the monad be merely a relabeling or could there still be nontrivial applications? Apr8 revised Do we lose everything, if the natural transformations in a monad are exactly inverse? added 21 characters in body Apr8 comment Do we lose everything, if the natural transformations in a monad are exactly inverse? @user21929: Okay, so does $\mu_{TTA}\circ\eta_{TA}=id_{TA}$ do it? The component of $\eta$ at $TA$ mapps to $TTA$ and the component of $\mu$ at $TTA$ should map back to $TA$ --- Remark: In any case, I should also emphasize that I want to speak of a bijection here (so that the (suitably well typed) reverse order of concatenations of the natural transform is the identity too.) Apr8 revised Do we lose everything, if the natural transformations in a monad are exactly inverse? deleted 78 characters in body Apr8 asked Do we lose everything, if the natural transformations in a monad are exactly inverse? Apr7 comment Is there a logical interpretation for equalizer and co-equalizer? Okay, then one last question: I've seen the category of context only in the Bart book and then mentioned in connection with computer science people? Who uses this construct? In particular, I'm a physicist and not convinced it's work looking at it further. Apr6 comment How to extract the sets “produced” by a axiomatic set theory, into some newly introduced collection? That's what I mean, yes. For some predicate $\phi$ my logic recognises. Apr6 revised How to extract the sets “produced” by a axiomatic set theory, into some newly introduced collection? deleted 12 characters in body Apr6 comment How to extract the sets “produced” by a axiomatic set theory, into some newly introduced collection? Thanks for the response. I wonder why not really just say ${\large\frac{{\bf ST}\vdash \phi(a)}{a\in\mathfrak U}}$? Apr6 comment Is there a logical interpretation for equalizer and co-equalizer? You keep saying "contains all free variables", do you emphasize that it might consider more? Apr6 accepted Is there a logical interpretation for equalizer and co-equalizer? Apr5 comment Is there a logical interpretation for equalizer and co-equalizer? I think I read about it in Barts "Categorical logic and type theory". Do the formulas essentially represent predicates of properties of the objects of the models? I.e. I.e. an object $\phi$ in $\mathrm{C}(T)$ might be a predicate and a set $M(\phi):=\{x\,|\,\phi(x)\}$ might be the model. Is my interpretation right? Apr5 comment If $f:N→N$ such that $f(f(x))=3x$, then find $f(2013)$ Spend a lot time thinking about this, very tricky. (For one, if $0\in N$ then $f=0$ is a solution.) Consider $f(f(f(x)))$. The function must fulfill $f(c^m·x)=c^m·f(x)$, with $c=3$. And there is a law for iterations of $f$. This means in particular that $f$ must pass any powers of $c$ through and is determined on the numbers $d$ which aren't divisible by $3$. But then, when the double application must multiply the result, how do you store the two data: a) value of input b) number of previous applications. I don't think it works if in- and output is just a number and you make no restrictions. Apr5 comment Is there a logical interpretation for equalizer and co-equalizer? Thanks for the response. I have a little problem to parse the sentence "let {x:t} denote a term in context, which means that t is a term of type A1,...,An;B and x denotes a sequence of variables, including the variables free in t." (Knuth says don't start a sentence with a mathematical symbol ;). So is '{x:t}' or 't' the "term in context"? Do you mean 't' is a term of type 'A1', 'A1,...,An' or 'A1,...,An;B'? I guess the second. As far as I can tell from the sentence below, you consider the category of contexts and arrows are terms. Then M is a functor and the codomain seemingly has products. Apr4 comment Advantage of ZF over other set theories such as New Foundation @Egbert: I'd have some questions, if you're up to it. I'm a physicist and take some formal notes (on the wiki you find on my page). I've written down a set theory axioms for foundations, but I also want to take notes on categories and types (+HoTT). For this I try to patch things together so I get some kind of consistency. In particular I try to squeeze sets into my type system somehow, this is the bulk of it. If you're motivated, please write me a mail (first paragraph) and make some comments/extend what I mean. Apr3 comment Is there a logical interpretation for equalizer and co-equalizer? @Hurkyl: And you say there is no clear logical interpretation, say in terms of higher order logic? Apr3 comment Is there a logical interpretation for equalizer and co-equalizer? Okay. The question arose in thinking about how the subobject classifier of a non-classical topos works (presheaf-category in particular). Since people say this gives a logic and, by the Yoneda lemma, its arrow structure will generally by quite full, don't I get more than just single arrows between two objects? Apr3 asked Is there a logical interpretation for equalizer and co-equalizer?