Applicative is Functor

coq-community · Dec 22, 2019 · d97d562 · d97d562
1 parent 8e1713c
commit d97d562
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/theories/Structures/Applicative.v b/theories/Structures/Applicative.v
@@ -1,3 +1,6 @@
+From ExtLib Require Import
+     Functor.
+
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
 Set Universe Polymorphism.
@@ -22,3 +25,13 @@ Section applicative.
   Definition liftA@{d c} {T : Type@{d} -> Type@{c}} {AT:Applicative@{d c} T} {A B : Type@{d}} (f:A -> B) (aT:T A) : T B := pure f <*> aT.
   Definition liftA2@{d c} {T : Type@{d} -> Type@{c}} {AT:Applicative@{d c} T} {A B C : Type@{d}} (f:A -> B -> C) (aT:T A) (bT:T B) : T C := liftA f aT <*> bT.
 End applicative.
+
+Section Instances.
+
+Universe d c.
+Context (T : Type@{d} -> Type@{c}) {AT : Applicative T}.
+
+Global Instance Functor_Applicative@{} : Functor T :=
+{ fmap := @liftA _ _ }.
+
+End Instances.