From Tealeaves Require Export
  Classes.Categorical.ContainerFunctor
  Functors.Early.List.

Import Monoid.
Import Subset.Notations.
Import Functor.Notations.
Import List.ListNotations.
Import ContainerFunctor.Notations.

#[local] Generalizable Variables G F A B.

(** * Shapely functors *)
(**********************************************************************)

(** * Operation <<tolist>> *)
(**********************************************************************)
Import Classes.Functor.Notations.

Class Tolist (F: Type -> Type) :=
  tolist: F ⇒ list.

#[global] Arguments tolist {F}%function_scope {Tolist} {A}%type_scope _.

(** ** Operation [shape] *)
(**********************************************************************)
Definition shape `{Map F} {A: Type}: F A -> F unit :=
  map (const tt).

(** *** Basic reasoning principles for <<shape>> *)
(**********************************************************************)
Theorem shape_map `{Functor F}: forall (A B: Type) (f: A -> B) (t: F A),
    shape (F := F) (map f t) =
      shape (F := F) t.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A B : Type) (f : A -> B) (t : F A),
shape (map f t) = shape t
Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A B : Type) (f : A -> B) (t : F A),
shape (map f t) = shape t
  intros.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
t: F A
shape (map f t) = shape t compose near t on left.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
t: F A
(shape ∘ map f) t = shape t
  unfold shape.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
t: F A
(map (const tt) ∘ map f) t = map (const tt) t now rewrite fun_map_map.
Qed.

Theorem shape_shape `{Functor F}: forall (A: Type) (t: F A),
    shape (shape t) = shape t.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A : Type) (t : F A), shape (shape t) = shape t
Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A : Type) (t : F A), shape (shape t) = shape t
  intros.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
t: F A
shape (shape t) = shape t  compose near t on left.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
t: F A
(shape ∘ shape) t = shape t
  unfold shape.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
t: F A
(map (const tt) ∘ map (const tt)) t = map (const tt) t now rewrite fun_map_map.
Qed.


Lemma shape_map_eq `{Functor F}:
  forall (A1 A2 B: Type) (f: A1 -> B) (g: A2 -> B) t u,
    map f t = map g u -> shape t = shape u.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A1 A2 B : Type) (f : A1 -> B) (g : A2 -> B)
  (t : F A1) (u : F A2),
map f t = map g u -> shape t = shape u
Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A1 A2 B : Type) (f : A1 -> B) (g : A2 -> B)
  (t : F A1) (u : F A2),
map f t = map g u -> shape t = shape u

  introv hyp.
F: Type -> Type
Map_F: Map F
H: Functor F
A1, A2, B: Type
f: A1 -> B
g: A2 -> B
t: F A1
u: F A2
hyp: map f t = map g u
shape t = shape u cut (shape (map f t) = shape (map g u)).
F: Type -> Type
Map_F: Map F
H: Functor F
A1, A2, B: Type
f: A1 -> B
g: A2 -> B
t: F A1
u: F A2
hyp: map f t = map g u
shape (map f t) = shape (map g u) -> shape t = shape u
F: Type -> Type
Map_F: Map F
H: Functor F
A1, A2, B: Type
f: A1 -> B
g: A2 -> B
t: F A1
u: F A2
hyp: map f t = map g u
shape (map f t) = shape (map g u)
  -
F: Type -> Type
Map_F: Map F
H: Functor F
A1, A2, B: Type
f: A1 -> B
g: A2 -> B
t: F A1
u: F A2
hyp: map f t = map g u
shape (map f t) = shape (map g u) -> shape t = shape u now rewrite 2(shape_map).
  -
F: Type -> Type
Map_F: Map F
H: Functor F
A1, A2, B: Type
f: A1 -> B
g: A2 -> B
t: F A1
u: F A2
hyp: map f t = map g u
shape (map f t) = shape (map g u) now rewrite hyp.
Qed.

(** ** Shapeliness Condition *)
(**********************************************************************)
Definition shapeliness (F: Type -> Type)
  `{Map F} `{Tolist F} := forall A (t1 t2: F A),
    shape t1 = shape t2 /\ tolist t1 = tolist t2 -> t1 = t2.

(** ** Typeclass *)
(**********************************************************************)
Class ShapelyFunctor
  (F: Type -> Type) `{Map F} `{Tolist F} :=
  { shp_natural :> Natural (@tolist F _);
    shp_functor :> Functor F;
    shp_shapeliness: shapeliness F;
  }.

