From 693ced621dfa90b069be1b101ee6c9f741a8fd93 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 2 Mar 2016 16:50:24 +0100
Subject: [PATCH] define functor for function space

---
 theories/base.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 41fb9c5b..575a0671 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -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 {_ _ _ _} _ _ !_ /.
-- 
GitLab