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.


Exercise 4.3.1.9

Section Exercise_4_3_1_9.

Problem

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)
                          ListFunctor.
    refine {| ComponentsOf := SingletonList |}.
    compute.
    reflexivity.
  Defined.
End Exercise_4_3_1_9.