# Library Exercise_4_3_2_5

Require Import Utf8.
Require Import FunctionalExtensionality.
Require Import NaturalTransformation FunctorCategory InitialTerminalCategory SetCategory Isomorphism.
Require Import Common FEqualDep.

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 4.3.2.5

Section Exercise_4_3_2_5.

## Problem

Let C := {A} be the category with Ob C = {A}, and Hom_C(A,A) = {id_A}. What is Fun(C, Set)? In particular, characterize the objects and the morphisms.
Let C := TerminalCategory.
Let FunCSet := FunctorCategory C CategoryOfSets.
Eval hnf in Object FunCSet.
Eval hnf in Morphism FunCSet.
Lemma FunCSet_Iso_Set : Object FunCSet Set.
refine {| isomorphic_morphism := (fun F : FunCSet ObjectOf F tt) |}.
refine {| isomorphism_inverse := (fun S : Set FunctorFromTerminal CategoryOfSets S) |};
abstract (repeat (reflexivity
|| intros []
|| intro
|| apply Functor_Eq
|| rewrite FIdentityOf
|| subst_eq_refl_in_match
|| compute)).
Defined.
Lemma FunCSet_Hom_Iso_Set (X Y : FunCSet)
(X' := FunCSet_Iso_Set X)
(Y' := FunCSet_Iso_Set Y)
: Morphism FunCSet X Y (X'Y').
refine {| isomorphic_morphism := (fun T : NaturalTransformation X Y T tt) |}.
refine {| isomorphism_inverse := (fun f : X' Y' Build_NaturalTransformation X Y
(fun x match x with tt f end)
_) |};
intros;
try apply NaturalTransformation_Eq;
simpl;
abstract (repeat (reflexivity || intros [])).
Grab Existential Variables.
abstract (intros [] ? []; simpl; repeat rewrite FIdentityOf; reflexivity).
Defined.
End Exercise_4_3_2_5.