(** ** Homomorphisms of Shapely Functors *)
(**********************************************************************)
Class ShapelyTransformation
      {F G: Type -> Type}
      `{! Map F} `{Tolist F}
      `{! Map G} `{Tolist G}
      (ϕ: F ⇒ G) :=
  { ltrans_commute: `(tolist (F := F) = tolist (F := G) ∘ ϕ A);
    ltrans_natural: Natural ϕ;
  }.

(** ** Various Characterizations of Shapeliness *)
(**********************************************************************)
Section listable_functor_respectful_definitions.

  Context
    (F: Type -> Type)
    `{Map F} `{Tolist F}.

  Definition tolist_map_injective :=
    forall A B (t1 t2: F A) (f g: A -> B),
      map f t1 = map g t2 ->
      shape t1 = shape t2 /\
      map f (tolist t1) = map g (tolist t2).

  Definition tolist_map_respectful :=
    forall A B (t1 t2: F A) (f g: A -> B),
      shape t1 = shape t2 ->
      map f (tolist t1) = map g (tolist t2) ->
      map f t1 = map g t2.

  Definition tolist_map_respectful_iff :=
    forall A B (t1 t2: F A) (f g: A -> B),
      shape t1 = shape t2 /\
      map f (tolist t1) = map g (tolist t2) <->
      map f t1 = map g t2.

End listable_functor_respectful_definitions.

Ltac unfold_list_properness :=
  unfold shapeliness,
  tolist_map_respectful,
    tolist_map_respectful_iff in *.

(** ** Equivalences *)
(**********************************************************************)
Section tolist_respectfulness_characterizations.

  Context
    `{Functor F}
    `{Tolist F}
    `{! Natural (@tolist F _)}.

  Theorem tolist_map_injective_proof: tolist_map_injective F.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
tolist_map_injective F
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
tolist_map_injective F
    introv heq.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) split.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
shape t1 = shape t2
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
map f (tolist t1) = map g (tolist t2)
    -
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
shape t1 = shape t2 cut (shape (map f t1) = shape (map g t2)).
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
shape (map f t1) = shape (map g t2) ->
shape t1 = shape t2
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
shape (map f t1) = shape (map g t2)
      +
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
shape (map f t1) = shape (map g t2) ->
shape t1 = shape t2 now rewrite 2(shape_map).
      +
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
shape (map f t1) = shape (map g t2) now rewrite heq.
    -
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
map f (tolist t1) = map g (tolist t2) compose near t1; compose near t2.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
(map f ∘ tolist) t1 = (map g ∘ tolist) t2
      do 2 rewrite natural.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
(tolist ∘ map f) t1 = (tolist ∘ map g) t2
      unfold compose.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A, B: Type
t1, t2: F A
f, g: A -> B
heq: map f t1 = map g t2
tolist (map f t1) = tolist (map g t2)
      now rewrite heq.
  Qed.

  Lemma shapeliness_equiv_1:
    shapeliness F -> tolist_map_respectful F.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
shapeliness F -> tolist_map_respectful F
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
shapeliness F -> tolist_map_respectful F
    unfold tolist_map_respectful.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
shapeliness F ->
forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
shape t1 = shape t2 ->
map f (tolist t1) = map g (tolist t2) ->
map f t1 = map g t2
    introv hyp hshape hcontents.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp: shapeliness F
A, B: Type
t1, t2: F A
f, g: A -> B
hshape: shape t1 = shape t2
hcontents: map f (tolist t1) = map g (tolist t2)
map f t1 = map g t2
    apply hyp.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp: shapeliness F
