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.Classes Require Import
Categorical.Applicative
Categorical.Monad
Kleisli.TraversableFunctor.Import Applicative.Notations.Import TraversableFunctor.Notations.#[local] Generalizable Variablesψ ϕ W F G M A B C D X Y O.#[local] Arguments map F%function_scope {Map}
{A B}%type_scope f%function_scope _.#[local] Arguments pure F%function_scope {Pure}
{A}%type_scope _.#[local] Arguments mult F%function_scope {Mult}
{A B}%type_scope _.(** * The [Batch] Functor *)(**********************************************************************)InductiveBatch (ABC: Type): Type :=
| Done: C -> Batch A B C
| Step: Batch A B (B -> C) -> A -> Batch A B C.#[global] Arguments Done {A B C}%type_scope _.#[global] Arguments Step {A B C}%type_scope _ _.#[local] Arguments Done: clear implicits.#[local] Arguments Step: clear implicits.#[local] Infix"⧆" :=
(Step _ _ _) (at level51, left associativity): tealeaves_scope.#[global] Notation"'BATCH1' B C" :=
(funA => Batch A B C) (at level0, B at level0, C at level0).#[global] Notation"'BATCH2' A C" :=
(funB => Batch A B C) (at level3).(** ** Map Operations *)(**********************************************************************)Fixpointmap_Batch
{AB: Type} (C1C2: Type) (f: C1 -> C2)
(b: Batch A B C1): Batch A B C2 :=
match b with
| Done _ _ _ c =>
Done A B C2 (f c)
| Step _ _ _ rest a =>
Step A B C2 (@map_Batch A B (B -> C1) (B -> C2) (compose f) rest) a
end.#[export] InstanceMap_Batch {AB: Type}:
Map (Batch A B) := @map_Batch A B.Fixpointmapfst_Batch
{BC: Type} (A1A2: Type) (f: A1 -> A2)
(b: Batch A1 B C): Batch A2 B C :=
match b with
| Done _ _ _ c => Done A2 B C c
| Step _ _ _ rest a =>
Step A2 B C (mapfst_Batch A1 A2 f rest) (f a)
end.#[export] InstanceMap_Batch1 {BC: Type}:
Map (BATCH1 B C) := @mapfst_Batch B C.Fixpointmapsnd_Batch
{A: Type} (B1B2: Type) {C: Type}
(f: B1 -> B2) (b: Batch A B2 C): Batch A B1 C :=
match b with
| Done _ _ _ c => Done A B1 C c
| Step _ _ _ rest c =>
Step A B1 C
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f rest)) c
end.(** ** Rewriting Principles *)(**********************************************************************)
A, B, C1, C2: Type f: C1 -> C2 c: C1
map (Batch A B) f (Done A B C1 c) = Done A B C2 (f c)
A, B, C1, C2: Type f: C1 -> C2 c: C1
map (Batch A B) f (Done A B C1 c) = Done A B C2 (f c)
reflexivity.Qed.
A, B, C1, C2: Type f: C1 -> C2 a: A rest: Batch A B (B -> C1)
map (Batch A B) f (rest ⧆ a) =
map (Batch A B) (compose f) rest ⧆ a
A, B, C1, C2: Type f: C1 -> C2 a: A rest: Batch A B (B -> C1)
map (Batch A B) f (rest ⧆ a) =
map (Batch A B) (compose f) rest ⧆ a
reflexivity.Qed.
A1, A2, B, C: Type f: A1 -> A2 c: C
mapfst_Batch A1 A2 f (Done A1 B C c) = Done A2 B C c
A1, A2, B, C: Type f: A1 -> A2 c: C
mapfst_Batch A1 A2 f (Done A1 B C c) = Done A2 B C c
reflexivity.Qed.
A1, A2, B, C: Type f: A1 -> A2 a: A1 b: Batch A1 B (B -> C)
mapfst_Batch A1 A2 f (b ⧆ a) =
mapfst_Batch A1 A2 f b ⧆ f a
A1, A2, B, C: Type f: A1 -> A2 a: A1 b: Batch A1 B (B -> C)
mapfst_Batch A1 A2 f (b ⧆ a) =
mapfst_Batch A1 A2 f b ⧆ f a
reflexivity.Qed.
A, B, B', C: Type f: B' -> B c: C
mapsnd_Batch B' B f (Done A B C c) = Done A B' C c
A, B, B', C: Type f: B' -> B c: C
mapsnd_Batch B' B f (Done A B C c) = Done A B' C c
reflexivity.Qed.
A, B, B', C: Type f: B -> B' a: A b: Batch A B' (B' -> C)
mapsnd_Batch B B' f (b ⧆ a) =
map (Batch A B) (precompose f) (mapsnd_Batch B B' f b)
⧆ a
A, B, B', C: Type f: B -> B' a: A b: Batch A B' (B' -> C)
mapsnd_Batch B B' f (b ⧆ a) =
map (Batch A B) (precompose f) (mapsnd_Batch B B' f b)
⧆ a
reflexivity.Qed.(** ** Functor Laws *)(**********************************************************************)Sectionfunctoriality.(** *** In the <<A>> Argument *)(**********************************************************************)
forallBCA : Type, mapfst_Batch A A id = id
forallBCA : Type, mapfst_Batch A A id = id
B, C, A: Type
mapfst_Batch A A id = id
B, C, A: Type b: Batch A B C
mapfst_Batch A A id b = id b
B, A, C: Type c: C
mapfst_Batch A A id (Done A B C c) = id (Done A B C c)
B, A, C: Type rest: Batch A B (B -> C) a: A IHrest: mapfst_Batch A A id rest = id rest
mapfst_Batch A A id (rest ⧆ a) = id (rest ⧆ a)
B, A, C: Type c: C
mapfst_Batch A A id (Done A B C c) = id (Done A B C c)
reflexivity.
B, A, C: Type rest: Batch A B (B -> C) a: A IHrest: mapfst_Batch A A id rest = id rest
mapfst_Batch A A id (rest ⧆ a) = id (rest ⧆ a)
B, A, C: Type rest: Batch A B (B -> C) a: A IHrest: mapfst_Batch A A id rest = id rest
mapfst_Batch A A id rest ⧆ id a = id (rest ⧆ a)
B, A, C: Type rest: Batch A B (B -> C) a: A IHrest: mapfst_Batch A A id rest = id rest
mapfst_Batch A2 A3 g ∘ mapfst_Batch A1 A2 f =
mapfst_Batch A1 A3 (g ∘ f)
B, C, A1, A2, A3: Type f: A1 -> A2 g: A2 -> A3 b: Batch A1 B C
(mapfst_Batch A2 A3 g ∘ mapfst_Batch A1 A2 f) b =
mapfst_Batch A1 A3 (g ∘ f) b
B, C, A1, A2, A3: Type f: A1 -> A2 g: A2 -> A3 b: Batch A1 B C
mapfst_Batch A2 A3 g (mapfst_Batch A1 A2 f b) =
mapfst_Batch A1 A3 (g ○ f) b
B, A1, A2, A3: Type f: A1 -> A2 g: A2 -> A3 C: Type c: C
mapfst_Batch A2 A3 g
(mapfst_Batch A1 A2 f (Done A1 B C c)) =
mapfst_Batch A1 A3 (g ○ f) (Done A1 B C c)
B, A1, A2, A3: Type f: A1 -> A2 g: A2 -> A3 C: Type rest: Batch A1 B (B -> C) a: A1 IHrest: mapfst_Batch A2 A3 g
(mapfst_Batch A1 A2 f rest) =
mapfst_Batch A1 A3 (g ○ f) rest
mapfst_Batch A2 A3 g (mapfst_Batch A1 A2 f (rest ⧆ a)) =
mapfst_Batch A1 A3 (g ○ f) (rest ⧆ a)
B, A1, A2, A3: Type f: A1 -> A2 g: A2 -> A3 C: Type c: C
mapfst_Batch A2 A3 g
(mapfst_Batch A1 A2 f (Done A1 B C c)) =
mapfst_Batch A1 A3 (g ○ f) (Done A1 B C c)
reflexivity.
B, A1, A2, A3: Type f: A1 -> A2 g: A2 -> A3 C: Type rest: Batch A1 B (B -> C) a: A1 IHrest: mapfst_Batch A2 A3 g
(mapfst_Batch A1 A2 f rest) =
mapfst_Batch A1 A3 (g ○ f) rest
mapfst_Batch A2 A3 g (mapfst_Batch A1 A2 f (rest ⧆ a)) =
mapfst_Batch A1 A3 (g ○ f) (rest ⧆ a)
B, A1, A2, A3: Type f: A1 -> A2 g: A2 -> A3 C: Type rest: Batch A1 B (B -> C) a: A1 IHrest: mapfst_Batch A2 A3 g
(mapfst_Batch A1 A2 f rest) =
mapfst_Batch A1 A3 (g ○ f) rest
mapfst_Batch A2 A3 g (mapfst_Batch A1 A2 f rest)
⧆ g (f a) = mapfst_Batch A1 A3 (g ○ f) rest ⧆ g (f a)
B, A1, A2, A3: Type f: A1 -> A2 g: A2 -> A3 C: Type rest: Batch A1 B (B -> C) a: A1 IHrest: mapfst_Batch A2 A3 g
(mapfst_Batch A1 A2 f rest) =
mapfst_Batch A1 A3 (g ○ f) rest
mapfst_Batch A2 A3 g (mapfst_Batch A1 A2 f rest) =
mapfst_Batch A1 A3 (g ○ f) rest
apply IHrest.Qed.#[export, program] InstanceFunctor_Batch1 {BC: Type}:
Functor (BATCH1 B C) :=
{| fun_map_id := @mapfst_id_Batch B C;
fun_map_map := @mapfst_mapfst_Batch B C;
|}.(** *** In the <<C>> Argument *)(**********************************************************************)
forallABC : Type, map (Batch A B) id = id
forallABC : Type, map (Batch A B) id = id
A, B, C: Type
map (Batch A B) id = id
A, B, C: Type b: Batch A B C
map (Batch A B) id b = id b
A, B, C: Type c: C
map (Batch A B) id (Done A B C c) = id (Done A B C c)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: map (Batch A B) id rest = id rest
map (Batch A B) id (rest ⧆ a) = id (rest ⧆ a)
A, B, C: Type c: C
map (Batch A B) id (Done A B C c) = id (Done A B C c)
reflexivity.
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: map (Batch A B) id rest = id rest
map (Batch A B) id (rest ⧆ a) = id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: map (Batch A B) id rest = id rest
map (Batch A B) (compose id) rest ⧆ a = id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: map (Batch A B) id rest = id rest
compose id = id
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: map (Batch A B) id rest = id rest lemma: compose id = id
map (Batch A B) (compose id) rest ⧆ a = id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: map (Batch A B) id rest = id rest
compose id = id
reflexivity.
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: map (Batch A B) id rest = id rest lemma: compose id = id
map (Batch A B) (compose id) rest ⧆ a = id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: map (Batch A B) id rest = id rest lemma: compose id = id
map (Batch A B) id rest ⧆ a = id (rest ⧆ a)
nowrewrite IHrest.Qed.
forall (ABC1C2C3 : Type) (f : C1 -> C2)
(g : C2 -> C3),
map (Batch A B) g ∘ map (Batch A B) f =
map (Batch A B) (g ∘ f)
forall (ABC1C2C3 : Type) (f : C1 -> C2)
(g : C2 -> C3),
map (Batch A B) g ∘ map (Batch A B) f =
map (Batch A B) (g ∘ f)
A, B, C1, C2, C3: Type f: C1 -> C2 g: C2 -> C3
map (Batch A B) g ∘ map (Batch A B) f =
map (Batch A B) (g ∘ f)
A, B, C1, C2, C3: Type f: C1 -> C2 g: C2 -> C3 b: Batch A B C1
(map (Batch A B) g ∘ map (Batch A B) f) b =
map (Batch A B) (g ∘ f) b
A, B, C1, C2, C3: Type f: C1 -> C2 g: C2 -> C3 b: Batch A B C1
map (Batch A B) g (map (Batch A B) f b) =
map (Batch A B) (g ○ f) b
A, B, C1, C2: Type f: C1 -> C2 b: Batch A B C1
forall (C3 : Type) (g : C2 -> C3),
map (Batch A B) g (map (Batch A B) f b) =
map (Batch A B) (g ○ f) b
A, B, C1: Type b: Batch A B C1
forall (C2 : Type) (f : C1 -> C2) (C3 : Type)
(g : C2 -> C3),
map (Batch A B) g (map (Batch A B) f b) =
map (Batch A B) (g ○ f) b
A, B, C: Type c: C C2: Type f: C -> C2 C3: Type g: C2 -> C3
map (Batch A B) g (map (Batch A B) f (Done A B C c)) =
map (Batch A B) (g ○ f) (Done A B C c)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: forall (C2 : Type) (f : (B -> C) -> C2) (C3 : Type) (g : C2 -> C3),
map (Batch A B) g (map (Batch A B) f b) = map (Batch A B) (g ○ f) b C2: Type f: C -> C2 C3: Type g: C2 -> C3
map (Batch A B) g (map (Batch A B) f (b ⧆ a)) =
map (Batch A B) (g ○ f) (b ⧆ a)
A, B, C: Type c: C C2: Type f: C -> C2 C3: Type g: C2 -> C3
map (Batch A B) g (map (Batch A B) f (Done A B C c)) =
map (Batch A B) (g ○ f) (Done A B C c)
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A IHb: forall (C2 : Type) (f : (B -> C) -> C2) (C3 : Type) (g : C2 -> C3),
map (Batch A B) g (map (Batch A B) f b) = map (Batch A B) (g ○ f) b C2: Type f: C -> C2 C3: Type g: C2 -> C3
map (Batch A B) g (map (Batch A B) f (b ⧆ a)) =
map (Batch A B) (g ○ f) (b ⧆ a)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: forall (C2 : Type) (f : (B -> C) -> C2) (C3 : Type) (g : C2 -> C3),
map (Batch A B) g (map (Batch A B) f b) = map (Batch A B) (g ○ f) b C2: Type f: C -> C2 C3: Type g: C2 -> C3
map (Batch A B) (compose g)
(map (Batch A B) (compose f) b) ⧆ a =
map (Batch A B) (compose (g ○ f)) b ⧆ a
A, B, C: Type b: Batch A B (B -> C) a: A IHb: forall (C2 : Type) (f : (B -> C) -> C2) (C3 : Type) (g : C2 -> C3),
map (Batch A B) g (map (Batch A B) f b) = map (Batch A B) (g ○ f) b C2: Type f: C -> C2 C3: Type g: C2 -> C3
map (Batch A B) (compose g)
(map (Batch A B) (compose f) b) =
map (Batch A B) (compose (g ○ f)) b
A, B, C: Type b: Batch A B (B -> C) a: A C2: Type f: C -> C2 C3: Type g: C2 -> C3 IHb: map (Batch A B) (compose g) (map (Batch A B) (compose f) b) =
map (Batch A B) (compose g ○ compose f) b
map (Batch A B) (compose g)
(map (Batch A B) (compose f) b) =
map (Batch A B) (compose (g ○ f)) b
A, B, C: Type b: Batch A B (B -> C) a: A C2: Type f: C -> C2 C3: Type g: C2 -> C3 IHb: map (Batch A B) (compose g) (map (Batch A B) (compose f) b) =
map (Batch A B) (compose g ○ compose f) b
map (Batch A B) (compose g ○ compose f) b =
map (Batch A B) (compose (g ○ f)) b
reflexivity.Qed.#[export, program] InstanceFunctor_Batch {AB: Type}:
Functor (Batch A B) :=
{| fun_map_id := @map_id_Batch A B;
fun_map_map := @map_map_Batch A B;
|}.(** ** Commuting Independent <<map>>s *)(**********************************************************************)
B, A1, A2: Type f: A1 -> A2 C1, C2: Type g: C1 -> C2 b: Batch A1 B C1
mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f b)
B, A1, A2: Type f: A1 -> A2 C1, C2: Type g: C1 -> C2 b: Batch A1 B C1
mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f b)
B, A1, A2: Type f: A1 -> A2 C1: Type b: Batch A1 B C1
forall (C2 : Type) (g : C1 -> C2),
mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f b)
A1, A2: Type f: A1 -> A2 C1: Type
forall (B : Type) (b : Batch A1 B C1) (C2 : Type)
(g : C1 -> C2),
mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f b)
A1, A2: Type f: A1 -> A2 B, C: Type c: C
forall (C2 : Type) (g : C -> C2),
mapfst_Batch A1 A2 f
(map (Batch A1 B) g (Done A1 B C c)) =
map (Batch A2 B) g
(mapfst_Batch A1 A2 f (Done A1 B C c))
A1, A2: Type f: A1 -> A2 B, C: Type b: Batch A1 B (B -> C) a: A1 IHb: forall (C2 : Type) (g : (B -> C) -> C2),
mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f b)
forall (C2 : Type) (g : C -> C2),
mapfst_Batch A1 A2 f (map (Batch A1 B) g (b ⧆ a)) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f (b ⧆ a))
A1, A2: Type f: A1 -> A2 B, C: Type c: C
forall (C2 : Type) (g : C -> C2),
mapfst_Batch A1 A2 f
(map (Batch A1 B) g (Done A1 B C c)) =
map (Batch A2 B) g
(mapfst_Batch A1 A2 f (Done A1 B C c))
reflexivity.
A1, A2: Type f: A1 -> A2 B, C: Type b: Batch A1 B (B -> C) a: A1 IHb: forall (C2 : Type) (g : (B -> C) -> C2),
mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f b)
forall (C2 : Type) (g : C -> C2),
mapfst_Batch A1 A2 f (map (Batch A1 B) g (b ⧆ a)) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f (b ⧆ a))
A1, A2: Type f: A1 -> A2 B, C: Type b: Batch A1 B (B -> C) a: A1 IHb: forall (C2 : Type) (g : (B -> C) -> C2),
mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f b) C2: Type g: C -> C2
mapfst_Batch A1 A2 f (map (Batch A1 B) g (b ⧆ a)) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f (b ⧆ a))
A1, A2: Type f: A1 -> A2 B, C: Type b: Batch A1 B (B -> C) a: A1 IHb: forall (C2 : Type) (g : (B -> C) -> C2),
mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f b) C2: Type g: C -> C2
mapfst_Batch A1 A2 f (map (Batch A1 B) (compose g) b)
⧆ f a =
map (Batch A2 B) (compose g) (mapfst_Batch A1 A2 f b)
⧆ f a
A1, A2: Type f: A1 -> A2 B, C: Type b: Batch A1 B (B -> C) a: A1 IHb: forall (C2 : Type) (g : (B -> C) -> C2),
mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
map (Batch A2 B) g (mapfst_Batch A1 A2 f b) C2: Type g: C -> C2
mapfst_Batch A1 A2 f (map (Batch A1 B) (compose g) b) =
map (Batch A2 B) (compose g) (mapfst_Batch A1 A2 f b)
A1, A2: Type f: A1 -> A2 B, C: Type b: Batch A1 B (B -> C) a: A1 C2: Type g: C -> C2 IHb: mapfst_Batch A1 A2 f (map (Batch A1 B) (compose g) b) =
map (Batch A2 B) (compose g) (mapfst_Batch A1 A2 f b)
mapfst_Batch A1 A2 f (map (Batch A1 B) (compose g) b) =
map (Batch A2 B) (compose g) (mapfst_Batch A1 A2 f b)
A1, A2: Type f: A1 -> A2 B, C: Type b: Batch A1 B (B -> C) a: A1 C2: Type g: C -> C2 IHb: mapfst_Batch A1 A2 f (map (Batch A1 B) (compose g) b) =
map (Batch A2 B) (compose g) (mapfst_Batch A1 A2 f b)
map (Batch A2 B) (compose g) (mapfst_Batch A1 A2 f b) =
map (Batch A2 B) (compose g) (mapfst_Batch A1 A2 f b)
reflexivity.Qed.
A, B1, B2: Type f: B1 -> B2 C1, C2: Type g: C1 -> C2 b: Batch A B2 C1
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b)
A, B1, B2: Type f: B1 -> B2 C1, C2: Type g: C1 -> C2 b: Batch A B2 C1
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b)
A, B1, B2: Type f: B1 -> B2 C1: Type b: Batch A B2 C1
forall (C2 : Type) (g : C1 -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b)
A, B1, B2: Type f: B1 -> B2 C: Type c: C
forall (C2 : Type) (g : C -> C2),
mapsnd_Batch B1 B2 f
(map (Batch A B2) g (Done A B2 C c)) =
map (Batch A B1) g
(mapsnd_Batch B1 B2 f (Done A B2 C c))
A, B1, B2: Type f: B1 -> B2 C: Type b: Batch A B2 (B2 -> C) a: A IHb: forall (C2 : Type) (g : (B2 -> C) -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b)
forall (C2 : Type) (g : C -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g (b ⧆ a)) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f (b ⧆ a))
A, B1, B2: Type f: B1 -> B2 C: Type c: C
forall (C2 : Type) (g : C -> C2),
mapsnd_Batch B1 B2 f
(map (Batch A B2) g (Done A B2 C c)) =
map (Batch A B1) g
(mapsnd_Batch B1 B2 f (Done A B2 C c))
reflexivity.
A, B1, B2: Type f: B1 -> B2 C: Type b: Batch A B2 (B2 -> C) a: A IHb: forall (C2 : Type) (g : (B2 -> C) -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b)
forall (C2 : Type) (g : C -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g (b ⧆ a)) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f (b ⧆ a))
A, B1, B2: Type f: B1 -> B2 C: Type b: Batch A B2 (B2 -> C) a: A IHb: forall (C2 : Type) (g : (B2 -> C) -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b) C2: Type g: C -> C2
mapsnd_Batch B1 B2 f (map (Batch A B2) g (b ⧆ a)) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f (b ⧆ a))
A, B1, B2: Type f: B1 -> B2 C: Type b: Batch A B2 (B2 -> C) a: A IHb: forall (C2 : Type) (g : (B2 -> C) -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b) C2: Type g: C -> C2
map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f
(map (Batch A B2) (compose g) b)) ⧆ a =
map (Batch A B1) (compose g)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f b)) ⧆ a
A, B1, B2: Type f: B1 -> B2 C: Type b: Batch A B2 (B2 -> C) a: A IHb: forall (C2 : Type) (g : (B2 -> C) -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b) C2: Type g: C -> C2
map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f
(map (Batch A B2) (compose g) b)) =
map (Batch A B1) (compose g)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f b))
A, B1, B2: Type f: B1 -> B2 C: Type b: Batch A B2 (B2 -> C) a: A IHb: forall (C2 : Type) (g : (B2 -> C) -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b) C2: Type g: C -> C2
map (Batch A B1) (precompose f)
(map (Batch A B1) (compose g)
(mapsnd_Batch B1 B2 f b)) =
map (Batch A B1) (compose g)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f b))
A, B1, B2: Type f: B1 -> B2 C: Type b: Batch A B2 (B2 -> C) a: A IHb: forall (C2 : Type) (g : (B2 -> C) -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b) C2: Type g: C -> C2
(map (Batch A B1) (precompose f)
∘ map (Batch A B1) (compose g))
(mapsnd_Batch B1 B2 f b) =
(map (Batch A B1) (compose g)
∘ map (Batch A B1) (precompose f))
(mapsnd_Batch B1 B2 f b)
A, B1, B2: Type f: B1 -> B2 C: Type b: Batch A B2 (B2 -> C) a: A IHb: forall (C2 : Type) (g : (B2 -> C) -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b) C2: Type g: C -> C2
map (Batch A B1) (precompose f ∘ compose g)
(mapsnd_Batch B1 B2 f b) =
map (Batch A B1) (compose g ∘ precompose f)
(mapsnd_Batch B1 B2 f b)
A, B1, B2: Type f: B1 -> B2 C: Type b: Batch A B2 (B2 -> C) a: A IHb: forall (C2 : Type) (g : (B2 -> C) -> C2),
mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
map (Batch A B1) g (mapsnd_Batch B1 B2 f b) C2: Type g: C -> C2
mapsnd_Batch B1 B2 f
(map (Batch A B2) (precompose f ∘ compose g) b) =
mapsnd_Batch B1 B2 f
(map (Batch A B2) (compose g ∘ precompose f) b)
reflexivity.Qed.
forall (CA1A2 : Type) (f : A1 -> A2) (B1B2 : Type)
(g : B1 -> B2) (b : Batch A1 B2 C),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b)
forall (CA1A2 : Type) (f : A1 -> A2) (B1B2 : Type)
(g : B1 -> B2) (b : Batch A1 B2 C),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b)
C, A1, A2: Type f: A1 -> A2 B1, B2: Type g: B1 -> B2 b: Batch A1 B2 C
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b)
C, A1, A2, B1, B2: Type g: B1 -> B2 b: Batch A1 B2 C
forallf : A1 -> A2,
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b)
C, A1, A2, B1, B2: Type b: Batch A1 B2 C
forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b)
A1, A2, B1, B2, C: Type c: C
forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f
(mapsnd_Batch B1 B2 g (Done A1 B2 C c)) =
mapsnd_Batch B1 B2 g
(mapfst_Batch A1 A2 f (Done A1 B2 C c))
A1, A2, B1, B2, C: Type b: Batch A1 B2 (B2 -> C) a: A1 IHb: forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b)
forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g (b ⧆ a)) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f (b ⧆ a))
A1, A2, B1, B2, C: Type c: C
forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f
(mapsnd_Batch B1 B2 g (Done A1 B2 C c)) =
mapsnd_Batch B1 B2 g
(mapfst_Batch A1 A2 f (Done A1 B2 C c))
reflexivity.
A1, A2, B1, B2, C: Type b: Batch A1 B2 (B2 -> C) a: A1 IHb: forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b)
forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g (b ⧆ a)) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f (b ⧆ a))
A1, A2, B1, B2, C: Type b: Batch A1 B2 (B2 -> C) a: A1 IHb: forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b) g: B1 -> B2 f: A1 -> A2
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g (b ⧆ a)) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f (b ⧆ a))
A1, A2, B1, B2, C: Type b: Batch A1 B2 (B2 -> C) a: A1 IHb: forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b) g: B1 -> B2 f: A1 -> A2
mapfst_Batch A1 A2 f
(map (Batch A1 B1) (precompose g)
(mapsnd_Batch B1 B2 g b)) ⧆ f a =
map (Batch A2 B1) (precompose g)
(mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b))
⧆ f a
A1, A2, B1, B2, C: Type b: Batch A1 B2 (B2 -> C) a: A1 IHb: forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b) g: B1 -> B2 f: A1 -> A2
mapfst_Batch A1 A2 f
(map (Batch A1 B1) (precompose g)
(mapsnd_Batch B1 B2 g b)) =
map (Batch A2 B1) (precompose g)
(mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b))
A1, A2, B1, B2, C: Type b: Batch A1 B2 (B2 -> C) a: A1 IHb: forall (g : B1 -> B2) (f : A1 -> A2),
mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b) g: B1 -> B2 f: A1 -> A2
map (Batch A2 B1) (precompose g)
(mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b)) =
map (Batch A2 B1) (precompose g)
(mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b))
nowrewrite IHb.Qed.(** ** Functoriality In the <<B>> Argument *)(**********************************************************************)
forallACB : Type, mapsnd_Batch B B id = id
forallACB : Type, mapsnd_Batch B B id = id
A, C, B: Type
mapsnd_Batch B B id = id
A, C, B: Type b: Batch A B C
mapsnd_Batch B B id b = id b
A, B, C: Type c: C
mapsnd_Batch B B id (Done A B C c) = id (Done A B C c)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: mapsnd_Batch B B id rest = id rest
mapsnd_Batch B B id (rest ⧆ a) = id (rest ⧆ a)
A, B, C: Type c: C
mapsnd_Batch B B id (Done A B C c) = id (Done A B C c)
reflexivity.
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: mapsnd_Batch B B id rest = id rest
mapsnd_Batch B B id (rest ⧆ a) = id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: mapsnd_Batch B B id rest = id rest
map (Batch A B) (precompose id)
(mapsnd_Batch B B id rest) ⧆ a = id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: mapsnd_Batch B B id rest = id rest
map (Batch A B) (precompose id) (id rest) ⧆ a =
id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: mapsnd_Batch B B id rest = id rest
map (Batch A B) id (id rest) ⧆ a = id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: mapsnd_Batch B B id rest = id rest
map (Batch A B) (funx : B -> C => x) rest ⧆ a =
rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: mapsnd_Batch B B id rest = id rest
reflexivity.Qed.(* There is no contravariant functor typeclass to instantiate *)Endfunctoriality.(** * Applicative Functor Instance *)(**********************************************************************)SectionApplicative_Batch.Context
{AB: Type}.(** ** Operations *)(********************************************************************)#[export] InstancePure_Batch: Pure (@Batch A B) :=
fun (C: Type) (c: C) => Done A B C c.Fixpointmult_Batch `(b1: Batch A B C) `(b2: Batch A B D):
@Batch A B (C * D) :=
match b2 with
| Done _ _ _ d => map (Batch A B) (fun (c: C) => (c, d)) b1
| Step _ _ _ rest a =>
Step A B (C * D)
(map (Batch A B) strength_arrow (mult_Batch b1 rest)) a
end.#[export] InstanceMult_Batch: Mult (@Batch A B) :=
funCD '(b1, b2) => mult_Batch b1 b2.(** *** Examples of operations *)(********************************************************************)(* Section demo. Context (A B C D: Type) (a1 a2 a3: A) (c1 c2 c3: C) (d1 d2 d3: D) (mk1: B -> C) (mk1': B -> D) (mk2: B -> B -> C). Compute Done A B C c1 ⊗ Done A B D d1. Compute Done A B C c1 ⊗ (Done A B (B -> D) mk1' ⧆ a1). Compute (Done A B _ mk1 ⧆ a1) ⊗ Done A B D d2. Compute (Done A B _ mk1 ⧆ a1) ⊗ (Done A B _ mk1' ⧆ a2). Compute (Done A B _ mk2 ⧆ a1 ⧆ a2) ⊗ (Done A B _ mk1' ⧆ a3). End demo. *)(** ** Rewriting Principles *)(********************************************************************)
A, B: Type
forall (C : Type) (c : C) (D : Type) (d : D),
Done A B C c ⊗ Done A B D d = Done A B (C * D) (c, d)
A, B: Type
forall (C : Type) (c : C) (D : Type) (d : D),
Done A B C c ⊗ Done A B D d = Done A B (C * D) (c, d)
reflexivity.Qed.
A, B: Type
forall (D : Type) (d : D) (C : Type)
(b1 : Batch A B C),
b1 ⊗ Done A B D d = map (Batch A B) (pair_right d) b1
A, B: Type
forall (D : Type) (d : D) (C : Type)
(b1 : Batch A B C),
b1 ⊗ Done A B D d = map (Batch A B) (pair_right d) b1
A, B, D: Type d: D C: Type b1: Batch A B C
b1 ⊗ Done A B D d = map (Batch A B) (pair_right d) b1
induction b1; easy.Qed.
A, B: Type
forall (D : Type) (b2 : Batch A B (B -> D)) (a : A)
(C : Type) (b1 : Batch A B C),
b1 ⊗ (b2 ⧆ a) =
map (Batch A B) strength_arrow (b1 ⊗ b2) ⧆ a
A, B: Type
forall (D : Type) (b2 : Batch A B (B -> D)) (a : A)
(C : Type) (b1 : Batch A B C),
b1 ⊗ (b2 ⧆ a) =
map (Batch A B) strength_arrow (b1 ⊗ b2) ⧆ a
reflexivity.Qed.
A, B: Type
forall (D : Type) (b2 : Batch A B D) (C : Type)
(c : C),
Done A B C c ⊗ b2 = map (Batch A B) (pair c) b2
A, B: Type
forall (D : Type) (b2 : Batch A B D) (C : Type)
(c : C),
Done A B C c ⊗ b2 = map (Batch A B) (pair c) b2
A, B, C: Type c: C
forall (C0 : Type) (c0 : C0),
Done A B C0 c0 ⊗ Done A B C c =
map (Batch A B) (pair c0) (Done A B C c)
A, B, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C0 : Type) (c : C0),
Done A B C0 c ⊗ b2 =
map (Batch A B) (pair c) b2
forall (C0 : Type) (c : C0),
Done A B C0 c ⊗ (b2 ⧆ a) =
map (Batch A B) (pair c) (b2 ⧆ a)
A, B, C: Type c: C
forall (C0 : Type) (c0 : C0),
Done A B C0 c0 ⊗ Done A B C c =
map (Batch A B) (pair c0) (Done A B C c)
reflexivity.
A, B, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C0 : Type) (c : C0),
Done A B C0 c ⊗ b2 =
map (Batch A B) (pair c) b2
forall (C0 : Type) (c : C0),
Done A B C0 c ⊗ (b2 ⧆ a) =
map (Batch A B) (pair c) (b2 ⧆ a)
A, B, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C0 : Type) (c : C0),
Done A B C0 c ⊗ b2 =
map (Batch A B) (pair c) b2 C0: Type c: C0
Done A B C0 c ⊗ (b2 ⧆ a) =
map (Batch A B) (pair c) (b2 ⧆ a)
A, B, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C0 : Type) (c : C0),
Done A B C0 c ⊗ b2 =
map (Batch A B) (pair c) b2 C0: Type c: C0
map (Batch A B) strength_arrow (Done A B C0 c ⊗ b2)
⧆ a = map (Batch A B) (compose (pair c)) b2 ⧆ a
A, B, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C0 : Type) (c : C0),
Done A B C0 c ⊗ b2 =
map (Batch A B) (pair c) b2 C0: Type c: C0
map (Batch A B) strength_arrow (Done A B C0 c ⊗ b2) =
map (Batch A B) (compose (pair c)) b2
A, B, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C0 : Type) (c : C0),
Done A B C0 c ⊗ b2 =
map (Batch A B) (pair c) b2 C0: Type c: C0
map (Batch A B) strength_arrow
(map (Batch A B) (pair c) b2) =
map (Batch A B) (compose (pair c)) b2
A, B, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C0 : Type) (c : C0),
Done A B C0 c ⊗ b2 =
map (Batch A B) (pair c) b2 C0: Type c: C0
(map (Batch A B) strength_arrow
∘ map (Batch A B) (pair c)) b2 =
map (Batch A B) (compose (pair c)) b2
nowrewrite (fun_map_map (F := Batch A B)).Qed.
A, B: Type
forall (a : A) (C : Type) (b1 : Batch A B (B -> C))
(D : Type) (d : D),
(b1 ⧆ a) ⊗ Done A B D d =
map (Batch A B) (costrength_arrow ∘ pair_right d) b1
⧆ a
A, B: Type
forall (a : A) (C : Type) (b1 : Batch A B (B -> C))
(D : Type) (d : D),
(b1 ⧆ a) ⊗ Done A B D d =
map (Batch A B) (costrength_arrow ∘ pair_right d) b1
⧆ a
reflexivity.Qed.
A, B: Type
forall (D : Type) (b2 : Batch A B (B -> D)) (C : Type)
(c : C) (a : A),
Done A B C c ⊗ (b2 ⧆ a) =
map (Batch A B) (strength_arrow ∘ pair c) b2 ⧆ a
A, B: Type
forall (D : Type) (b2 : Batch A B (B -> D)) (C : Type)
(c : C) (a : A),
Done A B C c ⊗ (b2 ⧆ a) =
map (Batch A B) (strength_arrow ∘ pair c) b2 ⧆ a
A, B, D: Type b2: Batch A B (B -> D) C: Type c: C a: A
Done A B C c ⊗ (b2 ⧆ a) =
map (Batch A B) (strength_arrow ∘ pair c) b2 ⧆ a
A, B, D: Type b2: Batch A B (B -> D) C: Type c: C a: A
map (Batch A B) strength_arrow (Done A B C c ⊗ b2) ⧆ a =
map (Batch A B) (strength_arrow ∘ pair c) b2 ⧆ a
A, B, D: Type b2: Batch A B (B -> D) C: Type c: C a: A
map (Batch A B) strength_arrow
(map (Batch A B) (pair c) b2) ⧆ a =
map (Batch A B) (strength_arrow ∘ pair c) b2 ⧆ a
A, B, D: Type b2: Batch A B (B -> D) C: Type c: C a: A
(map (Batch A B) strength_arrow
∘ map (Batch A B) (pair c)) b2 ⧆ a =
map (Batch A B) (strength_arrow ∘ pair c) b2 ⧆ a
nowrewrite (fun_map_map (F := Batch A B)).Qed.
A, B: Type
forall (a1a2 : A) (C : Type)
(b1 : Batch A B (B -> C)) (D : Type)
(b2 : Batch A B (B -> D)),
(b1 ⧆ a1) ⊗ (b2 ⧆ a2) =
map (Batch A B) strength_arrow ((b1 ⧆ a1) ⊗ b2) ⧆ a2
A, B: Type
forall (a1a2 : A) (C : Type)
(b1 : Batch A B (B -> C)) (D : Type)
(b2 : Batch A B (B -> D)),
(b1 ⧆ a1) ⊗ (b2 ⧆ a2) =
map (Batch A B) strength_arrow ((b1 ⧆ a1) ⊗ b2) ⧆ a2
forall (C1C2 : Type) (f : C1 -> C2) (c : C1),
map (Batch A B) f (pure (Batch A B) c) =
pure (Batch A B) (f c)
A, B: Type
forall (C1C2 : Type) (f : C1 -> C2) (c : C1),
map (Batch A B) f (pure (Batch A B) c) =
pure (Batch A B) (f c)
reflexivity.Qed.
A, B: Type
forall (C1C2D : Type) (f : C1 -> C2)
(b1 : Batch A B C1) (b2 : Batch A B D),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2)
A, B: Type
forall (C1C2D : Type) (f : C1 -> C2)
(b1 : Batch A B C1) (b2 : Batch A B D),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2)
A, B, C1, C2, D: Type f: C1 -> C2 b1: Batch A B C1 b2: Batch A B D
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2)
A, B, C2, D: Type b2: Batch A B D
forall (C1 : Type) (f : C1 -> C2) (b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2)
A, B, C2, C: Type c: C
forall (C1 : Type) (f : C1 -> C2) (b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ Done A B C c =
map (Batch A B) (map_fst f) (b1 ⊗ Done A B C c)
A, B, C2, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C1 : Type) (f : C1 -> C2)
(b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2)
forall (C1 : Type) (f : C1 -> C2) (b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ (b2 ⧆ a) =
map (Batch A B) (map_fst f) (b1 ⊗ (b2 ⧆ a))
A, B, C2, C: Type c: C
forall (C1 : Type) (f : C1 -> C2) (b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ Done A B C c =
map (Batch A B) (map_fst f) (b1 ⊗ Done A B C c)
A, B, C2, C: Type c: C C1: Type f: C1 -> C2 b1: Batch A B C1
map (Batch A B) (func0 : C2 => (c0, c))
(map (Batch A B) f b1) =
map (Batch A B) (map_fst f)
(map (Batch A B) (func0 : C1 => (c0, c)) b1)
A, B, C2, C: Type c: C C1: Type f: C1 -> C2 b1: Batch A B C1
(map (Batch A B) (func0 : C2 => (c0, c))
∘ map (Batch A B) f) b1 =
(map (Batch A B) (map_fst f)
∘ map (Batch A B) (func0 : C1 => (c0, c))) b1
nowdo2rewrite (fun_map_map (F := Batch A B)).
A, B, C2, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C1 : Type) (f : C1 -> C2)
(b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2)
forall (C1 : Type) (f : C1 -> C2) (b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ (b2 ⧆ a) =
map (Batch A B) (map_fst f) (b1 ⊗ (b2 ⧆ a))
A, B, C2, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C1 : Type) (f : C1 -> C2)
(b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2) C1: Type f: C1 -> C2 b1: Batch A B C1
map (Batch A B) strength_arrow
(mult_Batch (map (Batch A B) f b1) b2) ⧆ a =
map (Batch A B) (compose (map_fst f))
(map (Batch A B) strength_arrow (mult_Batch b1 b2))
⧆ a
A, B, C2, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C1 : Type) (f : C1 -> C2)
(b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2) C1: Type f: C1 -> C2 b1: Batch A B C1
map (Batch A B) strength_arrow
(map (Batch A B) f b1 ⊗ b2) ⧆ a =
map (Batch A B) (compose (map_fst f))
(map (Batch A B) strength_arrow (b1 ⊗ b2)) ⧆ a
A, B, C2, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C1 : Type) (f : C1 -> C2)
(b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2) C1: Type f: C1 -> C2 b1: Batch A B C1
map (Batch A B) strength_arrow
(map (Batch A B) (map_fst f) (b1 ⊗ b2)) ⧆ a =
map (Batch A B) (compose (map_fst f))
(map (Batch A B) strength_arrow (b1 ⊗ b2)) ⧆ a
A, B, C2, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C1 : Type) (f : C1 -> C2)
(b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2) C1: Type f: C1 -> C2 b1: Batch A B C1
(map (Batch A B) strength_arrow
∘ map (Batch A B) (map_fst f)) (b1 ⊗ b2) ⧆ a =
(map (Batch A B) (compose (map_fst f))
∘ map (Batch A B) strength_arrow) (b1 ⊗ b2) ⧆ a
A, B, C2, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C1 : Type) (f : C1 -> C2)
(b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2) C1: Type f: C1 -> C2 b1: Batch A B C1
map (Batch A B) (strength_arrow ∘ map_fst f) (b1 ⊗ b2)
⧆ a =
map (Batch A B) (compose (map_fst f) ∘ strength_arrow)
(b1 ⊗ b2) ⧆ a
A, B, C2, C: Type b2: Batch A B (B -> C) a: A IHb2: forall (C1 : Type) (f : C1 -> C2)
(b1 : Batch A B C1),
map (Batch A B) f b1 ⊗ b2 =
map (Batch A B) (map_fst f) (b1 ⊗ b2) C1: Type f: C1 -> C2 b1: Batch A B C1
strength_arrow ∘ map_fst f =
compose (map_fst f) ∘ strength_arrow
now ext [? ?].Qed.
A, B: Type
forall (CD1D2 : Type) (g : D1 -> D2)
(b1 : Batch A B C) (b2 : Batch A B D1),
b1 ⊗ map (Batch A B) g b2 =
map (Batch A B) (map_snd g) (b1 ⊗ b2)
A, B: Type
forall (CD1D2 : Type) (g : D1 -> D2)
(b1 : Batch A B C) (b2 : Batch A B D1),
b1 ⊗ map (Batch A B) g b2 =
map (Batch A B) (map_snd g) (b1 ⊗ b2)
A, B, C, D1, D2: Type g: D1 -> D2 b1: Batch A B C b2: Batch A B D1
b1 ⊗ map (Batch A B) g b2 =
map (Batch A B) (map_snd g) (b1 ⊗ b2)
A, B, C, D1: Type b1: Batch A B C b2: Batch A B D1
forall (D2 : Type) (g : D1 -> D2),
b1 ⊗ map (Batch A B) g b2 =
map (Batch A B) (map_snd g) (b1 ⊗ b2)
A, B, C: Type b1: Batch A B C ANY: Type any: ANY
forall (D2 : Type) (g : ANY -> D2),
b1 ⊗ map (Batch A B) g (Done A B ANY any) =
map (Batch A B) (map_snd g) (b1 ⊗ Done A B ANY any)
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A IH: forall (D2 : Type) (g : (B -> ANY) -> D2),
b1 ⊗ map (Batch A B) g rest =
map (Batch A B) (map_snd g) (b1 ⊗ rest)
forall (D2 : Type) (g : ANY -> D2),
b1 ⊗ map (Batch A B) g (rest ⧆ x') =
map (Batch A B) (map_snd g) (b1 ⊗ (rest ⧆ x'))
A, B, C: Type b1: Batch A B C ANY: Type any: ANY
forall (D2 : Type) (g : ANY -> D2),
b1 ⊗ map (Batch A B) g (Done A B ANY any) =
map (Batch A B) (map_snd g) (b1 ⊗ Done A B ANY any)
A, B, C: Type b1: Batch A B C ANY: Type any: ANY D2: Type g: ANY -> D2
map (Batch A B) (func : C => (c, g any)) b1 =
map (Batch A B) (map_snd g)
(map (Batch A B) (func : C => (c, any)) b1)
A, B, C: Type b1: Batch A B C ANY: Type any: ANY D2: Type g: ANY -> D2
map (Batch A B) (func : C => (c, g any)) b1 =
(map (Batch A B) (map_snd g)
∘ map (Batch A B) (func : C => (c, any))) b1
A, B, C: Type b1: Batch A B C ANY: Type any: ANY D2: Type g: ANY -> D2
map (Batch A B) (func : C => (c, g any)) b1 =
map (Batch A B) (map_snd g ∘ (func : C => (c, any)))
b1
reflexivity.
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A IH: forall (D2 : Type) (g : (B -> ANY) -> D2),
b1 ⊗ map (Batch A B) g rest =
map (Batch A B) (map_snd g) (b1 ⊗ rest)
forall (D2 : Type) (g : ANY -> D2),
b1 ⊗ map (Batch A B) g (rest ⧆ x') =
map (Batch A B) (map_snd g) (b1 ⊗ (rest ⧆ x'))
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A IH: forall (D2 : Type) (g : (B -> ANY) -> D2),
b1 ⊗ map (Batch A B) g rest =
map (Batch A B) (map_snd g) (b1 ⊗ rest) D2: Type g: ANY -> D2
map (Batch A B) strength_arrow
(mult_Batch b1 (map (Batch A B) (compose g) rest))
⧆ x' =
map (Batch A B) (compose (map_snd g))
(map (Batch A B) strength_arrow (mult_Batch b1 rest))
⧆ x'
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A IH: forall (D2 : Type) (g : (B -> ANY) -> D2),
b1 ⊗ map (Batch A B) g rest =
map (Batch A B) (map_snd g) (b1 ⊗ rest) D2: Type g: ANY -> D2
map (Batch A B) strength_arrow
(mult_Batch b1 (map (Batch A B) (compose g) rest)) =
map (Batch A B) (compose (map_snd g))
(map (Batch A B) strength_arrow (mult_Batch b1 rest))
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A IH: forall (D2 : Type) (g : (B -> ANY) -> D2),
b1 ⊗ map (Batch A B) g rest =
map (Batch A B) (map_snd g) (b1 ⊗ rest) D2: Type g: ANY -> D2
map (Batch A B) strength_arrow
(b1 ⊗ map (Batch A B) (compose g) rest) =
map (Batch A B) (compose (map_snd g))
(map (Batch A B) strength_arrow (b1 ⊗ rest))
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A IH: forall (D2 : Type) (g : (B -> ANY) -> D2),
b1 ⊗ map (Batch A B) g rest =
map (Batch A B) (map_snd g) (b1 ⊗ rest) D2: Type g: ANY -> D2
map (Batch A B) strength_arrow
(b1 ⊗ map (Batch A B) (compose g) rest) =
(map (Batch A B) (compose (map_snd g))
∘ map (Batch A B) strength_arrow) (b1 ⊗ rest)
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A IH: forall (D2 : Type) (g : (B -> ANY) -> D2),
b1 ⊗ map (Batch A B) g rest =
map (Batch A B) (map_snd g) (b1 ⊗ rest) D2: Type g: ANY -> D2
map (Batch A B) strength_arrow
(b1 ⊗ map (Batch A B) (compose g) rest) =
map (Batch A B) (compose (map_snd g) ∘ strength_arrow)
(b1 ⊗ rest)
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A D2: Type g: ANY -> D2 IH: b1 ⊗ map (Batch A B) (compose g) rest =
map (Batch A B) (map_snd (compose g)) (b1 ⊗ rest)
map (Batch A B) strength_arrow
(b1 ⊗ map (Batch A B) (compose g) rest) =
map (Batch A B) (compose (map_snd g) ∘ strength_arrow)
(b1 ⊗ rest)
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A D2: Type g: ANY -> D2 IH: b1 ⊗ map (Batch A B) (compose g) rest =
map (Batch A B) (map_snd (compose g)) (b1 ⊗ rest)
map (Batch A B) strength_arrow
(map (Batch A B) (map_snd (compose g)) (b1 ⊗ rest)) =
map (Batch A B) (compose (map_snd g) ∘ strength_arrow)
(b1 ⊗ rest)
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A D2: Type g: ANY -> D2 IH: b1 ⊗ map (Batch A B) (compose g) rest =
map (Batch A B) (map_snd (compose g)) (b1 ⊗ rest)
(map (Batch A B) strength_arrow
∘ map (Batch A B) (map_snd (compose g))) (b1 ⊗ rest) =
map (Batch A B) (compose (map_snd g) ∘ strength_arrow)
(b1 ⊗ rest)
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A D2: Type g: ANY -> D2 IH: b1 ⊗ map (Batch A B) (compose g) rest =
map (Batch A B) (map_snd (compose g)) (b1 ⊗ rest)
map (Batch A B) (strength_arrow ∘ map_snd (compose g))
(b1 ⊗ rest) =
map (Batch A B) (compose (map_snd g) ∘ strength_arrow)
(b1 ⊗ rest)
A, B, C: Type b1: Batch A B C ANY: Type rest: Batch A B (B -> ANY) x': A D2: Type g: ANY -> D2 IH: b1 ⊗ map (Batch A B) (compose g) rest =
map (Batch A B) (map_snd (compose g)) (b1 ⊗ rest)
forall (C1C2D1D2 : Type) (f : C1 -> C2)
(g : D1 -> D2) (b1 : Batch A B C1)
(b2 : Batch A B D1),
map (Batch A B) f b1 ⊗ map (Batch A B) g b2 =
map (Batch A B) (map_tensor f g) (b1 ⊗ b2)
A, B: Type
forall (C1C2D1D2 : Type) (f : C1 -> C2)
(g : D1 -> D2) (b1 : Batch A B C1)
(b2 : Batch A B D1),
map (Batch A B) f b1 ⊗ map (Batch A B) g b2 =
map (Batch A B) (map_tensor f g) (b1 ⊗ b2)
A, B, C1, C2, D1, D2: Type f: C1 -> C2 g: D1 -> D2 b1: Batch A B C1 b2: Batch A B D1
map (Batch A B) f b1 ⊗ map (Batch A B) g b2 =
map (Batch A B) (map_tensor f g) (b1 ⊗ b2)
A, B, C1, C2, D1, D2: Type f: C1 -> C2 g: D1 -> D2 b1: Batch A B C1 b2: Batch A B D1
map (Batch A B) (map_fst f)
(b1 ⊗ map (Batch A B) g b2) =
map (Batch A B) (map_tensor f g) (b1 ⊗ b2)
A, B, C1, C2, D1, D2: Type f: C1 -> C2 g: D1 -> D2 b1: Batch A B C1 b2: Batch A B D1
map (Batch A B) (map_fst f)
(map (Batch A B) (map_snd g) (b1 ⊗ b2)) =
map (Batch A B) (map_tensor f g) (b1 ⊗ b2)
A, B, C1, C2, D1, D2: Type f: C1 -> C2 g: D1 -> D2 b1: Batch A B C1 b2: Batch A B D1
(map (Batch A B) (map_fst f)
∘ map (Batch A B) (map_snd g)) (b1 ⊗ b2) =
map (Batch A B) (map_tensor f g) (b1 ⊗ b2)
A, B, C1, C2, D1, D2: Type f: C1 -> C2 g: D1 -> D2 b1: Batch A B C1 b2: Batch A B D1
map (Batch A B) (map_fst f ∘ map_snd g) (b1 ⊗ b2) =
map (Batch A B) (map_tensor f g) (b1 ⊗ b2)
A, B, C1, C2, D1, D2: Type f: C1 -> C2 g: D1 -> D2 b1: Batch A B C1 b2: Batch A B D1
map_fst f ∘ map_snd g = map_tensor f g
now ext [c1 d1].Qed.
A, B: Type
forall (CDE : Type) (b1 : Batch A B C)
(b2 : Batch A B D) (b3 : Batch A B E),
map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
A, B: Type
forall (CDE : Type) (b1 : Batch A B C)
(b2 : Batch A B D) (b3 : Batch A B E),
map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
A, B, C, D, E: Type b1: Batch A B C b2: Batch A B D b3: Batch A B E
map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type c: C0
map (Batch A B) associator (b1 ⊗ b2 ⊗ Done A B C0 c) =
b1 ⊗ (b2 ⊗ Done A B C0 c)
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) associator (b1 ⊗ b2 ⊗ (b3 ⧆ a)) =
b1 ⊗ (b2 ⊗ (b3 ⧆ a))
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type c: C0
map (Batch A B) associator (b1 ⊗ b2 ⊗ Done A B C0 c) =
b1 ⊗ (b2 ⊗ Done A B C0 c)
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type c: C0
map (Batch A B) associator
(map (Batch A B) (pair_right c) (b1 ⊗ b2)) =
b1 ⊗ map (Batch A B) (pair_right c) b2
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type c: C0
map (Batch A B) associator
(map (Batch A B) (pair_right c) (b1 ⊗ b2)) =
map (Batch A B) (map_snd (pair_right c)) (b1 ⊗ b2)
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type c: C0
(map (Batch A B) associator
∘ map (Batch A B) (pair_right c)) (b1 ⊗ b2) =
map (Batch A B) (map_snd (pair_right c)) (b1 ⊗ b2)
nowrewrite (fun_map_map (F := Batch A B)).
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) associator (b1 ⊗ b2 ⊗ (b3 ⧆ a)) =
b1 ⊗ (b2 ⊗ (b3 ⧆ a))
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) (compose associator)
(map (Batch A B) strength_arrow
(mult_Batch (mult_Batch b1 b2) b3)) ⧆ a =
map (Batch A B) strength_arrow
(mult_Batch b1
(map (Batch A B) strength_arrow
(mult_Batch b2 b3))) ⧆ a
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) (compose associator)
(map (Batch A B) strength_arrow (b1 ⊗ b2 ⊗ b3)) ⧆ a =
map (Batch A B) strength_arrow
(b1 ⊗ map (Batch A B) strength_arrow (b2 ⊗ b3)) ⧆ a
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) (compose associator)
(map (Batch A B) strength_arrow (b1 ⊗ b2 ⊗ b3)) =
map (Batch A B) strength_arrow
(b1 ⊗ map (Batch A B) strength_arrow (b2 ⊗ b3))
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) (compose associator)
(map (Batch A B) strength_arrow (b1 ⊗ b2 ⊗ b3)) =
map (Batch A B) strength_arrow
(map (Batch A B) (map_snd strength_arrow)
(b1 ⊗ (b2 ⊗ b3)))
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) (compose associator)
(map (Batch A B) strength_arrow (b1 ⊗ b2 ⊗ b3)) =
map (Batch A B) strength_arrow
(map (Batch A B) (map_snd strength_arrow)
(map (Batch A B) associator (b1 ⊗ b2 ⊗ b3)))
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
(map (Batch A B) (compose associator)
∘ map (Batch A B) strength_arrow) (b1 ⊗ b2 ⊗ b3) =
map (Batch A B) strength_arrow
((map (Batch A B) (map_snd strength_arrow)
∘ map (Batch A B) associator) (b1 ⊗ b2 ⊗ b3))
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) (compose associator ∘ strength_arrow)
(b1 ⊗ b2 ⊗ b3) =
map (Batch A B) strength_arrow
(map (Batch A B)
(map_snd strength_arrow ∘ associator)
(b1 ⊗ b2 ⊗ b3))
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) (compose associator ∘ strength_arrow)
(b1 ⊗ b2 ⊗ b3) =
(map (Batch A B) strength_arrow
∘ map (Batch A B)
(map_snd strength_arrow ∘ associator))
(b1 ⊗ b2 ⊗ b3)
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
map (Batch A B) (compose associator ∘ strength_arrow)
(b1 ⊗ b2 ⊗ b3) =
map (Batch A B)
(strength_arrow
∘ (map_snd strength_arrow ∘ associator))
(b1 ⊗ b2 ⊗ b3)
A, B, C, D: Type b1: Batch A B C b2: Batch A B D C0: Type b3: Batch A B (B -> C0) a: A IHb3: map (Batch A B) associator (b1 ⊗ b2 ⊗ b3) =
b1 ⊗ (b2 ⊗ b3)
forall (C : Type) (b : Batch A B C),
map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) =
b
A, B: Type
forall (C : Type) (b : Batch A B C),
map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) =
b
A, B, C: Type b: Batch A B C
map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) =
b
A, B, C: Type c: C
map (Batch A B) left_unitor
(pure (Batch A B) tt ⊗ Done A B C c) = Done A B C c
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b
map (Batch A B) left_unitor
(pure (Batch A B) tt ⊗ (b ⧆ a)) = b ⧆ a
A, B, C: Type c: C
map (Batch A B) left_unitor
(pure (Batch A B) tt ⊗ Done A B C c) = Done A B C c
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b
map (Batch A B) left_unitor
(pure (Batch A B) tt ⊗ (b ⧆ a)) = b ⧆ a
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b
map (Batch A B) (compose left_unitor)
(map (Batch A B) strength_arrow
(mult_Batch (pure (Batch A B) tt) b)) ⧆ a = b ⧆ a
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b
map (Batch A B) (compose left_unitor)
(map (Batch A B) strength_arrow
(pure (Batch A B) tt ⊗ b)) ⧆ a = b ⧆ a
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b
map (Batch A B) (compose left_unitor)
(map (Batch A B) strength_arrow
(pure (Batch A B) tt ⊗ b)) = b
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b
(map (Batch A B) (compose left_unitor)
∘ map (Batch A B) strength_arrow)
(pure (Batch A B) tt ⊗ b) = b
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b
map (Batch A B) (compose left_unitor ∘ strength_arrow)
(pure (Batch A B) tt ⊗ b) = b
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b
map (Batch A B) (compose left_unitor ∘ strength_arrow)
(pure (Batch A B) tt
⊗ map (Batch A B) left_unitor
(pure (Batch A B) tt ⊗ b)) =
map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b
map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) =
b
assumption.Qed.
A, B: Type
forall (C : Type) (b : Batch A B C),
map (Batch A B) right_unitor (b ⊗ pure (Batch A B) tt) =
b
A, B: Type
forall (C : Type) (b : Batch A B C),
map (Batch A B) right_unitor (b ⊗ pure (Batch A B) tt) =
b
A, B, C: Type b: Batch A B C
map (Batch A B) right_unitor (b ⊗ pure (Batch A B) tt) =
b
A, B, C: Type c: C
map (Batch A B) right_unitor
(Done A B C c ⊗ pure (Batch A B) tt) = Done A B C c
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) right_unitor (b ⊗ pure (Batch A B) tt) = b
map (Batch A B) right_unitor
((b ⧆ a) ⊗ pure (Batch A B) tt) = b ⧆ a
A, B, C: Type c: C
map (Batch A B) right_unitor
(Done A B C c ⊗ pure (Batch A B) tt) = Done A B C c
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) right_unitor (b ⊗ pure (Batch A B) tt) = b
map (Batch A B) right_unitor
((b ⧆ a) ⊗ pure (Batch A B) tt) = b ⧆ a
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) right_unitor (map (Batch A B) (func : B -> C => (c, tt)) b) =
b
map (Batch A B) (compose right_unitor)
(map (Batch A B) (compose (func : C => (c, tt))) b)
⧆ a = b ⧆ a
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) right_unitor (map (Batch A B) (func : B -> C => (c, tt)) b) =
b
map (Batch A B) (compose right_unitor)
(map (Batch A B) (compose (func : C => (c, tt))) b) =
b
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) right_unitor (map (Batch A B) (func : B -> C => (c, tt)) b) =
b
map (Batch A B) (compose right_unitor)
(map (Batch A B) (compose (func : C => (c, tt))) b) =
map (Batch A B) right_unitor
(map (Batch A B) (func : B -> C => (c, tt)) b)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: map (Batch A B) right_unitor (map (Batch A B) (func : B -> C => (c, tt)) b) =
b
(map (Batch A B) (compose right_unitor)
∘ map (Batch A B) (compose (func : C => (c, tt)))) b =
(map (Batch A B) right_unitor
∘ map (Batch A B) (func : B -> C => (c, tt))) b
nowdo2rewrite (fun_map_map (F := Batch A B)).Qed.
A, B: Type
forall (CD : Type) (c : C) (d : D),
pure (Batch A B) c ⊗ pure (Batch A B) d =
pure (Batch A B) (c, d)
A, B: Type
forall (CD : Type) (c : C) (d : D),
pure (Batch A B) c ⊗ pure (Batch A B) d =
pure (Batch A B) (c, d)
A, B, C, D: Type c: C d: D
pure (Batch A B) c ⊗ pure (Batch A B) d =
pure (Batch A B) (c, d)
map (Batch A B) f (pure (Batch A B) x) =
pure (Batch A B) (f x)
A, B, A0, B0, C, D: Type f: A0 -> C g: B0 -> D x: Batch A B A0 y: Batch A B B0
map (Batch A B) f x ⊗ map (Batch A B) g y =
map (Batch A B) (map_tensor f g) (x ⊗ y)
A, B, A0, B0, C: Type x: Batch A B A0 y: Batch A B B0 z: Batch A B C
map (Batch A B) associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
A, B, A0: Type x: Batch A B A0
map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ x) =
x
A, B, A0: Type x: Batch A B A0
map (Batch A B) right_unitor (x ⊗ pure (Batch A B) tt) =
x
A, B, A0, B0: Type a: A0 b: B0
pure (Batch A B) a ⊗ pure (Batch A B) b =
pure (Batch A B) (a, b)
A, B: Type
Functor (Batch A B)
typeclasses eauto.
A, B, A0, B0: Type f: A0 -> B0 x: A0
map (Batch A B) f (pure (Batch A B) x) =
pure (Batch A B) (f x)
reflexivity.
A, B, A0, B0, C, D: Type f: A0 -> C g: B0 -> D x: Batch A B A0 y: Batch A B B0
map (Batch A B) f x ⊗ map (Batch A B) g y =
map (Batch A B) (map_tensor f g) (x ⊗ y)
apply app_mult_natural_Batch.
A, B, A0, B0, C: Type x: Batch A B A0 y: Batch A B B0 z: Batch A B C
map (Batch A B) associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
apply app_assoc_Batch.
A, B, A0: Type x: Batch A B A0
map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ x) =
x
apply app_unital_l_Batch.
A, B, A0: Type x: Batch A B A0
map (Batch A B) right_unitor (x ⊗ pure (Batch A B) tt) =
x
apply app_unital_r_Batch.
A, B, A0, B0: Type a: A0 b: B0
pure (Batch A B) a ⊗ pure (Batch A B) b =
pure (Batch A B) (a, b)
reflexivity.Qed.EndApplicative_Batch.(** ** <<mapfst>> and <<mapsnd>> as Applicative Homomorphisms *)(**********************************************************************)
B, C, D, A1, A2: Type f: A1 -> A2 b1: Batch A1 B C b2: Batch A1 B D
mapfst_Batch A1 A2 f (b1 ⊗ b2) =
mapfst_Batch A1 A2 f b1 ⊗ mapfst_Batch A1 A2 f b2
B, C, D, A1, A2: Type f: A1 -> A2 b1: Batch A1 B C b2: Batch A1 B D
mapfst_Batch A1 A2 f (b1 ⊗ b2) =
mapfst_Batch A1 A2 f b1 ⊗ mapfst_Batch A1 A2 f b2
B, C, D, A1, A2: Type f: A1 -> A2 b2: Batch A1 B D
forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ b2) =
mapfst_Batch A1 A2 f b1 ⊗ mapfst_Batch A1 A2 f b2
B, C, A1, A2: Type f: A1 -> A2 C0: Type c: C0
forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ Done A1 B C0 c) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f (Done A1 B C0 c)
B, C, A1, A2: Type f: A1 -> A2 C0: Type b2: Batch A1 B (B -> C0) a: A1 IHb2: forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ b2) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f b2
forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ (b2 ⧆ a)) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f (b2 ⧆ a)
B, C, A1, A2: Type f: A1 -> A2 C0: Type c: C0
forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ Done A1 B C0 c) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f (Done A1 B C0 c)
B, C, A1, A2: Type f: A1 -> A2 C0: Type c: C0 b1: Batch A1 B C
mapfst_Batch A1 A2 f (b1 ⊗ Done A1 B C0 c) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f (Done A1 B C0 c)
B, C, A1, A2: Type f: A1 -> A2 C0: Type c: C0 b1: Batch A1 B C
mapfst_Batch A1 A2 f
(map (Batch A1 B) (func0 : C => (c0, c)) b1) =
map (Batch A2 B) (func0 : C => (c0, c))
(mapfst_Batch A1 A2 f b1)
nowrewrite mapfst_map_Batch.
B, C, A1, A2: Type f: A1 -> A2 C0: Type b2: Batch A1 B (B -> C0) a: A1 IHb2: forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ b2) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f b2
forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ (b2 ⧆ a)) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f (b2 ⧆ a)
B, C, A1, A2: Type f: A1 -> A2 C0: Type b2: Batch A1 B (B -> C0) a: A1 IHb2: forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ b2) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f b2
forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f
(map (Batch A1 B) strength_arrow (mult_Batch b1 b2))
⧆ f a =
map (Batch A2 B) strength_arrow
(mult_Batch (mapfst_Batch A1 A2 f b1)
(mapfst_Batch A1 A2 f b2)) ⧆ f a
B, C, A1, A2: Type f: A1 -> A2 C0: Type b2: Batch A1 B (B -> C0) a: A1 IHb2: forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ b2) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f b2
forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f
(map (Batch A1 B) strength_arrow (mult_Batch b1 b2))
⧆ f a =
map (Batch A2 B) strength_arrow
(mult_Batch (mapfst_Batch A1 A2 f b1)
(mapfst_Batch A1 A2 f b2)) ⧆ f a
B, C, A1, A2: Type f: A1 -> A2 C0: Type b2: Batch A1 B (B -> C0) a: A1 IHb2: forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ b2) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f b2 b1: Batch A1 B C
mapfst_Batch A1 A2 f
(map (Batch A1 B) strength_arrow (b1 ⊗ b2)) ⧆ f a =
map (Batch A2 B) strength_arrow
(mapfst_Batch A1 A2 f b1 ⊗ mapfst_Batch A1 A2 f b2)
⧆ f a
B, C, A1, A2: Type f: A1 -> A2 C0: Type b2: Batch A1 B (B -> C0) a: A1 IHb2: forallb1 : Batch A1 B C,
mapfst_Batch A1 A2 f (b1 ⊗ b2) =
mapfst_Batch A1 A2 f b1
⊗ mapfst_Batch A1 A2 f b2 b1: Batch A1 B C
mapfst_Batch A1 A2 f
(map (Batch A1 B) strength_arrow (b1 ⊗ b2)) ⧆ f a =
map (Batch A2 B) strength_arrow
(mapfst_Batch A1 A2 f (b1 ⊗ b2)) ⧆ f a
nowrewrite mapfst_map_Batch.Qed.
B, C, D, A1, A2: Type f: A1 -> A2 b1: Batch A1 B (C -> D) b2: Batch A1 B C
mapfst_Batch A1 A2 f (b1 <⋆> b2) =
mapfst_Batch A1 A2 f b1 <⋆> mapfst_Batch A1 A2 f b2
B, C, D, A1, A2: Type f: A1 -> A2 b1: Batch A1 B (C -> D) b2: Batch A1 B C
mapfst_Batch A1 A2 f (b1 <⋆> b2) =
mapfst_Batch A1 A2 f b1 <⋆> mapfst_Batch A1 A2 f b2
B, C, D, A1, A2: Type f: A1 -> A2 b1: Batch A1 B (C -> D) b2: Batch A1 B C
mapfst_Batch A1 A2 f
(map (Batch A1 B) (fun '(f, a) => f a) (b1 ⊗ b2)) =
map (Batch A2 B) (fun '(f, a) => f a)
(mapfst_Batch A1 A2 f b1 ⊗ mapfst_Batch A1 A2 f b2)
B, C, D, A1, A2: Type f: A1 -> A2 b1: Batch A1 B (C -> D) b2: Batch A1 B C
map (Batch A2 B) (fun '(f, a) => f a)
(mapfst_Batch A1 A2 f (b1 ⊗ b2)) =
map (Batch A2 B) (fun '(f, a) => f a)
(mapfst_Batch A1 A2 f b1 ⊗ mapfst_Batch A1 A2 f b2)
nowrewrite mapfst_Batch1.Qed.
B, A1, A2: Type f: A1 -> A2
ApplicativeMorphism (Batch A1 B) (Batch A2 B)
(funC : Type => mapfst_Batch A1 A2 f)
B, A1, A2: Type f: A1 -> A2
ApplicativeMorphism (Batch A1 B) (Batch A2 B)
(funC : Type => mapfst_Batch A1 A2 f)
B, A1, A2: Type f: A1 -> A2
ApplicativeMorphism (Batch A1 B) (Batch A2 B)
(funC : Type => mapfst_Batch A1 A2 f)
B, A1, A2: Type f: A1 -> A2
forall (AB0 : Type) (f0 : A -> B0) (x : Batch A1 B A),
mapfst_Batch A1 A2 f (map (Batch A1 B) f0 x) =
map (Batch A2 B) f0 (mapfst_Batch A1 A2 f x)
B, A1, A2: Type f: A1 -> A2
forall (A : Type) (a : A),
mapfst_Batch A1 A2 f (pure (Batch A1 B) a) =
pure (Batch A2 B) a
B, A1, A2: Type f: A1 -> A2
forall (AB0 : Type) (x : Batch A1 B A)
(y : Batch A1 B B0),
mapfst_Batch A1 A2 f (x ⊗ y) =
mapfst_Batch A1 A2 f x ⊗ mapfst_Batch A1 A2 f y
B, A1, A2: Type f: A1 -> A2
forall (AB0 : Type) (f0 : A -> B0) (x : Batch A1 B A),
mapfst_Batch A1 A2 f (map (Batch A1 B) f0 x) =
map (Batch A2 B) f0 (mapfst_Batch A1 A2 f x)
B, A1, A2: Type f: A1 -> A2 A, B0: Type f0: A -> B0 x: Batch A1 B A
mapfst_Batch A1 A2 f (map (Batch A1 B) f0 x) =
map (Batch A2 B) f0 (mapfst_Batch A1 A2 f x)
nowrewrite mapfst_map_Batch.
B, A1, A2: Type f: A1 -> A2
forall (A : Type) (a : A),
mapfst_Batch A1 A2 f (pure (Batch A1 B) a) =
pure (Batch A2 B) a
B, A1, A2: Type f: A1 -> A2 A: Type a: A
mapfst_Batch A1 A2 f (pure (Batch A1 B) a) =
pure (Batch A2 B) a
reflexivity.
B, A1, A2: Type f: A1 -> A2
forall (AB0 : Type) (x : Batch A1 B A)
(y : Batch A1 B B0),
mapfst_Batch A1 A2 f (x ⊗ y) =
mapfst_Batch A1 A2 f x ⊗ mapfst_Batch A1 A2 f y
B, A1, A2: Type f: A1 -> A2 A, B0: Type x: Batch A1 B A y: Batch A1 B B0
mapfst_Batch A1 A2 f (x ⊗ y) =
mapfst_Batch A1 A2 f x ⊗ mapfst_Batch A1 A2 f y
apply mapfst_Batch1.Qed.
A, C, D, B1, B2: Type f: B1 -> B2 b1: Batch A B2 C b2: Batch A B2 D
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2
A, C, D, B1, B2: Type f: B1 -> B2 b1: Batch A B2 C b2: Batch A B2 D
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2
A, C, D, B1, B2: Type f: B1 -> B2 b2: Batch A B2 D
forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2
A, C, B1, B2: Type f: B1 -> B2 C0: Type c: C0
forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ Done A B2 C0 c) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f (Done A B2 C0 c)
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2
forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ (b2 ⧆ a)) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f (b2 ⧆ a)
A, C, B1, B2: Type f: B1 -> B2 C0: Type c: C0
forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ Done A B2 C0 c) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f (Done A B2 C0 c)
A, C, B1, B2: Type f: B1 -> B2 C0: Type c: C0 b1: Batch A B2 C
mapsnd_Batch B1 B2 f (b1 ⊗ Done A B2 C0 c) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f (Done A B2 C0 c)
A, C, B1, B2: Type f: B1 -> B2 C0: Type c: C0 b1: Batch A B2 C
mapsnd_Batch B1 B2 f
(map (Batch A B2) (func0 : C => (c0, c)) b1) =
map (Batch A B1) (func0 : C => (c0, c))
(mapsnd_Batch B1 B2 f b1)
nowrewrite mapsnd_map_Batch.
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2
forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ (b2 ⧆ a)) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f (b2 ⧆ a)
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2
forallb1 : Batch A B2 C,
map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f
(map (Batch A B2) strength_arrow
(mult_Batch b1 b2))) ⧆ a =
map (Batch A B1) strength_arrow
(mult_Batch (mapsnd_Batch B1 B2 f b1)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f b2))) ⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2
forallb1 : Batch A B2 C,
map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f
(map (Batch A B2) strength_arrow
(mult_Batch b1 b2))) ⧆ a =
map (Batch A B1) strength_arrow
(mult_Batch (mapsnd_Batch B1 B2 f b1)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f b2))) ⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2 b1: Batch A B2 C
map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f
(map (Batch A B2) strength_arrow (b1 ⊗ b2))) ⧆ a =
map (Batch A B1) strength_arrow
(mapsnd_Batch B1 B2 f b1
⊗ map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f b2)) ⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2 b1: Batch A B2 C
map (Batch A B1) (precompose f)
(map (Batch A B1) strength_arrow
(mapsnd_Batch B1 B2 f (b1 ⊗ b2))) ⧆ a =
map (Batch A B1) strength_arrow
(mapsnd_Batch B1 B2 f b1
⊗ map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f b2)) ⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2 b1: Batch A B2 C
(map (Batch A B1) (precompose f)
∘ map (Batch A B1) strength_arrow)
(mapsnd_Batch B1 B2 f (b1 ⊗ b2)) ⧆ a =
map (Batch A B1) strength_arrow
(mapsnd_Batch B1 B2 f b1
⊗ map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f b2)) ⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2 b1: Batch A B2 C
map (Batch A B1) (precompose f ∘ strength_arrow)
(mapsnd_Batch B1 B2 f (b1 ⊗ b2)) ⧆ a =
map (Batch A B1) strength_arrow
(mapsnd_Batch B1 B2 f b1
⊗ map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f b2)) ⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2 b1: Batch A B2 C
map (Batch A B1) (precompose f ∘ strength_arrow)
(mapsnd_Batch B1 B2 f (b1 ⊗ b2)) ⧆ a =
map (Batch A B1) strength_arrow
(map (Batch A B1) (map_snd (precompose f))
(mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2)) ⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2 b1: Batch A B2 C
map (Batch A B1) (precompose f ∘ strength_arrow)
(mapsnd_Batch B1 B2 f (b1 ⊗ b2)) ⧆ a =
(map (Batch A B1) strength_arrow
∘ map (Batch A B1) (map_snd (precompose f)))
(mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2)
⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2 b1: Batch A B2 C
map (Batch A B1) (precompose f ∘ strength_arrow)
(mapsnd_Batch B1 B2 f (b1 ⊗ b2)) ⧆ a =
map (Batch A B1)
(strength_arrow ∘ map_snd (precompose f))
(mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2)
⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2 b1: Batch A B2 C
map (Batch A B1) (precompose f ∘ strength_arrow)
(mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2)
⧆ a =
map (Batch A B1)
(strength_arrow ∘ map_snd (precompose f))
(mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2)
⧆ a
A, C, B1, B2: Type f: B1 -> B2 C0: Type b2: Batch A B2 (B2 -> C0) a: A IHb2: forallb1 : Batch A B2 C,
mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
mapsnd_Batch B1 B2 f b1
⊗ mapsnd_Batch B1 B2 f b2 b1: Batch A B2 C c: C rest: B2 -> C0
A, C, D, B1, B2: Type f: B1 -> B2 b1: Batch A B2 (C -> D) b2: Batch A B2 C
mapsnd_Batch B1 B2 f (b1 <⋆> b2) =
mapsnd_Batch B1 B2 f b1 <⋆> mapsnd_Batch B1 B2 f b2
A, C, D, B1, B2: Type f: B1 -> B2 b1: Batch A B2 (C -> D) b2: Batch A B2 C
mapsnd_Batch B1 B2 f (b1 <⋆> b2) =
mapsnd_Batch B1 B2 f b1 <⋆> mapsnd_Batch B1 B2 f b2
A, C, D, B1, B2: Type f: B1 -> B2 b1: Batch A B2 (C -> D) b2: Batch A B2 C
mapsnd_Batch B1 B2 f
(map (Batch A B2) (fun '(f, a) => f a) (b1 ⊗ b2)) =
map (Batch A B1) (fun '(f, a) => f a)
(mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2)
A, C, D, B1, B2: Type f: B1 -> B2 b1: Batch A B2 (C -> D) b2: Batch A B2 C
map (Batch A B1) (fun '(f, a) => f a)
(mapsnd_Batch B1 B2 f (b1 ⊗ b2)) =
map (Batch A B1) (fun '(f, a) => f a)
(mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2)
nowrewrite mapsnd_Batch1.Qed.
A, B1, B2: Type f: B1 -> B2
ApplicativeMorphism (Batch A B2) (Batch A B1)
(funC : Type => mapsnd_Batch B1 B2 f)
A, B1, B2: Type f: B1 -> B2
ApplicativeMorphism (Batch A B2) (Batch A B1)
(funC : Type => mapsnd_Batch B1 B2 f)
A, B1, B2: Type f: B1 -> B2
ApplicativeMorphism (Batch A B2) (Batch A B1)
(funC : Type => mapsnd_Batch B1 B2 f)
A, B1, B2: Type f: B1 -> B2
forall (A0B : Type) (f0 : A0 -> B)
(x : Batch A B2 A0),
mapsnd_Batch B1 B2 f (map (Batch A B2) f0 x) =
map (Batch A B1) f0 (mapsnd_Batch B1 B2 f x)
A, B1, B2: Type f: B1 -> B2
forall (A0 : Type) (a : A0),
mapsnd_Batch B1 B2 f (pure (Batch A B2) a) =
pure (Batch A B1) a
A, B1, B2: Type f: B1 -> B2
forall (A0B : Type) (x : Batch A B2 A0)
(y : Batch A B2 B),
mapsnd_Batch B1 B2 f (x ⊗ y) =
mapsnd_Batch B1 B2 f x ⊗ mapsnd_Batch B1 B2 f y
A, B1, B2: Type f: B1 -> B2
forall (A0B : Type) (f0 : A0 -> B)
(x : Batch A B2 A0),
mapsnd_Batch B1 B2 f (map (Batch A B2) f0 x) =
map (Batch A B1) f0 (mapsnd_Batch B1 B2 f x)
A, B1, B2: Type f: B1 -> B2 A0, B: Type f0: A0 -> B x: Batch A B2 A0
mapsnd_Batch B1 B2 f (map (Batch A B2) f0 x) =
map (Batch A B1) f0 (mapsnd_Batch B1 B2 f x)
nowrewrite mapsnd_map_Batch.
A, B1, B2: Type f: B1 -> B2
forall (A0 : Type) (a : A0),
mapsnd_Batch B1 B2 f (pure (Batch A B2) a) =
pure (Batch A B1) a
A, B1, B2: Type f: B1 -> B2 A0: Type a: A0
mapsnd_Batch B1 B2 f (pure (Batch A B2) a) =
pure (Batch A B1) a
reflexivity.
A, B1, B2: Type f: B1 -> B2
forall (A0B : Type) (x : Batch A B2 A0)
(y : Batch A B2 B),
mapsnd_Batch B1 B2 f (x ⊗ y) =
mapsnd_Batch B1 B2 f x ⊗ mapsnd_Batch B1 B2 f y
A, B1, B2: Type f: B1 -> B2 A0, B: Type x: Batch A B2 A0 y: Batch A B2 B
mapsnd_Batch B1 B2 f (x ⊗ y) =
mapsnd_Batch B1 B2 f x ⊗ mapsnd_Batch B1 B2 f y
apply mapsnd_Batch1.Qed.(** * The <<runBatch>> Operation *)(**********************************************************************)FixpointrunBatch {AB: Type}
(F: Type -> Type) `{Map F} `{Mult F} `{Pure F}
(ϕ: A -> F B) (C: Type) (b: Batch A B C): F C :=
match b with
| Done _ _ _ c => pure F c
| Step _ _ _ rest a => runBatch F ϕ (B -> C) rest <⋆> ϕ a
end.(** ** Rewriting Principles *)(**********************************************************************)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type c: C
runBatch F ϕ C (Done A B C c) = pure F c
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type c: C
runBatch F ϕ C (Done A B C c) = pure F c
reflexivity.Qed.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B a: A C: Type rest: Batch A B (B -> C)
runBatch F ϕ C (rest ⧆ a) =
runBatch F ϕ (B -> C) rest <⋆> ϕ a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B a: A C: Type rest: Batch A B (B -> C)
runBatch F ϕ C (rest ⧆ a) =
runBatch F ϕ (B -> C) rest <⋆> ϕ a
reflexivity.Qed.(** ** Naturality of <<runBatch>> *)(**********************************************************************)SectionrunBatch_naturality.Context
`{Applicative F}.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B, C1, C2: Type ϕ: A -> F B f: C1 -> C2 b: Batch A B C1
map F f (runBatch F ϕ C1 b) =
runBatch F ϕ C2 (map (Batch A B) f b)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B, C1, C2: Type ϕ: A -> F B f: C1 -> C2 b: Batch A B C1
map F f (runBatch F ϕ C1 b) =
runBatch F ϕ C2 (map (Batch A B) f b)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B, C1: Type ϕ: A -> F B b: Batch A B C1
forall (C2 : Type) (f : C1 -> C2),
map F f (runBatch F ϕ C1 b) =
runBatch F ϕ C2 (map (Batch A B) f b)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type c: C C2: Type f: C -> C2
map F f (runBatch F ϕ C (Done A B C c)) =
runBatch F ϕ C2 (map (Batch A B) f (Done A B C c))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type b: Batch A B (B -> C) a: A IHb: forall (C2 : Type) (f : (B -> C) -> C2),
map F f (runBatch F ϕ (B -> C) b) =
runBatch F ϕ C2 (map (Batch A B) f b) C2: Type f: C -> C2
map F f (runBatch F ϕ C (b ⧆ a)) =
runBatch F ϕ C2 (map (Batch A B) f (b ⧆ a))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type c: C C2: Type f: C -> C2
map F f (runBatch F ϕ C (Done A B C c)) =
runBatch F ϕ C2 (map (Batch A B) f (Done A B C c))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type c: C C2: Type f: C -> C2
map F f (pure F c) = pure F (f c)
nowrewrite app_pure_natural.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type b: Batch A B (B -> C) a: A IHb: forall (C2 : Type) (f : (B -> C) -> C2),
map F f (runBatch F ϕ (B -> C) b) =
runBatch F ϕ C2 (map (Batch A B) f b) C2: Type f: C -> C2
map F f (runBatch F ϕ C (b ⧆ a)) =
runBatch F ϕ C2 (map (Batch A B) f (b ⧆ a))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type b: Batch A B (B -> C) a: A IHb: forall (C2 : Type) (f : (B -> C) -> C2),
map F f (runBatch F ϕ (B -> C) b) =
runBatch F ϕ C2 (map (Batch A B) f b) C2: Type f: C -> C2
map F f (runBatch F ϕ (B -> C) b <⋆> ϕ a) =
runBatch F ϕ (B -> C2) (map (Batch A B) (compose f) b) <⋆>
ϕ a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type b: Batch A B (B -> C) a: A IHb: forall (C2 : Type) (f : (B -> C) -> C2),
map F f (runBatch F ϕ (B -> C) b) =
runBatch F ϕ C2 (map (Batch A B) f b) C2: Type f: C -> C2
map F (compose f) (runBatch F ϕ (B -> C) b) <⋆> ϕ a =
runBatch F ϕ (B -> C2) (map (Batch A B) (compose f) b) <⋆>
ϕ a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C: Type b: Batch A B (B -> C) a: A IHb: forall (C2 : Type) (f : (B -> C) -> C2),
map F f (runBatch F ϕ (B -> C) b) =
runBatch F ϕ C2 (map (Batch A B) f b) C2: Type f: C -> C2
map F (compose f) (runBatch F ϕ (B -> C) b) =
runBatch F ϕ (B -> C2) (map (Batch A B) (compose f) b)
nowrewrite IHb.Qed.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
Natural (runBatch F ϕ)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
forall (A0B0 : Type) (f : A0 -> B0),
map F f ∘ runBatch F ϕ A0 =
runBatch F ϕ B0 ∘ map (Batch A B) f
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, D: Type f: C -> D
map F f ∘ runBatch F ϕ C =
runBatch F ϕ D ∘ map (Batch A B) f
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, D: Type f: C -> D b: Batch A B C
(map F f ∘ runBatch F ϕ C) b =
(runBatch F ϕ D ∘ map (Batch A B) f) b
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, D: Type f: C -> D b: Batch A B C
map F f (runBatch F ϕ C b) =
runBatch F ϕ D (map (Batch A B) f b)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, D: Type f: C -> D b: Batch A B C
runBatch F ϕ D (map (Batch A B) f b) =
runBatch F ϕ D (map (Batch A B) f b)
reflexivity.Qed.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
forall (A1BC : Type) (s : Batch A1 B C) (A2 : Type)
(ϕ : A2 -> F B) (f : A1 -> A2),
runBatch F (ϕ ∘ f) C s =
runBatch F ϕ C (mapfst_Batch A1 A2 f s)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
forall (A1BC : Type) (s : Batch A1 B C) (A2 : Type)
(ϕ : A2 -> F B) (f : A1 -> A2),
runBatch F (ϕ ∘ f) C s =
runBatch F ϕ C (mapfst_Batch A1 A2 f s)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A1, B, C: Type c: C A2: Type ϕ: A2 -> F B f: A1 -> A2
runBatch F (ϕ ∘ f) C (Done A1 B C c) =
runBatch F ϕ C (mapfst_Batch A1 A2 f (Done A1 B C c))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A1, B, C: Type s: Batch A1 B (B -> C) a: A1 A2: Type ϕ: A2 -> F B f: A1 -> A2 IHs: runBatch F (ϕ ∘ f) (B -> C) s =
runBatch F ϕ (B -> C) (mapfst_Batch A1 A2 f s)
runBatch F (ϕ ∘ f) C (s ⧆ a) =
runBatch F ϕ C (mapfst_Batch A1 A2 f (s ⧆ a))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A1, B, C: Type c: C A2: Type ϕ: A2 -> F B f: A1 -> A2
runBatch F (ϕ ∘ f) C (Done A1 B C c) =
runBatch F ϕ C (mapfst_Batch A1 A2 f (Done A1 B C c))
easy.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A1, B, C: Type s: Batch A1 B (B -> C) a: A1 A2: Type ϕ: A2 -> F B f: A1 -> A2 IHs: runBatch F (ϕ ∘ f) (B -> C) s =
runBatch F ϕ (B -> C) (mapfst_Batch A1 A2 f s)
runBatch F (ϕ ∘ f) C (s ⧆ a) =
runBatch F ϕ C (mapfst_Batch A1 A2 f (s ⧆ a))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A1, B, C: Type s: Batch A1 B (B -> C) a: A1 A2: Type ϕ: A2 -> F B f: A1 -> A2 IHs: runBatch F (ϕ ∘ f) (B -> C) s =
runBatch F ϕ (B -> C) (mapfst_Batch A1 A2 f s)
runBatch F (ϕ ∘ f) (B -> C) s <⋆> (ϕ ∘ f) a =
runBatch F ϕ (B -> C) (mapfst_Batch A1 A2 f s) <⋆>
ϕ (f a)
nowrewrite IHs.Qed.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
forall (A2B : Type) (ϕ : A2 -> F B) (A1 : Type)
(f : A1 -> A2) (C : Type),
runBatch F (ϕ ∘ f) C =
runBatch F ϕ C ∘ mapfst_Batch A1 A2 f
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
forall (A2B : Type) (ϕ : A2 -> F B) (A1 : Type)
(f : A1 -> A2) (C : Type),
runBatch F (ϕ ∘ f) C =
runBatch F ϕ C ∘ mapfst_Batch A1 A2 f
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A2, B: Type ϕ: A2 -> F B A1: Type f: A1 -> A2 C: Type
runBatch F (ϕ ∘ f) C =
runBatch F ϕ C ∘ mapfst_Batch A1 A2 f
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A2, B: Type ϕ: A2 -> F B A1: Type f: A1 -> A2 C: Type s: Batch A1 B C
runBatch F (ϕ ∘ f) C s =
(runBatch F ϕ C ∘ mapfst_Batch A1 A2 f) s
apply runBatch_mapfst.Qed.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
forall (AB2C : Type) (s : Batch A B2 C) (B1 : Type)
(ϕ : A -> F B1) (f : B1 -> B2),
runBatch F (map F f ∘ ϕ) C s =
runBatch F ϕ C (mapsnd_Batch B1 B2 f s)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F
forall (AB2C : Type) (s : Batch A B2 C) (B1 : Type)
(ϕ : A -> F B1) (f : B1 -> B2),
runBatch F (map F f ∘ ϕ) C s =
runBatch F ϕ C (mapsnd_Batch B1 B2 f s)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type s: Batch A B2 C B1: Type ϕ: A -> F B1 f: B1 -> B2
runBatch F (map F f ∘ ϕ) C s =
runBatch F ϕ C (mapsnd_Batch B1 B2 f s)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type c: C B1: Type ϕ: A -> F B1 f: B1 -> B2
runBatch F (map F f ∘ ϕ) C (Done A B2 C c) =
runBatch F ϕ C (mapsnd_Batch B1 B2 f (Done A B2 C c))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type s: Batch A B2 (B2 -> C) a: A B1: Type ϕ: A -> F B1 f: B1 -> B2 IHs: runBatch F (map F f ∘ ϕ) (B2 -> C) s =
runBatch F ϕ (B2 -> C) (mapsnd_Batch B1 B2 f s)
runBatch F (map F f ∘ ϕ) C (s ⧆ a) =
runBatch F ϕ C (mapsnd_Batch B1 B2 f (s ⧆ a))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type c: C B1: Type ϕ: A -> F B1 f: B1 -> B2
runBatch F (map F f ∘ ϕ) C (Done A B2 C c) =
runBatch F ϕ C (mapsnd_Batch B1 B2 f (Done A B2 C c))
easy.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type s: Batch A B2 (B2 -> C) a: A B1: Type ϕ: A -> F B1 f: B1 -> B2 IHs: runBatch F (map F f ∘ ϕ) (B2 -> C) s =
runBatch F ϕ (B2 -> C) (mapsnd_Batch B1 B2 f s)
runBatch F (map F f ∘ ϕ) C (s ⧆ a) =
runBatch F ϕ C (mapsnd_Batch B1 B2 f (s ⧆ a))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type s: Batch A B2 (B2 -> C) a: A B1: Type ϕ: A -> F B1 f: B1 -> B2 IHs: runBatch F (map F f ∘ ϕ) (B2 -> C) s =
runBatch F ϕ (B2 -> C) (mapsnd_Batch B1 B2 f s)
runBatch F (map F f ∘ ϕ) C (s ⧆ a) =
runBatch F ϕ C (mapsnd_Batch B1 B2 f (s ⧆ a))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type s: Batch A B2 (B2 -> C) a: A B1: Type ϕ: A -> F B1 f: B1 -> B2 IHs: runBatch F (map F f ∘ ϕ) (B2 -> C) s =
runBatch F ϕ (B2 -> C) (mapsnd_Batch B1 B2 f s)
runBatch F (map F f ∘ ϕ) (B2 -> C) s <⋆>
(map F f ∘ ϕ) a =
runBatch F ϕ (B1 -> C)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f s)) <⋆> ϕ a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type s: Batch A B2 (B2 -> C) a: A B1: Type ϕ: A -> F B1 f: B1 -> B2 IHs: runBatch F (map F f ∘ ϕ) (B2 -> C) s =
runBatch F ϕ (B2 -> C) (mapsnd_Batch B1 B2 f s)
runBatch F (map F f ∘ ϕ) (B2 -> C) s <⋆> map F f (ϕ a) =
runBatch F ϕ (B1 -> C)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f s)) <⋆> ϕ a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type s: Batch A B2 (B2 -> C) a: A B1: Type ϕ: A -> F B1 f: B1 -> B2 IHs: runBatch F (map F f ∘ ϕ) (B2 -> C) s =
runBatch F ϕ (B2 -> C) (mapsnd_Batch B1 B2 f s)
map F (precompose f)
(runBatch F (map F f ∘ ϕ) (B2 -> C) s) <⋆> ϕ a =
runBatch F ϕ (B1 -> C)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f s)) <⋆> ϕ a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type s: Batch A B2 (B2 -> C) a: A B1: Type ϕ: A -> F B1 f: B1 -> B2 IHs: runBatch F (map F f ∘ ϕ) (B2 -> C) s =
runBatch F ϕ (B2 -> C) (mapsnd_Batch B1 B2 f s)
map F (precompose f)
(runBatch F (map F f ∘ ϕ) (B2 -> C) s) =
runBatch F ϕ (B1 -> C)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f s))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B2, C: Type s: Batch A B2 (B2 -> C) a: A B1: Type ϕ: A -> F B1 f: B1 -> B2 IHs: runBatch F (map F f ∘ ϕ) (B2 -> C) s =
runBatch F ϕ (B2 -> C) (mapsnd_Batch B1 B2 f s)
map F (precompose f)
(runBatch F ϕ (B2 -> C) (mapsnd_Batch B1 B2 f s)) =
runBatch F ϕ (B1 -> C)
(map (Batch A B1) (precompose f)
(mapsnd_Batch B1 B2 f s))
nowrewrite natural_runBatch.Qed.Context
`{homomorphism: ApplicativeMorphism F G ψ}.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type b: Batch A B C
ψ C (runBatch F ϕ C b) = runBatch G (ψ B ∘ ϕ) C b
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type b: Batch A B C
ψ C (runBatch F ϕ C b) = runBatch G (ψ B ∘ ϕ) C b
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type c: C
ψ C (runBatch F ϕ C (Done A B C c)) =
runBatch G (ψ B ∘ ϕ) C (Done A B C c)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type b: Batch A B (B -> C) a: A IHb: ψ (B -> C) (runBatch F ϕ (B -> C) b) =
runBatch G (ψ B ∘ ϕ) (B -> C) b
ψ C (runBatch F ϕ C (b ⧆ a)) =
runBatch G (ψ B ∘ ϕ) C (b ⧆ a)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type c: C
ψ C (runBatch F ϕ C (Done A B C c)) =
runBatch G (ψ B ∘ ϕ) C (Done A B C c)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type c: C
ψ C (pure F c) = pure G c
nowrewrite appmor_pure.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type b: Batch A B (B -> C) a: A IHb: ψ (B -> C) (runBatch F ϕ (B -> C) b) =
runBatch G (ψ B ∘ ϕ) (B -> C) b
ψ C (runBatch F ϕ C (b ⧆ a)) =
runBatch G (ψ B ∘ ϕ) C (b ⧆ a)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type b: Batch A B (B -> C) a: A IHb: ψ (B -> C) (runBatch F ϕ (B -> C) b) =
runBatch G (ψ B ∘ ϕ) (B -> C) b
ψ C (runBatch F ϕ (B -> C) b <⋆> ϕ a) =
runBatch G (ψ B ∘ ϕ) (B -> C) b <⋆> (ψ B ∘ ϕ) a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type b: Batch A B (B -> C) a: A IHb: ψ (B -> C) (runBatch F ϕ (B -> C) b) =
runBatch G (ψ B ∘ ϕ) (B -> C) b
ψ (B -> C) (runBatch F ϕ (B -> C) b) <⋆> ψ B (ϕ a) =
runBatch G (ψ B ∘ ϕ) (B -> C) b <⋆> (ψ B ∘ ϕ) a
nowrewrite IHb.Qed.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B
forallC : Type,
ψ C ∘ runBatch F ϕ C = runBatch G (ψ B ∘ ϕ) C
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B
forallC : Type,
ψ C ∘ runBatch F ϕ C = runBatch G (ψ B ∘ ϕ) C
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type
ψ C ∘ runBatch F ϕ C = runBatch G (ψ B ∘ ϕ) C
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type b: Batch A B C
(ψ C ∘ runBatch F ϕ C) b = runBatch G (ψ B ∘ ϕ) C b
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type b: Batch A B C
ψ C (runBatch F ϕ C b) = runBatch G (ψ B ○ ϕ) C b
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F G: Type -> Type H0: Map F H1: Mult F H2: Pure F H3: Map G H4: Mult G H5: Pure G ψ: forallA : Type, F A -> G A homomorphism: ApplicativeMorphism F G ψ A, B: Type ϕ: A -> F B C: Type b: Batch A B C
runBatch G (ψ B ∘ ϕ) C b = runBatch G (ψ B ○ ϕ) C b
reflexivity.Qed.EndrunBatch_naturality.(** ** <<runBatch>> as an Applicative Homomorphism **)(**********************************************************************)SectionrunBatch_morphism.Context
`{Applicative F}
`{ϕ: A -> F B}.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
foralla : A,
runBatch F ϕ A (pure (Batch A B) a) = pure F a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
foralla : A,
runBatch F ϕ A (pure (Batch A B) a) = pure F a
easy.Qed.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
forall (CD : Type) (x : Batch A B C)
(y : Batch A B D),
runBatch F ϕ (C * D) (x ⊗ y) =
runBatch F ϕ C x ⊗ runBatch F ϕ D y
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
forall (CD : Type) (x : Batch A B C)
(y : Batch A B D),
runBatch F ϕ (C * D) (x ⊗ y) =
runBatch F ϕ C x ⊗ runBatch F ϕ D y
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, D: Type x: Batch A B C y: Batch A B D
runBatch F ϕ (C * D) (x ⊗ y) =
runBatch F ϕ C x ⊗ runBatch F ϕ D y
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, D: Type y: Batch A B D
forallx : Batch A B C,
runBatch F ϕ (C * D) (x ⊗ y) =
runBatch F ϕ C x ⊗ runBatch F ϕ D y
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type any: ANY
forallx : Batch A B C,
runBatch F ϕ (C * ANY) (x ⊗ Done A B ANY any) =
runBatch F ϕ C x ⊗ runBatch F ϕ ANY (Done A B ANY any)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A IH: forallx : Batch A B C,
runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) =
runBatch F ϕ C x ⊗ runBatch F ϕ (B -> ANY) rest
forallx : Batch A B C,
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
runBatch F ϕ C x ⊗ runBatch F ϕ ANY (rest ⧆ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type any: ANY
forallx : Batch A B C,
runBatch F ϕ (C * ANY) (x ⊗ Done A B ANY any) =
runBatch F ϕ C x ⊗ runBatch F ϕ ANY (Done A B ANY any)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type any: ANY x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ Done A B ANY any) =
runBatch F ϕ C x ⊗ runBatch F ϕ ANY (Done A B ANY any)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type any: ANY x: Batch A B C
runBatch F ϕ (C * ANY)
(map (Batch A B) (pair_right any) x) =
runBatch F ϕ C x ⊗ runBatch F ϕ ANY (Done A B ANY any)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type any: ANY x: Batch A B C
runBatch F ϕ (C * ANY)
(map (Batch A B) (pair_right any) x) =
runBatch F ϕ C x ⊗ pure F any
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type any: ANY x: Batch A B C
runBatch F ϕ (C * ANY)
(map (Batch A B) (pair_right any) x) =
map F (funb : C => (b, any)) (runBatch F ϕ C x)
nowrewrite natural_runBatch.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A IH: forallx : Batch A B C,
runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) =
runBatch F ϕ C x ⊗ runBatch F ϕ (B -> ANY) rest
forallx : Batch A B C,
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
runBatch F ϕ C x ⊗ runBatch F ϕ ANY (rest ⧆ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A IH: forallx : Batch A B C,
runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) =
runBatch F ϕ C x ⊗ runBatch F ϕ (B -> ANY) rest x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
runBatch F ϕ C x ⊗ runBatch F ϕ ANY (rest ⧆ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A IH: forallx : Batch A B C,
runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) =
runBatch F ϕ C x ⊗ runBatch F ϕ (B -> ANY) rest x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
runBatch F ϕ C x
⊗ (runBatch F ϕ (B -> ANY) rest <⋆> ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A IH: forallx : Batch A B C,
runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) =
runBatch F ϕ C x ⊗ runBatch F ϕ (B -> ANY) rest x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
runBatch F ϕ C x
⊗ map F (fun '(f, a) => f a)
(runBatch F ϕ (B -> ANY) rest ⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A IH: forallx : Batch A B C,
runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) =
runBatch F ϕ C x ⊗ runBatch F ϕ (B -> ANY) rest x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
map F (map_snd (fun '(f, a) => f a))
(runBatch F ϕ C x
⊗ (runBatch F ϕ (B -> ANY) rest ⊗ ϕ x'))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A IH: forallx : Batch A B C,
runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) =
runBatch F ϕ C x ⊗ runBatch F ϕ (B -> ANY) rest x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
map F (map_snd (fun '(f, a) => f a))
(map F associator
(runBatch F ϕ C x ⊗ runBatch F ϕ (B -> ANY) rest
⊗ ϕ x'))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A IH: forallx : Batch A B C,
runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) =
runBatch F ϕ C x ⊗ runBatch F ϕ (B -> ANY) rest x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
map F (map_snd (fun '(f, a) => f a))
(map F associator
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x'))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
map F (map_snd (fun '(f, a) => f a))
(map F associator
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x'))
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
(map F (map_snd (fun '(f, a) => f a))
∘ map F associator)
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
runBatch F ϕ (C * ANY) (x ⊗ (rest ⧆ x')) =
map F (map_snd (fun '(f, a) => f a) ∘ associator)
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
runBatch F ϕ (B -> C * ANY)
(map (Batch A B) strength_arrow (mult_Batch x rest)) <⋆>
ϕ x' =
map F (map_snd (fun '(f, a) => f a) ∘ associator)
(runBatch F ϕ (C * (B -> ANY)) (mult_Batch x rest)
⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
map F (fun '(f, a) => f a)
(runBatch F ϕ (B -> C * ANY)
(map (Batch A B) strength_arrow
(mult_Batch x rest)) ⊗ ϕ x') =
map F (map_snd (fun '(f, a) => f a) ∘ associator)
(runBatch F ϕ (C * (B -> ANY)) (mult_Batch x rest)
⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
map F (fun '(f, a) => f a)
(runBatch F ϕ (B -> C * ANY)
(map (Batch A B) strength_arrow (x ⊗ rest))
⊗ ϕ x') =
map F (map_snd (fun '(f, a) => f a) ∘ associator)
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
map F (fun '(f, a) => f a)
(map F strength_arrow
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest)) ⊗
ϕ x') =
map F (map_snd (fun '(f, a) => f a) ∘ associator)
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
map F (fun '(f, a) => f a)
(map F (map_fst strength_arrow)
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x')) =
map F (map_snd (fun '(f, a) => f a) ∘ associator)
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
(map F (fun '(f, a) => f a)
∘ map F (map_fst strength_arrow))
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x') =
map F (map_snd (fun '(f, a) => f a) ∘ associator)
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
map F ((fun '(f, a) => f a) ∘ map_fst strength_arrow)
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x') =
map F (map_snd (fun '(f, a) => f a) ∘ associator)
(runBatch F ϕ (C * (B -> ANY)) (x ⊗ rest) ⊗ ϕ x')
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B C, ANY: Type rest: Batch A B (B -> ANY) x': A x: Batch A B C
(fun '(f, a) => f a) ∘ map_fst strength_arrow =
map_snd (fun '(f, a) => f a) ∘ associator
now ext [[? ?] ?].Qed.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
ApplicativeMorphism (Batch A B) F (runBatch F ϕ)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
ApplicativeMorphism (Batch A B) F (runBatch F ϕ)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
forall (A0B0 : Type) (f : A0 -> B0)
(x : Batch A B A0),
runBatch F ϕ B0 (map (Batch A B) f x) =
map F f (runBatch F ϕ A0 x)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
forall (A0 : Type) (a : A0),
runBatch F ϕ A0 (pure (Batch A B) a) = pure F a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
forall (A0B0 : Type) (x : Batch A B A0)
(y : Batch A B B0),
runBatch F ϕ (A0 * B0) (x ⊗ y) =
runBatch F ϕ A0 x ⊗ runBatch F ϕ B0 y
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
forall (A0B0 : Type) (f : A0 -> B0)
(x : Batch A B A0),
runBatch F ϕ B0 (map (Batch A B) f x) =
map F f (runBatch F ϕ A0 x)
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B A0, B0: Type f: A0 -> B0 x: Batch A B A0
runBatch F ϕ B0 (map (Batch A B) f x) =
map F f (runBatch F ϕ A0 x)
nowrewrite natural_runBatch.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
forall (A0 : Type) (a : A0),
runBatch F ϕ A0 (pure (Batch A B) a) = pure F a
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B A0: Type a: A0
runBatch F ϕ A0 (pure (Batch A B) a) = pure F a
easy.
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B
forall (A0B0 : Type) (x : Batch A B A0)
(y : Batch A B B0),
runBatch F ϕ (A0 * B0) (x ⊗ y) =
runBatch F ϕ A0 x ⊗ runBatch F ϕ B0 y
F: Type -> Type Map_G: Map F Pure_G: Pure F Mult_G: Mult F H: Applicative F A, B: Type ϕ: A -> F B A0, B0: Type x: Batch A B A0 y: Batch A B B0
runBatch F ϕ (A0 * B0) (x ⊗ y) =
runBatch F ϕ A0 x ⊗ runBatch F ϕ B0 y
apply appmor_mult_runBatch.Qed.EndrunBatch_morphism.(** * <<Batch>> as a Parameterized Monad *)(**********************************************************************)Sectionparameterised_monad.(** ** Operations <<batch>> and <<join_Batch>> *)(********************************************************************)Definitionbatch (AB: Type): A -> Batch A B B :=
Step A B B (Done A B (B -> B) (@id B)).Fixpointjoin_Batch {ABCD: Type}
(b: Batch (Batch A B C) C D): Batch A B D :=
match b with
| Done _ _ _ d => Done _ _ _ d
| Step _ _ _ rest a =>
ap (Batch A B) (@join_Batch A B C (C -> D) rest) a
end.
A, B, C, D: Type
forall (rest : Batch (Batch A B C) C (C -> D))
(b : Batch A B C),
join_Batch (rest ⧆ b) = join_Batch rest <⋆> b
A, B, C, D: Type
forall (rest : Batch (Batch A B C) C (C -> D))
(b : Batch A B C),
join_Batch (rest ⧆ b) = join_Batch rest <⋆> b
reflexivity.Qed.(** ** <<join_Batch>> as <<runBatch (Batch A B) id>> *)(********************************************************************)
forallABC : Type,
@join_Batch A B C = runBatch (Batch A B) id
forallABC : Type,
@join_Batch A B C = runBatch (Batch A B) id
A, B, C: Type
@join_Batch A B C = runBatch (Batch A B) id
A, B, C, D: Type b: Batch (Batch A B C) C D
join_Batch b = runBatch (Batch A B) id D b
A, B, C, D: Type d: D
join_Batch (Done (Batch A B C) C D d) =
runBatch (Batch A B) id D (Done (Batch A B C) C D d)
A, B, C, D: Type rest: Batch (Batch A B C) C (C -> D) a: Batch A B C IHrest: join_Batch rest =
runBatch (Batch A B) id (C -> D) rest
join_Batch (rest ⧆ a) =
runBatch (Batch A B) id D (rest ⧆ a)
A, B, C, D: Type d: D
join_Batch (Done (Batch A B C) C D d) =
runBatch (Batch A B) id D (Done (Batch A B C) C D d)
reflexivity.
A, B, C, D: Type rest: Batch (Batch A B C) C (C -> D) a: Batch A B C IHrest: join_Batch rest =
runBatch (Batch A B) id (C -> D) rest
join_Batch (rest ⧆ a) =
runBatch (Batch A B) id D (rest ⧆ a)
A, B, C, D: Type rest: Batch (Batch A B C) C (C -> D) a: Batch A B C IHrest: join_Batch rest =
runBatch (Batch A B) id (C -> D) rest
join_Batch rest <⋆> a =
runBatch (Batch A B) id D (rest ⧆ a)
A, B, C, D: Type rest: Batch (Batch A B C) C (C -> D) a: Batch A B C IHrest: join_Batch rest =
runBatch (Batch A B) id (C -> D) rest
runBatch (Batch A B) id (C -> D) rest <⋆> a =
runBatch (Batch A B) id D (rest ⧆ a)
mapfst_Batch A1 A2 f ∘ batch A1 B = batch A2 B ∘ f
A1, A2, B: Type f: A1 -> A2
mapfst_Batch A1 A2 f ∘ batch A1 B = batch A2 B ∘ f
reflexivity.Qed.
A, B1, B2: Type f: B1 -> B2
mapsnd_Batch B1 B2 f ∘ batch A B2 =
map (Batch A B1) f ∘ batch A B1
A, B1, B2: Type f: B1 -> B2
mapsnd_Batch B1 B2 f ∘ batch A B2 =
map (Batch A B1) f ∘ batch A B1
reflexivity.Qed.(** ** <<join>> as an Applicative Homomorphism *)(********************************************************************)
forallABC : Type,
ApplicativeMorphism (Batch (Batch A B C) C)
(Batch A B) (@join_Batch A B C)
forallABC : Type,
ApplicativeMorphism (Batch (Batch A B C) C)
(Batch A B) (@join_Batch A B C)
A, B, C: Type
ApplicativeMorphism (Batch (Batch A B C) C)
(Batch A B) (@join_Batch A B C)
A, B, C: Type
ApplicativeMorphism (Batch (Batch A B C) C)
(Batch A B) (runBatch (Batch A B) id)
apply ApplicativeMorphism_runBatch.Qed.(** ** Other Laws *)(********************************************************************)
forall (G : Type -> Type) (Map_G : Map G)
(Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (AB : Type) (f : A -> G B),
runBatch G f B ∘ batch A B = f
forall (G : Type -> Type) (Map_G : Map G)
(Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (AB : Type) (f : A -> G B),
runBatch G f B ∘ batch A B = f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type f: A -> G B
runBatch G f B ∘ batch A B = f
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type f: A -> G B a: A
(runBatch G f B ∘ batch A B) a = f a
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B: Type f: A -> G B a: A
pure G id <⋆> f a = f a
nowrewrite ap1.Qed.
forallAB : Type,
runBatch (Batch A B) (batch A B) B = id
forallAB : Type,
runBatch (Batch A B) (batch A B) B = id
A, B: Type
runBatch (Batch A B) (batch A B) B = id
A, B: Type b: Batch A B B
runBatch (Batch A B) (batch A B) B b = id b
A, B, C: Type c: C
runBatch (Batch A B) (batch A B) C (Done A B C c) =
id (Done A B C c)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = id rest
runBatch (Batch A B) (batch A B) C (rest ⧆ a) =
id (rest ⧆ a)
A, B, C: Type c: C
runBatch (Batch A B) (batch A B) C (Done A B C c) =
id (Done A B C c)
reflexivity.
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = id rest
runBatch (Batch A B) (batch A B) C (rest ⧆ a) =
id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = id rest
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B) strength_arrow
(map (Batch A B) (func : B -> C => (c, id))
(runBatch (Batch A B) (batch A B) (B -> C)
rest))) ⧆ a = id (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B) strength_arrow
(map (Batch A B)
(func : B -> C => (c, funx : B => x))
(runBatch (Batch A B) (batch A B) (B -> C)
rest))) ⧆ a = rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B) strength_arrow
(map (Batch A B)
(func : B -> C => (c, funx : B => x))
(runBatch (Batch A B) (batch A B) (B -> C)
rest))) = rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B) strength_arrow
(map (Batch A B)
(func : B -> C => (c, funx : B => x)) rest)) =
rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
map (Batch A B) (compose (fun '(f, a) => f a))
((map (Batch A B) strength_arrow
∘ map (Batch A B)
(func : B -> C => (c, funx : B => x))) rest) =
rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B)
(strength_arrow
∘ (func : B -> C => (c, funx : B => x))) rest) =
rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
(map (Batch A B) (compose (fun '(f, a) => f a))
∘ map (Batch A B)
(strength_arrow
∘ (func : B -> C => (c, funx : B => x)))) rest =
rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
map (Batch A B)
(compose (fun '(f, a) => f a)
∘ (strength_arrow
∘ (func : B -> C => (c, funx : B => x)))) rest =
rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
map (Batch A B)
(funa : B -> C =>
fst (a, funx : B => x) ○ snd (a, funx : B => x))
rest = rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
map (Batch A B)
(funa : B -> C =>
fst (a, funx : B => x) ○ snd (a, funx : B => x))
rest = id rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch (Batch A B) (batch A B)
(B -> C) rest = rest
map (Batch A B)
(funa : B -> C =>
fst (a, funx : B => x) ○ snd (a, funx : B => x))
rest = map (Batch A B) id rest
forallABC : Type,
join_Batch ∘ batch (Batch A B C) C = id
forallABC : Type,
join_Batch ∘ batch (Batch A B C) C = id
A, B, C: Type
join_Batch ∘ batch (Batch A B C) C = id
A, B, C: Type b: Batch A B C
(join_Batch ∘ batch (Batch A B C) C) b = id b
A, B, C: Type b: Batch A B C
join_Batch (batch (Batch A B C) C b) = b
A, B, C: Type c: C
join_Batch (batch (Batch A B C) C (Done A B C c)) =
Done A B C c
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(batch (Batch A B (B -> C)) (B -> C) rest) =
rest
join_Batch (batch (Batch A B C) C (rest ⧆ a)) =
rest ⧆ a
A, B, C: Type c: C
join_Batch (batch (Batch A B C) C (Done A B C c)) =
Done A B C c
reflexivity.
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(batch (Batch A B (B -> C)) (B -> C) rest) =
rest
join_Batch (batch (Batch A B C) C (rest ⧆ a)) =
rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(batch (Batch A B (B -> C)) (B -> C) rest) =
rest
join_Batch
(Done (Batch A B C) C (C -> C) id ⧆ (rest ⧆ a)) =
rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(batch (Batch A B (B -> C)) (B -> C) rest) =
rest
Done A B (C -> C) id <⋆> (rest ⧆ a) = rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(batch (Batch A B (B -> C)) (B -> C) rest) =
rest
pure (Batch A B) id <⋆> (rest ⧆ a) = rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(batch (Batch A B (B -> C)) (B -> C) rest) =
rest
rest ⧆ a = rest ⧆ a
reflexivity.Qed.
forallABC : Type,
join_Batch ∘ mapfst_Batch A (Batch A B B) (batch A B) =
id
forallABC : Type,
join_Batch ∘ mapfst_Batch A (Batch A B B) (batch A B) =
id
A, B, C: Type
join_Batch ∘ mapfst_Batch A (Batch A B B) (batch A B) =
id
A, B, C: Type b: Batch A B C
(join_Batch ∘ mapfst_Batch A (Batch A B B) (batch A B))
b = id b
A, B, C: Type b: Batch A B C
join_Batch
(mapfst_Batch A (Batch A B B) (batch A B) b) = b
A, B, C: Type c: C
join_Batch
(mapfst_Batch A (Batch A B B) (batch A B)
(Done A B C c)) = Done A B C c
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
join_Batch
(mapfst_Batch A (Batch A B B) (batch A B) (rest ⧆ a)) =
rest ⧆ a
A, B, C: Type c: C
join_Batch
(mapfst_Batch A (Batch A B B) (batch A B)
(Done A B C c)) = Done A B C c
reflexivity.
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
join_Batch
(mapfst_Batch A (Batch A B B) (batch A B) (rest ⧆ a)) =
rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B) strength_arrow
(map (Batch A B) (func : B -> C => (c, id))
(join_Batch
(mapfst_Batch A (Batch A B B) (batch A B)
rest)))) ⧆ a = rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B) strength_arrow
(map (Batch A B) (func : B -> C => (c, id)) rest))
⧆ a = rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B) strength_arrow
(map (Batch A B) (func : B -> C => (c, id)) rest)) =
rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
map (Batch A B) (compose (fun '(f, a) => f a))
((map (Batch A B) strength_arrow
∘ map (Batch A B) (func : B -> C => (c, id)))
rest) = rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B)
(strength_arrow ∘ (func : B -> C => (c, id)))
rest) = rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
(map (Batch A B) (compose (fun '(f, a) => f a))
∘ map (Batch A B)
(strength_arrow ∘ (func : B -> C => (c, id))))
rest = rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
map (Batch A B)
(compose (fun '(f, a) => f a)
∘ (strength_arrow ∘ (func : B -> C => (c, id))))
rest = rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
map (Batch A B) id rest = rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
id =
compose (fun '(f, a0) => f a0)
∘ (strength_arrow ∘ (func : B -> C => (c, id)))
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
id =
compose (fun '(f, a0) => f a0)
∘ (strength_arrow ∘ (func : B -> C => (c, id)))
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
compose (fun '(f, a0) => f a0)
∘ (strength_arrow ∘ (func : B -> C => (c, id))) = id
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest f: B -> C b: B
(compose (fun '(f, a0) => f a0)
∘ (strength_arrow ∘ (func : B -> C => (c, id)))) f b =
id f b
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest f: B -> C b: B
fst (f, funx : B => x) (snd (f, funx : B => x) b) =
f b
reflexivity.
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
map (Batch A B) id rest = rest
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: join_Batch
(mapfst_Batch A (Batch A B B)
(batch A B) rest) = rest
id rest = rest
reflexivity.Qed.#[local] InstanceMap_Batch_Fst (B: Type):
Map (funA => Batch A B B) :=
funABf => mapfst_Batch _ _ f.#[local] InstanceReturn_Batch (B: Type):
Return (funA => Batch A B B) :=
(funA => batch A B).#[local] InstanceJoin_Batch (B: Type):
Join (funA => Batch A B B) :=
funA => @join_Batch A B B B.
forallB : Type, Monad BATCH1 B B
forallB : Type, Monad BATCH1 B B
B: Type
Monad BATCH1 B B
B: Type
Functor BATCH1 B B
B: Type
Natural (@ret BATCH1 B B (Return_Batch B))
B: Type
Natural (@join BATCH1 B B (Join_Batch B))
B: Type
forallA : Type, join ∘ ret = id
B: Type
forallA : Type, join ∘ map BATCH1 B B ret = id
B: Type
forallA : Type,
join ∘ join = join ∘ map BATCH1 B B join
B: Type
Functor BATCH1 B B
typeclasses eauto.
B: Type
Natural (@ret BATCH1 B B (Return_Batch B))
B: Type
Functor (funA : Type => A)
B: Type
Functor BATCH1 B B
B: Type
forall (AB0 : Type) (f : A -> B0),
map BATCH1 B B f ∘ ret =
ret ∘ map (funA0 : Type => A0) f
B: Type
Functor (funA : Type => A)
typeclasses eauto.
B: Type
Functor BATCH1 B B
typeclasses eauto.
B: Type
forall (AB0 : Type) (f : A -> B0),
map BATCH1 B B f ∘ ret =
ret ∘ map (funA0 : Type => A0) f
B: Type
forall (AB0 : Type) (f : A -> B0),
mapfst_Batch A B0 f ∘ ret =
ret ∘ map (funA0 : Type => A0) f
B: Type
forall (AB0 : Type) (f : A -> B0),
mapfst_Batch A B0 f ∘ batch A B =
batch B0 B ∘ map (funA0 : Type => A0) f
B: Type
forall (AB0 : Type) (f : A -> B0),
mapfst_Batch A B0 f ∘ batch A B = batch B0 B ∘ f
reflexivity.
B: Type
Natural (@join BATCH1 B B (Join_Batch B))
admit.
B: Type
forallA : Type, join ∘ ret = id
B: Type
forallA : Type,
join_Batch ∘ batch (Batch A B B) B = id
B, A: Type
join_Batch ∘ batch (Batch A B B) B = id
B, A: Type b: Batch A B B
(join_Batch ∘ batch (Batch A B B) B) b = id b
B, A, C: Type c: C
(join_Batch ∘ batch (Batch A B C) C) (Done A B C c) =
id (Done A B C c)
B, A, C: Type b: Batch A B (B -> C) a: A IHb: (join_Batch ∘ batch (Batch A B (B -> C)) (B -> C)) b = id b
(join_Batch ∘ batch (Batch A B C) C) (b ⧆ a) =
id (b ⧆ a)
B, A, C: Type c: C
(join_Batch ∘ batch (Batch A B C) C) (Done A B C c) =
id (Done A B C c)
reflexivity.
B, A, C: Type b: Batch A B (B -> C) a: A IHb: (join_Batch ∘ batch (Batch A B (B -> C)) (B -> C)) b = id b
(join_Batch ∘ batch (Batch A B C) C) (b ⧆ a) =
id (b ⧆ a)
B, A, C: Type b: Batch A B (B -> C) a: A IHb: (join_Batch ∘ batch (Batch A B (B -> C)) (B -> C)) b = id b
map (Batch A B) (compose (fun '(f, a) => f a))
(map (Batch A B) strength_arrow
(mult_Batch (Done A B (C -> C) id) b)) ⧆ a =
id (b ⧆ a)
Abort.Endparameterised_monad.(** * <<Batch>> as a Parameterized Comonad *)(**********************************************************************)Sectionparameterized.#[local] Unset Implicit Arguments.(** ** Operations <<extract_Batch>> and <<cojoin_Batch>> *)(********************************************************************)Fixpointextract_Batch {AB: Type} (b: Batch A A B): B :=
match b with
| Done _ _ _ b => b
| Step _ _ _ rest a => extract_Batch rest a
end.Fixpointcojoin_Batch {ABCD: Type} (b: Batch A C D):
Batch A B (Batch B C D) :=
match b with
| Done _ _ _ d => Done A B (Batch B C D) (Done B C D d)
| Step _ _ _ rest a =>
Step A B (Batch B C D)
(map (Batch A B) (Step B C D) (cojoin_Batch rest)) a
end.(** ** Rewriting Principles *)(********************************************************************)
forall (AC : Type) (c : C),
extract_Batch (Done A A C c) = c
forall (AC : Type) (c : C),
extract_Batch (Done A A C c) = c
reflexivity.Qed.
forall (AB : Type) (rest : Batch A A (A -> B))
(a : A),
extract_Batch (rest ⧆ a) = extract_Batch rest a
forall (AB : Type) (rest : Batch A A (A -> B))
(a : A),
extract_Batch (rest ⧆ a) = extract_Batch rest a
reflexivity.Qed.
forall (ABCD : Type) (d : D),
cojoin_Batch (Done A C D d) =
Done A B (Batch B C D) (Done B C D d)
forall (ABCD : Type) (d : D),
cojoin_Batch (Done A C D d) =
Done A B (Batch B C D) (Done B C D d)
reflexivity.Qed.
forall (ABCD : Type) (rest : Batch A C (C -> D))
(a : A),
cojoin_Batch (rest ⧆ a) =
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a
forall (ABCD : Type) (rest : Batch A C (C -> D))
(a : A),
cojoin_Batch (rest ⧆ a) =
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a
reflexivity.Qed.(** ** <<extract_Batch>> as <<runBatch (fun A => A) id>> *)(********************************************************************)
forallA : Type,
@extract_Batch A = runBatch (funA0 : Type => A0) id
forallA : Type,
@extract_Batch A = runBatch (funA0 : Type => A0) id
A: Type
@extract_Batch A = runBatch (funA : Type => A) id
A, B: Type b: Batch A A B
extract_Batch b = runBatch (funA : Type => A) id B b
A, C: Type c: C
extract_Batch (Done A A C c) =
runBatch (funA : Type => A) id C (Done A A C c)
A, C: Type b: Batch A A (A -> C) a: A IHb: extract_Batch b = runBatch (funA : Type => A) id (A -> C) b
extract_Batch (b ⧆ a) =
runBatch (funA : Type => A) id C (b ⧆ a)
A, C: Type c: C
extract_Batch (Done A A C c) =
runBatch (funA : Type => A) id C (Done A A C c)
reflexivity.
A, C: Type b: Batch A A (A -> C) a: A IHb: extract_Batch b = runBatch (funA : Type => A) id (A -> C) b
extract_Batch (b ⧆ a) =
runBatch (funA : Type => A) id C (b ⧆ a)
A, C: Type b: Batch A A (A -> C) a: A IHb: extract_Batch b = runBatch (funA : Type => A) id (A -> C) b
extract_Batch b a =
runBatch (funA : Type => A) id (A -> C) b (id a)
A, C: Type b: Batch A A (A -> C) a: A IHb: extract_Batch b = runBatch (funA : Type => A) id (A -> C) b
runBatch (funA : Type => A) id (A -> C) b a =
runBatch (funA : Type => A) id (A -> C) b (id a)
reflexivity.Qed.(** ** <<cojoin_Batch>> as <<runBatch double_batch>> *)(********************************************************************)Definitiondouble_batch {ABC: Type}:
A -> Batch A B (Batch B C C) :=
map (Batch A B) (batch B C) ∘ (batch A B).
A, B, C: Type a: A
double_batch a =
Done A B (B -> Batch B C C) (batch B C) ⧆ a
A, B, C: Type a: A
double_batch a =
Done A B (B -> Batch B C C) (batch B C) ⧆ a
reflexivity.Qed.
forallABC : Type,
double_batch = batch B C ⋆2 batch A B
forallABC : Type,
double_batch = batch B C ⋆2 batch A B
reflexivity.Qed.
forallABC : Type,
@cojoin_Batch A B C =
runBatch (Batch A B ∘ Batch B C) double_batch
forallABC : Type,
@cojoin_Batch A B C =
runBatch (Batch A B ∘ Batch B C) double_batch
A, B, C: Type
@cojoin_Batch A B C =
runBatch (Batch A B ∘ Batch B C) double_batch
A, B, C, D: Type
cojoin_Batch =
runBatch (Batch A B ∘ Batch B C) double_batch D
A, B, C, D: Type b: Batch A C D
cojoin_Batch b =
runBatch (Batch A B ∘ Batch B C) double_batch D b
A, B, C, D: Type d: D
cojoin_Batch (Done A C D d) =
runBatch (Batch A B ∘ Batch B C) double_batch D
(Done A C D d)
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
cojoin_Batch (rest ⧆ a) =
runBatch (Batch A B ∘ Batch B C) double_batch D
(rest ⧆ a)
A, B, C, D: Type d: D
cojoin_Batch (Done A C D d) =
runBatch (Batch A B ∘ Batch B C) double_batch D
(Done A C D d)
reflexivity.
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
cojoin_Batch (rest ⧆ a) =
runBatch (Batch A B ∘ Batch B C) double_batch D
(rest ⧆ a)
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (map (Batch B C) (fun '(f, a) => f a)))
(map (Batch A B) (compose (mult (Batch B C)))
(map (Batch A B) strength_arrow
(map (Batch A B)
(func : Batch B C (C -> D) =>
(c, batch B C ∘ id))
(runBatch (Batch A B ∘ Batch B C)
double_batch (C -> D) rest)))) ⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (map (Batch B C) (fun '(f, a) => f a)))
(map (Batch A B) (compose (mult (Batch B C)))
((map (Batch A B) strength_arrow
∘ map (Batch A B)
(func : Batch B C (C -> D) =>
(c, batch B C ∘ id)))
(runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest))) ⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (map (Batch B C) (fun '(f, a) => f a)))
(map (Batch A B) (compose (mult (Batch B C)))
(map (Batch A B)
(strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id)))
(runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest))) ⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (map (Batch B C) (fun '(f, a) => f a)))
((map (Batch A B) (compose (mult (Batch B C)))
∘ map (Batch A B)
(strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id))))
(runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest)) ⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (map (Batch B C) (fun '(f, a) => f a)))
(map (Batch A B)
(compose (mult (Batch B C))
∘ (strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id))))
(runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest)) ⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a =
(map (Batch A B)
(compose (map (Batch B C) (fun '(f, a) => f a)))
∘ map (Batch A B)
(compose (mult (Batch B C))
∘ (strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id)))))
(runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest) ⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (map (Batch B C) (fun '(f, a) => f a))
∘ (compose (mult (Batch B C))
∘ (strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id)))))
(runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest) ⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (map (Batch B C) (fun '(f, a) => f a))
∘ (compose (mult (Batch B C))
∘ (strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id)))))
(cojoin_Batch rest) ⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
map (Batch A B) (Step B C D) (cojoin_Batch rest) =
map (Batch A B)
(compose (map (Batch B C) (fun '(f, a) => f a))
∘ (compose (mult (Batch B C))
∘ (strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id)))))
(cojoin_Batch rest)
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch rest =
runBatch (Batch A B ∘ Batch B C) double_batch
(C -> D) rest
Step B C D =
compose (map (Batch B C) (fun '(f, a) => f a))
∘ (compose (mult (Batch B C))
∘ (strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id))))
B, C, D: Type
Step B C D =
compose (map (Batch B C) (fun '(f, a) => f a))
∘ (compose (mult (Batch B C))
∘ (strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id))))
B, C, D: Type rest: Batch B C (C -> D) b: B
rest ⧆ b =
(compose (map (Batch B C) (fun '(f, a) => f a))
∘ (compose (mult (Batch B C))
∘ (strength_arrow
∘ (func : Batch B C (C -> D) =>
(c, batch B C ∘ id))))) rest b
B, C, D: Type rest: Batch B C (C -> D) b: B
rest ⧆ b =
map (Batch B C) (compose (fun '(f, a) => f a))
(map (Batch B C) strength_arrow
(map (Batch B C) (func : C -> D => (c, id)) rest))
⧆ id b
B, C, D: Type rest: Batch B C (C -> D) b: B
rest ⧆ b =
map (Batch B C)
(fun (f : C -> (C -> D) * C) (a : C) =>
let '(f0, a0) := f a in f0 a0)
(map (Batch B C) strength_arrow
(map (Batch B C)
(func : C -> D => (c, funx : C => x)) rest))
⧆ b
B, C, D: Type rest: Batch B C (C -> D) b: B
rest =
map (Batch B C)
(fun (f : C -> (C -> D) * C) (a : C) =>
let '(f0, a0) := f a in f0 a0)
(map (Batch B C) strength_arrow
(map (Batch B C)
(func : C -> D => (c, funx : C => x)) rest))
B, C, D: Type rest: Batch B C (C -> D) b: B
rest =
map (Batch B C)
(fun (f : C -> (C -> D) * C) (a : C) =>
let '(f0, a0) := f a in f0 a0)
((map (Batch B C) strength_arrow
∘ map (Batch B C)
(func : C -> D => (c, funx : C => x))) rest)
B, C, D: Type rest: Batch B C (C -> D) b: B
rest =
map (Batch B C)
(fun (f : C -> (C -> D) * C) (a : C) =>
let '(f0, a0) := f a in f0 a0)
(map (Batch B C)
(strength_arrow
∘ (func : C -> D => (c, funx : C => x))) rest)
B, C, D: Type rest: Batch B C (C -> D) b: B
rest =
(map (Batch B C)
(fun (f : C -> (C -> D) * C) (a : C) =>
let '(f0, a0) := f a in f0 a0)
∘ map (Batch B C)
(strength_arrow
∘ (func : C -> D => (c, funx : C => x)))) rest
B, C, D: Type rest: Batch B C (C -> D) b: B
rest =
map (Batch B C)
((fun (f : C -> (C -> D) * C) (a : C) =>
let '(f0, a0) := f a in f0 a0)
∘ (strength_arrow
∘ (func : C -> D => (c, funx : C => x)))) rest
B, C, D: Type rest: Batch B C (C -> D) b: B
rest = id rest
reflexivity.Qed.(** ** <<extract_Batch>> and <<cojoin_Batch>> as Applicative Homomorphisms *)(********************************************************************)
forallA : Type,
ApplicativeMorphism (Batch A A) (funA0 : Type => A0)
(@extract_Batch A)
forallA : Type,
ApplicativeMorphism (Batch A A) (funA0 : Type => A0)
(@extract_Batch A)
A: Type
ApplicativeMorphism (Batch A A) (funA : Type => A)
(@extract_Batch A)
A: Type
ApplicativeMorphism (Batch A A) (funA : Type => A)
(runBatch (funA : Type => A) id)
apply ApplicativeMorphism_runBatch.Qed.
forallABC : Type,
ApplicativeMorphism (Batch A C)
(Batch A B ∘ Batch B C) (@cojoin_Batch A B C)
forallABC : Type,
ApplicativeMorphism (Batch A C)
(Batch A B ∘ Batch B C) (@cojoin_Batch A B C)
A, B, C: Type
ApplicativeMorphism (Batch A C)
(Batch A B ∘ Batch B C) (@cojoin_Batch A B C)
A, B, C: Type
ApplicativeMorphism (Batch A C)
(Batch A B ∘ Batch B C)
(runBatch (Batch A B ∘ Batch B C) double_batch)
apply ApplicativeMorphism_runBatch.Qed.(** ** Composition with <<ret>>/<<batch>> *)(********************************************************************)
forallA : Type, extract_Batch ∘ batch A A = id
forallA : Type, extract_Batch ∘ batch A A = id
reflexivity.Qed.
forallABC : Type,
cojoin_Batch ∘ batch A C = double_batch
forallABC : Type,
cojoin_Batch ∘ batch A C = double_batch
A, B, C: Type
cojoin_Batch ∘ batch A C = double_batch
A, B, C: Type
runBatch (Batch A B ∘ Batch B C) double_batch C
∘ batch A C = double_batch
forallb : Batch A A C,
extract_Batch (map (Batch A A) f b) =
f (extract_Batch b)
A, C, D: Type f: C -> D
forallb : Batch A A C,
extract_Batch (map (Batch A A) f b) =
f (extract_Batch b)
A, C, D: Type f: C -> D b: Batch A A C
extract_Batch (map (Batch A A) f b) =
f (extract_Batch b)
A, C: Type b: Batch A A C
forall (D : Type) (f : C -> D),
extract_Batch (map (Batch A A) f b) =
f (extract_Batch b)
A, C: Type c: C D: Type f: C -> D
extract_Batch (map (Batch A A) f (Done A A C c)) =
f (extract_Batch (Done A A C c))
A, C: Type rest: Batch A A (A -> C) a: A IHrest: forall (D : Type) (f : (A -> C) -> D),
extract_Batch (map (Batch A A) f rest) =
f (extract_Batch rest) D: Type f: C -> D
extract_Batch (map (Batch A A) f (rest ⧆ a)) =
f (extract_Batch (rest ⧆ a))
A, C: Type c: C D: Type f: C -> D
extract_Batch (map (Batch A A) f (Done A A C c)) =
f (extract_Batch (Done A A C c))
reflexivity.
A, C: Type rest: Batch A A (A -> C) a: A IHrest: forall (D : Type) (f : (A -> C) -> D),
extract_Batch (map (Batch A A) f rest) =
f (extract_Batch rest) D: Type f: C -> D
extract_Batch (map (Batch A A) f (rest ⧆ a)) =
f (extract_Batch (rest ⧆ a))
A, C: Type rest: Batch A A (A -> C) a: A IHrest: forall (D : Type) (f : (A -> C) -> D),
extract_Batch (map (Batch A A) f rest) =
f (extract_Batch rest) D: Type f: C -> D
extract_Batch (map (Batch A A) (compose f) rest) a =
f (extract_Batch rest a)
nowrewrite IHrest.Qed.
A, B, C: Type f: A -> B
forallb : Batch A B C,
extract_Batch (mapfst_Batch A B f b) =
extract_Batch (mapsnd_Batch A B f b)
A, B, C: Type f: A -> B
forallb : Batch A B C,
extract_Batch (mapfst_Batch A B f b) =
extract_Batch (mapsnd_Batch A B f b)
A, B, C: Type f: A -> B b: Batch A B C
extract_Batch (mapfst_Batch A B f b) =
extract_Batch (mapsnd_Batch A B f b)
A, B: Type f: A -> B C: Type c: C
extract_Batch (mapfst_Batch A B f (Done A B C c)) =
extract_Batch (mapsnd_Batch A B f (Done A B C c))
A, B: Type f: A -> B C: Type rest: Batch A B (B -> C) a: A IHrest: extract_Batch (mapfst_Batch A B f rest) =
extract_Batch (mapsnd_Batch A B f rest)
extract_Batch (mapfst_Batch A B f (rest ⧆ a)) =
extract_Batch (mapsnd_Batch A B f (rest ⧆ a))
A, B: Type f: A -> B C: Type c: C
extract_Batch (mapfst_Batch A B f (Done A B C c)) =
extract_Batch (mapsnd_Batch A B f (Done A B C c))
reflexivity.
A, B: Type f: A -> B C: Type rest: Batch A B (B -> C) a: A IHrest: extract_Batch (mapfst_Batch A B f rest) =
extract_Batch (mapsnd_Batch A B f rest)
extract_Batch (mapfst_Batch A B f (rest ⧆ a)) =
extract_Batch (mapsnd_Batch A B f (rest ⧆ a))
A, B: Type f: A -> B C: Type rest: Batch A B (B -> C) a: A IHrest: extract_Batch (mapfst_Batch A B f rest) =
extract_Batch (mapsnd_Batch A B f rest)
extract_Batch (mapfst_Batch A B f rest) (f a) =
extract_Batch
(map (Batch A A) (precompose f)
(mapsnd_Batch A B f rest)) a
A, B: Type f: A -> B C: Type rest: Batch A B (B -> C) a: A IHrest: extract_Batch (mapfst_Batch A B f rest) =
extract_Batch (mapsnd_Batch A B f rest)
extract_Batch (mapsnd_Batch A B f rest) (f a) =
extract_Batch
(map (Batch A A) (precompose f)
(mapsnd_Batch A B f rest)) a
A, B: Type f: A -> B C: Type rest: Batch A B (B -> C) a: A IHrest: extract_Batch (mapfst_Batch A B f rest) =
extract_Batch (mapsnd_Batch A B f rest)
extract_Batch (mapsnd_Batch A B f rest) (f a) =
precompose f (extract_Batch (mapsnd_Batch A B f rest))
a
reflexivity.Qed.
A, B, C, D, E: Type f: D -> E
forallb : Batch A C D,
cojoin_Batch (map (Batch A C) f b) =
map (Batch A B) (map (Batch B C) f) (cojoin_Batch b)
A, B, C, D, E: Type f: D -> E
forallb : Batch A C D,
cojoin_Batch (map (Batch A C) f b) =
map (Batch A B) (map (Batch B C) f) (cojoin_Batch b)
A, B, C, D, E: Type f: D -> E b: Batch A C D
cojoin_Batch (map (Batch A C) f b) =
map (Batch A B) (map (Batch B C) f) (cojoin_Batch b)
A, B, C, D: Type b: Batch A C D
forall (E : Type) (f : D -> E),
cojoin_Batch (map (Batch A C) f b) =
map (Batch A B) (map (Batch B C) f) (cojoin_Batch b)
A, B, C, D: Type d: D E: Type f: D -> E
cojoin_Batch (map (Batch A C) f (Done A C D d)) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch (Done A C D d))
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: forall (E : Type) (f : (C -> D) -> E),
cojoin_Batch (map (Batch A C) f rest) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch rest) E: Type f: D -> E
cojoin_Batch (map (Batch A C) f (rest ⧆ a)) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch (rest ⧆ a))
A, B, C, D: Type d: D E: Type f: D -> E
cojoin_Batch (map (Batch A C) f (Done A C D d)) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch (Done A C D d))
reflexivity.
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: forall (E : Type) (f : (C -> D) -> E),
cojoin_Batch (map (Batch A C) f rest) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch rest) E: Type f: D -> E
cojoin_Batch (map (Batch A C) f (rest ⧆ a)) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch (rest ⧆ a))
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: forall (E : Type) (f : (C -> D) -> E),
cojoin_Batch (map (Batch A C) f rest) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch rest) E: Type f: D -> E
map (Batch A B) (Step B C E)
(cojoin_Batch (map (Batch A C) (compose f) rest))
⧆ a =
map (Batch A B) (compose (map (Batch B C) f))
(map (Batch A B) (Step B C D) (cojoin_Batch rest))
⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: forall (E : Type) (f : (C -> D) -> E),
cojoin_Batch (map (Batch A C) f rest) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch rest) E: Type f: D -> E
map (Batch A B) (Step B C E)
(map (Batch A B) (map (Batch B C) (compose f))
(cojoin_Batch rest)) ⧆ a =
map (Batch A B) (compose (map (Batch B C) f))
(map (Batch A B) (Step B C D) (cojoin_Batch rest))
⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: forall (E : Type) (f : (C -> D) -> E),
cojoin_Batch (map (Batch A C) f rest) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch rest) E: Type f: D -> E
(map (Batch A B) (Step B C E)
∘ map (Batch A B) (map (Batch B C) (compose f)))
(cojoin_Batch rest) ⧆ a =
(map (Batch A B) (compose (map (Batch B C) f))
∘ map (Batch A B) (Step B C D)) (cojoin_Batch rest)
⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: forall (E : Type) (f : (C -> D) -> E),
cojoin_Batch (map (Batch A C) f rest) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch rest) E: Type f: D -> E
map (Batch A B)
(Step B C E ∘ map (Batch B C) (compose f))
(cojoin_Batch rest) ⧆ a =
(map (Batch A B) (compose (map (Batch B C) f))
∘ map (Batch A B) (Step B C D)) (cojoin_Batch rest)
⧆ a
A, B, C, D: Type rest: Batch A C (C -> D) a: A IHrest: forall (E : Type) (f : (C -> D) -> E),
cojoin_Batch (map (Batch A C) f rest) =
map (Batch A B) (map (Batch B C) f)
(cojoin_Batch rest) E: Type f: D -> E
map (Batch A B)
(Step B C E ∘ map (Batch B C) (compose f))
(cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (map (Batch B C) f) ∘ Step B C D)
(cojoin_Batch rest) ⧆ a
reflexivity.Qed.
A, A', B, C, D: Type f: A -> A'
forallb : Batch A C D,
cojoin_Batch (mapfst_Batch A A' f b) =
mapfst_Batch A A' f (cojoin_Batch b)
A, A', B, C, D: Type f: A -> A'
forallb : Batch A C D,
cojoin_Batch (mapfst_Batch A A' f b) =
mapfst_Batch A A' f (cojoin_Batch b)
A, A', B, C, D: Type f: A -> A' b: Batch A C D
cojoin_Batch (mapfst_Batch A A' f b) =
mapfst_Batch A A' f (cojoin_Batch b)
A, A', B, C: Type f: A -> A' D: Type d: D
cojoin_Batch (mapfst_Batch A A' f (Done A C D d)) =
mapfst_Batch A A' f (cojoin_Batch (Done A C D d))
A, A', B, C: Type f: A -> A' D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch (mapfst_Batch A A' f rest) =
mapfst_Batch A A' f (cojoin_Batch rest)
cojoin_Batch (mapfst_Batch A A' f (rest ⧆ a)) =
mapfst_Batch A A' f (cojoin_Batch (rest ⧆ a))
A, A', B, C: Type f: A -> A' D: Type d: D
cojoin_Batch (mapfst_Batch A A' f (Done A C D d)) =
mapfst_Batch A A' f (cojoin_Batch (Done A C D d))
reflexivity.
A, A', B, C: Type f: A -> A' D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch (mapfst_Batch A A' f rest) =
mapfst_Batch A A' f (cojoin_Batch rest)
cojoin_Batch (mapfst_Batch A A' f (rest ⧆ a)) =
mapfst_Batch A A' f (cojoin_Batch (rest ⧆ a))
A, A', B, C: Type f: A -> A' D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch (mapfst_Batch A A' f rest) =
mapfst_Batch A A' f (cojoin_Batch rest)
map (Batch A' B) (Step B C D)
(cojoin_Batch (mapfst_Batch A A' f rest)) ⧆ f a =
mapfst_Batch A A' f
(map (Batch A B) (Step B C D) (cojoin_Batch rest))
⧆ f a
A, A', B, C: Type f: A -> A' D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch (mapfst_Batch A A' f rest) =
mapfst_Batch A A' f (cojoin_Batch rest)
map (Batch A' B) (Step B C D)
(mapfst_Batch A A' f (cojoin_Batch rest)) ⧆ f a =
mapfst_Batch A A' f
(map (Batch A B) (Step B C D) (cojoin_Batch rest))
⧆ f a
A, A', B, C: Type f: A -> A' D: Type rest: Batch A C (C -> D) a: A IHrest: cojoin_Batch (mapfst_Batch A A' f rest) =
mapfst_Batch A A' f (cojoin_Batch rest)
mapfst_Batch A A' f
(map (Batch A B) (Step B C D) (cojoin_Batch rest))
⧆ f a =
mapfst_Batch A A' f
(map (Batch A B) (Step B C D) (cojoin_Batch rest))
⧆ f a
reflexivity.Qed.
A, B, C, C', D: Type f: C -> C'
forallb : Batch A C' D,
cojoin_Batch (mapsnd_Batch C C' f b) =
map (Batch A B) (mapsnd_Batch C C' f) (cojoin_Batch b)
A, B, C, C', D: Type f: C -> C'
forallb : Batch A C' D,
cojoin_Batch (mapsnd_Batch C C' f b) =
map (Batch A B) (mapsnd_Batch C C' f) (cojoin_Batch b)
A, B, C, C', D: Type f: C -> C' b: Batch A C' D
cojoin_Batch (mapsnd_Batch C C' f b) =
map (Batch A B) (mapsnd_Batch C C' f) (cojoin_Batch b)
A, B, C', D: Type b: Batch A C' D
forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f b) =
map (Batch A B) (mapsnd_Batch C C' f) (cojoin_Batch b)
A, B, C', D: Type d: D C: Type f: C -> C'
cojoin_Batch (mapsnd_Batch C C' f (Done A C' D d)) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch (Done A C' D d))
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
cojoin_Batch (mapsnd_Batch C C' f (rest ⧆ a)) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch (rest ⧆ a))
A, B, C', D: Type d: D C: Type f: C -> C'
cojoin_Batch (mapsnd_Batch C C' f (Done A C' D d)) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch (Done A C' D d))
reflexivity.
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
cojoin_Batch (mapsnd_Batch C C' f (rest ⧆ a)) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch (rest ⧆ a))
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
map (Batch A B) (Step B C D)
(cojoin_Batch
(map (Batch A C) (precompose f)
(mapsnd_Batch C C' f rest))) ⧆ a =
map (Batch A B) (compose (mapsnd_Batch C C' f))
(map (Batch A B) (Step B C' D) (cojoin_Batch rest))
⧆ a
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
map (Batch A B) (Step B C D)
(map (Batch A B) (map (Batch B C) (precompose f))
(cojoin_Batch (mapsnd_Batch C C' f rest))) ⧆ a =
map (Batch A B) (compose (mapsnd_Batch C C' f))
(map (Batch A B) (Step B C' D) (cojoin_Batch rest))
⧆ a
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
(map (Batch A B) (Step B C D)
∘ map (Batch A B) (map (Batch B C) (precompose f)))
(cojoin_Batch (mapsnd_Batch C C' f rest)) ⧆ a =
(map (Batch A B) (compose (mapsnd_Batch C C' f))
∘ map (Batch A B) (Step B C' D)) (cojoin_Batch rest)
⧆ a
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
map (Batch A B)
(Step B C D ∘ map (Batch B C) (precompose f))
(cojoin_Batch (mapsnd_Batch C C' f rest)) ⧆ a =
(map (Batch A B) (compose (mapsnd_Batch C C' f))
∘ map (Batch A B) (Step B C' D)) (cojoin_Batch rest)
⧆ a
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
map (Batch A B)
(Step B C D ∘ map (Batch B C) (precompose f))
(cojoin_Batch (mapsnd_Batch C C' f rest)) ⧆ a =
map (Batch A B)
(compose (mapsnd_Batch C C' f) ∘ Step B C' D)
(cojoin_Batch rest) ⧆ a
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
map (Batch A B)
(Step B C D ∘ map (Batch B C) (precompose f))
(map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest)) ⧆ a =
map (Batch A B)
(compose (mapsnd_Batch C C' f) ∘ Step B C' D)
(cojoin_Batch rest) ⧆ a
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
(map (Batch A B)
(Step B C D ∘ map (Batch B C) (precompose f))
∘ map (Batch A B) (mapsnd_Batch C C' f))
(cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (mapsnd_Batch C C' f) ∘ Step B C' D)
(cojoin_Batch rest) ⧆ a
A, B, C', D: Type rest: Batch A C' (C' -> D) a: A IHrest: forall (C : Type) (f : C -> C'),
cojoin_Batch (mapsnd_Batch C C' f rest) =
map (Batch A B) (mapsnd_Batch C C' f)
(cojoin_Batch rest) C: Type f: C -> C'
map (Batch A B)
(Step B C D ∘ map (Batch B C) (precompose f)
∘ mapsnd_Batch C C' f) (cojoin_Batch rest) ⧆ a =
map (Batch A B)
(compose (mapsnd_Batch C C' f) ∘ Step B C' D)
(cojoin_Batch rest) ⧆ a
reflexivity.Qed.
A, B, B', C, D: Type f: B -> B'
forallb : Batch A C D,
map (Batch A B) (mapfst_Batch B B' f) (cojoin_Batch b) =
mapsnd_Batch B B' f (cojoin_Batch b)
A, B, B', C, D: Type f: B -> B'
forallb : Batch A C D,
map (Batch A B) (mapfst_Batch B B' f) (cojoin_Batch b) =
mapsnd_Batch B B' f (cojoin_Batch b)
A, B, B', C, D: Type f: B -> B' b: Batch A C D
map (Batch A B) (mapfst_Batch B B' f) (cojoin_Batch b) =
mapsnd_Batch B B' f (cojoin_Batch b)
A, B, B', C: Type f: B -> B' D: Type d: D
map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch (Done A C D d)) =
mapsnd_Batch B B' f (cojoin_Batch (Done A C D d))
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch (rest ⧆ a)) =
mapsnd_Batch B B' f (cojoin_Batch (rest ⧆ a))
A, B, B', C: Type f: B -> B' D: Type d: D
map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch (Done A C D d)) =
mapsnd_Batch B B' f (cojoin_Batch (Done A C D d))
reflexivity.
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch (rest ⧆ a)) =
mapsnd_Batch B B' f (cojoin_Batch (rest ⧆ a))
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
map (Batch A B) (compose (mapfst_Batch B B' f))
(map (Batch A B) (Step B C D) (cojoin_Batch rest))
⧆ a =
map (Batch A B) (precompose f)
(mapsnd_Batch B B' f
(map (Batch A B') (Step B' C D)
(cojoin_Batch rest))) ⧆ a
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
(map (Batch A B) (compose (mapfst_Batch B B' f))
∘ map (Batch A B) (Step B C D)) (cojoin_Batch rest)
⧆ a =
map (Batch A B) (precompose f)
(mapsnd_Batch B B' f
(map (Batch A B') (Step B' C D)
(cojoin_Batch rest))) ⧆ a
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
map (Batch A B)
(compose (mapfst_Batch B B' f) ∘ Step B C D)
(cojoin_Batch rest) ⧆ a =
map (Batch A B) (precompose f)
(mapsnd_Batch B B' f
(map (Batch A B') (Step B' C D)
(cojoin_Batch rest))) ⧆ a
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
map (Batch A B)
(compose (mapfst_Batch B B' f) ∘ Step B C D)
(cojoin_Batch rest) ⧆ a =
map (Batch A B) (precompose f)
(map (Batch A B) (Step B' C D)
(mapsnd_Batch B B' f (cojoin_Batch rest))) ⧆ a
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
map (Batch A B)
(compose (mapfst_Batch B B' f) ∘ Step B C D)
(cojoin_Batch rest) ⧆ a =
(map (Batch A B) (precompose f)
∘ map (Batch A B) (Step B' C D))
(mapsnd_Batch B B' f (cojoin_Batch rest)) ⧆ a
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
map (Batch A B)
(compose (mapfst_Batch B B' f) ∘ Step B C D)
(cojoin_Batch rest) ⧆ a =
map (Batch A B) (precompose f ∘ Step B' C D)
(mapsnd_Batch B B' f (cojoin_Batch rest)) ⧆ a
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
map (Batch A B)
(compose (mapfst_Batch B B' f) ∘ Step B C D)
(cojoin_Batch rest) ⧆ a =
map (Batch A B) (precompose f ∘ Step B' C D)
(map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest)) ⧆ a
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
(Step A B (Batch B' C D)
∘ map (Batch A B)
(compose (mapfst_Batch B B' f) ∘ Step B C D))
(cojoin_Batch rest) a =
(map (Batch A B) (precompose f ∘ Step B' C D)
∘ map (Batch A B) (mapfst_Batch B B' f))
(cojoin_Batch rest) ⧆ a
A, B, B', C: Type f: B -> B' D: Type rest: Batch A C (C -> D) a: A IHrest: map (Batch A B) (mapfst_Batch B B' f)
(cojoin_Batch rest) =
mapsnd_Batch B B' f (cojoin_Batch rest)
(Step A B (Batch B' C D)
∘ map (Batch A B)
(compose (mapfst_Batch B B' f) ∘ Step B C D))
(cojoin_Batch rest) a =
map (Batch A B)
(precompose f ∘ Step B' C D ∘ mapfst_Batch B B' f)
(cojoin_Batch rest) ⧆ a
forallABC : Type, extract_Batch ∘ cojoin_Batch = id
forallABC : Type, extract_Batch ∘ cojoin_Batch = id
A, B, C: Type
extract_Batch ∘ cojoin_Batch = id
A, B, C: Type b: Batch A B C
(extract_Batch ∘ cojoin_Batch) b = id b
A, B, C: Type b: Batch A B C
(extract_Batch ∘ cojoin_Batch) b = b
A, B, C: Type c: C
(extract_Batch ∘ cojoin_Batch) (Done A B C c) =
Done A B C c
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: (extract_Batch ∘ cojoin_Batch) rest = rest
(extract_Batch ∘ cojoin_Batch) (rest ⧆ a) = rest ⧆ a
A, B, C: Type c: C
(extract_Batch ∘ cojoin_Batch) (Done A B C c) =
Done A B C c
A, B, C: Type c: C
extract_Batch (cojoin_Batch (Done A B C c)) =
Done A B C c
A, B, C: Type c: C
Done A B C c = Done A B C c
reflexivity.
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: (extract_Batch ∘ cojoin_Batch) rest = rest
(extract_Batch ∘ cojoin_Batch) (rest ⧆ a) = rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: extract_Batch (cojoin_Batch rest) = rest
extract_Batch (cojoin_Batch (rest ⧆ a)) = rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: extract_Batch (cojoin_Batch rest) = rest
extract_Batch
(map (Batch A A) (Step A B C) (cojoin_Batch rest)) a =
rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: extract_Batch (cojoin_Batch rest) = rest
extract_Batch (cojoin_Batch rest) ⧆ a = rest ⧆ a
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: extract_Batch (cojoin_Batch rest) = rest
rest ⧆ a = rest ⧆ a
reflexivity.Qed.(* TODO Finish rest of the parameterized comonad structure. *)Endparameterized.(** * <<Batch>> is Traversable in the First Argument *)(**********************************************************************)Fixpointtraverse_Batch (BC: Type) (G: Type -> Type)
`{Map G} `{Pure G} `{Mult G} (A A': Type) (f: A -> G A')
(b: Batch A B C): G (Batch A' B C) :=
match b with
| Done _ _ _ c => pure G (Done A' B C c)
| Step _ _ _ rest a =>
pure G (Step A' B C) <⋆>
traverse_Batch B (B -> C) G A A' f rest <⋆>
f a
end.#[export] InstanceTraverse_Batch1:
forall (BC: Type), Traverse (BATCH1 B C) := traverse_Batch.(** ** Rewriting Principles *)(**********************************************************************)
forall (BC : Type) (G : Type -> Type) (H : Map G)
(H0 : Pure G) (H1 : Mult G) (AA' : Type)
(f : A -> G A') (c : C),
traverse f (Done A B C c) = pure G (Done A' B C c)
forall (BC : Type) (G : Type -> Type) (H : Map G)
(H0 : Pure G) (H1 : Mult G) (AA' : Type)
(f : A -> G A') (c : C),
traverse f (Done A B C c) = pure G (Done A' B C c)
reflexivity.Qed.
forall (BC : Type) (G : Type -> Type) (H : Map G)
(H0 : Pure G) (H1 : Mult G) (AA' : Type)
(f : A -> G A'),
traverse f ∘ pure (Batch A B) = pure (G ∘ Batch A' B)
forall (BC : Type) (G : Type -> Type) (H : Map G)
(H0 : Pure G) (H1 : Mult G) (AA' : Type)
(f : A -> G A'),
traverse f ∘ pure (Batch A B) = pure (G ∘ Batch A' B)
B, C: Type G: Type -> Type H: Map G H0: Pure G H1: Mult G A, A': Type f: A -> G A'
traverse f ∘ pure (Batch A B) = pure (G ∘ Batch A' B)
B, C: Type G: Type -> Type H: Map G H0: Pure G H1: Mult G A, A': Type f: A -> G A'
traverse f ∘ (func : C => Done A B C c) =
pure (G ∘ Batch A' B)
B, C: Type G: Type -> Type H: Map G H0: Pure G H1: Mult G A, A': Type f: A -> G A'
traverse f ∘ (func : C => Done A B C c) =
pure G ○ pure (Batch A' B)
B, C: Type G: Type -> Type H: Map G H0: Pure G H1: Mult G A, A': Type f: A -> G A'
traverse f ∘ (func : C => Done A B C c) =
pure G ○ Done A' B C
B, C: Type G: Type -> Type H: Map G H0: Pure G H1: Mult G A, A': Type f: A -> G A' c: C
traverse f (Done A B C c) = pure G (Done A' B C c)
B, C: Type G: Type -> Type H: Map G H0: Pure G H1: Mult G A, A': Type f: A -> G A' c: C
pure G (Done A' B C c) = pure G (Done A' B C c)
reflexivity.Qed.
forall (G : Type -> Type) (H : Map G) (H0 : Pure G)
(H1 : Mult G),
Applicative G ->
forall (BCAA' : Type) (f : A -> G A')
(k : Batch A B (B -> C)) (a : A),
traverse f (k ⧆ a) =
map G (Step A' B C) (traverse f k) <⋆> f a
forall (G : Type -> Type) (H : Map G) (H0 : Pure G)
(H1 : Mult G),
Applicative G ->
forall (BCAA' : Type) (f : A -> G A')
(k : Batch A B (B -> C)) (a : A),
traverse f (k ⧆ a) =
map G (Step A' B C) (traverse f k) <⋆> f a
G: Type -> Type H: Map G H0: Pure G H1: Mult G Applicative0: Applicative G B, C, A, A': Type f: A -> G A' k: Batch A B (B -> C) a: A
traverse f (k ⧆ a) =
map G (Step A' B C) (traverse f k) <⋆> f a
G: Type -> Type H: Map G H0: Pure G H1: Mult G Applicative0: Applicative G B, C, A, A': Type f: A -> G A' k: Batch A B (B -> C) a: A
pure G (Step A' B C) <⋆>
Traverse_Batch1 B (B -> C) G H H0 H1 A A' f k <⋆>
f a = map G (Step A' B C) (traverse f k) <⋆> f a
G: Type -> Type H: Map G H0: Pure G H1: Mult G Applicative0: Applicative G B, C, A, A': Type f: A -> G A' k: Batch A B (B -> C) a: A
map G (Step A' B C)
(Traverse_Batch1 B (B -> C) G H H0 H1 A A' f k) <⋆>
f a = map G (Step A' B C) (traverse f k) <⋆> f a
reflexivity.Qed.
forall (G : Type -> Type) (H : Map G) (H0 : Pure G)
(H1 : Mult G),
Applicative G ->
forall (BCAA' : Type) (f : A -> G A')
(k : Batch A B (B -> C)) (a : A),
traverse f (k ⧆ a) =
map G (Step A' B C) (traverse f k) <⋆> f a
forall (G : Type -> Type) (H : Map G) (H0 : Pure G)
(H1 : Mult G),
Applicative G ->
forall (BCAA' : Type) (f : A -> G A')
(k : Batch A B (B -> C)) (a : A),
traverse f (k ⧆ a) =
map G (Step A' B C) (traverse f k) <⋆> f a
G: Type -> Type H: Map G H0: Pure G H1: Mult G Applicative0: Applicative G B, C, A, A': Type f: A -> G A' k: Batch A B (B -> C) a: A
traverse f (k ⧆ a) =
map G (Step A' B C) (traverse f k) <⋆> f a
G: Type -> Type H: Map G H0: Pure G H1: Mult G Applicative0: Applicative G B, C, A, A': Type f: A -> G A' k: Batch A B (B -> C) a: A
map G (Step A' B C) (traverse f k) <⋆> f a =
map G (Step A' B C) (traverse f k) <⋆> f a
reflexivity.Qed.
forall (G : Type -> Type) (H : Map G) (H0 : Pure G)
(H1 : Mult G),
Applicative G ->
forallB : Type,
Type ->
forall (AA' : Type) (f : A -> G A') (XY : Type)
(lhs : Batch A B (X -> Y)) (rhs : Batch A B X),
traverse f (lhs <⋆> rhs) =
pure G (ap (Batch A' B)) <⋆> traverse f lhs <⋆>
traverse f rhs
forall (G : Type -> Type) (H : Map G) (H0 : Pure G)
(H1 : Mult G),
Applicative G ->
forallB : Type,
Type ->
forall (AA' : Type) (f : A -> G A') (XY : Type)
(lhs : Batch A B (X -> Y)) (rhs : Batch A B X),
traverse f (lhs <⋆> rhs) =
pure G (ap (Batch A' B)) <⋆> traverse f lhs <⋆>
traverse f rhs
G: Type -> Type H: Map G H0: Pure G H1: Mult G Applicative0: Applicative G B, C, A, A': Type f: A -> G A' X, Y: Type lhs: Batch A B (X -> Y) rhs: Batch A B X
traverse f (lhs <⋆> rhs) =
pure G (ap (Batch A' B)) <⋆> traverse f lhs <⋆>
traverse f rhs
G: Type -> Type H: Map G H0: Pure G H1: Mult G Applicative0: Applicative G B, C, A, A': Type f: A -> G A' X, Y: Type y: X -> Y rhs: Batch A B X
traverse f (Done A B (X -> Y) y <⋆> rhs) =
pure G (ap (Batch A' B)) <⋆>
traverse f (Done A B (X -> Y) y) <⋆> traverse f rhs
G: Type -> Type H: Map G H0: Pure G H1: Mult G Applicative0: Applicative G B, C, A, A': Type f: A -> G A' X, Y: Type lhs: Batch A B (B -> X -> Y) a: A rhs: Batch A B X
traverse f ((lhs ⧆ a) <⋆> rhs) =
pure G (ap (Batch A' B)) <⋆> traverse f (lhs ⧆ a) <⋆>
traverse f rhs
traverse (funx : A => x) (Done A B C c) =
Done A B C c
B, A, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse (funx : A => x) rest = rest
traverse (funx : A => x) (rest ⧆ a) = rest ⧆ a
B, A, C: Type c: C
traverse (funx : A => x) (Done A B C c) =
Done A B C c
B, A, C: Type c: C
pure (funX : Type => X) (Done A B C c) = Done A B C c
reflexivity.
B, A, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse (funx : A => x) rest = rest
traverse (funx : A => x) (rest ⧆ a) = rest ⧆ a
B, A, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse (funx : A => x) rest = rest
pure (funX : Type => X) (Step A B C)
(Traverse_Batch1 B (B -> C) (funX : Type => X)
Map_I Pure_I Mult_I A A (funx : A => x) rest) a =
rest ⧆ a
B, A, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse (funx : A => x) rest = rest
pure (funX : Type => X) (Step A B C)
(traverse (funx : A => x) rest) a = rest ⧆ a
B, A, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse (funx : A => x) rest = rest
pure (funX : Type => X) (Step A B C) rest a =
rest ⧆ a
reflexivity.Qed.
B, C: Type
forall (G1 : Type -> Type) (H0 : Map G1)
(H1 : Pure G1) (H2 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H4 : Map G2)
(H5 : Pure G2) (H6 : Mult G2),
Applicative G2 ->
forall (AA'A'' : Type) (g : A' -> G2 A'')
(f : A -> G1 A'),
map G1 (traverse g) ∘ traverse f = traverse (g ⋆2 f)
B, C: Type
forall (G1 : Type -> Type) (H0 : Map G1)
(H1 : Pure G1) (H2 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H4 : Map G2)
(H5 : Pure G2) (H6 : Mult G2),
Applicative G2 ->
forall (AA'A'' : Type) (g : A' -> G2 A'')
(f : A -> G1 A'),
map G1 (traverse g) ∘ traverse f = traverse (g ⋆2 f)
B, C: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A'
B, C: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' b: Batch A B C
(map G1 (traverse g) ∘ traverse f) b =
traverse (g ⋆2 f) b
B, C: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' b: Batch A B C
(map G1 (traverse g) ∘ traverse f) b =
traverse (g ⋆2 f) b
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type c: C
(map G1 (traverse g) ∘ traverse f) (Done A B C c) =
traverse (g ⋆2 f) (Done A B C c)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
traverse (g ⋆2 f) (rest ⧆ a)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type c: C
(map G1 (traverse g) ∘ traverse f) (Done A B C c) =
traverse (g ⋆2 f) (Done A B C c)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type c: C
(map G1 (traverse g) ∘ traverse f) (Done A B C c) =
pure (G1 ∘ G2) (Done A'' B C c)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type c: C
map G1 (traverse g) (traverse f (Done A B C c)) =
pure (G1 ○ G2) (Done A'' B C c)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type c: C
map G1 (traverse g) (pure G1 (Done A' B C c)) =
pure (G1 ○ G2) (Done A'' B C c)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type c: C
pure G1 (traverse g (Done A' B C c)) =
pure (G1 ○ G2) (Done A'' B C c)
reflexivity.
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
traverse (g ⋆2 f) (rest ⧆ a)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure (G1 ∘ G2) (Step A'' B C) <⋆>
Traverse_Batch1 B (B -> C) (G1 ∘ G2)
(Map_compose G1 G2) (Pure_compose G1 G2)
(Mult_compose G1 G2) A A'' (g ⋆2 f) rest <⋆>
(g ⋆2 f) a
(* RHS *)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure (G1 ∘ G2) (Step A'' B C) <⋆>
traverse (g ⋆2 f) rest <⋆> (g ⋆2 f) a
(* cleanup *)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1 (ap G2) <⋆>
(pure (G1 ∘ G2) (Step A'' B C) <⋆>
traverse (g ⋆2 f) rest) <⋆> (g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1 (ap G2) <⋆>
(pure G1 (ap G2) <⋆> pure (G1 ∘ G2) (Step A'' B C) <⋆>
traverse (g ⋆2 f) rest) <⋆> (g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
map G1 (ap G2)
(pure G1 (ap G2) <⋆> pure (G1 ∘ G2) (Step A'' B C) <⋆>
traverse (g ⋆2 f) rest) <⋆> (g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
map G1 (compose (ap G2))
(pure G1 (ap G2) <⋆> pure (G1 ∘ G2) (Step A'' B C)) <⋆>
traverse (g ⋆2 f) rest <⋆> (g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
map G1 (compose (compose (ap G2))) (pure G1 (ap G2)) <⋆>
pure (G1 ∘ G2) (Step A'' B C) <⋆>
traverse (g ⋆2 f) rest <⋆> (g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1 (compose (ap G2) ∘ ap G2) <⋆>
pure (G1 ∘ G2) (Step A'' B C) <⋆>
traverse (g ⋆2 f) rest <⋆> (g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1 (compose (ap G2) ∘ ap G2) <⋆>
pure G1 (pure G2 (Step A'' B C)) <⋆>
traverse (g ⋆2 f) rest <⋆> (g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1
((compose (ap G2) ∘ ap G2) (pure G2 (Step A'' B C))) <⋆>
traverse (g ⋆2 f) rest <⋆> (g ⋆2 f) a
(* deal with <<rest>> *)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1
((compose (ap G2) ∘ ap G2) (pure G2 (Step A'' B C))) <⋆>
(map G1 (traverse g) ∘ traverse f) rest <⋆> (g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1
((compose (ap G2) ∘ ap G2) (pure G2 (Step A'' B C))) <⋆>
map G1 (traverse g) (traverse f rest) <⋆> (g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
map G1 (precompose (traverse g))
(pure G1
((compose (ap G2) ∘ ap G2)
(pure G2 (Step A'' B C)))) <⋆> traverse f rest <⋆>
(g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1
(precompose (traverse g)
((compose (ap G2) ∘ ap G2)
(pure G2 (Step A'' B C)))) <⋆> traverse f rest <⋆>
(g ⋆2 f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1
(precompose (traverse g)
((compose (ap G2) ∘ ap G2)
(pure G2 (Step A'' B C)))) <⋆> traverse f rest <⋆>
(map G1 g ∘ f) a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1
(precompose (traverse g)
((compose (ap G2) ∘ ap G2)
(pure G2 (Step A'' B C)))) <⋆> traverse f rest <⋆>
map G1 g (f a)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
map G1 (precompose g)
(pure G1
(precompose (traverse g)
((compose (ap G2) ∘ ap G2)
(pure G2 (Step A'' B C)))) <⋆>
traverse f rest) <⋆> f a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
map G1 (compose (precompose g))
(pure G1
(precompose (traverse g)
((compose (ap G2) ∘ ap G2)
(pure G2 (Step A'' B C))))) <⋆>
traverse f rest <⋆> f a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
(map G1 (traverse g) ∘ traverse f) (rest ⧆ a) =
pure G1
(precompose g
∘ precompose (traverse g)
((compose (ap G2) ∘ ap G2)
(pure G2 (Step A'' B C)))) <⋆>
traverse f rest <⋆> f a
(* LHS *)
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
map G1 (traverse g)
(pure G1 (Step A' B C) <⋆>
Traverse_Batch1 B (B -> C) G1 H0 H1 H2 A A' f rest <⋆>
f a) =
pure G1
(precompose g
○ precompose (traverse g)
(ap G2 ○ ap G2 (pure G2 (Step A'' B C)))) <⋆>
traverse f rest <⋆> f a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
map G1 (traverse g)
(pure G1 (Step A' B C) <⋆> traverse f rest <⋆> f a) =
pure G1
(precompose g
○ precompose (traverse g)
(ap G2 ○ ap G2 (pure G2 (Step A'' B C)))) <⋆>
traverse f rest <⋆> f a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
map G1 (compose (traverse g))
(pure G1 (Step A' B C) <⋆> traverse f rest) <⋆>
f a =
pure G1
(precompose g
○ precompose (traverse g)
(ap G2 ○ ap G2 (pure G2 (Step A'' B C)))) <⋆>
traverse f rest <⋆> f a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
map G1 (compose (compose (traverse g)))
(pure G1 (Step A' B C)) <⋆> traverse f rest <⋆>
f a =
pure G1
(precompose g
○ precompose (traverse g)
(ap G2 ○ ap G2 (pure G2 (Step A'' B C)))) <⋆>
traverse f rest <⋆> f a
B: Type G1: Type -> Type H0: Map G1 H1: Pure G1 H2: Mult G1 H: Applicative G1 G2: Type -> Type H4: Map G2 H5: Pure G2 H6: Mult G2 H3: Applicative G2 A, A', A'': Type g: A' -> G2 A'' f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (map G1 (traverse g) ∘ traverse f) rest =
traverse (g ⋆2 f) rest
pure G1 (compose (traverse g) ∘ Step A' B C) <⋆>
traverse f rest <⋆> f a =
pure G1
(precompose g
○ precompose (traverse g)
(ap G2 ○ ap G2 (pure G2 (Step A'' B C)))) <⋆>
traverse f rest <⋆> f a
reflexivity.Qed.
forall (BC : Type) (G1G2 : Type -> Type)
(H : Map G1) (H0 : Mult G1) (H1 : Pure G1)
(H2 : Map G2) (H3 : Mult G2) (H4 : Pure G2)
(ϕ : forallA : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (AA' : Type) (f : A -> G1 A'),
ϕ (BATCH1 B C A') ∘ traverse f = traverse (ϕ A' ∘ f)
forall (BC : Type) (G1G2 : Type -> Type)
(H : Map G1) (H0 : Mult G1) (H1 : Pure G1)
(H2 : Map G2) (H3 : Mult G2) (H4 : Pure G2)
(ϕ : forallA : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (AA' : Type) (f : A -> G1 A'),
ϕ (BATCH1 B C A') ∘ traverse f = traverse (ϕ A' ∘ f)
B, C: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A'
ϕ (BATCH1 B C A') ∘ traverse f = traverse (ϕ A' ∘ f)
B, C: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' b: Batch A B C
(ϕ (Batch A' B C) ∘ traverse f) b =
traverse (ϕ A' ∘ f) b
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type c: C
(ϕ (Batch A' B C) ∘ traverse f) (Done A B C c) =
traverse (ϕ A' ∘ f) (Done A B C c)
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
(ϕ (Batch A' B C) ∘ traverse f) (rest ⧆ a) =
traverse (ϕ A' ∘ f) (rest ⧆ a)
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type c: C
(ϕ (Batch A' B C) ∘ traverse f) (Done A B C c) =
traverse (ϕ A' ∘ f) (Done A B C c)
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type c: C
ϕ (Batch A' B C) (pure G1 (Done A' B C c)) =
pure G2 (Done A' B C c)
nowrewrite appmor_pure.
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
(ϕ (Batch A' B C) ∘ traverse f) (rest ⧆ a) =
traverse (ϕ A' ∘ f) (rest ⧆ a)
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
(ϕ (Batch A' B C) ∘ traverse f) (rest ⧆ a) =
pure G2 (Step A' B C) <⋆>
Traverse_Batch1 B (B -> C) G2 H2 H4 H3 A A' (ϕ A' ∘ f)
rest <⋆> (ϕ A' ∘ f) a
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
ϕ (Batch A' B C) (traverse f (rest ⧆ a)) =
pure G2 (Step A' B C) <⋆>
Traverse_Batch1 B (B -> C) G2 H2 H4 H3 A A' (ϕ A' ∘ f)
rest <⋆> (ϕ A' ∘ f) a
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
ϕ (Batch A' B C)
(pure G1 (Step A' B C) <⋆>
Traverse_Batch1 B (B -> C) G1 H H1 H0 A A' f rest <⋆>
f a) =
pure G2 (Step A' B C) <⋆>
Traverse_Batch1 B (B -> C) G2 H2 H4 H3 A A' (ϕ A' ∘ f)
rest <⋆> (ϕ A' ∘ f) a
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
ϕ (Batch A' B C)
(pure G1 (Step A' B C) <⋆> traverse f rest <⋆> f a) =
pure G2 (Step A' B C) <⋆> traverse (ϕ A' ∘ f) rest <⋆>
(ϕ A' ∘ f) a
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
ϕ (Batch A' B C)
(pure G1 (Step A' B C) <⋆> traverse f rest <⋆> f a) =
pure G2 (Step A' B C) <⋆>
(ϕ (Batch A' B (B -> C)) ∘ traverse f) rest <⋆>
(ϕ A' ∘ f) a
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
ϕ (Batch A' B C)
(pure G1 (Step A' B C) <⋆> traverse f rest <⋆> f a) =
ϕ (Batch A' B (B -> C) -> A' -> Batch A' B C)
(pure G1 (Step A' B C)) <⋆>
(ϕ (Batch A' B (B -> C)) ∘ traverse f) rest <⋆>
(ϕ A' ∘ f) a
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
ϕ (A' -> Batch A' B C)
(pure G1 (Step A' B C) <⋆> traverse f rest) <⋆>
ϕ A' (f a) =
ϕ (Batch A' B (B -> C) -> A' -> Batch A' B C)
(pure G1 (Step A' B C)) <⋆>
(ϕ (Batch A' B (B -> C)) ∘ traverse f) rest <⋆>
(ϕ A' ∘ f) a
B: Type G1, G2: Type -> Type H: Map G1 H0: Mult G1 H1: Pure G1 H2: Map G2 H3: Mult G2 H4: Pure G2 ϕ: forallA : Type, G1 A -> G2 A H5: ApplicativeMorphism G1 G2 ϕ A, A': Type f: A -> G1 A' C: Type rest: Batch A B (B -> C) a: A IHrest: (ϕ (Batch A' B (B -> C)) ∘ traverse f) rest =
traverse (ϕ A' ∘ f) rest
ϕ (Batch A' B (B -> C) -> A' -> Batch A' B C)
(pure G1 (Step A' B C)) <⋆>
ϕ (Batch A' B (B -> C)) (traverse f rest) <⋆>
ϕ A' (f a) =
ϕ (Batch A' B (B -> C) -> A' -> Batch A' B C)
(pure G1 (Step A' B C)) <⋆>
(ϕ (Batch A' B (B -> C)) ∘ traverse f) rest <⋆>
(ϕ A' ∘ f) a
reflexivity.Qed.(** *** Typeclass Instance *)(**********************************************************************)#[export] InstanceTraversableFunctor_Batch: forall (BC: Type),
TraversableFunctor (BATCH1 B C) :=
funBC =>
{| trf_traverse_id := trf_traverse_id_Batch B C;
trf_traverse_traverse := @trf_traverse_traverse_Batch B C;
trf_traverse_morphism := @trf_traverse_morphism_Batch B C;
|}.(** *** Compatibility with <<map>> *)(**********************************************************************)
forallBC : Type,
@map BATCH1 B C Map_Batch1 =
@traverse BATCH1 B C (Traverse_Batch1 B C)
(funA : Type => A) Map_I Pure_I Mult_I
forallBC : Type,
@map BATCH1 B C Map_Batch1 =
@traverse BATCH1 B C (Traverse_Batch1 B C)
(funA : Type => A) Map_I Pure_I Mult_I
B, C: Type
@map BATCH1 B C Map_Batch1 =
@traverse BATCH1 B C (Traverse_Batch1 B C)
(funA : Type => A) Map_I Pure_I Mult_I
B, C, A, A': Type f: A -> A' b: Batch A B C
map BATCH1 B C f b = traverse f b
B, A, A': Type f: A -> A' C: Type c: C
map BATCH1 B C f (Done A B C c) =
traverse f (Done A B C c)
B, A, A': Type f: A -> A' C: Type rest: Batch A B (B -> C) a: A IHrest: map BATCH1 B (B -> C) f rest =
traverse f rest
map BATCH1 B C f (rest ⧆ a) = traverse f (rest ⧆ a)
B, A, A': Type f: A -> A' C: Type c: C
map BATCH1 B C f (Done A B C c) =
traverse f (Done A B C c)
reflexivity.
B, A, A': Type f: A -> A' C: Type rest: Batch A B (B -> C) a: A IHrest: map BATCH1 B (B -> C) f rest =
traverse f rest
map BATCH1 B C f (rest ⧆ a) = traverse f (rest ⧆ a)
B, A, A': Type f: A -> A' C: Type rest: Batch A B (B -> C) a: A IHrest: map BATCH1 B (B -> C) f rest =
traverse f rest
mapfst_Batch A A' f rest ⧆ f a =
pure (funA : Type => A) (Step A' B C)
(Traverse_Batch1 B (B -> C) (funA : Type => A)
Map_I Pure_I Mult_I A A' f rest) (f a)
B, A, A': Type f: A -> A' C: Type rest: Batch A B (B -> C) a: A IHrest: map BATCH1 B (B -> C) f rest =
traverse f rest
mapfst_Batch A A' f rest ⧆ f a =
pure (funA : Type => A) (Step A' B C)
(traverse f rest) (f a)
B, A, A': Type f: A -> A' C: Type rest: Batch A B (B -> C) a: A IHrest: map BATCH1 B (B -> C) f rest =
traverse f rest
mapfst_Batch A A' f rest ⧆ f a =
pure (funA : Type => A) (Step A' B C)
(map BATCH1 B (B -> C) f rest) (f a)
reflexivity.Qed.
forallBC : Type, Compat_Map_Traverse BATCH1 B C
forallBC : Type, Compat_Map_Traverse BATCH1 B C
B, C: Type
Compat_Map_Traverse BATCH1 B C
B, C: Type
Map_Batch1 = DerivedOperations.Map_Traverse BATCH1 B C
B, C, X, Y: Type f: X -> Y
Map_Batch1 X Y f =
DerivedOperations.Map_Traverse BATCH1 B C X Y f
B, C, X, Y: Type f: X -> Y
map BATCH1 B C f =
DerivedOperations.Map_Traverse BATCH1 B C X Y f
B, C, X, Y: Type f: X -> Y
traverse f =
DerivedOperations.Map_Traverse BATCH1 B C X Y f
reflexivity.Qed.(** ** <<runBatch>> Characterized by <<traverse>> *)(**********************************************************************)
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type
runBatch F ϕ C = map F extract_Batch ∘ traverse ϕ
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type
runBatch F ϕ C = map F extract_Batch ∘ traverse ϕ
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type
runBatch F ϕ C = map F extract_Batch ∘ traverse ϕ
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type b: Batch A B C
runBatch F ϕ C b =
(map F extract_Batch ∘ traverse ϕ) b
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type c: C
runBatch F ϕ C (Done A B C c) =
(map F extract_Batch ∘ traverse ϕ) (Done A B C c)
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
runBatch F ϕ C (rest ⧆ a) =
(map F extract_Batch ∘ traverse ϕ) (rest ⧆ a)
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type c: C
runBatch F ϕ C (Done A B C c) =
(map F extract_Batch ∘ traverse ϕ) (Done A B C c)
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type c: C
pure F c = map F extract_Batch (pure F (Done B B C c))
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type c: C
pure F c = pure F (extract_Batch (Done B B C c))
reflexivity.
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
runBatch F ϕ C (rest ⧆ a) =
(map F extract_Batch ∘ traverse ϕ) (rest ⧆ a)
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
runBatch F ϕ (B -> C) rest <⋆> ϕ a =
(map F extract_Batch ∘ traverse ϕ) (rest ⧆ a)
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
(map F extract_Batch ∘ traverse ϕ) rest <⋆> ϕ a =
(map F extract_Batch ∘ traverse ϕ) (rest ⧆ a)
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
map F extract_Batch (traverse ϕ rest) <⋆> ϕ a =
map F extract_Batch
(pure F (Step B B C) <⋆>
Traverse_Batch1 B (B -> C) F H H1 H0 A B ϕ rest <⋆>
ϕ a)
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
map F extract_Batch (traverse ϕ rest) <⋆> ϕ a =
map F extract_Batch
(pure F (Step B B C) <⋆> traverse ϕ rest <⋆> ϕ a)
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
map F extract_Batch (traverse ϕ rest) <⋆> ϕ a =
map F (compose extract_Batch)
(pure F (Step B B C) <⋆> traverse ϕ rest) <⋆> ϕ a
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
map F extract_Batch (traverse ϕ rest) <⋆> ϕ a =
map F (compose (compose extract_Batch))
(pure F (Step B B C)) <⋆> traverse ϕ rest <⋆> ϕ a
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
map F extract_Batch (traverse ϕ rest) <⋆> ϕ a =
pure F (compose extract_Batch ∘ Step B B C) <⋆>
traverse ϕ rest <⋆> ϕ a
A, B: Type F: Type -> Type H: Map F H0: Mult F H1: Pure F Applicative0: Applicative F ϕ: A -> F B C: Type rest: Batch A B (B -> C) a: A IHrest: runBatch F ϕ (B -> C) rest =
(map F extract_Batch ∘ traverse ϕ) rest
pure F extract_Batch <⋆> traverse ϕ rest <⋆> ϕ a =
pure F (compose extract_Batch ∘ Step B B C) <⋆>
traverse ϕ rest <⋆> ϕ a