# 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.

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.