A, B: Type
t1, t2: F A
f, g: A -> B
hshape: shape t1 = shape t2
hcontents: map f (tolist t1) = map g (tolist t2)
shape (map f t1) = shape (map g t2) /\
tolist (map f t1) = tolist (map g t2) split.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp: shapeliness F
A, B: Type
t1, t2: F A
f, g: A -> B
hshape: shape t1 = shape t2
hcontents: map f (tolist t1) = map g (tolist t2)
shape (map f t1) = shape (map g t2)
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp: shapeliness F
A, B: Type
t1, t2: F A
f, g: A -> B
hshape: shape t1 = shape t2
hcontents: map f (tolist t1) = map g (tolist t2)
tolist (map f t1) = tolist (map g t2)
    -
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp: shapeliness F
A, B: Type
t1, t2: F A
f, g: A -> B
hshape: shape t1 = shape t2
hcontents: map f (tolist t1) = map g (tolist t2)
shape (map f t1) = shape (map g t2) now rewrite 2(shape_map).
    -
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp: shapeliness F
A, B: Type
t1, t2: F A
f, g: A -> B
hshape: shape t1 = shape t2
hcontents: map f (tolist t1) = map g (tolist t2)
tolist (map f t1) = tolist (map g t2) compose near t1 on left; compose near t2 on right.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp: shapeliness F
A, B: Type
t1, t2: F A
f, g: A -> B
hshape: shape t1 = shape t2
hcontents: map f (tolist t1) = map g (tolist t2)
(tolist ∘ map f) t1 = (tolist ∘ map g) t2
      now rewrite <- 2(natural).
  Qed.

  Lemma shapeliness_equiv_2:
    tolist_map_respectful F -> tolist_map_respectful_iff F.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
tolist_map_respectful F -> tolist_map_respectful_iff F
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
tolist_map_respectful F -> tolist_map_respectful_iff F
    unfold tolist_map_respectful, tolist_map_respectful_iff.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
(forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
 shape t1 = shape t2 ->
 map f (tolist t1) = map g (tolist t2) ->
 map f t1 = map g t2) ->
forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) <->
map f t1 = map g t2
    intros.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
H1: forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
shape t1 = shape t2 ->
map f (tolist t1) = map g (tolist t2) ->
map f t1 = map g t2
A, B: Type
t1, t2: F A
f, g: A -> B
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) <->
map f t1 = map g t2 split.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
H1: forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
shape t1 = shape t2 ->
map f (tolist t1) = map g (tolist t2) ->
map f t1 = map g t2
A, B: Type
t1, t2: F A
f, g: A -> B
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) ->
map f t1 = map g t2
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
H1: forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
shape t1 = shape t2 ->
map f (tolist t1) = map g (tolist t2) ->
map f t1 = map g t2
A, B: Type
t1, t2: F A
f, g: A -> B
map f t1 = map g t2 ->
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2)
    -
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
H1: forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
shape t1 = shape t2 ->
map f (tolist t1) = map g (tolist t2) ->
map f t1 = map g t2
A, B: Type
t1, t2: F A
f, g: A -> B
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) ->
map f t1 = map g t2 introv [? ?].
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
H1: forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
shape t1 = shape t2 ->
map f (tolist t1) = map g (tolist t2) ->
map f t1 = map g t2
A, B: Type
t1, t2: F A
f, g: A -> B
H2: shape t1 = shape t2
H3: map f (tolist t1) = map g (tolist t2)
map f t1 = map g t2 auto.
    -
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
H1: forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
shape t1 = shape t2 ->
map f (tolist t1) = map g (tolist t2) ->
map f t1 = map g t2
A, B: Type
t1, t2: F A
f, g: A -> B
map f t1 = map g t2 ->
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) apply tolist_map_injective_proof.
  Qed.

  Lemma shapeliness_equiv_3:
    tolist_map_respectful_iff F -> shapeliness F.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
tolist_map_respectful_iff F -> shapeliness F
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
tolist_map_respectful_iff F -> shapeliness F
    unfold shapeliness, tolist_map_respectful_iff.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
(forall (A B : Type) (t1 t2 : F A) (f g : A -> B),
 shape t1 = shape t2 /\
 map f (tolist t1) = map g (tolist t2) <->
 map f t1 = map g t2) ->
forall (A : Type) (t1 t2 : F A),
shape t1 = shape t2 /\ tolist t1 = tolist t2 ->
t1 = t2
    introv hyp1 hyp2.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp1: forall (A B : Type) (t1 t2 : F A)
  (f g : A -> B),
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) <->
map f t1 = map g t2
A: Type
t1, t2: F A
hyp2: shape t1 = shape t2 /\ tolist t1 = tolist t2
t1 = t2
    replace t1 with (map id t1) by (now rewrite (fun_map_id (F := F))).
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp1: forall (A B : Type) (t1 t2 : F A)
  (f g : A -> B),
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) <->
map f t1 = map g t2
A: Type
t1, t2: F A
hyp2: shape t1 = shape t2 /\ tolist t1 = tolist t2
map id t1 = t2
    replace t2 with (map id t2) by (now rewrite (fun_map_id (F := F))).
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp1: forall (A B : Type) (t1 t2 : F A)
  (f g : A -> B),
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) <->
map f t1 = map g t2
A: Type
t1, t2: F A
hyp2: shape t1 = shape t2 /\ tolist t1 = tolist t2
map id t1 = map id t2
    apply hyp1.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
