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.