# Commits

committed f4320bf

More work on applicative

# src/Applicative/Functors.v

`   Parameter f : Type -> Type.`
` End FT_TYPE.`
` `
`-Module Type APPLICATIVE.`
`+Module Type APPLICATIVE_RAW(T : FT_TYPE).`
` `
`-  Include FT_TYPE.`
`+  Include T.`
`+`
` `
`   Parameter pure : forall A, A -> f A.`
`   Parameter app : forall A B, f (A -> B) -> f A -> f B.`
`   Parameter first : forall A B, f A -> f B -> f A.`
`   Parameter second : forall A B, f A -> f B -> f B.`
` `
`-  Parameter Identity : forall A (y : A), app (pure (fun x => x)) y = y.`
`-  Parameter Composition :`
`+End APPLICATIVE_RAW.`
`+`
`+Module Type APPLICATIVE(T : FT_TYPE).`
`+`
`+  Module FT.`
`+    Parameter f : (Type -> Type) -> Type.`
`+  End FT.`
`+`
`+  Module Type AA := APPLICATIVE_RAW(FT).`
`+`
`+  Hypothesis Identity : forall A (y : A), app (AA.pure (fun x => x)) y = y.`
`+  Hypothesis Composition :`
`     forall A B C (u : A) (v : B) (w : C) (x : A) (f : A -> B) (g : B -> C),`
`       app (app (pure (fun x -> g (f x)) u) v) w = app u (app v w)`
`   .`
`-  Parameter Homomorphism : forall A B (x : A) (f : A -> B), app (pure f) (pure x) = pure (f x).`
`-  Parameter Interchange : app u (pure y) = app (pure (fun _ -> y) u).`
`+  Hypothesis Homomorphism : forall A B (x : A) (f : A -> B), app (pure f) (pure x) = pure (f x).`
`+  Hypothesis Interchange : app u (pure y) = app (pure (fun _ -> y) u).`
` `
`-End APPLICATIVE.`
`+`
`+`
`+Module Option <: APPLICATIVE.`
`+`
`+  Definition f := option.`
`+`
`+  Definition pure := Some.`
`+`
`+  Definition app {A B} (g : f (A -> B)) (a : f A) : f B :=`
`+    match (g,a) with`
`+      | ((Some g'),(Some a')) => Some (g' a')`
`+      | _ => None end.`
`+`
`+  Definition first {A B} (a : f A) (b : f B) :=`
`+    match (a,b) with`
`+        | (Some a', Some b') => a`
`+        | _ => None end.`
`+`
`+  Definition second {A B} (a : f A) (b : f B) :=`
`+    match (a,b) with`
`+        | (Some a', Some b') => b`
`+        | _ => None end.`
`+`
`+End Option.`