hyp1: forall (A B : Type) (t1 t2 : F A)
  (f g : A -> B),
shape t1 = shape t2 /\
map f (tolist t1) = map g (tolist t2) <->
map f t1 = map g t2
A: Type
t1, t2: F A
hyp2: shape t1 = shape t2 /\ tolist t1 = tolist t2
shape t1 = shape t2 /\
map id (tolist t1) = map id (tolist t2) now rewrite (fun_map_id (F := list)).
  Qed.

End tolist_respectfulness_characterizations.

(*
(** ** [fold] and [mapReduce] operations *)
(**********************************************************************)
Section fold.

  Generalizable Variable M ϕ.

  Context
    `{ShapelyFunctor F}.

  Definition crush
    `{monoid_op: Monoid_op M}
    `{monoid_unit: Monoid_unit M}:
    F M -> M := crush_list ∘ tolist.

  Definition mapReduce {A}
    `{monoid_op: Monoid_op M}
    `{monoid_unit: Monoid_unit M}
    (f: A -> M): F A -> M :=
    crush ∘ map f.

  Lemma crush_mon_hom:
  forall `(ϕ: M1 -> M2) `{Hϕ: Monoid_Morphism M1 M2 ϕ},
      ϕ ∘ crush = crush ∘ map ϕ.
  Proof.
    intros ? ? ϕ; intros.
    change left (ϕ ∘ crush_list ∘ tolist).
    change right (crush_list ∘ (tolist ∘ map ϕ)).
    rewrite <- natural.
    rewrite (crush_list_mon_hom ϕ).
    reflexivity.
  Qed.

  Lemma mapReduce_map {A B} `{Monoid M} {f: A -> B} {g: B -> M}:
    mapReduce g ∘ map f = mapReduce (g ∘ f).
  Proof.
    intros. unfold mapReduce.
    now rewrite <- (fun_map_map (F := F)).
  Qed.

  Theorem mapReduce_hom {A} `{Monoid_Morphism M1 M2 ϕ} {f: A -> M1}:
    ϕ ∘ mapReduce f = mapReduce (ϕ ∘ f).
  Proof.
    intros. unfold mapReduce.
    reassociate <- on left.
    rewrite (crush_mon_hom ϕ).
    now rewrite <- (fun_map_map (F := F)).
  Qed.

End fold.
*)

(*
(** ** Folding over identity and composition functors *)
(**********************************************************************)
Section fold_monoidal_structure.

  Theorem fold_I (A: Type) `(Monoid A): forall (a: A),
      mapReduce a = a.
  Proof.
    intros. cbn. now rewrite (monoid_id_r).
  Qed.

End fold_monoidal_structure.
*)

(** * Derived <<Container>> Instance *)
(**********************************************************************)

(** ** Enumerating Elements of Shapely Functors *)
(**********************************************************************)
Section ToSubset_Tolist.

  #[local] Instance ToSubset_Tolist `{Tolist F}: ToSubset F :=
  fun A => tosubset ∘ tolist.

End ToSubset_Tolist.

Class Compat_ToSubset_Tolist
  (F: Type -> Type)
  `{H_tosubset: ToSubset F}
  `{H_tolist: Tolist F}: Prop :=
  compat_element_tolist:
    @tosubset F H_tosubset =
      @tosubset F (@ToSubset_Tolist F H_tolist).

Lemma tosubset_to_tolist `{Compat_ToSubset_Tolist F}:
  forall (A: Type),
    tosubset (F := F) (A := A) = tosubset (F := list) ∘ tolist.
F: Type -> Type
H_tosubset: ToSubset F
H_tolist: Tolist F
H: Compat_ToSubset_Tolist F
forall A : Type, tosubset = tosubset ∘ tolist
Proof.
F: Type -> Type
H_tosubset: ToSubset F
H_tolist: Tolist F
H: Compat_ToSubset_Tolist F
forall A : Type, tosubset = tosubset ∘ tolist
  now rewrite compat_element_tolist.
Qed.

Theorem in_iff_in_tolist `{Compat_ToSubset_Tolist F}:
  forall (A: Type) (t: F A) (a: A),
    a ∈ t <-> a ∈ tolist t.
