(*|
This file implements the ordinary endofunctors of functional
programming.
|*)

From Tealeaves Require Export
  Tactics.Prelude.

#[local] Generalizable Variables F G A B.

#[local] Notation "F ⇒ G" :=
  (∀ A: Type, F A → G A) (at level 50): tealeaves_scope.

Class Map (F: Type → Type): Type :=
  map: ∀ (A B: Type) (f: A → B), F A → F B.

#[global] Arguments map {F}%function_scope {Map}
  {A B}%type_scope f%function_scope.
#[local] Arguments map F%function_scope {Map}
  (A B)%type_scope f%function_scope.

Class Functor (F: Type → Type) `{Map_F: Map F}: Type :=
  { fun_map_id: ∀ (A: Type),
      map F A A (@id A) = @id (F A);
    fun_map_map: ∀ (A B C: Type) (f: A → B) (g: B → C),
      map F B C g ∘ map F A B f = map F A C (g ∘ f);
  }.

Class Natural `{Map F} `{Map G} (ϕ: F ⇒ G) :=
  { natural_src: Functor F;
    natural_tgt: Functor G;
    natural: ∀ `(f: A → B),
      map G A B f ∘ ϕ A = ϕ B ∘ map F A B f
  }.

Module Notations.
  Notation "F ⇒ G" :=
    (∀ A: Type, F A → G A) (at level 50): tealeaves_scope.
End Notations.