From Tealeaves Require Import
  Classes.Kleisli.DecoratedContainerFunctor
  Classes.Kleisli.DecoratedFunctor
  Classes.Categorical.Comonad (Extract, extract).

#[local] Generalizable Variables E T.

Import DecoratedContainerFunctor.Notations.
Import ContainerFunctor.Notations.
Import Subset.Notations.

(** * Derived Properties of <<DecoratedContainerFunctor>> *)
(**********************************************************************)

(** ** Relating <<a ∈ t>> to <<(e, a) ∈d t>> *)
(**********************************************************************)
Section relating_element_to_element_ctx.

  Context
    `{ToCtxset_inst: ToCtxset E T}
    `{ToSubset_inst: ToSubset T}
    `{! Compat_ToSubset_ToCtxset E T}.

  Lemma ind_iff_in:
    forall (A: Type) (t: T A) (a: A),
      a ∈ t <-> exists (e: E), (e, a) ∈d t.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
forall (A : Type) (t : T A) (a : A),
a ∈ t <-> (exists e : E, (e, a) ∈d t)
  Proof.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
forall (A : Type) (t : T A) (a : A),
a ∈ t <-> (exists e : E, (e, a) ∈d t)
    intros.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
a ∈ t <-> (exists e : E, (e, a) ∈d t)
    change_left ((evalAt a ∘ tosubset) t).
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
(evalAt a ∘ tosubset) t <->
(exists e : E, (e, a) ∈d t)
    rewrite tosubset_to_toctxset.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
(evalAt a ∘ (map extract ∘ toctxset)) t <->
(exists e : E, (e, a) ∈d t)
    unfold_ops @Map_subset.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
(evalAt a
 ∘ ((fun (s : E * A -> Prop) (b : A) =>
     exists a : E * A, s a /\ extract a = b)
    ∘ toctxset)) t <-> (exists e : E, (e, a) ∈d t)
    unfold evalAt, compose.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
(exists a0 : E * A, toctxset t a0 /\ extract a0 = a) <->
(exists e : E, (e, a) ∈d t)
    split.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
(exists a0 : E * A, toctxset t a0 /\ extract a0 = a) ->
exists e : E, (e, a) ∈d t
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
(exists e : E, (e, a) ∈d t) ->
exists a0 : E * A, toctxset t a0 /\ extract a0 = a
    -
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
(exists a0 : E * A, toctxset t a0 /\ extract a0 = a) ->
exists e : E, (e, a) ∈d t intros [[e a'] [Hin Heq]].
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
e: E
a': A
Hin: toctxset t (e, a')
Heq: extract (e, a') = a
exists e : E, (e, a) ∈d t
      cbn in Heq.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
e: E
a': A
Hin: toctxset t (e, a')
Heq: a' = a
exists e : E, (e, a) ∈d t subst.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
e: E
Hin: toctxset t (e, a)
exists e : E, (e, a) ∈d t eauto.
    -
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
(exists e : E, (e, a) ∈d t) ->
exists a0 : E * A, toctxset t a0 /\ extract a0 = a intros [e Hin].
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
t: T A
a: A
e: E
Hin: (e, a) ∈d t
exists a0 : E * A, toctxset t a0 /\ extract a0 = a
      eauto.
  Qed.

  Lemma ind_implies_in:
    forall (A: Type) (e: E) (a: A) (t: T A),
      (e, a) ∈d t -> a ∈ t.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
forall (A : Type) (e : E) (a : A) (t : T A),
(e, a) ∈d t -> a ∈ t
  Proof.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
forall (A : Type) (e : E) (a : A) (t : T A),
(e, a) ∈d t -> a ∈ t
    intros.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
e: E
a: A
t: T A
H: (e, a) ∈d t
a ∈ t
    rewrite ind_iff_in.
E: Type
T: Type -> Type
ToCtxset_inst: ToCtxset E T
ToSubset_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
A: Type
e: E
a: A
t: T A
H: (e, a) ∈d t
exists e : E, (e, a) ∈d t
    eauto.
  Qed.

End relating_element_to_element_ctx.

(** * Basic Properties of Decorated Containers *)
(**********************************************************************)
Section decorated_container_functor_theory.

  Context
    `{DecoratedFunctor E T}
    `{Map_T: Map T}
    `{ToCtxset_ET: ToCtxset E T}
    `{ToSubset_T: ToSubset T}
    `{! Compat_Map_Mapd E T}
    `{! Compat_ToSubset_ToCtxset E T}
    `{! DecoratedContainerFunctor E T}
    {A B: Type}.

  Implicit Types (t: T A) (b: B) (e: E) (a: A).

  (** ** Respectful Properties between (∈d) and <<mapd>> *)
  (********************************************************************)
  Theorem ind_mapd_iff: forall e t f b,
      (e, b) ∈d mapd f t <-> exists a: A, (e, a) ∈d t /\ f (e, a) = b.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall e t (f : E * A -> B) b,
