6,126 reputation
1623
bio website poisson.phc.unipi.it/~mossa
location Earth
age 26
visits member for 3 years, 1 month
seen 8 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.


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
19
answered How do definitions work in Martin-Lof type theory?
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
answered Typed Category Theory?
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?
Jun
12
answered Types, Sets and Categories
Jun
8
awarded  Yearling
May
24
answered Is the collection of dinatural transformations between two functors a category?
May
19
answered Tensor product of a vector space and a field
May
19
revised What's the significance of defining group as a group object in category $\mathcal{Set}$?
added stuff
May
19
answered What's the significance of defining group as a group object in category $\mathcal{Set}$?
May
16
answered Quotient modules isomorphic $ \Rightarrow$ submodules isomorphic
May
14
answered Doubt about Yoneda Embedding as image of the hom functor
May
13
answered question about $p$-Sylow subgroups
May
13
revised Unit for Left Adjoint to the Inclusion Functor
Fixed some typos (functor $i$ cannot be composed with object of the category $\mathbf{Set}/I$)
May
13
answered Clarification about the definition of term algebras
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.