From Tealeaves Require Export
  Functors.Early.Ctxset
  Classes.Kleisli.DecoratedContainerFunctor
  Classes.Kleisli.Theory.DecoratedContainerFunctor.

Import DecoratedContainerFunctor.Notations.

(** * <<DecoratedContainerFunctor>> Instance for <<ctxset>> *)
(**********************************************************************)
Section Container_ctxset.

  Context {E: Type}.

  #[local] Instance ToCtxset_ctxset: ToCtxset E (ctxset E) :=
    fun (A: Type) (s: ctxset E A) => s.

  Instance Natural_elements_ctx_ctxset:
    DecoratedHom E (ctxset E) (ctxset E)
      (@toctxset E (ctxset E) _).
E: Type
DecoratedHom E (ctxset E) (ctxset E)
  (@toctxset E (ctxset E) ToCtxset_ctxset)
  Proof.
E: Type
DecoratedHom E (ctxset E) (ctxset E)
  (@toctxset E (ctxset E) ToCtxset_ctxset)
    constructor.
E: Type
forall (A B : Type) (f : E * A -> B),
mapd f ∘ toctxset = toctxset ∘ mapd f reflexivity.
  Qed.

  Lemma ctxset_pointwise: forall (A B: Type) (t: ctxset E A) (f g: E * A -> B),
      (forall (e: E) (a: A), (e, a) ∈d t -> f (e, a) = g (e, a)) ->
      mapd f t = mapd g t.
E: Type
forall (A B : Type) (t : ctxset E A)
  (f g : E * A -> B),
(forall (e : E) (a : A),
 (e, a) ∈d t -> f (e, a) = g (e, a)) ->
mapd f t = mapd g t
  Proof.
E: Type
forall (A B : Type) (t : ctxset E A)
  (f g : E * A -> B),
(forall (e : E) (a : A),
 (e, a) ∈d t -> f (e, a) = g (e, a)) ->
mapd f t = mapd g t
    introv hyp.
E, A, B: Type
t: ctxset E A
f, g: E * A -> B
hyp: forall (e : E) (a : A), (e, a) ∈d t -> f (e, a) = g (e, a)
mapd f t = mapd g t ext [e b].
E, A, B: Type
t: ctxset E A
f, g: E * A -> B
hyp: forall (e : E) (a : A), (e, a) ∈d t -> f (e, a) = g (e, a)
e: E
b: B
mapd f t (e, b) = mapd g t (e, b) cbv in *.
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
hyp: forall (e : E) (a : A), t (e, a) -> f (e, a) = g (e, a)
e: E
b: B
(exists a : A, t (e, a) /\ f (e, a) = b) =
(exists a : A, t (e, a) /\ g (e, a) = b) propext.
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
hyp: forall (e : E) (a : A), t (e, a) -> f (e, a) = g (e, a)
e: E
b: B
(exists a : A, t (e, a) /\ f (e, a) = b) ->
exists a : A, t (e, a) /\ g (e, a) = b
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
hyp: forall (e : E) (a : A), t (e, a) -> f (e, a) = g (e, a)
e: E
b: B
(exists a : A, t (e, a) /\ g (e, a) = b) ->
exists a : A, t (e, a) /\ f (e, a) = b
    -
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
hyp: forall (e : E) (a : A), t (e, a) -> f (e, a) = g (e, a)
e: E
b: B
(exists a : A, t (e, a) /\ f (e, a) = b) ->
exists a : A, t (e, a) /\ g (e, a) = b intros [a [Hin Heq]].
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
hyp: forall (e : E) (a : A), t (e, a) -> f (e, a) = g (e, a)
e: E
b: B
a: A
Hin: t (e, a)
Heq: f (e, a) = b
exists a : A, t (e, a) /\ g (e, a) = b
      specialize (hyp e a Hin).
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
e: E
a: A
hyp: f (e, a) = g (e, a)
b: B
Hin: t (e, a)
Heq: f (e, a) = b
exists a : A, t (e, a) /\ g (e, a) = b
      subst.
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
e: E
a: A
hyp: f (e, a) = g (e, a)
Hin: t (e, a)
exists a0 : A, t (e, a0) /\ g (e, a0) = f (e, a) eauto.
    -
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
hyp: forall (e : E) (a : A), t (e, a) -> f (e, a) = g (e, a)
e: E
b: B
(exists a : A, t (e, a) /\ g (e, a) = b) ->
exists a : A, t (e, a) /\ f (e, a) = b intros [a [Hin Heq]].
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
hyp: forall (e : E) (a : A), t (e, a) -> f (e, a) = g (e, a)
e: E
b: B
a: A
Hin: t (e, a)
Heq: g (e, a) = b
exists a : A, t (e, a) /\ f (e, a) = b
      specialize (hyp e a Hin).
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
e: E
a: A
hyp: f (e, a) = g (e, a)
b: B
Hin: t (e, a)
Heq: g (e, a) = b
exists a : A, t (e, a) /\ f (e, a) = b
      subst.
E, A, B: Type
t: E * A -> Prop
f, g: E * A -> B
e: E
a: A
hyp: f (e, a) = g (e, a)
Hin: t (e, a)
exists a0 : A, t (e, a0) /\ f (e, a0) = g (e, a) eauto.
  Qed.

  #[local] Instance DecoratedContainerFunctor_ctxset:
    DecoratedContainerFunctor E (ctxset E) :=
    {| dcont_pointwise := ctxset_pointwise;
    |}.

End Container_ctxset.