(e, b) ∈d mapd f t <->
(exists a, (e, a) ∈d t /\ f (e, a) = b)
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall e t (f : E * A -> B) b,
(e, b) ∈d mapd f t <->
(exists a, (e, a) ∈d t /\ f (e, a) = b)
    introv.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
e: E
t: T A
f: E * A -> B
b: B
(e, b) ∈d mapd f t <->
(exists a, (e, a) ∈d t /\ f (e, a) = b)
    compose near t on left.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
e: E
t: T A
f: E * A -> B
b: B
(element_ctx_of (e, b) ∘ mapd f) t <->
(exists a, (e, a) ∈d t /\ f (e, a) = b)
    rewrite element_ctx_of_toctxset.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
e: E
t: T A
f: E * A -> B
b: B
(evalAt (e, b) ∘ toctxset ∘ mapd f) t <->
(exists a, (e, a) ∈d t /\ f (e, a) = b)
    reassociate -> on left.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
e: E
t: T A
f: E * A -> B
b: B
(evalAt (e, b) ∘ (toctxset ∘ mapd f)) t <->
(exists a, (e, a) ∈d t /\ f (e, a) = b)
    rewrite <- (dhom_natural (ϕ := @toctxset E T _)).
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
e: E
t: T A
f: E * A -> B
b: B
(evalAt (e, b) ∘ (mapd f ∘ toctxset)) t <->
(exists a, (e, a) ∈d t /\ f (e, a) = b)
    reflexivity.
  Qed.

  Corollary in_mapd_iff: forall t f b,
      b ∈ mapd f t <-> exists (e: E) (a: A), (e, a) ∈d t /\ f (e, a) = b.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall t (f : E * A -> B) b,
b ∈ mapd f t <->
(exists e a, (e, a) ∈d t /\ f (e, a) = b)
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall t (f : E * A -> B) b,
b ∈ mapd f t <->
(exists e a, (e, a) ∈d t /\ f (e, a) = b)
    introv.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
t: T A
f: E * A -> B
b: B
b ∈ mapd f t <->
(exists e a, (e, a) ∈d t /\ f (e, a) = b)
    rewrite ind_iff_in.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
t: T A
f: E * A -> B
b: B
(exists e, (e, b) ∈d mapd f t) <->
(exists e a, (e, a) ∈d t /\ f (e, a) = b)
    setoid_rewrite ind_mapd_iff.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
t: T A
f: E * A -> B
b: B
(exists e a, (e, a) ∈d t /\ f (e, a) = b) <->
(exists e a, (e, a) ∈d t /\ f (e, a) = b)
    reflexivity.
  Qed.

  Corollary ind_map_iff: forall e t f b,
      (e, b) ∈d map f t <-> exists a: A, (e, a) ∈d t /\ f a = b.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall e t (f : A -> B) b,
(e, b) ∈d map f t <->
(exists a, (e, a) ∈d t /\ f a = b)
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall e t (f : A -> B) b,
(e, b) ∈d map f t <->
(exists a, (e, a) ∈d t /\ f a = b)
    introv.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
e: E
t: T A
f: A -> B
b: B
(e, b) ∈d map f t <->
(exists a, (e, a) ∈d t /\ f a = b)
    rewrite map_to_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
e: E
t: T A
f: A -> B
b: B
(e, b) ∈d mapd (f ∘ extract) t <->
(exists a, (e, a) ∈d t /\ f a = b)
    rewrite ind_mapd_iff.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
