Commit 693ced62 authored by Ralf Jung's avatar Ralf Jung

define functor for function space

parent 089f7cd8
......@@ -91,6 +91,8 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope.
Notation "p .1" := (fst p) (at level 10, format "p .1").
Notation "p .2" := (snd p) (at level 10, format "p .2").
Definition fun_map {A A' B B'} (f : A' -> A) (g : B -> B')
(h : A -> B) : A' -> B' := g h f.
Definition prod_map {A A' B B'} (f : A A') (g : B B')
(p : A * B) : A' * B' := (f (p.1), g (p.2)).
Arguments prod_map {_ _ _ _} _ _ !_ /.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment