6,136 reputation
1623
bio website poisson.phc.unipi.it/~mossa
location Earth
age 26
visits member for 3 years, 2 months
seen Aug 6 at 12:58

I'm math student, in particular I'm interested in algebra, geometry, topology and category theory (especially higher dimensional category theory) and its application in mathematics.


Jul
17
comment Proof completion: if $Y$ is a closed term in strong nf, then $Yx$ weakly reduces to a strong nf $Z$
@RoyO. After a deep reading of the book you cited above I think I've finally found a solution to your problem, take a look and let me know if it's not clear :)
Jul
16
comment Algebras of the environment monad
@MartinBrandenburg aaaaaah I see now. I'm sorry I've misread the question, anyway since it seems that the OP seems interested I think it would better leave it....
Jul
16
comment Algebras of the environment monad
@JeffRussell yes, because $(-)^E \circ (-)^E={(-)^E}^E$ so by the isomorphism ${(-)^E}^E \cong (-)^{E \times E}$ (a.k.a. the exponential law) we get the monad structure.
Jul
15
comment Algebras of the environment monad
@MartinBrandenburg The OP asked "Is there a more natural way to describe these things?" I presented such monad as the image of the comonoid through the yoneda embedding, isn't it a different way to describe the monad?
Jul
8
comment Proof completion: if $Y$ is a closed term in strong nf, then $Yx$ weakly reduces to a strong nf $Z$
@RoyO. I'm probably a little rusty, but isn't it true that a reduction of a term has complexity less than the starting term?
Jul
4
comment On the category of Sets as an example of an algebraic category
@DanaeKissinger Ok, then I think my answer said something about that too, let me edit a little bit to make it clear.
Jun
20
comment How do definitions work in Martin-Lof type theory?
Anyway if you have more question I suppose it's better to go in chat :)
Jun
20
comment How do definitions work in Martin-Lof type theory?
Definitions are the rules for the type.
Jun
20
comment How do definitions work in Martin-Lof type theory?
@user18921 Definition of inductive type in a type theory works like the definition of any other type: you state a rule for the introduction of the type (one that state that the constant of language that represent the type is indeed a type) and some constructors, eliminators and computational rules. The only difference is that such rules are required to have a certain format.
Jun
12
comment Types, Sets and Categories
@CristianGarcia $C_0$ is the type, so of course they have all the same type :), at least this is the usual type theoretic definition of category.
Jun
12
comment Using types instead for basic proofs
@ChristianGarcia Are you trying to consider membership as a relations in the proposition as type paradigm?
May
12
comment Ultrafilter Lemma and Dimension Theorem
@AsafKaragila Ah, ok thanks. For me the dimension theorem was the one stating the existance of a basis... guess I was wrong :)
May
12
comment Ultrafilter Lemma and Dimension Theorem
I belive there's a mistake: the dimension theorem for arbitrary vector spaces is equivalent to the axioms of choice while, as you stated above, the ultrafilter lemma is not.
May
10
comment Homotopy equivalence between $X/A$ and $X$?
Touche, my bad ... Too work and sleep make Giorgio a dull boy.
May
10
comment Homotopy equivalence between $X/A$ and $X$?
This is a very well known theorem, you can find it every book of algebraic topology, for instance in Hatcher Algebraic Topology.
May
6
comment Showing that every map $f : S^2 \rightarrow S^1$ is homotopic to the trivial map
@user125103 yes your proof is correct.
May
4
comment Natural transformation is a mono iff the components are.
@magma I see that probably I should have made clear my intent from the beginning. I've edited the answer, is it ok now?
May
4
comment Natural transformation is a mono iff the components are.
I wanted to emphatize the fact that is one of the two implications that require the functors to be $\mathbf{Set}$-valued, while the other holds in the generic case.
May
4
comment Natural transformation is a mono iff the components are.
@magma that's not what I meant. The first part of the proof show that one of the two implication does hold for every category $\mathbf D$ as codomain of functors, i.e. it holds also for $\mathbf {Set}$. The second part shows how the other implication holds for $\mathbf{Set}$ valued functors, indeed if I remember well this second implication doesn't hold for a generic category $\mathbf D$.
Apr
29
comment Does Gödel's Completeness Theorem still hold even if the set of variables is finite?
@MauroALLEGRANZA I agree that probably Manin assume the hypothesis of infinite set of variables. Nonetheless my observation is that the proof of completeness theorem doesn't seems requiring the infinity of the set of variables in order to be proven.