e: E
t: T A
f: A -> B
b: B
(exists a, (e, a) ∈d t /\ (f ∘ extract) (e, a) = b) <->
(exists a, (e, a) ∈d t /\ f a = b)
    reflexivity.
  Qed.

  Corollary ind_mapd_mono: forall t e a (f: E * A -> B),
      (e, a) ∈d t -> (e, f (e, a)) ∈d mapd f t.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall t e a (f : E * A -> B),
(e, a) ∈d t -> (e, f (e, a)) ∈d mapd f t
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall t e a (f : E * A -> B),
(e, a) ∈d t -> (e, f (e, a)) ∈d mapd f t
    introv.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
t: T A
e: E
a: A
f: E * A -> B
(e, a) ∈d t -> (e, f (e, a)) ∈d mapd f t rewrite ind_mapd_iff.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
t: T A
e: E
a: A
f: E * A -> B
(e, a) ∈d t ->
exists a0, (e, a0) ∈d t /\ f (e, a0) = f (e, a) now exists a.
  Qed.

  Corollary ind_map_mono: forall t e a (f: A -> B),
      (e, a) ∈d t -> (e, f a) ∈d map f t.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall t e a (f : A -> B),
(e, a) ∈d t -> (e, f a) ∈d map f t
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall t e a (f : A -> B),
(e, a) ∈d t -> (e, f a) ∈d map f t
    introv.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
t: T A
e: E
a: A
f: A -> B
(e, a) ∈d t -> (e, f a) ∈d map f t rewrite ind_map_iff.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
t: T A
e: E
a: A
f: A -> B
(e, a) ∈d t -> exists a0, (e, a0) ∈d t /\ f a0 = f a now exists a.
  Qed.

  Corollary mapd_respectful: forall t (f g: E * A -> A),
      (forall e a, (e, a) ∈d t -> f (e, a) = g (e, a)) ->
      mapd f t = mapd g t.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall t (f g : E * A -> A),
(forall e a, (e, a) ∈d t -> f (e, a) = g (e, a)) ->
mapd f t = mapd g t
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
forall t (f g : E * A -> A),
(forall e a, (e, a) ∈d t -> f (e, a) = g (e, a)) ->
mapd f t = mapd g t
    apply dcont_pointwise.
  Qed.

  Corollary mapd_respectful_id `{! Functor T}:
    forall (t: T A) (f: E * A -> A),
      (forall e a, (e, a) ∈d t -> f (e, a) = a) -> mapd f t = t.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
Functor0: Functor T
forall t (f : E * A -> A),
(forall e a, (e, a) ∈d t -> f (e, a) = a) ->
mapd f t = t
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
Functor0: Functor T
forall t (f : E * A -> A),
(forall e a, (e, a) ∈d t -> f (e, a) = a) ->
mapd f t = t
    introv hyp.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
Functor0: Functor T
t: T A
f: E * A -> A
hyp: forall e a, (e, a) ∈d t -> f (e, a) = a
mapd f t = t
    change t with (id t) at 2.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
Functor0: Functor T
t: T A
f: E * A -> A
hyp: forall e a, (e, a) ∈d t -> f (e, a) = a
mapd f t = id t
    rewrite <- fun_map_id.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
Functor0: Functor T
t: T A
f: E * A -> A
hyp: forall e a, (e, a) ∈d t -> f (e, a) = a
mapd f t = map id t
    rewrite map_to_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
Functor0: Functor T
t: T A
f: E * A -> A
hyp: forall e a, (e, a) ∈d t -> f (e, a) = a
mapd f t = mapd (id ∘ extract) t
    apply dcont_pointwise.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
ToCtxset_ET: ToCtxset E T
ToSubset_T: ToSubset T
Compat_Map_Mapd0: Compat_Map_Mapd E T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset E
  T
DecoratedContainerFunctor0: DecoratedContainerFunctor
  E T
A, B: Type
Functor0: Functor T
t: T A
f: E * A -> A
hyp: forall e a, (e, a) ∈d t -> f (e, a) = a
forall e a,
(e, a) ∈d t -> f (e, a) = (id ∘ extract) (e, a)
    apply hyp.
  Qed.

End decorated_container_functor_theory.