関手

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).
Setting notation at level 1
to match previous notation with longest common prefix: "_ .1".
Notations "_ .1" defined at level 1 with arguments constr at level 1
and "_ .1 _" defined at level 1 with arguments constr at next level
have incompatible prefixes. One of them will likely not work.
[notation-incompatible-prefix,parsing,default]

Check _ .1 _.
F1 ?f ?h
     : ?D [?f ?a, ?f ?b]
where
?C : [ |- category_data]
?D : [ |- category_data]
?f : [ |- functor_data ?C ?D]
?a : [ |- ob ?C]
?b : [ |- ob ?C]
?h : [ |- ?C [?a, ?b]]

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;
  }.