F: Type -> Type
H_tosubset: ToSubset F
H_tolist: Tolist F
H: Compat_ToSubset_Tolist F
forall (A : Type) (t : F A) (a : A),
a ∈ t <-> a ∈ tolist t
Proof.
F: Type -> Type
H_tosubset: ToSubset F
H_tolist: Tolist F
H: Compat_ToSubset_Tolist F
forall (A : Type) (t : F A) (a : A),
a ∈ t <-> a ∈ tolist t
  intros.
F: Type -> Type
H_tosubset: ToSubset F
H_tolist: Tolist F
H: Compat_ToSubset_Tolist F
A: Type
t: F A
a: A
a ∈ t <-> a ∈ tolist t unfold element_of.
F: Type -> Type
H_tosubset: ToSubset F
H_tolist: Tolist F
H: Compat_ToSubset_Tolist F
A: Type
t: F A
a: A
tosubset t a <-> tosubset (tolist t) a
  now rewrite compat_element_tolist.
Qed.

#[export] Instance Natural_Element_Tolist:
  forall `{ShapelyFunctor F}, Natural (@tosubset F ToSubset_Tolist).
forall (F : Type -> Type) (H : Map F) (H0 : Tolist F),
ShapelyFunctor F ->
Natural (@tosubset F ToSubset_Tolist)
Proof.
forall (F : Type -> Type) (H : Map F) (H0 : Tolist F),
ShapelyFunctor F ->
Natural (@tosubset F ToSubset_Tolist)
  constructor; try typeclasses eauto.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
forall (A B : Type) (f : A -> B),
map f ∘ tosubset = tosubset ∘ map f
  intros A B f.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
f: A -> B
map f ∘ tosubset = tosubset ∘ map f unfold tosubset, ToSubset_Tolist.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
f: A -> B
map f ∘ (tosubset ∘ tolist) =
tosubset ∘ tolist ∘ map f
  reassociate <- on left.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
f: A -> B
map f ∘ tosubset ∘ tolist = tosubset ∘ tolist ∘ map f
  rewrite (natural (G := subset)).
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
f: A -> B
tosubset ∘ map f ∘ tolist = tosubset ∘ tolist ∘ map f
  reassociate -> on left.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
f: A -> B
tosubset ∘ (map f ∘ tolist) =
tosubset ∘ tolist ∘ map f now rewrite natural.
Qed.

(** ** Container Laws *)
(**********************************************************************)
Section ShapelyFunctor_setlike.

  Context
    `{ShapelyFunctor F}.

  Lemma shapeliness_iff:
    forall (A: Type) (t u: F A),
      t = u <-> shape t = shape u /\ tolist t = tolist u.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
forall (A : Type) (t u : F A),
t = u <-> shape t = shape u /\ tolist t = tolist u
  Proof.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
forall (A : Type) (t u : F A),
t = u <-> shape t = shape u /\ tolist t = tolist u
    intros.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A: Type
t, u: F A
t = u <-> shape t = shape u /\ tolist t = tolist u split.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A: Type
t, u: F A
t = u -> shape t = shape u /\ tolist t = tolist u
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A: Type
t, u: F A
shape t = shape u /\ tolist t = tolist u -> t = u
    +
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A: Type
t, u: F A
t = u -> shape t = shape u /\ tolist t = tolist u intros; subst; auto.
    +
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A: Type
t, u: F A
shape t = shape u /\ tolist t = tolist u -> t = u apply (shp_shapeliness).
  Qed.

  Lemma shapely_map_eq_iff:
    forall (A B: Type) (t: F A) (f g: A -> B),
      map f t = map g t <->
      map f (tolist t) = map g (tolist t).
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
forall (A B : Type) (t : F A) (f g : A -> B),
map f t = map g t <->
map f (tolist t) = map g (tolist t)
  Proof.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
forall (A B : Type) (t : F A) (f g : A -> B),
map f t = map g t <->
map f (tolist t) = map g (tolist t)
    intros.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
map f t = map g t <->
map f (tolist t) = map g (tolist t)
    compose near t on right.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
map f t = map g t <->
(map f ∘ tolist) t = (map g ∘ tolist) t rewrite 2(natural).
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
map f t = map g t <->
(tolist ∘ map f) t = (tolist ∘ map g) t
    unfold compose.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
