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.


Section Exercise_4_3_2_5.


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)).
  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)
                                                                                      _) |};
      try apply NaturalTransformation_Eq;
      abstract (repeat (reflexivity || intros [])).
    Grab Existential Variables.
    abstract (intros [] ? []; simpl; repeat rewrite FIdentityOf; reflexivity).
End Exercise_4_3_2_5.