6,366 reputation
1625
bio website poisson.phc.unipi.it/~mossa
location Earth
age 26
visits member for 3 years, 5 months
seen 49 mins ago

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.


Nov
24
comment System of generators and surjective homomorphism
@MartinBrandenburg ops... thanks for pointing out, I'm going to edit immediately.
Nov
23
comment Homotopy Groups for Categories
I wouldn't dare to call this constuction $\pi_1$ of a category, mainly because this is structure distinguish an n-tuple of composable arrows in the category and their composite....
Nov
21
comment Why is this not a category?
A little add: if instead one consider the families $mor_{\mathbb P}(O,Q)$ of decreasing monotone functions these data do not form a category.... well not in the natural way.
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?