map f t = map g t <->
tolist (map f t) = tolist (map g t) split.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
map f t = map g t ->
tolist (map f t) = tolist (map g t)
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
tolist (map f t) = tolist (map g t) ->
map f t = map g t
    -
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
map f t = map g t ->
tolist (map f t) = tolist (map g t) introv heq.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
heq: map f t = map g t
tolist (map f t) = tolist (map g t) now rewrite heq.
    -
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
tolist (map f t) = tolist (map g t) ->
map f t = map g t intros.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
H2: tolist (map f t) = tolist (map g t)
map f t = map g t apply (shp_shapeliness).
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
H2: tolist (map f t) = tolist (map g t)
shape (map f t) = shape (map g t) /\
tolist (map f t) = tolist (map g t) rewrite 2(shape_map).
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
A, B: Type
t: F A
f, g: A -> B
H2: tolist (map f t) = tolist (map g t)
shape t = shape t /\
tolist (map f t) = tolist (map g t)
      auto.
  Qed.

  Context
    `{ToSubset F}
    `{! Compat_ToSubset_Tolist F}.

  Lemma compat_element_tolist_natural:
    `{Natural (@tosubset F _)}.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
Natural (@tosubset F H2)
  Proof.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
Natural (@tosubset F H2)
    constructor; try typeclasses eauto.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
forall (A B : Type) (f : A -> B),
map f ∘ tosubset = tosubset ∘ map f
    intros.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
A, B: Type
f: A -> B
map f ∘ tosubset = tosubset ∘ map f
    rewrite compat_element_tolist.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
A, B: Type
f: A -> B
map f ∘ tosubset = tosubset ∘ map f
    rewrite (natural (Natural := Natural_Element_Tolist)).
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
A, B: Type
f: A -> B
tosubset ∘ map f = tosubset ∘ map f
    reflexivity.
  Qed.

  Theorem shapely_pointwise_iff:
    forall (A B: Type) (t: F A) (f g: A -> B),
      (forall (a: A), a ∈ t -> f a = g a) <-> map f t = map g t.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
forall (A B : Type) (t : F A) (f g : A -> B),
(forall a : A, a ∈ t -> f a = g a) <->
map f t = map g t
  Proof.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
forall (A B : Type) (t : F A) (f g : A -> B),
(forall a : A, a ∈ t -> f a = g a) <->
map f t = map g t
    introv.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
A, B: Type
t: F A
f, g: A -> B
(forall a : A, a ∈ t -> f a = g a) <->
map f t = map g t
    rewrite shapely_map_eq_iff.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
A, B: Type
t: F A
f, g: A -> B
(forall a : A, a ∈ t -> f a = g a) <->
map f (tolist t) = map g (tolist t)
    setoid_rewrite in_iff_in_tolist.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
A, B: Type
t: F A
f, g: A -> B
(forall a : A, a ∈ tolist t -> f a = g a) <->
map f (tolist t) = map g (tolist t)
    rewrite map_rigidly_respectful_list.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
A, B: Type
t: F A
f, g: A -> B
map f (tolist t) = map g (tolist t) <->
map f (tolist t) = map g (tolist t)
    reflexivity.
  Qed.

  Corollary shapely_pointwise:
    forall (A B: Type) (t: F A) (f g: A -> B),
      (forall (a: A), a ∈ t -> f a = g a) -> map f t = map g t.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
forall (A B : Type) (t : F A) (f g : A -> B),
(forall a : A, a ∈ t -> f a = g a) ->
map f t = map g t
  Proof.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
forall (A B : Type) (t : F A) (f g : A -> B),
(forall a : A, a ∈ t -> f a = g a) ->
map f t = map g t
   introv.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
A, B: Type
t: F A
f, g: A -> B
(forall a : A, a ∈ t -> f a = g a) ->
map f t = map g t rewrite shapely_pointwise_iff.
F: Type -> Type
H: Map F
H0: Tolist F
H1: ShapelyFunctor F
H2: ToSubset F
Compat_ToSubset_Tolist0: Compat_ToSubset_Tolist F
A, B: Type
t: F A
f, g: A -> B
map f t = map g t -> map f t = map g t auto.
  Qed.

  (** ** Typeclass Instance *)
  (********************************************************************)
  #[export] Instance ContainerFunctor_ShapelyFunctor:
    ContainerFunctor F :=
    {| cont_natural := compat_element_tolist_natural;
       cont_pointwise := shapely_pointwise;
    |}.

End ShapelyFunctor_setlike.