From Tealeaves Require Export
  Classes.Functor.

#[local] Set Implicit Arguments.
#[local] Generalizable Variables X Y A B F i o.

(** * The [Store] functor *)
(**********************************************************************)
Section fix_parameters.

  Context
    {A B: Type}.

  Inductive Store C: Type :=
  | MkStore: (B -> C) -> A -> Store C.


  (** ** Functor Instance *)
  (********************************************************************)
  Definition map_Store `{f: X -> Y} (c: Store X): Store Y :=
    match c with
    | MkStore mk a => MkStore (f ∘ mk) a
    end.

  #[export] Instance Map_Batch: Map Store := @map_Store.

  #[export, program] Instance Functor_Batch: Functor Store.

  Solve All Obligations with (intros; now ext [?]).

End fix_parameters.

(** ** <<Store>> as a Parameterized Comonad *)
(**********************************************************************)
Section parameterized.

  #[local] Unset Implicit Arguments.

  Definition extract_Store {A B: Type} (s: @Store A A B): B :=
    match s with
    | MkStore mk b => mk b
    end.

  Definition cojoin_Store {A C X: Type} (B: Type)
    (s: @Store A C X): @Store A B (@Store B C X) :=
    match s with
    | MkStore mk a => MkStore (fun b => MkStore mk b) a
    end.

  Context
    (A B C X: Type).

  Lemma extr_cojoin:
    `(extract_Store ∘ cojoin_Store A = @id (@Store A B C)).
A, B, C, X: Type
extract_Store ∘ cojoin_Store A = id
  Proof.
A, B, C, X: Type
extract_Store ∘ cojoin_Store A = id
    intros.
A, B, C, X: Type
extract_Store ∘ cojoin_Store A = id now ext [i1 mk].
  Qed.

  Lemma map_extr_cojoin:
    `(map extract_Store ∘ cojoin_Store B = @id (@Store A B C)).
A, B, C, X: Type
map extract_Store ∘ cojoin_Store B = id
  Proof.
A, B, C, X: Type
map extract_Store ∘ cojoin_Store B = id
    intros.
A, B, C, X: Type
map extract_Store ∘ cojoin_Store B = id now ext [i1 mk].
  Qed.

  Lemma cojoin_cojoin:
    `(cojoin_Store B2 ∘ @cojoin_Store A C X B1 =
        map (cojoin_Store B1) ∘ cojoin_Store B2).
A, B, C, X: Type
forall B2 B1 : Type,
cojoin_Store B2 ∘ cojoin_Store B1 =
map (cojoin_Store B1) ∘ cojoin_Store B2
  Proof.
A, B, C, X: Type
forall B2 B1 : Type,
cojoin_Store B2 ∘ cojoin_Store B1 =
map (cojoin_Store B1) ∘ cojoin_Store B2
    intros.
A, B, C, X, B2, B1: Type
cojoin_Store B2 ∘ cojoin_Store B1 =
map (cojoin_Store B1) ∘ cojoin_Store B2 now ext [i1 mk].
  Qed.

End parameterized.

(** ** A Representation Lemma *)
(**********************************************************************)
Definition runStore `{Map F} `(f: A -> F B):
  forall X, Store X -> F X :=
  fun A '(MkStore mk a) => map mk (f a).

Definition runStore_inv `{Map F}
  `(run: forall X, @Store A B X -> F X): A -> F B :=
  fun (a: A) => run B (MkStore id a).

Section representation.

  Context
    `{Functor F}.

  Lemma store_repr1: forall `(f: i -> F o),
      runStore_inv (runStore f) = f.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (i o : Type) (f : i -> F o),
runStore_inv (runStore f) = f
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (i o : Type) (f : i -> F o),
runStore_inv (runStore f) = f
    intros.
F: Type -> Type
Map_F: Map F
H: Functor F
i, o: Type
f: i -> F o
runStore_inv (runStore f) = f ext i1.
F: Type -> Type
Map_F: Map F
H: Functor F
i, o: Type
f: i -> F o
i1: i
runStore_inv (runStore f) i1 = f i1 cbn.
F: Type -> Type
Map_F: Map F
H: Functor F
i, o: Type
f: i -> F o
i1: i
map id (f i1) = f i1 now rewrite (fun_map_id).
  Qed.

  Lemma runStore2: forall `(ϕ: forall X, @Store A B X -> F X),
      Natural ϕ ->
      runStore (runStore_inv ϕ) = ϕ.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A B : Type)
  (ϕ : forall X : Type, Store X -> F X),
Natural ϕ -> runStore (runStore_inv ϕ) = ϕ
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A B : Type)
  (ϕ : forall X : Type, Store X -> F X),
Natural ϕ -> runStore (runStore_inv ϕ) = ϕ
    intros.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
ϕ: forall X : Type, Store X -> F X
H0: Natural ϕ
runStore (runStore_inv ϕ) = ϕ unfold runStore, runStore_inv.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
ϕ: forall X : Type, Store X -> F X
H0: Natural ϕ
(fun (A0 : Type) '(MkStore mk a) =>
 map mk (ϕ B (MkStore id a))) = ϕ
    ext X [mk a].
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
ϕ: forall X : Type, Store X -> F X
H0: Natural ϕ
X: Type
mk: B -> X
a: A
map mk (ϕ B (MkStore id a)) = ϕ X (MkStore mk a) compose near (MkStore (@id B) a) on left.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
ϕ: forall X : Type, Store X -> F X
H0: Natural ϕ
X: Type
mk: B -> X
a: A
(map mk ∘ ϕ B) (MkStore id a) = ϕ X (MkStore mk a)
    now rewrite (natural (ϕ := ϕ)).
  Qed.

End representation.