(*|
関手
====
|*)

Require Import category.

Set Implicit Arguments.

Record functor_data (C D : category_data) : Type :=
  make_functor_data {
    F0       :> C -> D;
    F1 {a b} :  C[a, b] -> D[F0 a, F0 b];
  }.

Notation "F .1 f" := (F.(F1) f).

Check _ .1 _.

Record is_functor
  (C D : category_data)
  (F : functor_data C D)
  : Prop :=
  make_is_category {
    preserve_identity {a}
      : F.(F1) (id (x := a)) = id;

    preserve_comp {a b c}
      (f : C[a, b])
      (g : C[b, c])
      : F.1 (g ∘ f) = F.1 g ∘ F.1 f;
  }.

Record functor
  (C D : category)
  : Type :=
  make_functor {
    F            :> functor_data C D;
    F_is_functor :> is_functor F;
  }.