length は リスト函手から定数函手への自然変換だよ on Coq.

length_as_natrans.v

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Setoids.Setoid Morphisms.
Generalizable All Variables.

Class Setoid :=
  {
    carrier: Type;
    equal: carrier -> carrier -> Prop;
    prf_Setoid:> Equivalence equal
  }.
Coercion carrier: Setoid >-> Sortclass.
Coercion prf_Setoid: Setoid >-> Equivalence.
Existing Instance prf_Setoid.
Notation "(== :> X )" := (equal (Setoid:=X)).
Notation "(==)" := (==:>_) (only parsing).
Notation "x == y :> X" := (equal (Setoid:=X) x y) (at level 90, no associativity).
Notation "x == y" := (equal x y) (at level 90, no associativity, only parsing).

Class Map (X Y: Setoid) :=
  {
    map: X -> Y;
    substitute:> Proper ((==) ==> (==)) map
  }.
Coercion map: Map >-> Funclass.
Existing Instance substitute.
Class Category :=
  {
    obj: Type;
    hom: obj -> obj -> Setoid;
    comp: forall {X Y Z: obj}, hom X Y -> hom Y Z -> hom X Z;
    id: forall (X: obj), hom X X;

    comp_subst:> forall X Y Z, Proper ((==:> hom X Y) ==> (==:> hom Y Z) ==> (==:> hom X Z)) (@comp X Y Z);

    comp_assoc:
      forall {X Y Z W: obj}(f: hom X Y)(g: hom Y Z)(h: hom Z W),
        comp f (comp g h) == comp (comp f g) h;

    comp_id_dom:
      forall {X Y: obj}(f: hom X Y),
        comp (id X) f == f;

    comp_id_cod:
      forall {X Y: obj}(f: hom X Y),
        comp f (id Y) == f
  }.
Coercion obj: Category >-> Sortclass.
Coercion hom: Category >-> Funclass.
Notation "g \o{ C } f" := (comp (Category:=C) f g) (at level 60, right associativity).
Notation "g \o f" := (g \o{_} f) (at level 60, right associativity).
Notation "'Id' X" := (id X) (at level 60, right associativity).


Obligation Tactic := try now idtac.
Program Instance function_setoid (X Y: Type): Setoid :=
  {
    carrier := X -> Y;
    equal f g := forall x, f x = g x
  }.
Next Obligation.
  intros X Y; split.
  - now intros f x.
  - now intros f g Heq x.
  - intros f g h Heq Heq' x.
    now rewrite Heq.
Qed.

Program Instance Types: Category :=
  {
    obj := Type;
    hom := function_setoid;
    comp X Y Z f g := fun x => g (f x);
    id X := fun x => x
  }.
Next Obligation.
  intros X Y Z f f' Heqf g g' Heqg x; simpl.
  now rewrite Heqf, Heqg.
Qed.

Class Functor (C D: Category) :=
  {
    fobj:> C -> D;
    fmap: forall {X Y: C}, hom X Y -> hom (fobj X) (fobj Y);

    fmap_subst:> forall X Y: C, Proper ((==:> hom X Y) ==> (==:> hom (fobj X) (fobj Y))) (@fmap X Y);
    fmap_comp: forall (X Y Z: C)(f: hom X Y)(g: hom Y Z), fmap (g \o f) == fmap g \o fmap f;
    fmap_id: forall X: C, fmap (Id X) == Id (fobj X)
  }.
Coercion fobj: Functor >-> Funclass.
Arguments fmap {C D}(Functor){X Y}(f): clear implicits.

(* const functor *)
Program Instance const_functor {C: Category}(X: C)(D: Category): Functor D C :=
  {
    fobj a := X;
    fmap a b f := Id X
  }.
Next Obligation.
  intros.
  now rewrite comp_id_dom.
Qed.

(* list functor *)
Require Import List.
Import List.ListNotations.

Program Instance list_functor: Functor Types Types :=
  {
    fmap X Y f := map f
  }.
Next Obligation.
  now intros X Y f g Heq l; apply map_ext, Heq.
Qed.
Next Obligation.
  intros X Y Z f g x; simpl.
  now rewrite map_map.
Qed.
Next Obligation.
  intros X l; simpl.
  now rewrite map_id.
Qed.

Class Natrans {C D: Category}(F G: Functor C D) :=
  {
    natrans: forall (X: C), hom (F X) (G X);
    naturality:
      forall (X Y: C)(f: hom X Y),
        fmap G f \o natrans X == natrans Y \o fmap F f
  }.
Coercion natrans: Natrans >-> Funclass.

Program Instance length_natrans: Natrans list_functor (const_functor (nat: Types) Types) :=
  {
    natrans := length
  }.
Next Obligation.
  intros X Y f l; simpl.
  now rewrite map_length.
Qed.