Library ListFunctor


Require Import Utf8.
Require Import FunctionalExtensionality.
Require Export List.
Require Export Category Functor SetCategory.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

List Functor

Section ListFunctor.
For any set X, there is a set List(X) consisting of all lists whose entries are elements of X. In fact List : Set Set is a functor because for any function f : X Y we can apply it entry-by-entry to a list of X's to get a list of Y's (this was worked out in Exercise 4.1.2.17). But then we can compose List with itself to get a functor ListList : Set Set. Given X : Ob Set, the set ListList X is the set of lists of lists. For example if X := {1, 2, 3} then [ListList X] contains [[[1, 2, 3, 2], [2, 2] , [], [3]].

  Definition ListFunctor : Functor CategoryOfTypes CategoryOfTypes.
    refine (Build_Functor CategoryOfTypes CategoryOfTypes
                          list
                          map
                          _
                          _);
    abstract (
        simpl; intros;
        let x := fresh in
        apply functional_extensionality_dep; intro x;
        induction x;
        trivial;
        simpl;
        match goal with
          | [ H : _ |- _ ] ⇒ rewrite H; reflexivity
        end
      ).
  Defined.
End ListFunctor.