> 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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
