Mixing
notation for cartesian product with dependent types?
Clash Royale CLAN TAG#URR8PPP
up vote
0
down vote
favorite
Normally, for a cartesian product between sets $A$ and $B$, we have the notation
$$Atimes B$$
But what if the set $B$ depends on the first element of the cartesian product?
i.e., for each $ain A$, we have a set $B_a$, such that for all elements of our cartesian product $(a,b)$, we have $bin B_a$.
Is there a concise notation for this?
notation
asked Jul 26 at 13:37
Programmer2134
3,17321043
add a comment |Â
up vote
0
down vote
favorite
Normally, for a cartesian product between sets $A$ and $B$, we have the notation
$$Atimes B$$
But what if the set $B$ depends on the first element of the cartesian product?
i.e., for each $ain A$, we have a set $B_a$, such that for all elements of our cartesian product $(a,b)$, we have $bin B_a$.
Is there a concise notation for this?
notation
asked Jul 26 at 13:37
Programmer2134
3,17321043
I am not sure I am following, from where $b$ in the $(a,b)$?
– Holo
Jul 26 at 13:51
I think this is what is usually called a "multivalued function" or "set-valued function".
– Kusma
Jul 26 at 14:03
@Kusma multivalued function is defined using the 2-tuple $(a,bin Bmid aRb)$ for some well defined $R$ over $Atimes B$, there is a single tuple for each $a$ so it does not the same as OP asking(I think)
– Holo
Jul 26 at 14:08
This is exactly the disjoint union of the $B_a$.
– Malice Vidrine
Jul 26 at 15:56
add a comment |Â
up vote
0
down vote
favorite
up vote
0
down vote
favorite
Normally, for a cartesian product between sets $A$ and $B$, we have the notation
$$Atimes B$$
But what if the set $B$ depends on the first element of the cartesian product?
i.e., for each $ain A$, we have a set $B_a$, such that for all elements of our cartesian product $(a,b)$, we have $bin B_a$.
Is there a concise notation for this?
notation
asked Jul 26 at 13:37
Programmer2134
3,17321043
Normally, for a cartesian product between sets $A$ and $B$, we have the notation
$$Atimes B$$
But what if the set $B$ depends on the first element of the cartesian product?
i.e., for each $ain A$, we have a set $B_a$, such that for all elements of our cartesian product $(a,b)$, we have $bin B_a$.
Is there a concise notation for this?
notation
asked Jul 26 at 13:37
Programmer2134
3,17321043
asked Jul 26 at 13:37
Programmer2134
3,17321043
asked Jul 26 at 13:37
Programmer2134
3,17321043
asked Jul 26 at 13:37
Programmer2134
3,17321043
3,17321043
I am not sure I am following, from where $b$ in the $(a,b)$?
– Holo
Jul 26 at 13:51
I think this is what is usually called a "multivalued function" or "set-valued function".
– Kusma
Jul 26 at 14:03
@Kusma multivalued function is defined using the 2-tuple $(a,bin Bmid aRb)$ for some well defined $R$ over $Atimes B$, there is a single tuple for each $a$ so it does not the same as OP asking(I think)
– Holo
Jul 26 at 14:08
This is exactly the disjoint union of the $B_a$.
– Malice Vidrine
Jul 26 at 15:56
add a comment |Â
I am not sure I am following, from where $b$ in the $(a,b)$?
– Holo
Jul 26 at 13:51
I think this is what is usually called a "multivalued function" or "set-valued function".
– Kusma
Jul 26 at 14:03
@Kusma multivalued function is defined using the 2-tuple $(a,bin Bmid aRb)$ for some well defined $R$ over $Atimes B$, there is a single tuple for each $a$ so it does not the same as OP asking(I think)
– Holo
Jul 26 at 14:08
This is exactly the disjoint union of the $B_a$.
– Malice Vidrine
Jul 26 at 15:56
I am not sure I am following, from where $b$ in the $(a,b)$?
– Holo
Jul 26 at 13:51
I am not sure I am following, from where $b$ in the $(a,b)$?
– Holo
Jul 26 at 13:51
I think this is what is usually called a "multivalued function" or "set-valued function".
– Kusma
Jul 26 at 14:03
I think this is what is usually called a "multivalued function" or "set-valued function".
– Kusma
Jul 26 at 14:03
@Kusma multivalued function is defined using the 2-tuple $(a,bin Bmid aRb)$ for some well defined $R$ over $Atimes B$, there is a single tuple for each $a$ so it does not the same as OP asking(I think)
– Holo
Jul 26 at 14:08
@Kusma multivalued function is defined using the 2-tuple $(a,bin Bmid aRb)$ for some well defined $R$ over $Atimes B$, there is a single tuple for each $a$ so it does not the same as OP asking(I think)
– Holo
Jul 26 at 14:08
This is exactly the disjoint union of the $B_a$.
– Malice Vidrine
Jul 26 at 15:56
This is exactly the disjoint union of the $B_a$.
– Malice Vidrine
Jul 26 at 15:56
add a comment |Â
3 Answers
3
active
oldest
votes
up vote
1
down vote
accepted
Since you are talking about dependent types, I suggest
$(a:A) to B_a$
or
$(a in A) to B_a,$
where the former is more "typish" and the latter more mathematical.
If you think "that's a function, not a pair", remember that in mathematics, a function $f : X to Y$ is defined as a subset of $X times Y$ such that for all $x in X$ there exists a unique $y in Y$ such that $(x,y) in f.$
But if you want it to look more like a Cartesian product, you could write it as $(a in A) times B_a.$
These notations are not standard in mathematics, so make sure to define them in whatever you write.
answered Jul 26 at 19:34
md2perpe
5,80511022
"These notations are not standard in mathematics". Do you mean that they are "sometimes used" but not standard, or do you mean that you've just made them up? Either way, I like the notation.
– Programmer2134
Jul 27 at 6:12
In Agda dependent types are written as $(a : A) to B a$. The notations in the post are made up by me based on the one in Agda.
– md2perpe
Jul 27 at 6:25
If we're talking about type theory, the notation $sum_a:AB_a$ is entirely standard, and makes clearer the difference between an indexed family of types and the object the poster is taking about.
– Malice Vidrine
Jul 27 at 17:01
add a comment |Â
up vote
0
down vote
This is the particular case, where $A times B$ cannot be used, since the set does not have a product structure. Thus, there is not really a notation since it wouldn't make sense. As such a notation would always imply a product structure.
You can always define
$$C = (a,b) : a in A, b in B_a$$
answered Jul 26 at 14:39
Jonas
284210
But $B_a$ is not well defined
– Holo
Jul 26 at 14:40
This is indeed what I mean. Is there not a more compact , concise way of writing this?
– Programmer2134
Jul 26 at 15:44
add a comment |Â
up vote
0
down vote
Given an indexed family of sets $(B_a)_ain A$, the set $;ain Awedge bin B_a$ is just the disjoint union of the indexed family. Depending on context, you may see this as $$biguplus_ain AB_a$$ or $$coprod_ain AB_a$$ or $$sum_ain AB_a.$$
answered Jul 26 at 16:44
Malice Vidrine
5,32121019
Also noting that the last of these is more often associated with viewing the structure as a collection of pairs than the others, since in dependent type theories the pair-hood of the elements matters. The other notations tend to appear more often without the connotations of pairhood and with more emphasis on "sets gathered in a non-overlapping manner". But this is an informal comment on the notation, and may be skewed by the specific material I'm familiar with.
– Malice Vidrine
Jul 26 at 16:57
add a comment |Â
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
accepted
Since you are talking about dependent types, I suggest
$(a:A) to B_a$
or
$(a in A) to B_a,$
where the former is more "typish" and the latter more mathematical.
If you think "that's a function, not a pair", remember that in mathematics, a function $f : X to Y$ is defined as a subset of $X times Y$ such that for all $x in X$ there exists a unique $y in Y$ such that $(x,y) in f.$
But if you want it to look more like a Cartesian product, you could write it as $(a in A) times B_a.$
These notations are not standard in mathematics, so make sure to define them in whatever you write.
answered Jul 26 at 19:34
md2perpe
5,80511022
"These notations are not standard in mathematics". Do you mean that they are "sometimes used" but not standard, or do you mean that you've just made them up? Either way, I like the notation.
– Programmer2134
Jul 27 at 6:12
In Agda dependent types are written as $(a : A) to B a$. The notations in the post are made up by me based on the one in Agda.
– md2perpe
Jul 27 at 6:25
If we're talking about type theory, the notation $sum_a:AB_a$ is entirely standard, and makes clearer the difference between an indexed family of types and the object the poster is taking about.
– Malice Vidrine
Jul 27 at 17:01
add a comment |Â
up vote
1
down vote
accepted
Since you are talking about dependent types, I suggest
$(a:A) to B_a$
or
$(a in A) to B_a,$
where the former is more "typish" and the latter more mathematical.
If you think "that's a function, not a pair", remember that in mathematics, a function $f : X to Y$ is defined as a subset of $X times Y$ such that for all $x in X$ there exists a unique $y in Y$ such that $(x,y) in f.$
But if you want it to look more like a Cartesian product, you could write it as $(a in A) times B_a.$
These notations are not standard in mathematics, so make sure to define them in whatever you write.
answered Jul 26 at 19:34
md2perpe
5,80511022
"These notations are not standard in mathematics". Do you mean that they are "sometimes used" but not standard, or do you mean that you've just made them up? Either way, I like the notation.
– Programmer2134
Jul 27 at 6:12
In Agda dependent types are written as $(a : A) to B a$. The notations in the post are made up by me based on the one in Agda.
– md2perpe
Jul 27 at 6:25
If we're talking about type theory, the notation $sum_a:AB_a$ is entirely standard, and makes clearer the difference between an indexed family of types and the object the poster is taking about.
– Malice Vidrine
Jul 27 at 17:01
add a comment |Â
up vote
1
down vote
accepted
up vote
1
down vote
accepted
Since you are talking about dependent types, I suggest
$(a:A) to B_a$
or
$(a in A) to B_a,$
where the former is more "typish" and the latter more mathematical.
If you think "that's a function, not a pair", remember that in mathematics, a function $f : X to Y$ is defined as a subset of $X times Y$ such that for all $x in X$ there exists a unique $y in Y$ such that $(x,y) in f.$
But if you want it to look more like a Cartesian product, you could write it as $(a in A) times B_a.$
These notations are not standard in mathematics, so make sure to define them in whatever you write.
answered Jul 26 at 19:34
md2perpe
5,80511022
Since you are talking about dependent types, I suggest
$(a:A) to B_a$
or
$(a in A) to B_a,$
where the former is more "typish" and the latter more mathematical.
If you think "that's a function, not a pair", remember that in mathematics, a function $f : X to Y$ is defined as a subset of $X times Y$ such that for all $x in X$ there exists a unique $y in Y$ such that $(x,y) in f.$
But if you want it to look more like a Cartesian product, you could write it as $(a in A) times B_a.$
These notations are not standard in mathematics, so make sure to define them in whatever you write.
answered Jul 26 at 19:34
md2perpe
5,80511022
answered Jul 26 at 19:34
md2perpe
5,80511022
answered Jul 26 at 19:34
md2perpe
5,80511022
answered Jul 26 at 19:34
md2perpe
5,80511022
5,80511022
"These notations are not standard in mathematics". Do you mean that they are "sometimes used" but not standard, or do you mean that you've just made them up? Either way, I like the notation.
– Programmer2134
Jul 27 at 6:12
In Agda dependent types are written as $(a : A) to B a$. The notations in the post are made up by me based on the one in Agda.
– md2perpe
Jul 27 at 6:25
If we're talking about type theory, the notation $sum_a:AB_a$ is entirely standard, and makes clearer the difference between an indexed family of types and the object the poster is taking about.
– Malice Vidrine
Jul 27 at 17:01
add a comment |Â
"These notations are not standard in mathematics". Do you mean that they are "sometimes used" but not standard, or do you mean that you've just made them up? Either way, I like the notation.
– Programmer2134
Jul 27 at 6:12
In Agda dependent types are written as $(a : A) to B a$. The notations in the post are made up by me based on the one in Agda.
– md2perpe
Jul 27 at 6:25
If we're talking about type theory, the notation $sum_a:AB_a$ is entirely standard, and makes clearer the difference between an indexed family of types and the object the poster is taking about.
– Malice Vidrine
Jul 27 at 17:01
"These notations are not standard in mathematics". Do you mean that they are "sometimes used" but not standard, or do you mean that you've just made them up? Either way, I like the notation.
– Programmer2134
Jul 27 at 6:12
"These notations are not standard in mathematics". Do you mean that they are "sometimes used" but not standard, or do you mean that you've just made them up? Either way, I like the notation.
– Programmer2134
Jul 27 at 6:12
In Agda dependent types are written as $(a : A) to B a$. The notations in the post are made up by me based on the one in Agda.
– md2perpe
Jul 27 at 6:25
In Agda dependent types are written as $(a : A) to B a$. The notations in the post are made up by me based on the one in Agda.
– md2perpe
Jul 27 at 6:25
If we're talking about type theory, the notation $sum_a:AB_a$ is entirely standard, and makes clearer the difference between an indexed family of types and the object the poster is taking about.
– Malice Vidrine
Jul 27 at 17:01
If we're talking about type theory, the notation $sum_a:AB_a$ is entirely standard, and makes clearer the difference between an indexed family of types and the object the poster is taking about.
– Malice Vidrine
Jul 27 at 17:01
add a comment |Â
up vote
0
down vote
This is the particular case, where $A times B$ cannot be used, since the set does not have a product structure. Thus, there is not really a notation since it wouldn't make sense. As such a notation would always imply a product structure.
You can always define
$$C = (a,b) : a in A, b in B_a$$
answered Jul 26 at 14:39
Jonas
284210
But $B_a$ is not well defined
– Holo
Jul 26 at 14:40
This is indeed what I mean. Is there not a more compact , concise way of writing this?
– Programmer2134
Jul 26 at 15:44
add a comment |Â
up vote
0
down vote
This is the particular case, where $A times B$ cannot be used, since the set does not have a product structure. Thus, there is not really a notation since it wouldn't make sense. As such a notation would always imply a product structure.
You can always define
$$C = (a,b) : a in A, b in B_a$$
answered Jul 26 at 14:39
Jonas
284210
But $B_a$ is not well defined
– Holo
Jul 26 at 14:40
This is indeed what I mean. Is there not a more compact , concise way of writing this?
– Programmer2134
Jul 26 at 15:44
add a comment |Â
up vote
0
down vote
up vote
0
down vote
This is the particular case, where $A times B$ cannot be used, since the set does not have a product structure. Thus, there is not really a notation since it wouldn't make sense. As such a notation would always imply a product structure.
You can always define
$$C = (a,b) : a in A, b in B_a$$
answered Jul 26 at 14:39
Jonas
284210
This is the particular case, where $A times B$ cannot be used, since the set does not have a product structure. Thus, there is not really a notation since it wouldn't make sense. As such a notation would always imply a product structure.
You can always define
$$C = (a,b) : a in A, b in B_a$$
answered Jul 26 at 14:39
Jonas
284210
answered Jul 26 at 14:39
Jonas
284210
answered Jul 26 at 14:39
Jonas
284210
answered Jul 26 at 14:39
Jonas
284210
284210
But $B_a$ is not well defined
– Holo
Jul 26 at 14:40
This is indeed what I mean. Is there not a more compact , concise way of writing this?
– Programmer2134
Jul 26 at 15:44
add a comment |Â
But $B_a$ is not well defined
– Holo
Jul 26 at 14:40
This is indeed what I mean. Is there not a more compact , concise way of writing this?
– Programmer2134
Jul 26 at 15:44
But $B_a$ is not well defined
– Holo
Jul 26 at 14:40
But $B_a$ is not well defined
– Holo
Jul 26 at 14:40
This is indeed what I mean. Is there not a more compact , concise way of writing this?
– Programmer2134
Jul 26 at 15:44
This is indeed what I mean. Is there not a more compact , concise way of writing this?
– Programmer2134
Jul 26 at 15:44
add a comment |Â
up vote
0
down vote
Given an indexed family of sets $(B_a)_ain A$, the set $;ain Awedge bin B_a$ is just the disjoint union of the indexed family. Depending on context, you may see this as $$biguplus_ain AB_a$$ or $$coprod_ain AB_a$$ or $$sum_ain AB_a.$$
answered Jul 26 at 16:44
Malice Vidrine
5,32121019
Also noting that the last of these is more often associated with viewing the structure as a collection of pairs than the others, since in dependent type theories the pair-hood of the elements matters. The other notations tend to appear more often without the connotations of pairhood and with more emphasis on "sets gathered in a non-overlapping manner". But this is an informal comment on the notation, and may be skewed by the specific material I'm familiar with.
– Malice Vidrine
Jul 26 at 16:57
add a comment |Â
up vote
0
down vote
Given an indexed family of sets $(B_a)_ain A$, the set $;ain Awedge bin B_a$ is just the disjoint union of the indexed family. Depending on context, you may see this as $$biguplus_ain AB_a$$ or $$coprod_ain AB_a$$ or $$sum_ain AB_a.$$
answered Jul 26 at 16:44
Malice Vidrine
5,32121019
Also noting that the last of these is more often associated with viewing the structure as a collection of pairs than the others, since in dependent type theories the pair-hood of the elements matters. The other notations tend to appear more often without the connotations of pairhood and with more emphasis on "sets gathered in a non-overlapping manner". But this is an informal comment on the notation, and may be skewed by the specific material I'm familiar with.
– Malice Vidrine
Jul 26 at 16:57
add a comment |Â
up vote
0
down vote
up vote
0
down vote
Given an indexed family of sets $(B_a)_ain A$, the set $;ain Awedge bin B_a$ is just the disjoint union of the indexed family. Depending on context, you may see this as $$biguplus_ain AB_a$$ or $$coprod_ain AB_a$$ or $$sum_ain AB_a.$$
answered Jul 26 at 16:44
Malice Vidrine
5,32121019
Given an indexed family of sets $(B_a)_ain A$, the set $;ain Awedge bin B_a$ is just the disjoint union of the indexed family. Depending on context, you may see this as $$biguplus_ain AB_a$$ or $$coprod_ain AB_a$$ or $$sum_ain AB_a.$$
answered Jul 26 at 16:44
Malice Vidrine
5,32121019
answered Jul 26 at 16:44
Malice Vidrine
5,32121019
answered Jul 26 at 16:44
Malice Vidrine
5,32121019
answered Jul 26 at 16:44
Malice Vidrine
5,32121019
5,32121019
Also noting that the last of these is more often associated with viewing the structure as a collection of pairs than the others, since in dependent type theories the pair-hood of the elements matters. The other notations tend to appear more often without the connotations of pairhood and with more emphasis on "sets gathered in a non-overlapping manner". But this is an informal comment on the notation, and may be skewed by the specific material I'm familiar with.
– Malice Vidrine
Jul 26 at 16:57
add a comment |Â
Also noting that the last of these is more often associated with viewing the structure as a collection of pairs than the others, since in dependent type theories the pair-hood of the elements matters. The other notations tend to appear more often without the connotations of pairhood and with more emphasis on "sets gathered in a non-overlapping manner". But this is an informal comment on the notation, and may be skewed by the specific material I'm familiar with.
– Malice Vidrine
Jul 26 at 16:57
Also noting that the last of these is more often associated with viewing the structure as a collection of pairs than the others, since in dependent type theories the pair-hood of the elements matters. The other notations tend to appear more often without the connotations of pairhood and with more emphasis on "sets gathered in a non-overlapping manner". But this is an informal comment on the notation, and may be skewed by the specific material I'm familiar with.
– Malice Vidrine
Jul 26 at 16:57
Also noting that the last of these is more often associated with viewing the structure as a collection of pairs than the others, since in dependent type theories the pair-hood of the elements matters. The other notations tend to appear more often without the connotations of pairhood and with more emphasis on "sets gathered in a non-overlapping manner". But this is an informal comment on the notation, and may be skewed by the specific material I'm familiar with.
– Malice Vidrine
Jul 26 at 16:57
add a comment |Â
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2863404%2fnotation-for-cartesian-product-with-dependent-types%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
I am not sure I am following, from where $b$ in the $(a,b)$?
– Holo
Jul 26 at 13:51
I think this is what is usually called a "multivalued function" or "set-valued function".
– Kusma
Jul 26 at 14:03
@Kusma multivalued function is defined using the 2-tuple $(a,bin Bmid aRb)$ for some well defined $R$ over $Atimes B$, there is a single tuple for each $a$ so it does not the same as OP asking(I think)
– Holo
Jul 26 at 14:08
This is exactly the disjoint union of the $B_a$.
– Malice Vidrine
Jul 26 at 15:56