Built with Alectryon, running Coq+SerAPI v8.16.0+0.16.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
From Tealeaves Require Export
Tactics.Prelude
Classes.Functor
Misc.Product
Misc.Strength
Functors.Identity
Functors.Compose.Import Product.Notations.#[local] Generalizable Variablesϕ F G A B C.(** * Applicative Functors *)(**********************************************************************)ClassPure (F: Type -> Type) :=
pure: forall {A}, A -> F A.ClassMult (F: Type -> Type) :=
mult: forall {AB: Type}, F A * F B -> F (A * B).#[local] Notation"x ⊗ y" :=
(mult (x, y)) (at level50, left associativity).ClassApplicative (G: Type -> Type)
`{Map_G: Map G} `{Pure_G: Pure G} `{Mult_G: Mult G} :=
{ app_functor :> Functor G;
app_pure_natural: forall (AB: Type) (f: A -> B) (x: A),
map f (pure x) = pure (f x);
app_mult_natural:
forall (ABCD: Type) (f: A -> C) (g: B -> D) (x: G A) (y: G B),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y);
app_assoc: forall (ABC: Type) (x: G A) (y: G B) (z: G C),
map α ((x ⊗ y) ⊗ z) = x ⊗ (y ⊗ z);
app_unital_l: forall (A: Type) (x: G A),
map left_unitor (pure tt ⊗ x) = x;
app_unital_r: forall (A: Type) (x: G A),
map right_unitor (x ⊗ pure tt) = x;
app_mult_pure: forall (AB: Type) (a: A) (b: B),
pure a ⊗ pure b = pure (a, b);
}.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Natural (@pure G Pure_G)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Natural (@pure G Pure_G)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (AB : Type) (f : A -> B),
map f ∘ pure = pure ∘ map f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (AB : Type) (f : A -> B),
map f ∘ pure = pure ∘ map f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type f: A -> B
map f ∘ pure = pure ∘ map f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type f: A -> B
map f ○ pure = pure ○ map f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type f: A -> B a: A
map f (pure a) = pure (map f a)
nowrewrite app_pure_natural.Qed.(** ** Homomorphisms Between Applicative Functors *)(**********************************************************************)ClassApplicativeMorphism (FG: Type -> Type)
`{Map F} `{Mult F} `{Pure F}
`{Map G} `{Mult G} `{Pure G}
(ϕ: forall {A}, F A -> G A) :=
{ appmor_app_F: Applicative F;
appmor_app_G: Applicative G;
appmor_natural: forall (AB: Type) (f: A -> B) (x: F A),
ϕ (map f x) = map f (ϕ x);
appmor_pure: forall (A: Type) (a: A),
ϕ (pure a) = pure a;
appmor_mult: forall (AB: Type) (x: F A) (y: F B),
ϕ (x ⊗ y) = ϕ x ⊗ ϕ y;
}.Sectionpointfree.Context `{ApplicativeMorphism F G ϕ}.
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A H5: ApplicativeMorphism F G ϕ
forall (AB : Type) (f : A -> B),
ϕ B ∘ map f = map f ∘ ϕ A
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A H5: ApplicativeMorphism F G ϕ
forall (AB : Type) (f : A -> B),
ϕ B ∘ map f = map f ∘ ϕ A
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A H5: ApplicativeMorphism F G ϕ A, B: Type f: A -> B
ϕ B ∘ map f = map f ∘ ϕ A
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A H5: ApplicativeMorphism F G ϕ A, B: Type f: A -> B x: F A
(ϕ B ∘ map f) x = (map f ∘ ϕ A) x
apply appmor_natural.Qed.
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A H5: ApplicativeMorphism F G ϕ
forallA : Type, ϕ A ∘ pure = pure
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A H5: ApplicativeMorphism F G ϕ
forallA : Type, ϕ A ∘ pure = pure
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A H5: ApplicativeMorphism F G ϕ A: Type
ϕ A ∘ pure = pure
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A H5: ApplicativeMorphism F G ϕ A: Type x: A
(ϕ A ∘ pure) x = pure x
apply appmor_pure.Qed.Endpointfree.
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ
Natural ϕ
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ
Natural ϕ
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
Natural ϕ
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
Functor F
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
Functor G
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
forall (AB : Type) (f : A -> B),
map f ∘ ϕ A = ϕ B ∘ map f
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
Functor F
typeclasses eauto.
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
Functor G
typeclasses eauto.
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
forall (AB : Type) (f : A -> B),
map f ∘ ϕ A = ϕ B ∘ map f
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y A, B: Type f: A -> B
map f ∘ ϕ A = ϕ B ∘ map f
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y A, B: Type f: A -> B fa: F A
(map f ∘ ϕ A) fa = (ϕ B ∘ map f) fa
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y A, B: Type f: A -> B fa: F A
map f (ϕ A fa) = ϕ B (map f fa)
F, G: Type -> Type H: Map F H0: Mult F H1: Pure F H2: Map G H3: Mult G H4: Pure G ϕ: forallA : Type, F A -> G A morphism: ApplicativeMorphism F G ϕ appmor_app_F0: Applicative F appmor_app_G0: Applicative G appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F A),
ϕ B (map f x) = map f (ϕ A x) appmor_pure0: forall (A : Type) (a : A),
ϕ A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F A) (y : F B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y A, B: Type f: A -> B fa: F A
map f (ϕ A fa) = map f (ϕ A fa)
reflexivity.Qed.Ltacinfer_applicative_instances :=
match goal with
| H: ApplicativeMorphism ?G1?G2?ϕ |- _ =>
letapp1 := fresh"app1"inassert (app1: Applicative G1) bynowinversion H
end; match goal with
| H: ApplicativeMorphism ?G1?G2?ϕ |- _ =>
letapp2 := fresh"app2"inassert (app2: Applicative G2) bynowinversion H
end.(** *** The identity transformation on any <<F>> is a homomorphism *)(**********************************************************************)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
ApplicativeMorphism F F (@id ○ F)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
forall (ABC : Type) (x : F A) (y : F B) (z : F C),
map α^-1 (x ⊗ (y ⊗ z)) = x ⊗ y ⊗ z
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
forall (ABC : Type) (x : F A) (y : F B) (z : F C),
map α^-1 (x ⊗ (y ⊗ z)) = x ⊗ y ⊗ z
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B, C: Type x: F A y: F B z: F C
map α^-1 (x ⊗ (y ⊗ z)) = x ⊗ y ⊗ z
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B, C: Type x: F A y: F B z: F C
map α^-1 (map α (x ⊗ y ⊗ z)) = x ⊗ y ⊗ z
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B, C: Type x: F A y: F B z: F C
(map α^-1 ∘ map α) (x ⊗ y ⊗ z) = x ⊗ y ⊗ z
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B, C: Type x: F A y: F B z: F C
map (α^-1 ∘ α) (x ⊗ y ⊗ z) = x ⊗ y ⊗ z
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B, C: Type x: F A y: F B z: F C
map id (x ⊗ y ⊗ z) = x ⊗ y ⊗ z
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B, C: Type x: F A y: F B z: F C
id (x ⊗ y ⊗ z) = x ⊗ y ⊗ z
reflexivity.Qed.EndApplicative_corollaries.(** * The Category of Applicative Functors *)(**********************************************************************)(** ** The Identity Applicative Functor *)(**********************************************************************)#[export] InstancePure_I: Pure (funA => A) := @id.#[export] InstanceMult_I: Mult (funA => A) := funAB (p: A * B) => p.#[export, program] InstanceApplicative_I: Applicative (funA => A).(** *** <<pure F>> is a Homomorphism from <<I>> to <<F>> *)(**********************************************************************)Sectionpure_as_applicative_transformation.Context
`{Applicative G}.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (AB : Type) (f : A -> B) (t : A),
pure (map f t) = map f (pure t)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (AB : Type) (f : A -> B) (t : A),
pure (map f t) = map f (pure t)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type f: A -> B t: A
pure (map f t) = map f (pure t)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type f: A -> B t: A
pure (map f t) = pure (f t)
reflexivity.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (A : Type) (a : A), pure (pure a) = pure a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (A : Type) (a : A), pure (pure a) = pure a
reflexivity.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (AB : Type) (a : A) (b : B),
pure (a ⊗ b) = pure a ⊗ pure b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (AB : Type) (a : A) (b : B),
pure (a ⊗ b) = pure a ⊗ pure b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type a: A b: B
pure (a ⊗ b) = pure a ⊗ pure b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type a: A b: B
pure (a, b) = pure a ⊗ pure b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type a: A b: B
pure (a, b) = pure (a, b)
reflexivity.Qed.#[export] InstanceApplicativeMorphism_pure:
ApplicativeMorphism (funA => A) G (@pure G _) :=
{| appmor_natural := pure_appmor_1;
appmor_pure := pure_appmor_2;
appmor_mult := pure_appmor_3;
|}.Endpure_as_applicative_transformation.(** ** Composition of Applicative Functors *)(**********************************************************************)Sectionapplicative_compose.Context
(G2G1: Type -> Type)
`{Applicative G1}
`{Applicative G2}.#[export] InstancePure_compose: Pure (G2 ∘ G1) :=
fun (A: Type) (a: A) => pure (F := G2) (pure (F := G1) a).#[export] InstanceMult_compose: Mult (G2 ∘ G1) :=
fun (AB: Type) (p: G2 (G1 A) * G2 (G1 B)) =>
map (F := G2) (mult (F := G1))
(mult (F := G2) (fst p, snd p)): G2 (G1 (A * B)).
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (AB : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (AB : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type f: A -> B x: A
map f (pure x) = pure (f x)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type f: A -> B x: A
map (map f) (pure (pure x)) = pure (pure (f x))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type f: A -> B x: A
pure (pure (f x)) = pure (pure (f x))
reflexivity.Qed.
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (ABCD : Type) (f : A -> C) (g : B -> D)
(x : G2 (G1 A)) (y : G2 (G1 B)),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (ABCD : Type) (f : A -> C) (g : B -> D)
(x : G2 (G1 A)) (y : G2 (G1 B)),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B)
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B)
map mult (map (map f) x ⊗ map (map g) y) =
map (map (map_tensor f g)) (map mult (x ⊗ y))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B)
map mult (map (map_tensor (map f) (map g)) (x ⊗ y)) =
map (map (map_tensor f g)) (map mult (x ⊗ y))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B)
(map mult ∘ map (map_tensor (map f) (map g))) (x ⊗ y) =
map (map (map_tensor f g)) (map mult (x ⊗ y))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B)
mult ∘ map_tensor (map f) (map g) =
map (map_tensor f g) ∘ mult
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B) fa: G1 A fb: G1 B
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B) fa: G1 A fb: G1 B
mult (map_tensor (map f) (map g) (fa, fb)) =
map (map_tensor f g) (fa ⊗ fb)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C, D: Type f: A -> C g: B -> D x: G2 (G1 A) y: G2 (G1 B) fa: G1 A fb: G1 B
mult (map_tensor (map f) (map g) (fa, fb)) =
map f fa ⊗ map g fb
reflexivity.Qed.
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map α (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α)
(map mult
(fst (map mult (fst (x, y) ⊗ snd (x, y)), z)
⊗ snd (map mult (fst (x, y) ⊗ snd (x, y)), z))) =
map mult
(fst (x, map mult (fst (y, z) ⊗ snd (y, z)))
⊗ snd (x, map mult (fst (y, z) ⊗ snd (y, z))))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α) (map mult (map mult (x ⊗ y) ⊗ z)) =
map mult (x ⊗ map mult (y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α)
(map mult (map (map_tensor mult id) (x ⊗ y ⊗ z))) =
map mult (x ⊗ map mult (y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map_tensor mult id) (x ⊗ y ⊗ z) =
map mult (x ⊗ y) ⊗ z
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map_tensor mult id) (x ⊗ y ⊗ z) =
map mult (x ⊗ y) ⊗ z
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map mult (x ⊗ y) ⊗ map id z = map mult (x ⊗ y) ⊗ z
nowrewrite fun_map_id.
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α)
(map mult (map (map_tensor mult id) (x ⊗ y ⊗ z))) =
map mult (x ⊗ map mult (y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α)
((map mult ∘ map (map_tensor mult id)) (x ⊗ y ⊗ z)) =
map mult (x ⊗ map mult (y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α)
(map (mult ∘ map_tensor mult id) (x ⊗ y ⊗ z)) =
map mult (x ⊗ map mult (y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
(map (map α) ∘ map (mult ∘ map_tensor mult id))
(x ⊗ y ⊗ z) = map mult (x ⊗ map mult (y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α ∘ (mult ∘ map_tensor mult id)) (x ⊗ y ⊗ z) =
map mult (x ⊗ map mult (y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α ∘ (mult ∘ map_tensor mult id)) (x ⊗ y ⊗ z) =
map mult (map (map_tensor id mult) (x ⊗ (y ⊗ z)))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map_tensor id mult) (x ⊗ (y ⊗ z)) =
x ⊗ map mult (y ⊗ z)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map_tensor id mult) (x ⊗ (y ⊗ z)) =
x ⊗ map mult (y ⊗ z)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map id x ⊗ map mult (y ⊗ z) = x ⊗ map mult (y ⊗ z)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
id x ⊗ map mult (y ⊗ z) = x ⊗ map mult (y ⊗ z)
reflexivity.
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α ∘ (mult ∘ map_tensor mult id)) (x ⊗ y ⊗ z) =
map mult (map (map_tensor id mult) (x ⊗ (y ⊗ z)))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α ∘ (mult ∘ map_tensor mult id)) (x ⊗ y ⊗ z) =
(map mult ∘ map (map_tensor id mult)) (x ⊗ (y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α ∘ (mult ∘ map_tensor mult id)) (x ⊗ y ⊗ z) =
map (mult ∘ map_tensor id mult) (x ⊗ (y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α ∘ (mult ∘ map_tensor mult id)) (x ⊗ y ⊗ z) =
map (mult ∘ map_tensor id mult) (map α (x ⊗ y ⊗ z))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α ∘ (mult ∘ map_tensor mult id)) (x ⊗ y ⊗ z) =
(map (mult ∘ map_tensor id mult) ∘ map α) (x ⊗ y ⊗ z)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α ∘ (mult ∘ map_tensor mult id)) (x ⊗ y ⊗ z) =
map (mult ∘ map_tensor id mult ∘ α) (x ⊗ y ⊗ z)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map (map α ∘ (mult ∘ map_tensor mult id)) (x ⊗ y ⊗ z) =
map (mult ∘ map_tensor id mult ∘ α) (x ⊗ y ⊗ z)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C)
map α ∘ (mult ∘ map_tensor mult id) =
mult ∘ map_tensor id mult ∘ α
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C) ga: G1 A gb: G1 B gc: G1 C
(map α ∘ (mult ∘ map_tensor mult id)) (ga, gb, gc) =
(mult ∘ map_tensor id mult ∘ α) (ga, gb, gc)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C) ga: G1 A gb: G1 B gc: G1 C
map α (ga ⊗ gb ⊗ gc) = ga ⊗ (gb ⊗ gc)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B, C: Type x: G2 (G1 A) y: G2 (G1 B) z: G2 (G1 C) ga: G1 A gb: G1 B gc: G1 C
ga ⊗ (gb ⊗ gc) = ga ⊗ (gb ⊗ gc)
reflexivity.Qed.
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (A : Type) (x : G2 (G1 A)),
map left_unitor (pure tt ⊗ x) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (A : Type) (x : G2 (G1 A)),
map left_unitor (pure tt ⊗ x) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map left_unitor (pure tt ⊗ x) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map (map left_unitor)
(map mult
(fst (pure (pure tt), x)
⊗ snd (pure (pure tt), x))) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map (map left_unitor) (map mult (pure (pure tt) ⊗ x)) =
x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
(map (map left_unitor ∘ mult) ∘ map (pair (pure tt)))
x = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map (map left_unitor ∘ mult ∘ pair (pure tt)) x = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map id x = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
id x = x
reflexivity.Qed.
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (A : Type) (x : (G2 ∘ G1) A),
map right_unitor (x ⊗ pure tt) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (A : Type) (x : (G2 ∘ G1) A),
map right_unitor (x ⊗ pure tt) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: (G2 ∘ G1) A
map right_unitor (x ⊗ pure tt) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map right_unitor (x ⊗ pure tt) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map (map right_unitor)
(map mult
(fst (x, pure (pure tt))
⊗ snd (x, pure (pure tt)))) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map (map right_unitor) (map mult (x ⊗ pure (pure tt))) =
x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
(map (map right_unitor) ∘ map mult)
(x ⊗ pure (pure tt)) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map (map right_unitor ∘ mult) (x ⊗ pure (pure tt)) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map (map right_unitor ∘ mult)
(map (funb : G1 A => (b, pure tt)) x) = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
(map (map right_unitor ∘ mult)
∘ map (funb : G1 A => (b, pure tt))) x = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map
(map right_unitor ∘ mult
∘ (funb : G1 A => (b, pure tt))) x = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
map id x = x
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A: Type x: G2 (G1 A)
id x = x
reflexivity.Qed.
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (AB : Type) (a : A) (b : B),
pure a ⊗ pure b = pure (a, b)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2
forall (AB : Type) (a : A) (b : B),
pure a ⊗ pure b = pure (a, b)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B
pure a ⊗ pure b = pure (a, b)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B
map mult
(fst (pure (pure a), pure (pure b))
⊗ snd (pure (pure a), pure (pure b))) =
pure (pure (a, b))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B
map mult (pure (pure a) ⊗ pure (pure b)) =
pure (pure (a, b))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B
forallp : G1 A * G1 B,
map mult (pure p) = pure (mult p)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B square: forallp : G1 A * G1 B,
map mult (pure p) = pure (mult p)
map mult (pure (pure a) ⊗ pure (pure b)) =
pure (pure (a, b))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B
forallp : G1 A * G1 B,
map mult (pure p) = pure (mult p)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B p: G1 A * G1 B
map mult (pure p) = pure (mult p)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B p: G1 A * G1 B
pure (mult p) = pure (mult p)
reflexivity.
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B square: forallp : G1 A * G1 B,
map mult (pure p) = pure (mult p)
map mult (pure (pure a) ⊗ pure (pure b)) =
pure (pure (a, b))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B square: forallp : G1 A * G1 B,
map mult (pure p) = pure (mult p)
map mult (pure (pure a) ⊗ pure (pure b)) =
pure (pure a ⊗ pure b)
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B square: forallp : G1 A * G1 B,
map mult (pure p) = pure (mult p)
map mult (pure (pure a) ⊗ pure (pure b)) =
map mult (pure (pure a, pure b))
G2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 A, B: Type a: A b: B square: forallp : G1 A * G1 B,
map mult (pure p) = pure (mult p)
map mult (pure (pure a) ⊗ pure (pure b)) =
map mult (pure (pure a) ⊗ pure (pure b))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Pure_compose G (funA : Type => A) = @pure G Pure_G
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Pure_compose G (funA : Type => A) = @pure G Pure_G
easy.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Pure_compose (funA : Type => A) G = @pure G Pure_G
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Pure_compose (funA : Type => A) G = @pure G Pure_G
easy.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Mult_compose G (funA : Type => A) = @mult G Mult_G
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Mult_compose G (funA : Type => A) = @mult G Mult_G
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type x: (G ∘ (funA : Type => A)) A y: (G ∘ (funA : Type => A)) B
Mult_compose G (funA : Type => A) A B (x, y) = x ⊗ y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type x: G A y: G B
Mult_compose G (funA : Type => A) A B (x, y) = x ⊗ y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type x: G A y: G B
map mult (fst (x, y) ⊗ snd (x, y)) = x ⊗ y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type x: G A y: G B
id (fst (x, y) ⊗ snd (x, y)) = x ⊗ y
reflexivity.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Mult_compose (funA : Type => A) G = @mult G Mult_G
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
Mult_compose (funA : Type => A) G = @mult G Mult_G
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type x: ((funA : Type => A) ∘ G) A y: ((funA : Type => A) ∘ G) B
Mult_compose (funA : Type => A) G A B (x, y) = x ⊗ y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type x: G A y: G B
Mult_compose (funA : Type => A) G A B (x, y) = x ⊗ y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type x: G A y: G B
map mult (fst (x, y) ⊗ snd (x, y)) = x ⊗ y
reflexivity.Qed.Endapplicative_compose_laws.(** ** Parallel Composition of Applicative Homomorphisms *)(**********************************************************************)Sectionapplicative_compose_laws.
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
ApplicativeMorphism (F1 ∘ F2) (G1 ∘ G2)
(funA : Type => ϕ1 (G2 A) ∘ map (ϕ2 A))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
ApplicativeMorphism (F1 ∘ F2) (G1 ∘ G2)
(funA : Type => ϕ1 (G2 A) ∘ map (ϕ2 A))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y
ApplicativeMorphism (F1 ∘ F2) (G1 ∘ G2)
(funA : Type => ϕ1 (G2 A) ∘ map (ϕ2 A))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y
ApplicativeMorphism (F1 ∘ F2) (G1 ∘ G2)
(funA : Type => ϕ1 (G2 A) ∘ map (ϕ2 A))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y
forall (AB : Type) (f : A -> B) (x : (F1 ∘ F2) A),
(ϕ1 (G2 B) ∘ map (ϕ2 B)) (map f x) =
map f ((ϕ1 (G2 A) ∘ map (ϕ2 A)) x)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y
forall (A : Type) (a : A),
(ϕ1 (G2 A) ∘ map (ϕ2 A)) (pure a) = pure a
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y
forall (AB : Type) (x : (F1 ∘ F2) A)
(y : (F1 ∘ F2) B),
(ϕ1 (G2 (A * B)) ∘ map (ϕ2 (A * B))) (x ⊗ y) =
(ϕ1 (G2 A) ∘ map (ϕ2 A)) x
⊗ (ϕ1 (G2 B) ∘ map (ϕ2 B)) y
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y
forall (AB : Type) (f : A -> B) (x : (F1 ∘ F2) A),
(ϕ1 (G2 B) ∘ map (ϕ2 B)) (map f x) =
map f ((ϕ1 (G2 A) ∘ map (ϕ2 A)) x)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A
(ϕ1 (G2 B) ∘ map (ϕ2 B)) (map f x) =
map f ((ϕ1 (G2 A) ∘ map (ϕ2 A)) x)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A
ϕ1 (G2 B) (map (ϕ2 B) (map (map f) x)) =
map (map f) (ϕ1 (G2 A) (map (ϕ2 A) x))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A
ϕ1 (G2 B) ((map (ϕ2 B) ∘ map (map f)) x) =
map (map f) ((ϕ1 (G2 A) ∘ map (ϕ2 A)) x)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A
ϕ1 (G2 B) (map (ϕ2 B ∘ map f) x) =
map (map f) ((ϕ1 (G2 A) ∘ map (ϕ2 A)) x)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A
forall (AB : Type) (f : A -> B),
ϕ2 B ∘ map f = map f ∘ ϕ2 A
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A appmor_natural1': forall (AB : Type) (f : A -> B),
ϕ2 B ∘ map f = map f ∘ ϕ2 A
ϕ1 (G2 B) (map (ϕ2 B ∘ map f) x) =
map (map f) ((ϕ1 (G2 A) ∘ map (ϕ2 A)) x)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A
forall (AB : Type) (f : A -> B),
ϕ2 B ∘ map f = map f ∘ ϕ2 A
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A A0, B0: Type f0: A0 -> B0
ϕ2 B0 ∘ map f0 = map f0 ∘ ϕ2 A0
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A A0, B0: Type f0: A0 -> B0 f2a: F2 A0
(ϕ2 B0 ∘ map f0) f2a = (map f0 ∘ ϕ2 A0) f2a
apply appmor_natural1.
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A appmor_natural1': forall (AB : Type) (f : A -> B),
ϕ2 B ∘ map f = map f ∘ ϕ2 A
ϕ1 (G2 B) (map (ϕ2 B ∘ map f) x) =
map (map f) ((ϕ1 (G2 A) ∘ map (ϕ2 A)) x)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A appmor_natural1': forall (AB : Type) (f : A -> B),
ϕ2 B ∘ map f = map f ∘ ϕ2 A
ϕ1 (G2 B) (map (map f ∘ ϕ2 A) x) =
map (map f) ((ϕ1 (G2 A) ∘ map (ϕ2 A)) x)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A appmor_natural1': forall (AB : Type) (f : A -> B),
ϕ2 B ∘ map f = map f ∘ ϕ2 A
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A appmor_natural1': forall (AB : Type) (f : A -> B),
ϕ2 B ∘ map f = map f ∘ ϕ2 A
ϕ1 (G2 B) (map (map f) (map (ϕ2 A) x)) =
map (map f) (ϕ1 (G2 A) (map (ϕ2 A) x))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type f: A -> B x: (F1 ∘ F2) A appmor_natural1': forall (AB : Type) (f : A -> B),
ϕ2 B ∘ map f = map f ∘ ϕ2 A
map (map f) (ϕ1 (G2 A) (map (ϕ2 A) x)) =
map (map f) (ϕ1 (G2 A) (map (ϕ2 A) x))
reflexivity.
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y
forall (A : Type) (a : A),
(ϕ1 (G2 A) ∘ map (ϕ2 A)) (pure a) = pure a
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A: Type a: A
(ϕ1 (G2 A) ∘ map (ϕ2 A)) (pure a) = pure a
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A: Type a: A
(ϕ1 (G2 A) ∘ map (ϕ2 A)) (pure (pure a)) =
pure (pure a)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A: Type a: A
ϕ1 (G2 A) (map (ϕ2 A) (pure (pure a))) = pure (pure a)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A: Type a: A
ϕ1 (G2 A) (pure (ϕ2 A (pure a))) = pure (pure a)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A: Type a: A
pure (ϕ2 A (pure a)) = pure (pure a)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A: Type a: A
pure (pure a) = pure (pure a)
reflexivity.
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y
forall (AB : Type) (x : (F1 ∘ F2) A)
(y : (F1 ∘ F2) B),
(ϕ1 (G2 (A * B)) ∘ map (ϕ2 (A * B))) (x ⊗ y) =
(ϕ1 (G2 A) ∘ map (ϕ2 A)) x
⊗ (ϕ1 (G2 B) ∘ map (ϕ2 B)) y
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: (F1 ∘ F2) A y: (F1 ∘ F2) B
(ϕ1 (G2 (A * B)) ∘ map (ϕ2 (A * B))) (x ⊗ y) =
(ϕ1 (G2 A) ∘ map (ϕ2 A)) x
⊗ (ϕ1 (G2 B) ∘ map (ϕ2 B)) y
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: (F1 ∘ F2) A y: (F1 ∘ F2) B
(ϕ1 (G2 (A * B)) ∘ map (ϕ2 (A * B)))
(map mult (fst (x, y) ⊗ snd (x, y))) =
map mult
(fst
((ϕ1 (G2 A) ∘ map (ϕ2 A)) x,
(ϕ1 (G2 B) ∘ map (ϕ2 B)) y)
⊗ snd
((ϕ1 (G2 A) ∘ map (ϕ2 A)) x,
(ϕ1 (G2 B) ∘ map (ϕ2 B)) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B)
ϕ1 (G2 (A * B))
(map (ϕ2 (A * B))
(map mult (fst (x, y) ⊗ snd (x, y)))) =
map mult
(fst
(ϕ1 (G2 A) (map (ϕ2 A) x),
ϕ1 (G2 B) (map (ϕ2 B) y))
⊗ snd
(ϕ1 (G2 A) (map (ϕ2 A) x),
ϕ1 (G2 B) (map (ϕ2 B) y)))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B)
ϕ1 (G2 (A * B)) (map (ϕ2 (A * B)) (map mult (x ⊗ y))) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B)
ϕ1 (G2 (A * B))
((map (ϕ2 (A * B)) ∘ map mult) (x ⊗ y)) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B)
ϕ1 (G2 (A * B)) (map (ϕ2 (A * B) ∘ mult) (x ⊗ y)) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B)
forallAB : Type,
ϕ2 (A * B) ∘ mult = mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
ϕ1 (G2 (A * B)) (map (ϕ2 (A * B) ∘ mult) (x ⊗ y)) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B)
forallAB : Type,
ϕ2 (A * B) ∘ mult = mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) A0, B0: Type
ϕ2 (A0 * B0) ∘ mult =
mult ∘ map_tensor (ϕ2 A0) (ϕ2 B0)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) A0, B0: Type x': F2 A0 y': F2 B0
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) A0, B0: Type x': F2 A0 y': F2 B0
ϕ2 (A0 * B0) (x' ⊗ y') = ϕ2 A0 x' ⊗ ϕ2 B0 y'
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) A0, B0: Type x': F2 A0 y': F2 B0
ϕ2 A0 x' ⊗ ϕ2 B0 y' = ϕ2 A0 x' ⊗ ϕ2 B0 y'
reflexivity.
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
ϕ1 (G2 (A * B)) (map (ϕ2 (A * B) ∘ mult) (x ⊗ y)) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
ϕ1 (G2 (A * B))
(map (mult ∘ map_tensor (ϕ2 A) (ϕ2 B)) (x ⊗ y)) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
map (mult ∘ map_tensor (ϕ2 A) (ϕ2 B))
(ϕ1 (F2 A * F2 B) (x ⊗ y)) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
(map mult ∘ map (map_tensor (ϕ2 A) (ϕ2 B)))
(ϕ1 (F2 A * F2 B) (x ⊗ y)) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
(map mult ∘ map (map_tensor (ϕ2 A) (ϕ2 B)))
(ϕ1 (F2 A) x ⊗ ϕ1 (F2 B) y) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
map mult
(map (map_tensor (ϕ2 A) (ϕ2 B))
(ϕ1 (F2 A) x ⊗ ϕ1 (F2 B) y)) =
map mult
(ϕ1 (G2 A) (map (ϕ2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
(* rhs *)
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
map mult
(map (map_tensor (ϕ2 A) (ϕ2 B))
(ϕ1 (F2 A) x ⊗ ϕ1 (F2 B) y)) =
map mult
(map (ϕ2 A) (ϕ1 (F2 A) x) ⊗ ϕ1 (G2 B) (map (ϕ2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
map mult
(map (map_tensor (ϕ2 A) (ϕ2 B))
(ϕ1 (F2 A) x ⊗ ϕ1 (F2 B) y)) =
map mult
(map (ϕ2 A) (ϕ1 (F2 A) x) ⊗ map (ϕ2 B) (ϕ1 (F2 B) y))
F1, F2, G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: Applicative G2 Map_G1: Map F1 Pure_G1: Pure F1 Mult_G1: Mult F1 H1: Applicative F1 Map_G2: Map F2 Pure_G2: Pure F2 Mult_G2: Mult F2 H2: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2 appmor_app_F0: Applicative F1 appmor_app_G0: Applicative G1 appmor_natural0: forall (AB : Type) (f : A -> B)
(x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x) appmor_pure0: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a appmor_mult0: forall (AB : Type) (x : F1 A)
(y : F1 B),
ϕ1 (A * B) (x ⊗ y) = ϕ1 A x ⊗ ϕ1 B y appmor_app_F1: Applicative F2 appmor_app_G1: Applicative G2 appmor_natural1: forall (AB : Type) (f : A -> B)
(x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x) appmor_pure1: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a appmor_mult1: forall (AB : Type) (x : F2 A)
(y : F2 B),
ϕ2 (A * B) (x ⊗ y) = ϕ2 A x ⊗ ϕ2 B y A, B: Type x: F1 (F2 A) y: F1 (F2 B) appmor_mult1': forallAB : Type,
ϕ2 (A * B) ∘ mult =
mult ∘ map_tensor (ϕ2 A) (ϕ2 B)
map mult
(map (map_tensor (ϕ2 A) (ϕ2 B))
(ϕ1 (F2 A) x ⊗ ϕ1 (F2 B) y)) =
map mult
(map (map_tensor (ϕ2 A) (ϕ2 B))
(ϕ1 (F2 A) x ⊗ ϕ1 (F2 B) y))
reflexivity.Qed.
F1, F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism (F1 ∘ F2) (G1 ∘ F2) (ϕ1 ○ F2)
F1, F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism (F1 ∘ F2) (G1 ∘ F2) (ϕ1 ○ F2)
F1, F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism (F1 ∘ F2) (G1 ∘ F2)
(funA : Type => ϕ1 (F2 A) ∘ map id)
F1, F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
(funA : Type => ϕ1 (F2 A) ∘ map id) = ϕ1 ○ F2
F1, F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism (F1 ∘ F2) (G1 ∘ F2)
(funA : Type => ϕ1 (F2 A) ∘ map id)
apply (ApplicativeMorphism_parallel F1 F2 G1 F2).
F1, F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
(funA : Type => ϕ1 (F2 A) ∘ map id) = ϕ1 ○ F2
F1, F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ1: forallA : Type, F1 A -> G1 A ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1 A: Type
ϕ1 (F2 A) ∘ map id = ϕ1 (F2 A)
nowrewrite (fun_map_id (F := F1)).Qed.
F1, F2, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: Applicative G2 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism0: ApplicativeMorphism F2 G2 ϕ2
F1, F2, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: Applicative G2 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism0: ApplicativeMorphism F2 G2 ϕ2
F1, F2, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: Applicative G2 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 Map_G1: Map F2 Pure_G1: Pure F2 Mult_G1: Mult F2 H1: Applicative F2 ϕ2: forallA : Type, F2 A -> G2 A ApplicativeMorphism0: ApplicativeMorphism F2 G2 ϕ2
ApplicativeMorphism (F1 ∘ F2) (F1 ∘ G2)
(funA : Type => (@id ○ F1) (G2 A) ∘ map (ϕ2 A))
apply (ApplicativeMorphism_parallel F1 F2 F1 G2).Qed.
F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F2 Pure_G0: Pure F2 Mult_G0: Mult F2 H0: Applicative F2 ϕ1: forallA : Type, (funA0 : Type => A0) A -> G1 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G1 ϕ1
ApplicativeMorphism F2 (G1 ∘ F2) (ϕ1 ○ F2)
F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F2 Pure_G0: Pure F2 Mult_G0: Mult F2 H0: Applicative F2 ϕ1: forallA : Type, (funA0 : Type => A0) A -> G1 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G1 ϕ1
ApplicativeMorphism F2 (G1 ∘ F2) (ϕ1 ○ F2)
F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F2 Pure_G0: Pure F2 Mult_G0: Mult F2 H0: Applicative F2 ϕ1: forallA : Type, (funA0 : Type => A0) A -> G1 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G1 ϕ1
ApplicativeMorphism ((funA : Type => A) ∘ F2)
(G1 ∘ F2) (ϕ1 ○ F2)
F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F2 Pure_G0: Pure F2 Mult_G0: Mult F2 H0: Applicative F2 ϕ1: forallA : Type, (funA0 : Type => A0) A -> G1 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G1 ϕ1
ApplicativeMorphism ((funA : Type => A) ∘ F2)
(G1 ∘ F2) (ϕ1 ○ F2)
F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F2 Pure_G0: Pure F2 Mult_G0: Mult F2 H0: Applicative F2 ϕ1: forallA : Type, (funA0 : Type => A0) A -> G1 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G1 ϕ1
ApplicativeMorphism ((funA : Type => A) ∘ F2)
(G1 ∘ F2) (ϕ1 ○ F2)
F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F2 Pure_G0: Pure F2 Mult_G0: Mult F2 H0: Applicative F2 ϕ1: forallA : Type, (funA0 : Type => A0) A -> G1 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G1 ϕ1
ApplicativeMorphism ((funA : Type => A) ∘ F2)
(G1 ∘ F2) (ϕ1 ○ F2)
F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F2 Pure_G0: Pure F2 Mult_G0: Mult F2 H0: Applicative F2 ϕ1: forallA : Type, (funA0 : Type => A0) A -> G1 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G1 ϕ1
ApplicativeMorphism ((funA : Type => A) ∘ F2)
(G1 ∘ F2) (ϕ1 ○ F2)
F2, G1: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: Applicative G1 Map_G0: Map F2 Pure_G0: Pure F2 Mult_G0: Mult F2 H0: Applicative F2 ϕ1: forallA : Type, (funA0 : Type => A0) A -> G1 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G1 ϕ1
ApplicativeMorphism ((funA : Type => A) ∘ F2)
(G1 ∘ F2) (ϕ1 ○ F2)
F1, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: Applicative G2 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 ϕ2: forallA : Type, (funA0 : Type => A0) A -> G2 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G2 ϕ2
ApplicativeMorphism F1 (F1 ∘ G2)
(funA : Type => map (ϕ2 A))
F1, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: Applicative G2 Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: Applicative F1 ϕ2: forallA : Type, (funA0 : Type => A0) A -> G2 A ApplicativeMorphism0: ApplicativeMorphism
(funA : Type => A) G2 ϕ2
ApplicativeMorphism F1 (F1 ∘ G2)
(funA : Type => map (ϕ2 A))
F1, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: @Applicative G2 Map_G Pure_G Mult_G Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: @Applicative F1 Map_G0 Pure_G0 Mult_G0 ϕ2: forallA : Type, (funA0 : Type => A0) A -> G2 A ApplicativeMorphism0: @ApplicativeMorphism
(funA : Type => A) G2 Map_I
Mult_I Pure_I Map_G Mult_G
Pure_G ϕ2
@ApplicativeMorphism F1 (F1 ∘ G2) Map_G0 Mult_G0
Pure_G0 (@Map_compose F1 G2 Map_G Map_G0)
(@Mult_compose F1 G2 Mult_G Map_G0 Mult_G0)
(@Pure_compose F1 G2 Pure_G Pure_G0)
(funA : Type => @map F1 Map_G0 A (G2 A) (ϕ2 A))
F1, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: @Applicative G2 Map_G Pure_G Mult_G Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: @Applicative F1 Map_G0 Pure_G0 Mult_G0 ϕ2: forallA : Type, (funA0 : Type => A0) A -> G2 A ApplicativeMorphism0: @ApplicativeMorphism
(funA : Type => A) G2 Map_I
Mult_I Pure_I Map_G Mult_G
Pure_G ϕ2
@ApplicativeMorphism (F1 ∘ (funA : Type => A))
(F1 ∘ G2) Map_G0 Mult_G0 Pure_G0
(@Map_compose F1 G2 Map_G Map_G0)
(@Mult_compose F1 G2 Mult_G Map_G0 Mult_G0)
(@Pure_compose F1 G2 Pure_G Pure_G0)
(funA : Type => @map F1 Map_G0 A (G2 A) (ϕ2 A))
F1, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: @Applicative G2 Map_G Pure_G Mult_G Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: @Applicative F1 Map_G0 Pure_G0 Mult_G0 ϕ2: forallA : Type, (funA0 : Type => A0) A -> G2 A ApplicativeMorphism0: @ApplicativeMorphism
(funA : Type => A) G2 Map_I
Mult_I Pure_I Map_G Mult_G
Pure_G ϕ2
@ApplicativeMorphism (F1 ∘ (funA : Type => A))
(F1 ∘ G2)
(@Map_compose F1 (funX : Type => X) Map_I Map_G0)
Mult_G0 Pure_G0 (@Map_compose F1 G2 Map_G Map_G0)
(@Mult_compose F1 G2 Mult_G Map_G0 Mult_G0)
(@Pure_compose F1 G2 Pure_G Pure_G0)
(funA : Type => @map F1 Map_G0 A (G2 A) (ϕ2 A))
F1, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: @Applicative G2 Map_G Pure_G Mult_G Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: @Applicative F1 Map_G0 Pure_G0 Mult_G0 ϕ2: forallA : Type, (funA0 : Type => A0) A -> G2 A ApplicativeMorphism0: @ApplicativeMorphism
(funA : Type => A) G2 Map_I
Mult_I Pure_I Map_G Mult_G
Pure_G ϕ2
@ApplicativeMorphism (F1 ∘ (funA : Type => A))
(F1 ∘ G2)
(@Map_compose F1 (funX : Type => X) Map_I Map_G0)
(@mult F1 Mult_G0) Pure_G0
(@Map_compose F1 G2 Map_G Map_G0)
(@Mult_compose F1 G2 Mult_G Map_G0 Mult_G0)
(@Pure_compose F1 G2 Pure_G Pure_G0)
(funA : Type => @map F1 Map_G0 A (G2 A) (ϕ2 A))
F1, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: @Applicative G2 Map_G Pure_G Mult_G Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: @Applicative F1 Map_G0 Pure_G0 Mult_G0 ϕ2: forallA : Type, (funA0 : Type => A0) A -> G2 A ApplicativeMorphism0: @ApplicativeMorphism
(funA : Type => A) G2 Map_I
Mult_I Pure_I Map_G Mult_G
Pure_G ϕ2
@ApplicativeMorphism (F1 ∘ (funA : Type => A))
(F1 ∘ G2)
(@Map_compose F1 (funX : Type => X) Map_I Map_G0)
(@Mult_compose F1 (funA : Type => A) Mult_I Map_G0
Mult_G0) Pure_G0
(@Map_compose F1 G2 Map_G Map_G0)
(@Mult_compose F1 G2 Mult_G Map_G0 Mult_G0)
(@Pure_compose F1 G2 Pure_G Pure_G0)
(funA : Type => @map F1 Map_G0 A (G2 A) (ϕ2 A))
F1, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: @Applicative G2 Map_G Pure_G Mult_G Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: @Applicative F1 Map_G0 Pure_G0 Mult_G0 ϕ2: forallA : Type, (funA0 : Type => A0) A -> G2 A ApplicativeMorphism0: @ApplicativeMorphism
(funA : Type => A) G2 Map_I
Mult_I Pure_I Map_G Mult_G
Pure_G ϕ2
@ApplicativeMorphism (F1 ∘ (funA : Type => A))
(F1 ∘ G2)
(@Map_compose F1 (funX : Type => X) Map_I Map_G0)
(@Mult_compose F1 (funA : Type => A) Mult_I Map_G0
Mult_G0) (@pure F1 Pure_G0)
(@Map_compose F1 G2 Map_G Map_G0)
(@Mult_compose F1 G2 Mult_G Map_G0 Mult_G0)
(@Pure_compose F1 G2 Pure_G Pure_G0)
(funA : Type => @map F1 Map_G0 A (G2 A) (ϕ2 A))
F1, G2: Type -> Type Map_G: Map G2 Pure_G: Pure G2 Mult_G: Mult G2 H: @Applicative G2 Map_G Pure_G Mult_G Map_G0: Map F1 Pure_G0: Pure F1 Mult_G0: Mult F1 H0: @Applicative F1 Map_G0 Pure_G0 Mult_G0 ϕ2: forallA : Type, (funA0 : Type => A0) A -> G2 A ApplicativeMorphism0: @ApplicativeMorphism
(funA : Type => A) G2 Map_I
Mult_I Pure_I Map_G Mult_G
Pure_G ϕ2
@ApplicativeMorphism (F1 ∘ (funA : Type => A))
(F1 ∘ G2)
(@Map_compose F1 (funX : Type => X) Map_I Map_G0)
(@Mult_compose F1 (funA : Type => A) Mult_I Map_G0
Mult_G0)
(@Pure_compose F1 (funA : Type => A) Pure_I Pure_G0)
(@Map_compose F1 G2 Map_G Map_G0)
(@Mult_compose F1 G2 Mult_G Map_G0 Mult_G0)
(@Pure_compose F1 G2 Pure_G Pure_G0)
(funA : Type => @map F1 Map_G0 A (G2 A) (ϕ2 A))
apply (ApplicativeMorphism_parallel_right
F1 (funX => X) G2).Qed.Endapplicative_compose_laws.(** * The "ap" combinator << <⋆> >> *)(**********************************************************************)Definitionap (G: Type -> Type) `{Map G} `{Mult G} {A B: Type}:
G (A -> B) -> G A -> G B
:= funGfGa => map (fun '(f, a) => f a) (Gf ⊗ Ga).#[local] Notation"Gf <⋆> Ga" :=
(ap _ Gf Ga) (at level50, left associativity).SectionApplicativeFunctor_ap.Context
`{Applicative G}.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (AB : Type) (f : A -> B) (t : G A),
@map G Map_G A B f t = @pure G Pure_G (A -> B) f <⋆> t
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (AB : Type) (f : A -> B) (t : G A),
@map G Map_G A B f t = @pure G Pure_G (A -> B) f <⋆> t
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: A -> B t: G A
@map G Map_G A B f t = @pure G Pure_G (A -> B) f <⋆> t
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: A -> B t: G A
@map G Map_G A B f t =
@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
(@pure G Pure_G (A -> B) f ⊗ t)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: A -> B t: G A
@map G Map_G A B f t =
@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
(@strength G Map_G (A -> B) A (f, t))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: A -> B t: G A
@map G Map_G A B f t =
@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
(@map G Map_G A ((A -> B) * A) (@pair (A -> B) A f)
t)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: A -> B t: G A
@map G Map_G A B f t =
(@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
∘ @map G Map_G A ((A -> B) * A) (@pair (A -> B) A f))
t
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: A -> B t: G A
@map G Map_G A B f t =
@map G Map_G A B
((fun '(f, a) => f a) ∘ @pair (A -> B) A f) t
reflexivity.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (G2 : Type -> Type) (H0 : Map G) (H1 : Mult G)
(H2 : Pure G) (H3 : Map G2) (H4 : Mult G2)
(H5 : Pure G2) (ϕ : forallA : Type, G A -> G2 A),
@ApplicativeMorphism G G2 H0 H1 H2 H3 H4 H5 ϕ ->
forall (AB : Type) (x : G (A -> B)) (y : G A),
ϕ B (x <⋆> y) = ϕ (A -> B) x <⋆> ϕ A y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (G2 : Type -> Type) (H0 : Map G) (H1 : Mult G)
(H2 : Pure G) (H3 : Map G2) (H4 : Mult G2)
(H5 : Pure G2) (ϕ : forallA : Type, G A -> G2 A),
@ApplicativeMorphism G G2 H0 H1 H2 H3 H4 H5 ϕ ->
forall (AB : Type) (x : G (A -> B)) (y : G A),
ϕ B (x <⋆> y) = ϕ (A -> B) x <⋆> ϕ A y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G G2: Type -> Type H0: Map G H1: Mult G H2: Pure G H3: Map G2 H4: Mult G2 H5: Pure G2 ϕ: forallA : Type, G A -> G2 A H6: @ApplicativeMorphism G G2 H0 H1 H2 H3 H4 H5 ϕ A, B: Type x: G (A -> B) y: G A
ϕ B (x <⋆> y) = ϕ (A -> B) x <⋆> ϕ A y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G G2: Type -> Type H0: Map G H1: Mult G H2: Pure G H3: Map G2 H4: Mult G2 H5: Pure G2 ϕ: forallA : Type, G A -> G2 A H6: @ApplicativeMorphism G G2 H0 H1 H2 H3 H4 H5 ϕ A, B: Type x: G (A -> B) y: G A
ϕ B
(@map G H0 ((A -> B) * A) B (fun '(f, a) => f a)
(x ⊗ y)) =
@map G2 H3 ((A -> B) * A) B (fun '(f, a) => f a)
(ϕ (A -> B) x ⊗ ϕ A y)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G G2: Type -> Type H0: Map G H1: Mult G H2: Pure G H3: Map G2 H4: Mult G2 H5: Pure G2 ϕ: forallA : Type, G A -> G2 A H6: @ApplicativeMorphism G G2 H0 H1 H2 H3 H4 H5 ϕ A, B: Type x: G (A -> B) y: G A
@map G2 H3 ((A -> B) * A) B (fun '(f, a) => f a)
(ϕ ((A -> B) * A) (x ⊗ y)) =
@map G2 H3 ((A -> B) * A) B (fun '(f, a) => f a)
(ϕ (A -> B) x ⊗ ϕ A y)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G G2: Type -> Type H0: Map G H1: Mult G H2: Pure G H3: Map G2 H4: Mult G2 H5: Pure G2 ϕ: forallA : Type, G A -> G2 A H6: @ApplicativeMorphism G G2 H0 H1 H2 H3 H4 H5 ϕ A, B: Type x: G (A -> B) y: G A
@map G2 H3 ((A -> B) * A) B (fun '(f, a) => f a)
(ϕ (A -> B) x ⊗ ϕ A y) =
@map G2 H3 ((A -> B) * A) B (fun '(f, a) => f a)
(ϕ (A -> B) x ⊗ ϕ A y)
reflexivity.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (A : Type) (t : G A),
@pure G Pure_G (A -> A) (@id A) <⋆> t = t
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (A : Type) (t : G A),
@pure G Pure_G (A -> A) (@id A) <⋆> t = t
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A: Type t: G A
@pure G Pure_G (A -> A) (@id A) <⋆> t = t
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A: Type t: G A
@map G Map_G A A (@id A) t = t
nowrewrite (fun_map_id).Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (AB : Type) (f : A -> B) (a : A),
@pure G Pure_G (A -> B) f <⋆> @pure G Pure_G A a =
@pure G Pure_G B (f a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (AB : Type) (f : A -> B) (a : A),
@pure G Pure_G (A -> B) f <⋆> @pure G Pure_G A a =
@pure G Pure_G B (f a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: A -> B a: A
@pure G Pure_G (A -> B) f <⋆> @pure G Pure_G A a =
@pure G Pure_G B (f a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: A -> B a: A
@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
(@pure G Pure_G (A -> B) f ⊗ @pure G Pure_G A a) =
@pure G Pure_G B (f a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: A -> B a: A
@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
(@pure G Pure_G ((A -> B) * A) (f, a)) =
@pure G Pure_G B (f a)
nowrewrite app_pure_natural.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (AB : Type) (f : G (A -> B)) (a : A),
f <⋆> @pure G Pure_G A a =
@pure G Pure_G ((A -> B) -> B) (@evalAt A B a) <⋆> f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (AB : Type) (f : G (A -> B)) (a : A),
f <⋆> @pure G Pure_G A a =
@pure G Pure_G ((A -> B) -> B) (@evalAt A B a) <⋆> f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: G (A -> B) a: A
f <⋆> @pure G Pure_G A a =
@pure G Pure_G ((A -> B) -> B) (@evalAt A B a) <⋆> f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: G (A -> B) a: A
@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
(f ⊗ @pure G Pure_G A a) =
@map G Map_G (((A -> B) -> B) * (A -> B)) B
(fun '(f, a) => f a)
(@pure G Pure_G ((A -> B) -> B) (@evalAt A B a) ⊗ f)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: G (A -> B) a: A
@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
(@map G Map_G (A -> B) ((A -> B) * A)
(funb : A -> B => (b, a)) f) =
@map G Map_G (((A -> B) -> B) * (A -> B)) B
(fun '(f, a) => f a)
(@strength G Map_G ((A -> B) -> B) (A -> B)
(@evalAt A B a, f))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: G (A -> B) a: A
@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
(@map G Map_G (A -> B) ((A -> B) * A)
(funb : A -> B => (b, a)) f) =
@map G Map_G (((A -> B) -> B) * (A -> B)) B
(fun '(f, a) => f a)
(@map G Map_G (A -> B) (((A -> B) -> B) * (A -> B))
(@pair ((A -> B) -> B) (A -> B) (@evalAt A B a))
f)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B: Type f: G (A -> B) a: A
(@map G Map_G ((A -> B) * A) B (fun '(f, a) => f a)
∘ @map G Map_G (A -> B) ((A -> B) * A)
(funb : A -> B => (b, a))) f =
(@map G Map_G (((A -> B) -> B) * (A -> B)) B
(fun '(f, a) => f a)
∘ @map G Map_G (A -> B) (((A -> B) -> B) * (A -> B))
(@pair ((A -> B) -> B) (A -> B) (@evalAt A B a)))
f
nowdo2rewrite (fun_map_map).Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (ABC : Type) (f : G (B -> C))
(g : G (A -> B)) (a : G A),
@pure G Pure_G ((B -> C) -> (A -> B) -> A -> C)
(@compose A B C) <⋆> f <⋆> g <⋆> a = f <⋆> (g <⋆> a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G
forall (ABC : Type) (f : G (B -> C))
(g : G (A -> B)) (a : G A),
@pure G Pure_G ((B -> C) -> (A -> B) -> A -> C)
(@compose A B C) <⋆> f <⋆> g <⋆> a = f <⋆> (g <⋆> a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@pure G Pure_G ((B -> C) -> (A -> B) -> A -> C)
(@compose A B C) <⋆> f <⋆> g <⋆> a = f <⋆> (g <⋆> a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G ((A -> C) * A) C (fun '(f, a) => f a)
(@map G Map_G (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a)
(@map G Map_G
(((B -> C) -> (A -> B) -> A -> C) * (B -> C))
((A -> B) -> A -> C) (fun '(f, a) => f a)
(@pure G Pure_G
((B -> C) -> (A -> B) -> A -> C)
(@compose A B C) ⊗ f) ⊗ g) ⊗ a) =
@map G Map_G ((B -> C) * B) C (fun '(f, a) => f a)
(f
⊗ @map G Map_G ((A -> B) * A) B
(fun '(f, a) => f a) (g ⊗ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G
(((B -> C) -> (A -> B) -> A -> C) * (B -> C))
((A -> B) -> A -> C) (fun '(f, a) => f a)
(@pure G Pure_G ((B -> C) -> (A -> B) -> A -> C)
(@compose A B C) ⊗ f) ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * B) C (fun '(f, a) => f a)
(f
⊗ @map G Map_G ((A -> B) * A) B
(fun '(f, a) => f a) (g ⊗ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G
(((B -> C) -> (A -> B) -> A -> C) * (B -> C))
((A -> B) -> A -> C) (fun '(f, a) => f a)
(@pure G Pure_G ((B -> C) -> (A -> B) -> A -> C)
(@compose A B C) ⊗ f) ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * ((A -> B) * A)) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a)) (f ⊗ (g ⊗ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G
(((B -> C) -> (A -> B) -> A -> C) * (B -> C))
((A -> B) -> A -> C) (fun '(f, a) => f a)
(@strength G Map_G
((B -> C) -> (A -> B) -> A -> C) (B -> C)
(@compose A B C, f)) ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * ((A -> B) * A)) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a)) (f ⊗ (g ⊗ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G
(((B -> C) -> (A -> B) -> A -> C) * (B -> C))
((A -> B) -> A -> C) (fun '(f, a) => f a)
(@map G Map_G (B -> C)
(((B -> C) -> (A -> B) -> A -> C) * (B -> C))
(@pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) f) ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * ((A -> B) * A)) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a)) (f ⊗ (g ⊗ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
((@map G Map_G
(((B -> C) -> (A -> B) -> A -> C) * (B -> C))
((A -> B) -> A -> C) (fun '(f, a) => f a)
∘ @map G Map_G (B -> C)
(((B -> C) -> (A -> B) -> A -> C) * (B -> C))
(@pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C))) f ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * ((A -> B) * A)) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a)) (f ⊗ (g ⊗ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G (B -> C) ((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) f ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * ((A -> B) * A)) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a)) (f ⊗ (g ⊗ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G (B -> C) ((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) f ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * ((A -> B) * A)) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a))
(@map G Map_G ((B -> C) * (A -> B) * A)
((B -> C) * ((A -> B) * A)) α (f ⊗ g ⊗ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G (B -> C) ((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) f ⊗ g ⊗ a) =
(@map G Map_G ((B -> C) * ((A -> B) * A)) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a))
∘ @map G Map_G ((B -> C) * (A -> B) * A)
((B -> C) * ((A -> B) * A)) α) (f ⊗ g ⊗ a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G (B -> C) ((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) f ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a) ∘ α) (f ⊗ g ⊗ a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G
(((A -> B) -> A -> C) * ((A -> B) * A))
(((A -> B) -> A -> C) * (A -> B) * A) α^-1
(@map G Map_G (B -> C) ((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) f ⊗ (g ⊗ a))) =
@map G Map_G ((B -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a) ∘ α) (f ⊗ g ⊗ a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G ((B -> C) * ((A -> B) * A))
(((A -> B) -> A -> C) * (A -> B) * A)
(α^-1
∘ @map_fst ((A -> B) * A) (B -> C)
((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)))
(f ⊗ (g ⊗ a))) =
@map G Map_G ((B -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a) ∘ α) (f ⊗ g ⊗ a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G ((B -> C) * ((A -> B) * A))
(((A -> B) -> A -> C) * (A -> B) * A)
(α^-1
∘ @map_fst ((A -> B) * A) (B -> C)
((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)))
(@map G Map_G ((B -> C) * (A -> B) * A)
((B -> C) * ((A -> B) * A)) α (f ⊗ g ⊗ a))) =
@map G Map_G ((B -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a) ∘ α) (f ⊗ g ⊗ a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
((@map G Map_G ((B -> C) * ((A -> B) * A))
(((A -> B) -> A -> C) * (A -> B) * A)
(α^-1
∘ @map_fst ((A -> B) * A) (B -> C)
((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)))
∘ @map G Map_G ((B -> C) * (A -> B) * A)
((B -> C) * ((A -> B) * A)) α) (f ⊗ g ⊗ a)) =
@map G Map_G ((B -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a) ∘ α) (f ⊗ g ⊗ a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
(@map G Map_G ((B -> C) * (A -> B) * A)
(((A -> B) -> A -> C) * (A -> B) * A)
(α^-1
∘ @map_fst ((A -> B) * A) (B -> C)
((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) ∘ α)
(f ⊗ g ⊗ a)) =
@map G Map_G ((B -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a) ∘ α) (f ⊗ g ⊗ a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
(@map G Map_G (((A -> B) -> A -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a))
∘ @map G Map_G ((B -> C) * (A -> B) * A)
(((A -> B) -> A -> C) * (A -> B) * A)
(α^-1
∘ @map_fst ((A -> B) * A) (B -> C)
((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) ∘ α))
(f ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a) ∘ α) (f ⊗ g ⊗ a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
@map G Map_G ((B -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a)
∘ (α^-1
∘ @map_fst ((A -> B) * A) (B -> C)
((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) ∘ α))
(f ⊗ g ⊗ a) =
@map G Map_G ((B -> C) * (A -> B) * A) C
((fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a) ∘ α) (f ⊗ g ⊗ a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C: Type f: G (B -> C) g: G (A -> B) a: G A
(fun '(f, a) => f a)
∘ @map_fst A (((A -> B) -> A -> C) * (A -> B))
(A -> C) (fun '(f, a) => f a)
∘ (α^-1
∘ @map_fst ((A -> B) * A) (B -> C)
((A -> B) -> A -> C)
((fun '(f, a) => f a)
∘ @pair ((B -> C) -> (A -> B) -> A -> C)
(B -> C) (@compose A B C)) ∘ α) =
(fun '(f, a) => f a)
∘ @map_snd (B -> C) ((A -> B) * A) B
(fun '(f, a) => f a) ∘ α
now ext [[x y] z].Qed.EndApplicativeFunctor_ap.(** ** Convenience Laws for <<ap>> *)(**********************************************************************)SectionApplicativeFunctor_ap_utility.Context
`{Applicative G}
{A B C D: Type}.(** Fuse <<pure>> into <<map>> *)(*ap5*)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forall (f : A -> B) (g : B -> C) (a : G A),
@pure G Pure_G (B -> C) g <⋆> @map G Map_G A B f a =
@map G Map_G A C (g ∘ f) a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forall (f : A -> B) (g : B -> C) (a : G A),
@pure G Pure_G (B -> C) g <⋆> @map G Map_G A B f a =
@map G Map_G A C (g ∘ f) a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type f: A -> B g: B -> C a: G A
@pure G Pure_G (B -> C) g <⋆> @map G Map_G A B f a =
@map G Map_G A C (g ∘ f) a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type f: A -> B g: B -> C a: G A
@pure G Pure_G (B -> C) g <⋆>
(@pure G Pure_G (A -> B) f <⋆> a) =
@pure G Pure_G (A -> C) (g ∘ f) <⋆> a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type f: A -> B g: B -> C a: G A
@pure G Pure_G ((B -> C) -> (A -> B) -> A -> C)
(@compose A B C) <⋆> @pure G Pure_G (B -> C) g <⋆>
@pure G Pure_G (A -> B) f <⋆> a =
@pure G Pure_G (A -> C) (g ∘ f) <⋆> a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type f: A -> B g: B -> C a: G A
@pure G Pure_G (A -> C) (g ∘ f) <⋆> a =
@pure G Pure_G (A -> C) (g ∘ f) <⋆> a
reflexivity.Qed.(** Push an <<map>> under an <<ap>> *)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forall (f : G (A -> B)) (g : B -> C) (a : G A),
@map G Map_G B C g (f <⋆> a) =
@map G Map_G (A -> B) (A -> C) (@compose A B C g) f <⋆>
a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forall (f : G (A -> B)) (g : B -> C) (a : G A),
@map G Map_G B C g (f <⋆> a) =
@map G Map_G (A -> B) (A -> C) (@compose A B C g) f <⋆>
a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type f: G (A -> B) g: B -> C a: G A
@map G Map_G B C g (f <⋆> a) =
@map G Map_G (A -> B) (A -> C) (@compose A B C g) f <⋆>
a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type f: G (A -> B) g: B -> C a: G A
@pure G Pure_G (B -> C) g <⋆> (f <⋆> a) =
@pure G Pure_G ((A -> B) -> A -> C) (@compose A B C g) <⋆>
f <⋆> a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type f: G (A -> B) g: B -> C a: G A
@pure G Pure_G ((B -> C) -> (A -> B) -> A -> C)
(@compose A B C) <⋆> @pure G Pure_G (B -> C) g <⋆> f <⋆>
a =
@pure G Pure_G ((A -> B) -> A -> C) (@compose A B C g) <⋆>
f <⋆> a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type f: G (A -> B) g: B -> C a: G A
@pure G Pure_G ((A -> B) -> A -> C) (@compose A B C g) <⋆>
f <⋆> a =
@pure G Pure_G ((A -> B) -> A -> C) (@compose A B C g) <⋆>
f <⋆> a
reflexivity.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forallg : B -> C,
@compose (G A) (G B) (G C) (@map G Map_G B C g)
∘ @ap G Map_G Mult_G A B =
@ap G Map_G Mult_G A C
∘ @map G Map_G (A -> B) (A -> C) (@compose A B C g)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forallg : B -> C,
@compose (G A) (G B) (G C) (@map G Map_G B C g)
∘ @ap G Map_G Mult_G A B =
@ap G Map_G Mult_G A C
∘ @map G Map_G (A -> B) (A -> C) (@compose A B C g)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type g: B -> C
@compose (G A) (G B) (G C) (@map G Map_G B C g)
∘ @ap G Map_G Mult_G A B =
@ap G Map_G Mult_G A C
∘ @map G Map_G (A -> B) (A -> C) (@compose A B C g)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type g: B -> C f: G (A -> B) a: G A
(@compose (G A) (G B) (G C) (@map G Map_G B C g)
∘ @ap G Map_G Mult_G A B) f a =
(@ap G Map_G Mult_G A C
∘ @map G Map_G (A -> B) (A -> C) (@compose A B C g))
f a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type g: B -> C f: G (A -> B) a: G A
@map G Map_G B C g (f <⋆> a) =
@map G Map_G (A -> B) (A -> C)
(funf : A -> B => g ○ f) f <⋆> a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type g: B -> C f: G (A -> B) a: G A
@map G Map_G (A -> B) (A -> C) (@compose A B C g) f <⋆>
a =
@map G Map_G (A -> B) (A -> C)
(funf : A -> B => g ○ f) f <⋆> a
reflexivity.Qed.(** Bring an <<map>> from right of an <<ap>> to left *)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forall (ABC : Type) (x : G (A -> B)) (y : G C)
(f : C -> A),
@map G Map_G (A -> B) (C -> B) (@precompose C A B f) x <⋆>
y = x <⋆> @map G Map_G C A f y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forall (ABC : Type) (x : G (A -> B)) (y : G C)
(f : C -> A),
@map G Map_G (A -> B) (C -> B) (@precompose C A B f) x <⋆>
y = x <⋆> @map G Map_G C A f y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D, A0, B0, C0: Type x: G (A0 -> B0) y: G C0 f: C0 -> A0
@map G Map_G (A0 -> B0) (C0 -> B0)
(@precompose C0 A0 B0 f) x <⋆> y =
x <⋆> @map G Map_G C0 A0 f y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D, A0, B0, C0: Type x: G (A0 -> B0) y: G C0 f: C0 -> A0
@pure G Pure_G ((A0 -> B0) -> C0 -> B0)
(@precompose C0 A0 B0 f) <⋆> x <⋆> y =
x <⋆> (@pure G Pure_G (C0 -> A0) f <⋆> y)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D, A0, B0, C0: Type x: G (A0 -> B0) y: G C0 f: C0 -> A0
@pure G Pure_G ((A0 -> B0) -> C0 -> B0)
(@precompose C0 A0 B0 f) <⋆> x <⋆> y =
@pure G Pure_G ((A0 -> B0) -> (C0 -> A0) -> C0 -> B0)
(@compose C0 A0 B0) <⋆> x <⋆>
@pure G Pure_G (C0 -> A0) f <⋆> y
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D, A0, B0, C0: Type x: G (A0 -> B0) y: G C0 f: C0 -> A0
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D, A0, B0, C0: Type x: G (A0 -> B0) y: G C0 f: C0 -> A0
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D, A0, B0, C0: Type x: G (A0 -> B0) y: G C0 f: C0 -> A0
@pure G Pure_G ((A0 -> B0) -> C0 -> B0)
(@precompose C0 A0 B0 f) <⋆> x <⋆> y =
@pure G Pure_G ((A0 -> B0) -> C0 -> B0)
(@evalAt (C0 -> A0) (C0 -> B0) f ∘ @compose C0 A0 B0) <⋆>
x <⋆> y
reflexivity.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forall (a : G A) (b : G B) (f : A -> B -> C),
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@pure G Pure_G (A -> B -> C) f <⋆> a <⋆> b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type
forall (a : G A) (b : G B) (f : A -> B -> C),
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@pure G Pure_G (A -> B -> C) f <⋆> a <⋆> b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@pure G Pure_G (A -> B -> C) f <⋆> a <⋆> b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@map G Map_G ((B -> C) * B) C (fun '(f, a) => f a)
(@map G Map_G ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a)
(@pure G Pure_G (A -> B -> C) f ⊗ a) ⊗ b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@map G Map_G ((B -> C) * B) C (fun '(f, a) => f a)
(@map G Map_G ((A -> B -> C) * A * B) ((B -> C) * B)
(@map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a))
(@pure G Pure_G (A -> B -> C) f ⊗ a ⊗ b))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
(@map G Map_G ((B -> C) * B) C (fun '(f, a) => f a)
∘ @map G Map_G ((A -> B -> C) * A * B) ((B -> C) * B)
(@map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a)))
(@pure G Pure_G (A -> B -> C) f ⊗ a ⊗ b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@map G Map_G ((A -> B -> C) * A * B) C
((fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a))
(@pure G Pure_G (A -> B -> C) f ⊗ a ⊗ b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@map G Map_G ((A -> B -> C) * A * B) C
((fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a))
(@map G Map_G ((A -> B -> C) * (A * B))
((A -> B -> C) * A * B) α^-1
(@pure G Pure_G (A -> B -> C) f ⊗ (a ⊗ b)))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
(@map G Map_G ((A -> B -> C) * A * B) C
((fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a))
∘ @map G Map_G ((A -> B -> C) * (A * B))
((A -> B -> C) * A * B) α^-1)
(@pure G Pure_G (A -> B -> C) f ⊗ (a ⊗ b))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@map G Map_G ((A -> B -> C) * (A * B)) C
((fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a) ∘ α^-1)
(@pure G Pure_G (A -> B -> C) f ⊗ (a ⊗ b))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@map G Map_G ((A -> B -> C) * (A * B)) C
((fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a) ∘ α^-1)
(@strength G Map_G (A -> B -> C) (A * B) (f, a ⊗ b))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@map G Map_G ((A -> B -> C) * (A * B)) C
((fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a) ∘ α^-1)
(@map G Map_G (A * B) ((A -> B -> C) * (A * B))
(@pair (A -> B -> C) (A * B) f) (a ⊗ b))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
(@map G Map_G ((A -> B -> C) * (A * B)) C
((fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a) ∘ α^-1)
∘ @map G Map_G (A * B) ((A -> B -> C) * (A * B))
(@pair (A -> B -> C) (A * B) f)) (a ⊗ b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@map G Map_G (A * B) C (@uncurry A B C f) (a ⊗ b) =
@map G Map_G (A * B) C
((fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a) ∘ α^-1
∘ @pair (A -> B -> C) (A * B) f) (a ⊗ b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C
@uncurry A B C f =
(fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a) ∘ α^-1
∘ @pair (A -> B -> C) (A * B) f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G A, B, C, D: Type a: G A b: G B f: A -> B -> C a': A b': B
@uncurry A B C f (a', b') =
((fun '(f, a) => f a)
∘ @map_fst B ((A -> B -> C) * A) (B -> C)
(fun '(f, a) => f a) ∘ α^-1
∘ @pair (A -> B -> C) (A * B) f) (a', b')
reflexivity.Qed.EndApplicativeFunctor_ap_utility.(** ** Composition of Functors and <<ap>> / << <⋆> >> *)(**********************************************************************)Sectionap_compose.Context
(G1G2: Type -> Type)
`{Applicative G1}
`{Applicative G2}
{A B: Type}.
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type
forall (f : G2 (G1 (A -> B))) (a : G2 (G1 A)),
f <⋆> a =
@pure G2 Pure_G0 (G1 (A -> B) -> G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) <⋆> f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type
forall (f : G2 (G1 (A -> B))) (a : G2 (G1 A)),
f <⋆> a =
@pure G2 Pure_G0 (G1 (A -> B) -> G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) <⋆> f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
f <⋆> a =
@pure G2 Pure_G0 (G1 (A -> B) -> G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) <⋆> f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map (G2 ∘ G1) (@Map_compose G2 G1 Map_G Map_G0)
((A -> B) * A) B (fun '(f, a) => f a) (f ⊗ a) =
@pure G2 Pure_G0 (G1 (A -> B) -> G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) <⋆> f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G2 Map_G0 (G1 ((A -> B) * A)) (G1 B)
(@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a))
(f ⊗ a) =
@pure G2 Pure_G0 (G1 (A -> B) -> G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) <⋆> f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G2 Map_G0 (G1 ((A -> B) * A)) (G1 B)
(@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a))
(@map G2 Map_G0 (G1 (A -> B) * G1 A)
(G1 ((A -> B) * A)) (@mult G1 Mult_G (A -> B) A)
(@fst (G2 (G1 (A -> B))) (G2 (G1 A)) (f, a)
⊗ @snd (G2 (G1 (A -> B))) (G2 (G1 A)) (f, a))) =
@pure G2 Pure_G0 (G1 (A -> B) -> G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) <⋆> f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G2 Map_G0 (G1 ((A -> B) * A)) (G1 B)
(@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a))
(@map G2 Map_G0 (G1 (A -> B) * G1 A)
(G1 ((A -> B) * A)) (@mult G1 Mult_G (A -> B) A)
(f ⊗ a)) =
@pure G2 Pure_G0 (G1 (A -> B) -> G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) <⋆> f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G2 Map_G0 (G1 ((A -> B) * A)) (G1 B)
(@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a))
(@map G2 Map_G0 (G1 (A -> B) * G1 A)
(G1 ((A -> B) * A)) (@mult G1 Mult_G (A -> B) A)
(f ⊗ a)) =
@map G2 Map_G0 (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
(@map G2 Map_G0 (G1 ((A -> B) * A)) (G1 B)
(@map G1 Map_G ((A -> B) * A) B
(fun '(f, a) => f a))
∘ @map G2 Map_G0 (G1 (A -> B) * G1 A)
(G1 ((A -> B) * A)) (@mult G1 Mult_G (A -> B) A))
(f ⊗ a) =
@map G2 Map_G0 (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G2 Map_G0 (G1 (A -> B) * G1 A) (G1 B)
(@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a)
∘ @mult G1 Mult_G (A -> B) A) (f ⊗ a) =
@map G2 Map_G0 (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G2 Map_G0 (G1 (A -> B) * G1 A) (G1 B)
(@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a)
∘ @mult G1 Mult_G (A -> B) A) (f ⊗ a) =
@map G2 Map_G0 ((G1 A -> G1 B) * G1 A) (G1 B)
(fun '(f, a) => f a)
(@map G2 Map_G0 (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) f ⊗ a)
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G2 Map_G0 (G1 (A -> B) * G1 A) (G1 B)
(@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a)
∘ @mult G1 Mult_G (A -> B) A) (f ⊗ a) =
@map G2 Map_G0 ((G1 A -> G1 B) * G1 A) (G1 B)
(fun '(f, a) => f a)
(@map G2 Map_G0 (G1 (A -> B) * G1 A)
((G1 A -> G1 B) * G1 A)
(@map_fst (G1 A) (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B)) (f ⊗ a))
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G2 Map_G0 (G1 (A -> B) * G1 A) (G1 B)
(@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a)
∘ @mult G1 Mult_G (A -> B) A) (f ⊗ a) =
(@map G2 Map_G0 ((G1 A -> G1 B) * G1 A) (G1 B)
(fun '(f, a) => f a)
∘ @map G2 Map_G0 (G1 (A -> B) * G1 A)
((G1 A -> G1 B) * G1 A)
(@map_fst (G1 A) (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B))) (f ⊗ a)
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G2 Map_G0 (G1 (A -> B) * G1 A) (G1 B)
(@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a)
∘ @mult G1 Mult_G (A -> B) A) (f ⊗ a) =
@map G2 Map_G0 (G1 (A -> B) * G1 A) (G1 B)
((fun '(f, a) => f a)
∘ @map_fst (G1 A) (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B)) (f ⊗ a)
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@map G1 Map_G ((A -> B) * A) B (fun '(f, a) => f a)
∘ @mult G1 Mult_G (A -> B) A =
(fun '(f, a) => f a)
∘ @map_fst (G1 A) (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B)
now ext [G1f G1a].Qed.
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type
forall (f : G2 (G1 (A -> B))) (a : G2 (G1 A)),
f <⋆> a =
@map G2 Map_G0 (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type
forall (f : G2 (G1 (A -> B))) (a : G2 (G1 A)),
f <⋆> a =
@map G2 Map_G0 (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
f <⋆> a =
@map G2 Map_G0 (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) f <⋆> a
G1, G2: Type -> Type Map_G: Map G1 Pure_G: Pure G1 Mult_G: Mult G1 H: @Applicative G1 Map_G Pure_G Mult_G Map_G0: Map G2 Pure_G0: Pure G2 Mult_G0: Mult G2 H0: @Applicative G2 Map_G0 Pure_G0 Mult_G0 A, B: Type f: G2 (G1 (A -> B)) a: G2 (G1 A)
@pure G2 Pure_G0 (G1 (A -> B) -> G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) <⋆> f <⋆> a =
@map G2 Map_G0 (G1 (A -> B)) (G1 A -> G1 B)
(@ap G1 Map_G Mult_G A B) f <⋆> a
nowrewrite map_to_ap.Qed.(* Theorem ap_compose3: ap (G2 ∘ G1) (A := A) (B := B) = ap G2 ∘ map G2 (ap G1). Proof. intros. ext f a. rewrite (ap_compose1). now rewrite <- map_to_ap. Qed. Theorem ap_compose_new: forall `{Applicative G1} `{Applicative G2}, forall (A B: Type) (x: G1 (G2 A))(f: A -> B), P (G1 ∘ G2) f <⋆> x = P G1 (ap G2 (P G2 f)) <⋆> x. Proof. intros. rewrite (ap_compose1 G2 G1). unfold_ops @Pure_compose. rewrite ap2. reflexivity. Qed. *)Endap_compose.(** * Monoids as Constant Applicative Functors *)(**********************************************************************)From Tealeaves Require Import
Classes.Monoid.Import Monoid.Notations.Sectionwith_monoid.Context
(G: Type -> Type)
(M: Type)
`{Applicative G}
`{Monoid M}.#[export] InstanceMonoid_op_applicative: Monoid_op (G M) :=
funm1m2 => map (F := G) (uncurry monoid_op) (m1 ⊗ m2).#[export] InstanceMonoid_unit_applicative: Monoid_unit (G M) :=
pure (F := G) Ƶ.
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0
@Monoid (G M) Monoid_op_applicative
Monoid_unit_applicative
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0
@Monoid (G M) Monoid_op_applicative
Monoid_unit_applicative
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0
forallxyz : G M, (x ● y) ● z = x ● (y ● z)
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0
forallx : G M, x ● Ƶ = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0
forallx : G M, Ƶ ● x = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0
forallxyz : G M, (x ● y) ● z = x ● (y ● z)
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
(x ● y) ● z = x ● (y ● z)
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
(x ● y) ● z = x ● (y ● z)
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op)) (x ⊗ y) ⊗ z) =
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(x
⊗ @map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op)) (y ⊗ z))
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(@map G Map_G (M * M * M) (M * M)
(@map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op)))
(x ⊗ y ⊗ z)) =
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(x
⊗ @map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op)) (y ⊗ z))
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
(@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
∘ @map G Map_G (M * M * M) (M * M)
(@map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op))))
(x ⊗ y ⊗ z) =
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(x
⊗ @map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op)) (y ⊗ z))
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@map G Map_G (M * M * M) M
(@uncurry M M M (@monoid_op M op)
∘ @map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op))) (x ⊗ y ⊗ z) =
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(x
⊗ @map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op)) (y ⊗ z))
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@map G Map_G (M * M * M) M
(@uncurry M M M (@monoid_op M op)
∘ @map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op))) (x ⊗ y ⊗ z) =
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(@map G Map_G (M * (M * M)) (M * M)
(@map_snd M (M * M) M
(@uncurry M M M (@monoid_op M op)))
(x ⊗ (y ⊗ z)))
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@map G Map_G (M * M * M) M
(@uncurry M M M (@monoid_op M op)
∘ @map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op))) (x ⊗ y ⊗ z) =
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(@map G Map_G (M * (M * M)) (M * M)
(@map_snd M (M * M) M
(@uncurry M M M (@monoid_op M op)))
(@map G Map_G (M * M * M) (M * (M * M)) α
(x ⊗ y ⊗ z)))
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@map G Map_G (M * M * M) M
(@uncurry M M M (@monoid_op M op)
∘ @map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op))) (x ⊗ y ⊗ z) =
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
((@map G Map_G (M * (M * M)) (M * M)
(@map_snd M (M * M) M
(@uncurry M M M (@monoid_op M op)))
∘ @map G Map_G (M * M * M) (M * (M * M)) α)
(x ⊗ y ⊗ z))
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@map G Map_G (M * M * M) M
(@uncurry M M M (@monoid_op M op)
∘ @map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op))) (x ⊗ y ⊗ z) =
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(@map G Map_G (M * M * M) (M * M)
(@map_snd M (M * M) M
(@uncurry M M M (@monoid_op M op)) ∘ α)
(x ⊗ y ⊗ z))
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@map G Map_G (M * M * M) M
(@uncurry M M M (@monoid_op M op)
∘ @map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op))) (x ⊗ y ⊗ z) =
(@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
∘ @map G Map_G (M * M * M) (M * M)
(@map_snd M (M * M) M
(@uncurry M M M (@monoid_op M op)) ∘ α))
(x ⊗ y ⊗ z)
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@map G Map_G (M * M * M) M
(@uncurry M M M (@monoid_op M op)
∘ @map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op))) (x ⊗ y ⊗ z) =
@map G Map_G (M * M * M) M
(@uncurry M M M (@monoid_op M op)
∘ (@map_snd M (M * M) M
(@uncurry M M M (@monoid_op M op)) ∘ α))
(x ⊗ y ⊗ z)
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M
@uncurry M M M (@monoid_op M op)
∘ @map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op)) =
@uncurry M M M (@monoid_op M op)
∘ (@map_snd M (M * M) M
(@uncurry M M M (@monoid_op M op)) ∘ α)
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M m1, m2, m3: M
(@uncurry M M M (@monoid_op M op)
∘ @map_fst M (M * M) M
(@uncurry M M M (@monoid_op M op))) (m1, m2, m3) =
(@uncurry M M M (@monoid_op M op)
∘ (@map_snd M (M * M) M
(@uncurry M M M (@monoid_op M op)) ∘ α))
(m1, m2, m3)
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M m1, m2, m3: M
(m1 ● m2) ● @id M m3 = @id M m1 ● (m2 ● m3)
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x, y, z: G M m1, m2, m3: M
m1 ● (m2 ● @id M m3) = @id M m1 ● (m2 ● m3)
reflexivity.
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0
forallx : G M, x ● Ƶ = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
x ● Ƶ = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op)) (x ⊗ Ƶ) = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(x ⊗ @pure G Pure_G M Ƶ) = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@pure G Pure_G (M -> M -> M) (@monoid_op M op) <⋆> x <⋆>
@pure G Pure_G M Ƶ = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G M (M -> M) (@monoid_op M op) x <⋆>
@pure G Pure_G M Ƶ = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@pure G Pure_G ((M -> M) -> M) (@evalAt M M Ƶ) <⋆>
@map G Map_G M (M -> M) (@monoid_op M op) x = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@pure G Pure_G ((M -> M) -> M) (funf : M -> M => f Ƶ) <⋆>
@map G Map_G M (M -> M) (@monoid_op M op) x = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G M M
((funf : M -> M => f Ƶ) ∘ @monoid_op M op) x = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G M M
((funf : M -> M => f Ƶ) ∘ @monoid_op M op) x =
@id (G M) x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G M M
((funf : M -> M => f Ƶ) ∘ @monoid_op M op) x =
@map G Map_G M M (@id M) x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
(funf : M -> M => f Ƶ) ∘ @monoid_op M op = @id M
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M m: M
((funf : M -> M => f Ƶ) ∘ @monoid_op M op) m =
@id M m
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M m: M
m ● Ƶ = @id M m
nowrewrite monoid_id_r.
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0
forallx : G M, Ƶ ● x = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
Ƶ ● x = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op)) (Ƶ ⊗ x) = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G (M * M) M
(@uncurry M M M (@monoid_op M op))
(@pure G Pure_G M Ƶ ⊗ x) = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@pure G Pure_G (M -> M -> M) (@monoid_op M op) <⋆>
@pure G Pure_G M Ƶ <⋆> x = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@pure G Pure_G (M -> M) (@monoid_op M op Ƶ) <⋆> x = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G M M (@monoid_op M op Ƶ) x = x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G M M (@monoid_op M op Ƶ) x = @id (G M) x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@map G Map_G M M (@monoid_op M op Ƶ) x =
@map G Map_G M M (@id M) x
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M
@monoid_op M op Ƶ = @id M
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M m: M
Ƶ ● m = @id M m
G: Type -> Type M: Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: @Applicative G Map_G Pure_G Mult_G op: Monoid_op M unit0: Monoid_unit M H0: @Monoid M op unit0 x: G M m: M