Library Containers.Functor

Require Export HoTT.

Record Functor := {
  f_fun : Type → Type;
  f_map : ∀ {A1 A2: Type}, (A1 → A2) → f_fun A1 → f_fun A2;
  f_map_path_id : ∀ A : Type, @f_map A A idmap = idmap;
  f_map_path_composition :
      ∀ {A1 A2 A3} (f : A1 → A2) (g : A2 → A3),
      f_map (g o f) = f_map g o f_map f
}.
Coercion f_fun : Functor >-> Funclass.

Definition map := f_map.
Arguments map {_ _ _} _ _.