# Some theorems about traversals in Coq 8.3pl4

```(* This files proves that the Identity and Composition laws of traversals
are equivalent to the laws of coalgebroid for an indexed Kleene store comonad.

Assumptions:
- functional extensionality
- an instance of a parametricity law
*)

Require Import FunctionalExtensionality.

Set Implicit Arguments.
Unset Strict Implicit.

Record Applicative := applicative
{ carrier :> Type -> Type
; pure : forall a, a -> carrier a
; ap : forall a b, carrier (a -> b) -> carrier a -> carrier b
; map := fun a b (f : a -> b) x => ap (pure f) x
; _ : forall (a : Type) x, map _ _ (fun (y : a) => y) x = x
; _ : forall a b c x y z,
ap (ap (map _ _ (fun (f : b -> c) (g : a -> b) (w:a) => f (g w)) x) y) z =
ap x (ap y z)
; _ : forall a b (f : a -> b) x, map _ _ f (pure x) = pure (f x)
; _ : forall a b (f : carrier (a -> b)) x,
ap f (pure x) = map _ _ (fun g => g x) f
}.

Record IdiomaticTransformation (F G:Applicative) := idomaticTransformation
{ transform :> forall a, F a -> G a
; _ : forall a (x:a), transform (pure F x) = pure G x
; _ : forall a b (f : F (a -> b)) x, transform (ap f x) = ap (transform f) (transform x)
}.

Definition TraversableSig a a' b b' := forall (f:Applicative), (b -> f b') -> (a -> f a').

Axiom parametricity_instance :
forall a a' b b' (t : TraversableSig a a' b b') F G (eta : IdiomaticTransformation F G) f x,
eta _ (t F f x) = t G (fun a => eta _ (f a)) x.

Lemma identity_law (F : Applicative) a (x : F a) : map (fun (y : a) => y) x = x.
Proof.
destruct F.
auto.
Qed.

Lemma composition_law (F : Applicative) a b c x y (z : F a) :
ap (ap (map (fun (f : b -> c) (g : a -> b) (w:a) => f (g w)) x) y) z =
ap x (ap y z).
Proof.
destruct F.
auto.
Qed.

Lemma homomorphism_law (F : Applicative) a b (f : a -> b) x :
ap (pure F f) (pure F x) = pure F (f x).
Proof.
fold (map f (pure F x)).
destruct F.
auto.
Qed.

Lemma interchange_law (F : Applicative) a b (f : F (a -> b)) x :
ap f (pure F x) = map (fun g => g x) f.
Proof.
destruct F.
auto.
Qed.

Definition IdApplicative : Applicative.
exists (fun A => A) (fun a (x : a) => x) (fun a b (f : a -> b) => f);
try reflexivity.
Defined.

Section ComposeApplicative.

Variable (F G :Applicative).

Let FG (a:Type) := F (G a).

Definition Compose_pure (a:Type) (x:a) : FG a :=
pure F (pure G x).

Definition Compose_ap (a b:Type) (f:FG (a -> b)) (x:FG a) : FG b :=
ap (ap (pure F (fun g x => ap g x)) f) x.

Lemma Compose_identity (a:Type) (x : FG a):
Compose_ap (Compose_pure (fun y : a => y)) x = x.
Proof.
unfold Compose_ap, Compose_pure.
rewrite homomorphism_law.
replace (fun x0 : G a => ap (a:=G) (a0:=a) (b:=a) (pure G (fun y : a => y)) x0)
with (fun (y : G a) => y).
apply identity_law.
apply functional_extensionality; intro y.
symmetry.
apply identity_law.
Qed.

Lemma Compose_composition (a b c:Type) x y (z : FG a) :
Compose_ap (Compose_ap (Compose_ap (Compose_pure (fun (f : b -> c) (g : a -> b) (w:a) => f (g w)))
x) y) z =
Compose_ap x (Compose_ap y z).
Proof.
unfold Compose_ap, Compose_pure.
repeat rewrite homomorphism_law.
repeat (unfold map; simpl; (repeat rewrite homomorphism_law); rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; (repeat rewrite homomorphism_law); rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
replace (fun (w : G (b -> c)) (w0 : G (a -> b)) (x0 : G a) =>
ap (a:=G) (a0:=a) (b:=c)
(ap (a:=G) (a0:=a -> b) (b:=a -> c)
(ap (a:=G) (a0:=b -> c) (b:=(a -> b) -> a -> c)
(pure G
(fun (f : b -> c) (g : a -> b) (w1 : a) => f (g w1)))
w) w0) x0)
with (fun (w : G (b -> c)) (w0 : G (a -> b)) (w1 : G a) =>
ap (a:=G) (a0:=b) (b:=c) w (ap (a:=G) (a0:=a) (b:=b) w0 w1)).
reflexivity.
repeat (apply functional_extensionality; intro).
symmetry.
apply composition_law.
Qed.

Lemma Compose_homomorphism a b (f : a -> b) x :
Compose_ap (Compose_pure f) (Compose_pure x) = Compose_pure (f x).
Proof.
unfold Compose_ap, Compose_pure.
repeat rewrite homomorphism_law.
reflexivity.
Qed.

Lemma Compose_interchange a b (f : FG (a -> b)) x :
Compose_ap f (Compose_pure x) = Compose_ap (Compose_pure (fun g => g x)) f.
Proof.
unfold Compose_ap, Compose_pure.
repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; (repeat rewrite homomorphism_law); rewrite <- composition_law).
repeat rewrite interchange_law.
unfold map; simpl; repeat rewrite homomorphism_law.
replace (fun w : G (a -> b) => ap (a:=G) (a0:=a) (b:=b) w (pure G x))
with (fun x0 : G (a -> b) =>
ap (a:=G) (a0:=a -> b) (b:=b) (pure G (fun g : a -> b => g x)) x0).
reflexivity.
apply functional_extensionality; intro.
symmetry.
apply interchange_law.
Qed.

Definition ComposeApplicative : Applicative.
exists FG Compose_pure Compose_ap.
apply Compose_identity.
apply Compose_composition.
apply Compose_homomorphism.
apply Compose_interchange.
Defined.

End ComposeApplicative.

Inductive KleeneStore (i j a : Type) :=
| Unit : a -> KleeneStore i j a
| Battery : KleeneStore i j (j -> a) -> i -> KleeneStore i j a.

Fixpoint KleeneStore_map (i j a b: Type) (f : (a -> b))
(x : KleeneStore i j a) : KleeneStore i j b :=
match x with
| Unit y => Unit _ _ (f y)
| Battery v a => Battery (KleeneStore_map (fun g z => f (g z)) v) a
end.

Lemma KleeneStore_map_id (i j a : Type) (x : KleeneStore i j a) :
KleeneStore_map (fun a => a) x = x.
Proof.
induction x.
reflexivity.
simpl.
replace (fun (g : j -> a) (z : j) => g z) with (fun (g : j -> a) => g).
rewrite IHx.
reflexivity.
apply functional_extensionality.
apply eta_expansion.
Qed.

Lemma KleeneStore_map_comp (i j a b c : Type) (f : b -> c) (g : a -> b)
(x : KleeneStore i j a) :
KleeneStore_map f (KleeneStore_map g x) = KleeneStore_map (fun a => f (g a)) x.
Proof.
revert b c f g.
induction x.
reflexivity.
simpl.
intros b c f g.
rewrite IHx.
reflexivity.
Qed.

Fixpoint KleeneStore_apH (i j a b c : Type) (h : c -> a -> b) (f : KleeneStore i j c) {struct f} :
KleeneStore i j a -> KleeneStore i j b :=
match f with
| Unit g => KleeneStore_map (h g)
| Battery v a => fun y =>
Battery (KleeneStore_apH (fun r s t => (h (r t) s)) v y) a
end.

Definition KleeneStore_ap (i j a b : Type) :
KleeneStore i j (a -> b) -> KleeneStore i j a -> KleeneStore i j b
:= KleeneStore_apH (fun x => x).

Lemma KleeneStore_map_ap i j a b (f : a -> b) x : KleeneStore_map f x =
KleeneStore_ap (Unit i j f) x.
Proof.
reflexivity.
Qed.

Lemma KleeneStore_identity i j a x : KleeneStore_ap (Unit i j (fun (y : a) => y)) x = x.
Proof.
induction x.
reflexivity.
unfold KleeneStore_ap in *; simpl in *.
replace (fun (g : j -> a) (z : j) => g z) with (fun (g : j -> a) => g).
rewrite IHx; reflexivity.
apply functional_extensionality.
apply eta_expansion.
Qed.

Lemma KleeneStore_apH_ap i j a b c h f x : @KleeneStore_apH i j a b c h f x =
KleeneStore_ap (KleeneStore_map h f) x.
Proof.
cut (forall i j a b c d h (g : d -> c) f x,
@KleeneStore_apH i j a b c h (KleeneStore_map g f) x =
KleeneStore_ap (KleeneStore_map (fun z => h (g z)) f) x).
intros H.
assert (H0 := H i j a b c c h (fun z => z) f x).
rewrite KleeneStore_map_ap, KleeneStore_identity in H0.
rewrite H0.
rewrite (eta_expansion h).
reflexivity.
clear i j a b c h f x.
intros i j a b c d h g f x.
revert b c g h.
induction f.
reflexivity.
intros b c g h.
unfold KleeneStore_ap; simpl.
rewrite IHf, IHf.
reflexivity.
Qed.

Lemma KleeneStore_interchange i j a b (f : KleeneStore i j (a -> b)) x :
KleeneStore_ap f (Unit i j x) = KleeneStore_ap (Unit i j (fun g => g x)) f.
Proof.
cut (forall i j a b c (h : c -> a -> b) (f : KleeneStore i j c) x,
KleeneStore_apH h f (Unit i j x) = KleeneStore_ap (Unit i j (fun g => h g x)) f).
intros H.
apply H.
clear i j a b f x.
intros i j a b c h f.
revert a b h.
induction f.
reflexivity.
intros a0 b h x.
unfold KleeneStore_ap; simpl.
rewrite IHf.
reflexivity.
Qed.

Lemma KleeneStore_composition i j a b c x y z :
KleeneStore_ap (KleeneStore_ap (KleeneStore_ap (Unit i j (fun (f : b -> c) (g : a -> b) (w:a) => f (g w))) x) y) z =
KleeneStore_ap x (KleeneStore_ap y z).
Proof.
unfold KleeneStore_ap; simpl.
cut (forall c0 c1 (h0 : c0 -> b -> c) (x0 : KleeneStore i j c0) (h1 : c1 -> a -> b) (y0 : KleeneStore i j c1),
KleeneStore_ap
(KleeneStore_ap
(KleeneStore_ap
(Unit i j (fun (f : b -> c) (g : a -> b) (w : a) => f (g w)))
(KleeneStore_map h0 x0)) (KleeneStore_map h1 y0)) z =
KleeneStore_apH h0 x0 (KleeneStore_apH h1 y0 z)).
intros H.
rewrite <- H, <- KleeneStore_map_ap.
do 2 rewrite (KleeneStore_map_ap (fun g => g)), KleeneStore_identity.
reflexivity.
clear x y.
assert (H : forall (a b c : Type) (h0 : b -> c) c0  (h1 : c0 -> a -> b) (z : KleeneStore i j a) (y : KleeneStore i j c0),
KleeneStore_ap
(KleeneStore_map (fun (a' : c0) (w : a) => h0 (h1 a' w)) y) z =
KleeneStore_map h0 (KleeneStore_apH h1 y z)).
clear - i j.
intros a b c h0 c0 h1 z y.
revert a b c h0 h1 z.
induction y; intros a' b c h0 h1 z; simpl.
rewrite KleeneStore_map_comp.
reflexivity.
rewrite <- IHy.
unfold KleeneStore_ap; simpl.
repeat rewrite KleeneStore_apH_ap.
repeat rewrite KleeneStore_map_comp.
reflexivity.
intros c0 c1 h0 x.
revert b c h0 c1 a z.
unfold KleeneStore_ap; simpl.
induction x; intros b c h0 c1 a' z h1 y; simpl.
generalize (h0 a0).
clear a h0 a0.
intros h0.
rewrite KleeneStore_map_comp.
apply H.
rewrite <- IHx.
repeat rewrite KleeneStore_map_comp.
repeat rewrite KleeneStore_apH_ap.
repeat rewrite KleeneStore_map_comp.
unfold KleeneStore_ap; simpl.
repeat (rewrite <- H; repeat rewrite KleeneStore_map_comp).
reflexivity.
Qed.

Definition KleeneStoreApplicative (i j : Type) : Applicative.
exists (KleeneStore i j) (Unit i j) (@KleeneStore_ap i j).
apply KleeneStore_identity.
apply KleeneStore_composition.
reflexivity.
apply KleeneStore_interchange.
Defined.

Canonical Structure KleeneStoreApplicative.

Fixpoint KleeneExtract i a (f : KleeneStore i i a) : a :=
match f with
| Unit x => x
| Battery v y => KleeneExtract v y
end.

Fixpoint KleeneDuplicate i j k a (f : KleeneStore i k a) :
KleeneStore i j (KleeneStore j k a) :=
match f with
| Unit x => Unit i j (Unit j k x)
| Battery v y => Battery (KleeneStore_map (@Battery _ _ _) (KleeneDuplicate j v)) y
end.

Lemma KleeneExtract_map i a b (f : a -> b) (x : KleeneStore i i a) :
KleeneExtract (KleeneStore_map f x) = f (KleeneExtract x).
Proof.
revert b f.
induction x; intros b f.
reflexivity.
simpl.
rewrite IHx.
reflexivity.
Qed.

Lemma KleeneDuplicate_map i j k a b (f : a -> b) (x : KleeneStore i k a) :
KleeneDuplicate j (KleeneStore_map f x) = KleeneStore_map (KleeneStore_map f) (KleeneDuplicate j x).
Proof.
revert b f.
induction x; intros b f.
reflexivity.
simpl.
rewrite IHx.
repeat rewrite KleeneStore_map_comp.
simpl.
replace (fun (a0 : KleeneStore j k (k -> a)) (z : j) =>
Battery (KleeneStore_map (fun (g : k -> a) (z0 : k) => f (g z0)) a0) z)
with (fun a0 : KleeneStore j k (k -> a) =>
Battery (KleeneStore_map (fun (g : k -> a) (z : k) => f (g z)) a0)).
reflexivity.
apply functional_extensionality; intro.
apply eta_expansion.
Qed.

Lemma KleeneStore_law1 i j a (x : KleeneStore i j a) :
KleeneExtract (KleeneDuplicate _ x) = x.
Proof.
induction x.
reflexivity.
simpl.
rewrite KleeneExtract_map.
rewrite IHx.
reflexivity.
Qed.

Lemma KleeneStore_law2 i j a (x : KleeneStore i j a) :
KleeneStore_map (@KleeneExtract _ _) (KleeneDuplicate _ x) = x.
Proof.
induction x.
reflexivity.
simpl.
rewrite KleeneStore_map_comp.
simpl.
replace (fun (a0 : KleeneStore j j (j -> a)) (z : j) => KleeneExtract a0 z)
with (@KleeneExtract j (j -> a)).
rewrite IHx.
reflexivity.
do 2 (apply functional_extensionality; intro).
reflexivity.
Qed.

Lemma KleeneStore_law3 i j k l a (x : KleeneStore i l a) :
KleeneDuplicate j (KleeneDuplicate k x) = KleeneStore_map (fun z => KleeneDuplicate k z) (KleeneDuplicate j x).
Proof.
induction x.
reflexivity.
simpl.
rewrite KleeneDuplicate_map, IHx.
repeat rewrite KleeneStore_map_comp.
simpl.
replace (fun (a0 : KleeneStore j l (l -> a)) (z : j) =>
@Battery j k (KleeneStore k l a)
(@KleeneStore_map j k (KleeneStore k l (l -> a))
(k -> KleeneStore k l a) (@Battery k l a)
(@KleeneDuplicate j k l (l -> a) a0)) z)
with (fun (a0 : KleeneStore j l (l -> a)) =>
Battery (KleeneStore_map (@Battery k l a) (KleeneDuplicate k a0))).
reflexivity.
do 2 (apply functional_extensionality; intro); reflexivity.
Qed.

Fixpoint experiment i j (F : Applicative) (g : i -> F j) a (k : KleeneStore i j a) :
F a :=
match k with
| Unit x => pure F x
| Battery v b => ap (map (fun x f => f x) (g b)) (experiment g v)
end.

Lemma experiment_map i j a b (F : Applicative) (g : i -> F j) (f : a -> b) (x : KleeneStore i j a) :
experiment g (KleeneStore_map f x) = map f (experiment g x).
Proof.
revert b f.
induction x; intros b f; simpl.
rewrite <- homomorphism_law.
reflexivity.
rewrite IHx.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
reflexivity.
Qed.

Lemma experiment_ap i j a b (f : Applicative) (g : i -> f j)
(h : KleeneStore i j (a -> b)) (x : KleeneStore i j a) :
experiment g (ap h x) = ap (experiment g h) (experiment g x).
Proof.
cut (forall c (h0 : c -> a -> b) (h : KleeneStore i j c),
experiment g (KleeneStore_apH h0 h x) = ap (experiment g (map h0 h)) (experiment g x)).
intros H.
simpl; unfold KleeneStore_ap; simpl.
rewrite H, identity_law.
reflexivity.
clear h.
intros c h0 h.
revert b h0.
induction h; intros b h0; simpl.
apply experiment_map.
rewrite IHh.
simpl.
rewrite <- KleeneStore_map_ap.
rewrite experiment_map, experiment_map.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
replace (fun (w : j) (w0 : j -> a0) (w1 : a) => h0 (w0 w) w1)
with (fun (w : j) (w0 : j -> a0) => h0 (w0 w)).
reflexivity.
do 2 (apply functional_extensionality; intro); apply eta_expansion.
Qed.

Definition experiment_idomaticTransformation i j (F : Applicative) (g : i -> F j) :
IdiomaticTransformation (KleeneStoreApplicative i j) F.
exists (@experiment i j F g).
reflexivity.
intros a b f x.
apply experiment_ap.
Defined.

Definition impure i j : i -> KleeneStore i j j :=
Battery (Unit _ _ (fun x => x)).

Lemma experiment_impure i j a (x: KleeneStore i j a) : experiment (impure j) x = x.
Proof.
induction x.
reflexivity.
simpl.
rewrite IHx.
unfold KleeneStore_ap; simpl.
replace (fun (s : j -> a) (t : j) => s t) with (fun x : j -> a => x).
rewrite KleeneStore_map_id.
reflexivity.
repeat (apply functional_extensionality; intro); reflexivity.
Qed.

Lemma experiment_duplicate i j k a (x: KleeneStore i k a) :
experiment (F:=ComposeApplicative (KleeneStoreApplicative i j)
(KleeneStoreApplicative j k)) (fun z : i => Battery (Unit i j (impure k)) z) x = KleeneDuplicate j x.
Proof.
induction x.
reflexivity.
simpl; rewrite <- IHx.
simpl; unfold KleeneStore_ap; simpl.
replace (fun (s : KleeneStore j k (k -> a)) (t : j) =>
Battery (KleeneStore_map (fun (s0 : k -> a) (t0 : k) => s0 t0) s) t)
with (@Battery j k a).
reflexivity.
repeat (apply functional_extensionality; intros).
replace (fun (s0 : k -> a) (t0 : k) => s0 t0)
with (fun s0 : k -> a => s0).
rewrite KleeneStore_map_id.
reflexivity.
repeat (apply functional_extensionality; intros).
reflexivity.
Qed.

Definition CoalgebroidSig a a' b b' := a -> KleeneStore b b' a'.

(*** TraversableSig and CoalgebraSig are isomorphic ***)

Definition Traversable_to_Coalgebroid a a' b b'
(f : TraversableSig a a' b b') : CoalgebroidSig a a' b b' :=
f (KleeneStoreApplicative b b') (Battery (Unit b b' (fun x => x))).

Definition Coalgebroid_to_Traversable a a' b b'
(g : CoalgebroidSig a a' b b') : TraversableSig a a' b b' :=
fun f h x => experiment h (g x).

Lemma Traversable_Coalgebroid_iso1 a a' b b' (x : CoalgebroidSig a a' b b') y :
Traversable_to_Coalgebroid (Coalgebroid_to_Traversable x) y = x y.
Proof.
unfold Traversable_to_Coalgebroid, Coalgebroid_to_Traversable.
generalize (x y).
clear x y.
induction k.
reflexivity.
simpl.
rewrite IHk.
clear a IHk.
unfold KleeneStore_ap; simpl.
rewrite KleeneStore_map_ap.
replace (fun (s : b' -> a0) (t : b') => s t) with (fun (s : b' -> a0) => s).
rewrite KleeneStore_identity.
reflexivity.
apply functional_extensionality.
apply eta_expansion.
Qed.

Lemma Traversable_Coalgebroid_iso2 a a' b b' (x : TraversableSig a a' b b') F g y :
Coalgebroid_to_Traversable (Traversable_to_Coalgebroid x) g y = x F g y.
Proof.
unfold Traversable_to_Coalgebroid, Coalgebroid_to_Traversable.
assert (P := (@parametricity_instance _ _ _ _ x _ _ (experiment_idomaticTransformation g) (Battery (Unit b b' (fun y => y))))) .
simpl in P.
rewrite P.
clear P.
replace (fun a0 : b =>
ap (a:=F) (a0:=b' -> b') (b:=b')
(map (a:=F) (fun (x0 : b') (f : b' -> b') => f x0) (g a0))
(pure F (fun y0 : b' => y0))) with g.
reflexivity.
apply functional_extensionality; intros z.
rewrite interchange_law.
repeat (unfold map; simpl; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
fold (map (fun w => w) (g z)).
rewrite identity_law.
reflexivity.
Qed.

Definition TraversableIdLaw a b (t : TraversableSig a a b b) :=
(forall x, t IdApplicative (fun a => a) x = x).

Definition CoalgebroidExtractLaw a b (t : CoalgebroidSig a a b b) :=
(forall x, KleeneExtract (t x) = x).

Lemma equiv_law1 a b (t : CoalgebroidSig a a b b) :
TraversableIdLaw (Coalgebroid_to_Traversable t) <->
CoalgebroidExtractLaw t.
Proof.
cut (forall x, (Coalgebroid_to_Traversable t) IdApplicative (fun a => a) x =
KleeneExtract (t x)).
intros E.
split; intros H x; simpl; rewrite <- H; auto.
intros x.
unfold Coalgebroid_to_Traversable.
generalize (t x).
clear t x.
induction k.
reflexivity.
simpl.
rewrite IHk.
reflexivity.
Qed.

Definition TraversableComposeLaw (i o : Type -> Type)
(t : forall (a b : Type), TraversableSig (o a) (o b) (i a) (i b)) :=
(forall a b c (F G:Applicative) (f : i a -> F (i b)) (g : i b -> G (i c)) x,
t a c (ComposeApplicative F G) (fun z => map g (f z)) x = map (t _ _ _ g) (t _ _ _ f x)).

Definition CoalgebroidDuplicateLaw (i o : Type -> Type)
(t : forall (a b : Type), CoalgebroidSig (o a) (o b) (i a) (i b)) :=
forall a b c x, KleeneDuplicate _ (t a c x) = KleeneStore_map (t _ _) (t a b x).

Lemma equiv_law2 i o t :
@TraversableComposeLaw i o (fun a b => Coalgebroid_to_Traversable (t a b)) <->
@CoalgebroidDuplicateLaw i o t.
Proof.
split.
intros H a b c x.
assert (H0 := H a b c _ _ (impure _) (impure _) x).
unfold impure in H0; simpl in H0.
unfold KleeneStore_ap in H0; simpl in H0.
unfold Coalgebroid_to_Traversable in H0; simpl in H0.
rewrite experiment_impure in H0.
replace (fun x : o b =>
experiment (F:=KleeneStoreApplicative (i b) (i c))
(Battery (Unit (i b) (i c) (fun x0 : i c => x0))) (t b c x))
with (t b c) in H0.
rewrite <- H0.
rewrite <- experiment_duplicate.
unfold impure; simpl.
replace (fun z0 : i b => Battery (Unit (i b) (i c) (fun x0 : i c => x0)) z0)
with (Battery (Unit (i b) (i c) (fun x0 : i c => x0))).
reflexivity.
apply functional_extensionality; reflexivity.
apply functional_extensionality; intros z.
rewrite experiment_impure.
reflexivity.
intros H a b c F G f g x.
assert (H0 := H a b c x).
unfold Coalgebroid_to_Traversable.
set (fg := (fun z : i a => map (a:=F) g (f z))).
rewrite <- experiment_map.
rewrite <- KleeneStore_map_comp.
rewrite <- H0.
generalize (t a c x).
revert f g fg.
clear H0.
generalize (i a) (i b) (i c) (o c).
clear - F G.
(* This probably should be its own algebraic law but...*)
intros a b c x f g fg k.
induction k.
reflexivity.
simpl.
rewrite IHk.
unfold Compose_ap, Compose_pure, map; simpl.
rewrite KleeneStore_map_comp.
repeat (unfold map; simpl; repeat rewrite homomorpishm_law; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite experiment_map.
repeat (unfold map; simpl; repeat rewrite homomorpishm_law; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
repeat rewrite interchange_law.
repeat (unfold map; simpl; repeat rewrite homomorpishm_law; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
unfold fg.
repeat (unfold map; simpl; repeat rewrite homomorpishm_law; rewrite <- composition_law).
unfold map; simpl; repeat rewrite homomorphism_law.
reflexivity.
Qed.
```
• #### Simplicity is the Initial Distributive Category

Simplicity is a combinator-based typed language with the unit type, sum types and product types. Types: 𝟙; A + B; A × B Every Simplicity…

• #### From Van Laarhoven Isomorphisms in one shot.

The type ∀ f, g : Functor. (g a → f b) → g s → f t is isomorphic to the type (s → a)×(b → t). The Van…

• #### A new case for the pointed functor class

There has been some debate for some time as to whether there should be a superclass for Applicative with just the pure function should exist:…

• Post a new comment

#### Error

default userpic
When you submit the form an invisible reCAPTCHA check will be performed.