[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural
Andrei Popescu
uuomul at yahoo.com
Sun May 11 13:55:50 CEST 2014
> Johannes wrote:
> Theorems about complex numbers are now stated only using Re and Im, the Complex
> constructor is not used anymore. It is possible to use primcorec to defined the behaviour of a complex-valued function.
>> Makarius wrote:
>> That is indeed very nice. Is that a new invention or an old trick that every category theorist knows?
The fact that one can use primcorec to obtain the Re/Im view is simply a consequence of the syntactic sugar for the top
"sum of products" layer of (co)datatypes and the associated convenience for the (co)recursor.
IMO, the proximate genus of this Re/Im species is not codatatype, but functor adjunction.
Consider the functor Duplicate : Set --> Set * Set that sends each set A to the pair (A,A) and similarly each function
f : A -> B to (f,f). Then the product functor _*_ : Set * Set -> Set is its right adjoint,
whereas the sum functor _+_ : Set * Set -> Set is its left adjoint. These mean:
(1) Giving a function from A to B * C is equivalent to giving a morphism in Set * Set from (A,A) to (B,C), i.e., two functions:
one from A to B and one from A to C -- this is the case for Re/Im
(2) Giving a function from A + B to C is equivalent to giving a morphism in Set * Set from (A,B) to C, i.e., two functions:
one from A to C and one from B to C.
Andrei
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140511/8501e17d/attachment.html>
More information about the isabelle-dev
mailing list