Reputation
6,811
Top tag
Next privilege 10,000 Rep.
Access moderator tools
Badges
1 7 29
Impact
~70k people reached

Jul
4
revised On the category of Sets as an example of an algebraic category
Improved answer
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.
Jul
4
answered On the category of Sets as an example of an algebraic category
Jul
2
awarded  Curious
Jun
25
answered Variables in Types in type theory
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
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