Library Exercise_4_3_1_9

Require Import Utf8.
Require Import List.
Require Import ListFunctor NaturalTransformation SetCategory.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.


Section Exercise_4_3_1_9.


Let List : Set Set be as above. If someone said "singleton lists give a natural transformation from id_Set to List", what might they mean? Would they be correct?

  Definition SingletonList (S : CategoryOfTypes)
  : Morphism CategoryOfTypes
             ((IdentityFunctor CategoryOfTypes) S)
             (ListFunctor S)
    := fun xx :: nil.

  Definition SingletonNaturalTransformation
  : NaturalTransformation (IdentityFunctor CategoryOfTypes)
    refine {| ComponentsOf := SingletonList |}.
End Exercise_4_3_1_9.