(* 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.
Some theorems about traversals in Coq 8.3pl4
-
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
- 0 comments
- Post a new comment
- 0 comments