Mixing
Constructive proof of exponential law in a category
Clash Royale CLAN TAG#URR8PPP
up vote
5
down vote
favorite
I'm trying to write a constructive proof of the isomorphism $Z^X times Y equiv (Z^Y)^X$ in a category with exponential objects.
I can construct a map $(Z^Y)^X rightarrow Z^X times Y$, but I'm stuck trying to construct the reverse - $Z^X times Y rightarrow (Z^Y)^X$
Here's my inventory so far:
$$pi_1 : A times B rightarrow A$$
$$pi_2 : A times B rightarrow B$$
$$swap : A times B rightarrow B times A$$
$$assoc : A times (B times C) rightarrow (A times B) times C$$
$$intro(f_1 : A rightarrow B, f_2 : A rightarrow C) : A rightarrow B times C$$
$$apply : Z^Y times Y rightarrow Z$$
$$curry(f : X times Y rightarrow Z) : X rightarrow Z^Y$$
The first map, $(Z^Y)^X rightarrow Z^X times Y$, arises as follows:
$$curry(apply circ intro(apply circ pi_1, pi_2) circ assoc circ intro(pi_2, swap circ pi_2))$$
Any ideas on how to proceed for the second?
If anyone is wondering why, it's for some code I'm writing
ct.category-theory
asked 10 hours ago
lightandlight
1283
New contributor
lightandlight is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
add a comment |Â
up vote
5
down vote
favorite
I'm trying to write a constructive proof of the isomorphism $Z^X times Y equiv (Z^Y)^X$ in a category with exponential objects.
I can construct a map $(Z^Y)^X rightarrow Z^X times Y$, but I'm stuck trying to construct the reverse - $Z^X times Y rightarrow (Z^Y)^X$
Here's my inventory so far:
$$pi_1 : A times B rightarrow A$$
$$pi_2 : A times B rightarrow B$$
$$swap : A times B rightarrow B times A$$
$$assoc : A times (B times C) rightarrow (A times B) times C$$
$$intro(f_1 : A rightarrow B, f_2 : A rightarrow C) : A rightarrow B times C$$
$$apply : Z^Y times Y rightarrow Z$$
$$curry(f : X times Y rightarrow Z) : X rightarrow Z^Y$$
The first map, $(Z^Y)^X rightarrow Z^X times Y$, arises as follows:
$$curry(apply circ intro(apply circ pi_1, pi_2) circ assoc circ intro(pi_2, swap circ pi_2))$$
Any ideas on how to proceed for the second?
If anyone is wondering why, it's for some code I'm writing
ct.category-theory
asked 10 hours ago
lightandlight
1283
New contributor
lightandlight is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
You might want to check out enriched categories. For example: www-lmpa.univ-littoral.fr/~stubbe/PDF/EnrichedCatsKLUWER.pdf . They deal with this kind of stuff. They are also related to arrows from functional programming.
– Gerrit Begher
7 hours ago
4
It's a challenge to prove this non-constructively. I suppose you could start with "Suppose $(Z^Y)^X$ and $Z^X times Y$ are not isomorphic."
– Andrej Bauer
4 hours ago
add a comment |Â
up vote
5
down vote
favorite
up vote
5
down vote
favorite
I'm trying to write a constructive proof of the isomorphism $Z^X times Y equiv (Z^Y)^X$ in a category with exponential objects.
I can construct a map $(Z^Y)^X rightarrow Z^X times Y$, but I'm stuck trying to construct the reverse - $Z^X times Y rightarrow (Z^Y)^X$
Here's my inventory so far:
$$pi_1 : A times B rightarrow A$$
$$pi_2 : A times B rightarrow B$$
$$swap : A times B rightarrow B times A$$
$$assoc : A times (B times C) rightarrow (A times B) times C$$
$$intro(f_1 : A rightarrow B, f_2 : A rightarrow C) : A rightarrow B times C$$
$$apply : Z^Y times Y rightarrow Z$$
$$curry(f : X times Y rightarrow Z) : X rightarrow Z^Y$$
The first map, $(Z^Y)^X rightarrow Z^X times Y$, arises as follows:
$$curry(apply circ intro(apply circ pi_1, pi_2) circ assoc circ intro(pi_2, swap circ pi_2))$$
Any ideas on how to proceed for the second?
If anyone is wondering why, it's for some code I'm writing
ct.category-theory
asked 10 hours ago
lightandlight
1283
New contributor
lightandlight is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
I'm trying to write a constructive proof of the isomorphism $Z^X times Y equiv (Z^Y)^X$ in a category with exponential objects.
I can construct a map $(Z^Y)^X rightarrow Z^X times Y$, but I'm stuck trying to construct the reverse - $Z^X times Y rightarrow (Z^Y)^X$
Here's my inventory so far:
$$pi_1 : A times B rightarrow A$$
$$pi_2 : A times B rightarrow B$$
$$swap : A times B rightarrow B times A$$
$$assoc : A times (B times C) rightarrow (A times B) times C$$
$$intro(f_1 : A rightarrow B, f_2 : A rightarrow C) : A rightarrow B times C$$
$$apply : Z^Y times Y rightarrow Z$$
$$curry(f : X times Y rightarrow Z) : X rightarrow Z^Y$$
The first map, $(Z^Y)^X rightarrow Z^X times Y$, arises as follows:
$$curry(apply circ intro(apply circ pi_1, pi_2) circ assoc circ intro(pi_2, swap circ pi_2))$$
Any ideas on how to proceed for the second?
If anyone is wondering why, it's for some code I'm writing
ct.category-theory
ct.category-theory
asked 10 hours ago
lightandlight
1283
New contributor
lightandlight is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 10 hours ago
lightandlight
1283
New contributor
lightandlight is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 10 hours ago
lightandlight
1283
New contributor
lightandlight is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 10 hours ago
lightandlight
1283
asked 10 hours ago
lightandlight
1283
1283
New contributor
lightandlight is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
lightandlight is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
lightandlight is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
You might want to check out enriched categories. For example: www-lmpa.univ-littoral.fr/~stubbe/PDF/EnrichedCatsKLUWER.pdf . They deal with this kind of stuff. They are also related to arrows from functional programming.
– Gerrit Begher
7 hours ago
4
It's a challenge to prove this non-constructively. I suppose you could start with "Suppose $(Z^Y)^X$ and $Z^X times Y$ are not isomorphic."
– Andrej Bauer
4 hours ago
add a comment |Â
You might want to check out enriched categories. For example: www-lmpa.univ-littoral.fr/~stubbe/PDF/EnrichedCatsKLUWER.pdf . They deal with this kind of stuff. They are also related to arrows from functional programming.
– Gerrit Begher
7 hours ago
4
It's a challenge to prove this non-constructively. I suppose you could start with "Suppose $(Z^Y)^X$ and $Z^X times Y$ are not isomorphic."
– Andrej Bauer
4 hours ago
You might want to check out enriched categories. For example: www-lmpa.univ-littoral.fr/~stubbe/PDF/EnrichedCatsKLUWER.pdf . They deal with this kind of stuff. They are also related to arrows from functional programming.
– Gerrit Begher
7 hours ago
You might want to check out enriched categories. For example: www-lmpa.univ-littoral.fr/~stubbe/PDF/EnrichedCatsKLUWER.pdf . They deal with this kind of stuff. They are also related to arrows from functional programming.
– Gerrit Begher
7 hours ago
4
4
It's a challenge to prove this non-constructively. I suppose you could start with "Suppose $(Z^Y)^X$ and $Z^X times Y$ are not isomorphic."
– Andrej Bauer
4 hours ago
It's a challenge to prove this non-constructively. I suppose you could start with "Suppose $(Z^Y)^X$ and $Z^X times Y$ are not isomorphic."
– Andrej Bauer
4 hours ago
add a comment |Â
3 Answers
3
active
oldest
votes
up vote
6
down vote
accepted
There's a systematic way to to this -- it's an exercise in how to "unpack" the Yoneda lemma. After all, the quickest proof of this isomorphism goes like this:
$Hom(A,(Z^Y)^X) cong Hom(A times X, Z^Y) \
qquadqquadqquadquad cong Hom((A times X) times Y, Z) \
qquadqquadqquadquad cong Hom(A times (Xtimes Y), Z) \
qquadqquadqquadquad cong Hom(A, Z^X times Y)$
Since the isomorphism is natural in $A$, we have $(Z^Y)^X cong Z^X times Y$ by the Yoneda lemma.
The nice thing about this proof is that it's easy to write down without getting drowned in syntax. But it seems you really want access to that hidden syntax. Never fear! Once we've written down the proof in this form, it's actually very easy to "unpack" the Yoneda lemma to get an explicit syntactic representation of this isomorphism: all you have to do is take the natural bijection you've written down and apply it to the identity map.
You've already done one direction. In the other direction, we step through the above sequence of natural isomorphisms in reverse order:
$id: Z^X times Y to Z^X times Y$
$mapsto curry_X times Y(id) : Z^X times Y times (X times Y) to Z$
$mapsto curry_X times Y(id) circ assoc^-1 : (Z^X times Y times X) times Y to Z$
$mapsto curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y times X to Z^Y$
$mapsto curry_X(curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y to (Z^Y)^X$
Note that $apply_X times Y$ is another name for $curry_X times Y(id)$.
answered 3 hours ago
Tim Campion
12.3k349114
That's a great way of doing it. Thanks a bunch. I don't see howcurry id = apply, though.
– lightandlight
1 hour ago
Oh-- I may have said "curry" where I meant "uncurry".
– Tim Campion
1 hour ago
Ah yep,uncurry idisapply
– lightandlight
1 hour ago
add a comment |Â
up vote
2
down vote
Not the full formula (I left out some stuff involving $swap$, $intro$, etc...) but you should be able to derive it from the following sketch wich contains the idea:
Take the map $$apply:Z^Xtimes Ytimes Xtimes Y to Z$$ and apply $curry$ to arrive at $$Z^Xtimes Ytimes Xto Z^Y$$ Then $curry$ again to get $$Z^Xtimes Yto (Z^Y)^X$$
answered 8 hours ago
Gerrit Begher
1,60411224
2
I believe the only thing you need is an inverse to $assoc$: it is then$$curry(curry(applycirc(assoc)^-1))$$(and I believe you cannot do it without this inverse)
– áƒ›áƒÂმუკრჯიბლáƒÂძე
5 hours ago
add a comment |Â
up vote
1
down vote
$$defcurrymathsfcurry,$$
$$defapplymathsfapply,$$
$$defIdmathsfId$$
$$defassocmathsfassoc$$
Recall the
$$textExponential Characterisation: qquadqquad
k = curryf quadequivquad f = apply ∘ (k × Id) $$
and the typings
$$ curry ;:; (X × Y → Z) ;⟶; (X → Z^Y)$$
$$ apply ;:; Z^Y × Y → Z$$
From these, we can find the desired morphism by investigating the types:
beginalign*
& k : Z^X × Y → (Z ^ Y) ^ X
\ ⇠quad & k = curry f ;land; f : Z^X × Y × X → Z ^ Y
\ ⇠quad & f = curry g ;land; g : (Z^X × Y × X) × Y → Z
\ ⇠quad & g = h circ assoc⻹ ;land; h : Z^X × Y × (X × Y) → Z
\ ⇠quad & h = apply
endalign*
Hence, $$k = curry f = curry (curry g) = curry (curry (apply circ assoc⻹))$$
I've avoided the position-switching of $X$ and $Y$ for simplicity; for that case you should be able to come up with
yourExpCurry = curry (curry (apply ∘ ⟨ fst , swap ∘ snd ⟩ ∘ assocr))
Associated code along with a partially complete proof of the inverse laws can be found here: https://github.com/alhassy/RandomProgramming/blob/master/Agda/Exponentials.agda
answered 33 mins ago
Musa Al-hassy
131115
add a comment |Â
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
6
down vote
accepted
There's a systematic way to to this -- it's an exercise in how to "unpack" the Yoneda lemma. After all, the quickest proof of this isomorphism goes like this:
$Hom(A,(Z^Y)^X) cong Hom(A times X, Z^Y) \
qquadqquadqquadquad cong Hom((A times X) times Y, Z) \
qquadqquadqquadquad cong Hom(A times (Xtimes Y), Z) \
qquadqquadqquadquad cong Hom(A, Z^X times Y)$
Since the isomorphism is natural in $A$, we have $(Z^Y)^X cong Z^X times Y$ by the Yoneda lemma.
The nice thing about this proof is that it's easy to write down without getting drowned in syntax. But it seems you really want access to that hidden syntax. Never fear! Once we've written down the proof in this form, it's actually very easy to "unpack" the Yoneda lemma to get an explicit syntactic representation of this isomorphism: all you have to do is take the natural bijection you've written down and apply it to the identity map.
You've already done one direction. In the other direction, we step through the above sequence of natural isomorphisms in reverse order:
$id: Z^X times Y to Z^X times Y$
$mapsto curry_X times Y(id) : Z^X times Y times (X times Y) to Z$
$mapsto curry_X times Y(id) circ assoc^-1 : (Z^X times Y times X) times Y to Z$
$mapsto curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y times X to Z^Y$
$mapsto curry_X(curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y to (Z^Y)^X$
Note that $apply_X times Y$ is another name for $curry_X times Y(id)$.
answered 3 hours ago
Tim Campion
12.3k349114
That's a great way of doing it. Thanks a bunch. I don't see howcurry id = apply, though.
– lightandlight
1 hour ago
Oh-- I may have said "curry" where I meant "uncurry".
– Tim Campion
1 hour ago
Ah yep,uncurry idisapply
– lightandlight
1 hour ago
add a comment |Â
up vote
6
down vote
accepted
There's a systematic way to to this -- it's an exercise in how to "unpack" the Yoneda lemma. After all, the quickest proof of this isomorphism goes like this:
$Hom(A,(Z^Y)^X) cong Hom(A times X, Z^Y) \
qquadqquadqquadquad cong Hom((A times X) times Y, Z) \
qquadqquadqquadquad cong Hom(A times (Xtimes Y), Z) \
qquadqquadqquadquad cong Hom(A, Z^X times Y)$
Since the isomorphism is natural in $A$, we have $(Z^Y)^X cong Z^X times Y$ by the Yoneda lemma.
The nice thing about this proof is that it's easy to write down without getting drowned in syntax. But it seems you really want access to that hidden syntax. Never fear! Once we've written down the proof in this form, it's actually very easy to "unpack" the Yoneda lemma to get an explicit syntactic representation of this isomorphism: all you have to do is take the natural bijection you've written down and apply it to the identity map.
You've already done one direction. In the other direction, we step through the above sequence of natural isomorphisms in reverse order:
$id: Z^X times Y to Z^X times Y$
$mapsto curry_X times Y(id) : Z^X times Y times (X times Y) to Z$
$mapsto curry_X times Y(id) circ assoc^-1 : (Z^X times Y times X) times Y to Z$
$mapsto curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y times X to Z^Y$
$mapsto curry_X(curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y to (Z^Y)^X$
Note that $apply_X times Y$ is another name for $curry_X times Y(id)$.
answered 3 hours ago
Tim Campion
12.3k349114
That's a great way of doing it. Thanks a bunch. I don't see howcurry id = apply, though.
– lightandlight
1 hour ago
Oh-- I may have said "curry" where I meant "uncurry".
– Tim Campion
1 hour ago
Ah yep,uncurry idisapply
– lightandlight
1 hour ago
add a comment |Â
up vote
6
down vote
accepted
up vote
6
down vote
accepted
There's a systematic way to to this -- it's an exercise in how to "unpack" the Yoneda lemma. After all, the quickest proof of this isomorphism goes like this:
$Hom(A,(Z^Y)^X) cong Hom(A times X, Z^Y) \
qquadqquadqquadquad cong Hom((A times X) times Y, Z) \
qquadqquadqquadquad cong Hom(A times (Xtimes Y), Z) \
qquadqquadqquadquad cong Hom(A, Z^X times Y)$
Since the isomorphism is natural in $A$, we have $(Z^Y)^X cong Z^X times Y$ by the Yoneda lemma.
The nice thing about this proof is that it's easy to write down without getting drowned in syntax. But it seems you really want access to that hidden syntax. Never fear! Once we've written down the proof in this form, it's actually very easy to "unpack" the Yoneda lemma to get an explicit syntactic representation of this isomorphism: all you have to do is take the natural bijection you've written down and apply it to the identity map.
You've already done one direction. In the other direction, we step through the above sequence of natural isomorphisms in reverse order:
$id: Z^X times Y to Z^X times Y$
$mapsto curry_X times Y(id) : Z^X times Y times (X times Y) to Z$
$mapsto curry_X times Y(id) circ assoc^-1 : (Z^X times Y times X) times Y to Z$
$mapsto curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y times X to Z^Y$
$mapsto curry_X(curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y to (Z^Y)^X$
Note that $apply_X times Y$ is another name for $curry_X times Y(id)$.
answered 3 hours ago
Tim Campion
12.3k349114
There's a systematic way to to this -- it's an exercise in how to "unpack" the Yoneda lemma. After all, the quickest proof of this isomorphism goes like this:
$Hom(A,(Z^Y)^X) cong Hom(A times X, Z^Y) \
qquadqquadqquadquad cong Hom((A times X) times Y, Z) \
qquadqquadqquadquad cong Hom(A times (Xtimes Y), Z) \
qquadqquadqquadquad cong Hom(A, Z^X times Y)$
Since the isomorphism is natural in $A$, we have $(Z^Y)^X cong Z^X times Y$ by the Yoneda lemma.
The nice thing about this proof is that it's easy to write down without getting drowned in syntax. But it seems you really want access to that hidden syntax. Never fear! Once we've written down the proof in this form, it's actually very easy to "unpack" the Yoneda lemma to get an explicit syntactic representation of this isomorphism: all you have to do is take the natural bijection you've written down and apply it to the identity map.
You've already done one direction. In the other direction, we step through the above sequence of natural isomorphisms in reverse order:
$id: Z^X times Y to Z^X times Y$
$mapsto curry_X times Y(id) : Z^X times Y times (X times Y) to Z$
$mapsto curry_X times Y(id) circ assoc^-1 : (Z^X times Y times X) times Y to Z$
$mapsto curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y times X to Z^Y$
$mapsto curry_X(curry_Y(curry_X times Y(id) circ assoc^-1): Z^X times Y to (Z^Y)^X$
Note that $apply_X times Y$ is another name for $curry_X times Y(id)$.
answered 3 hours ago
Tim Campion
12.3k349114
answered 3 hours ago
Tim Campion
12.3k349114
answered 3 hours ago
Tim Campion
12.3k349114
answered 3 hours ago
Tim Campion
12.3k349114
12.3k349114
That's a great way of doing it. Thanks a bunch. I don't see howcurry id = apply, though.
– lightandlight
1 hour ago
Oh-- I may have said "curry" where I meant "uncurry".
– Tim Campion
1 hour ago
Ah yep,uncurry idisapply
– lightandlight
1 hour ago
add a comment |Â
That's a great way of doing it. Thanks a bunch. I don't see howcurry id = apply, though.
– lightandlight
1 hour ago
Oh-- I may have said "curry" where I meant "uncurry".
– Tim Campion
1 hour ago
Ah yep,uncurry idisapply
– lightandlight
1 hour ago
That's a great way of doing it. Thanks a bunch. I don't see how
curry id = apply, though.– lightandlight
1 hour ago
That's a great way of doing it. Thanks a bunch. I don't see how
curry id = apply, though.– lightandlight
1 hour ago
Oh-- I may have said "curry" where I meant "uncurry".
– Tim Campion
1 hour ago
Oh-- I may have said "curry" where I meant "uncurry".
– Tim Campion
1 hour ago
Ah yep,
uncurry id is apply– lightandlight
1 hour ago
Ah yep,
uncurry id is apply– lightandlight
1 hour ago
add a comment |Â
up vote
2
down vote
Not the full formula (I left out some stuff involving $swap$, $intro$, etc...) but you should be able to derive it from the following sketch wich contains the idea:
Take the map $$apply:Z^Xtimes Ytimes Xtimes Y to Z$$ and apply $curry$ to arrive at $$Z^Xtimes Ytimes Xto Z^Y$$ Then $curry$ again to get $$Z^Xtimes Yto (Z^Y)^X$$
answered 8 hours ago
Gerrit Begher
1,60411224
2
I believe the only thing you need is an inverse to $assoc$: it is then$$curry(curry(applycirc(assoc)^-1))$$(and I believe you cannot do it without this inverse)
– áƒ›áƒÂმუკრჯიბლáƒÂძე
5 hours ago
add a comment |Â
up vote
2
down vote
Not the full formula (I left out some stuff involving $swap$, $intro$, etc...) but you should be able to derive it from the following sketch wich contains the idea:
Take the map $$apply:Z^Xtimes Ytimes Xtimes Y to Z$$ and apply $curry$ to arrive at $$Z^Xtimes Ytimes Xto Z^Y$$ Then $curry$ again to get $$Z^Xtimes Yto (Z^Y)^X$$
answered 8 hours ago
Gerrit Begher
1,60411224
2
I believe the only thing you need is an inverse to $assoc$: it is then$$curry(curry(applycirc(assoc)^-1))$$(and I believe you cannot do it without this inverse)
– áƒ›áƒÂმუკრჯიბლáƒÂძე
5 hours ago
add a comment |Â
up vote
2
down vote
up vote
2
down vote
Not the full formula (I left out some stuff involving $swap$, $intro$, etc...) but you should be able to derive it from the following sketch wich contains the idea:
Take the map $$apply:Z^Xtimes Ytimes Xtimes Y to Z$$ and apply $curry$ to arrive at $$Z^Xtimes Ytimes Xto Z^Y$$ Then $curry$ again to get $$Z^Xtimes Yto (Z^Y)^X$$
answered 8 hours ago
Gerrit Begher
1,60411224
Not the full formula (I left out some stuff involving $swap$, $intro$, etc...) but you should be able to derive it from the following sketch wich contains the idea:
Take the map $$apply:Z^Xtimes Ytimes Xtimes Y to Z$$ and apply $curry$ to arrive at $$Z^Xtimes Ytimes Xto Z^Y$$ Then $curry$ again to get $$Z^Xtimes Yto (Z^Y)^X$$
answered 8 hours ago
Gerrit Begher
1,60411224
edited 7 hours ago
answered 8 hours ago
Gerrit Begher
1,60411224
answered 8 hours ago
Gerrit Begher
1,60411224
answered 8 hours ago
Gerrit Begher
1,60411224
1,60411224
2
I believe the only thing you need is an inverse to $assoc$: it is then$$curry(curry(applycirc(assoc)^-1))$$(and I believe you cannot do it without this inverse)
– áƒ›áƒÂმუკრჯიბლáƒÂძე
5 hours ago
add a comment |Â
2
I believe the only thing you need is an inverse to $assoc$: it is then$$curry(curry(applycirc(assoc)^-1))$$(and I believe you cannot do it without this inverse)
– áƒ›áƒÂმუკრჯიბლáƒÂძე
5 hours ago
2
2
I believe the only thing you need is an inverse to $assoc$: it is then$$curry(curry(applycirc(assoc)^-1))$$(and I believe you cannot do it without this inverse)
– áƒ›áƒÂმუკრჯიბლáƒÂძე
5 hours ago
I believe the only thing you need is an inverse to $assoc$: it is then$$curry(curry(applycirc(assoc)^-1))$$(and I believe you cannot do it without this inverse)
– áƒ›áƒÂმუკრჯიბლáƒÂძე
5 hours ago
add a comment |Â
up vote
1
down vote
$$defcurrymathsfcurry,$$
$$defapplymathsfapply,$$
$$defIdmathsfId$$
$$defassocmathsfassoc$$
Recall the
$$textExponential Characterisation: qquadqquad
k = curryf quadequivquad f = apply ∘ (k × Id) $$
and the typings
$$ curry ;:; (X × Y → Z) ;⟶; (X → Z^Y)$$
$$ apply ;:; Z^Y × Y → Z$$
From these, we can find the desired morphism by investigating the types:
beginalign*
& k : Z^X × Y → (Z ^ Y) ^ X
\ ⇠quad & k = curry f ;land; f : Z^X × Y × X → Z ^ Y
\ ⇠quad & f = curry g ;land; g : (Z^X × Y × X) × Y → Z
\ ⇠quad & g = h circ assoc⻹ ;land; h : Z^X × Y × (X × Y) → Z
\ ⇠quad & h = apply
endalign*
Hence, $$k = curry f = curry (curry g) = curry (curry (apply circ assoc⻹))$$
I've avoided the position-switching of $X$ and $Y$ for simplicity; for that case you should be able to come up with
yourExpCurry = curry (curry (apply ∘ ⟨ fst , swap ∘ snd ⟩ ∘ assocr))
Associated code along with a partially complete proof of the inverse laws can be found here: https://github.com/alhassy/RandomProgramming/blob/master/Agda/Exponentials.agda
answered 33 mins ago
Musa Al-hassy
131115
add a comment |Â
up vote
1
down vote
$$defcurrymathsfcurry,$$
$$defapplymathsfapply,$$
$$defIdmathsfId$$
$$defassocmathsfassoc$$
Recall the
$$textExponential Characterisation: qquadqquad
k = curryf quadequivquad f = apply ∘ (k × Id) $$
and the typings
$$ curry ;:; (X × Y → Z) ;⟶; (X → Z^Y)$$
$$ apply ;:; Z^Y × Y → Z$$
From these, we can find the desired morphism by investigating the types:
beginalign*
& k : Z^X × Y → (Z ^ Y) ^ X
\ ⇠quad & k = curry f ;land; f : Z^X × Y × X → Z ^ Y
\ ⇠quad & f = curry g ;land; g : (Z^X × Y × X) × Y → Z
\ ⇠quad & g = h circ assoc⻹ ;land; h : Z^X × Y × (X × Y) → Z
\ ⇠quad & h = apply
endalign*
Hence, $$k = curry f = curry (curry g) = curry (curry (apply circ assoc⻹))$$
I've avoided the position-switching of $X$ and $Y$ for simplicity; for that case you should be able to come up with
yourExpCurry = curry (curry (apply ∘ ⟨ fst , swap ∘ snd ⟩ ∘ assocr))
Associated code along with a partially complete proof of the inverse laws can be found here: https://github.com/alhassy/RandomProgramming/blob/master/Agda/Exponentials.agda
answered 33 mins ago
Musa Al-hassy
131115
add a comment |Â
up vote
1
down vote
up vote
1
down vote
$$defcurrymathsfcurry,$$
$$defapplymathsfapply,$$
$$defIdmathsfId$$
$$defassocmathsfassoc$$
Recall the
$$textExponential Characterisation: qquadqquad
k = curryf quadequivquad f = apply ∘ (k × Id) $$
and the typings
$$ curry ;:; (X × Y → Z) ;⟶; (X → Z^Y)$$
$$ apply ;:; Z^Y × Y → Z$$
From these, we can find the desired morphism by investigating the types:
beginalign*
& k : Z^X × Y → (Z ^ Y) ^ X
\ ⇠quad & k = curry f ;land; f : Z^X × Y × X → Z ^ Y
\ ⇠quad & f = curry g ;land; g : (Z^X × Y × X) × Y → Z
\ ⇠quad & g = h circ assoc⻹ ;land; h : Z^X × Y × (X × Y) → Z
\ ⇠quad & h = apply
endalign*
Hence, $$k = curry f = curry (curry g) = curry (curry (apply circ assoc⻹))$$
I've avoided the position-switching of $X$ and $Y$ for simplicity; for that case you should be able to come up with
yourExpCurry = curry (curry (apply ∘ ⟨ fst , swap ∘ snd ⟩ ∘ assocr))
Associated code along with a partially complete proof of the inverse laws can be found here: https://github.com/alhassy/RandomProgramming/blob/master/Agda/Exponentials.agda
answered 33 mins ago
Musa Al-hassy
131115
$$defcurrymathsfcurry,$$
$$defapplymathsfapply,$$
$$defIdmathsfId$$
$$defassocmathsfassoc$$
Recall the
$$textExponential Characterisation: qquadqquad
k = curryf quadequivquad f = apply ∘ (k × Id) $$
and the typings
$$ curry ;:; (X × Y → Z) ;⟶; (X → Z^Y)$$
$$ apply ;:; Z^Y × Y → Z$$
From these, we can find the desired morphism by investigating the types:
beginalign*
& k : Z^X × Y → (Z ^ Y) ^ X
\ ⇠quad & k = curry f ;land; f : Z^X × Y × X → Z ^ Y
\ ⇠quad & f = curry g ;land; g : (Z^X × Y × X) × Y → Z
\ ⇠quad & g = h circ assoc⻹ ;land; h : Z^X × Y × (X × Y) → Z
\ ⇠quad & h = apply
endalign*
Hence, $$k = curry f = curry (curry g) = curry (curry (apply circ assoc⻹))$$
I've avoided the position-switching of $X$ and $Y$ for simplicity; for that case you should be able to come up with
yourExpCurry = curry (curry (apply ∘ ⟨ fst , swap ∘ snd ⟩ ∘ assocr))
Associated code along with a partially complete proof of the inverse laws can be found here: https://github.com/alhassy/RandomProgramming/blob/master/Agda/Exponentials.agda
answered 33 mins ago
Musa Al-hassy
131115
answered 33 mins ago
Musa Al-hassy
131115
answered 33 mins ago
Musa Al-hassy
131115
answered 33 mins ago
Musa Al-hassy
131115
131115
add a comment |Â
add a comment |Â
lightandlight is a new contributor. Be nice, and check out our Code of Conduct.
lightandlight is a new contributor. Be nice, and check out our Code of Conduct.
lightandlight is a new contributor. Be nice, and check out our Code of Conduct.
lightandlight is a new contributor. Be nice, and check out our Code of Conduct.
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%2fmathoverflow.net%2fquestions%2f313733%2fconstructive-proof-of-exponential-law-in-a-category%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
You might want to check out enriched categories. For example: www-lmpa.univ-littoral.fr/~stubbe/PDF/EnrichedCatsKLUWER.pdf . They deal with this kind of stuff. They are also related to arrows from functional programming.
– Gerrit Begher
7 hours ago
4
It's a challenge to prove this non-constructively. I suppose you could start with "Suppose $(Z^Y)^X$ and $Z^X times Y$ are not isomorphic."
– Andrej Bauer
4 hours ago