Library Exercise_4_1_2_21


Require Import Utf8.
Require Import Category CategoryIsomorphisms Functor.

Set Implicit Arguments.

Generalizable All Variables.

Exercise 4.1.2.21

Problem

Suppose that C and D are categories, c c' : Ob C are objects, and F : C D is a functor. Suppose that c and c' are isomorphic in C. Show that this implies that F(c) and F(c') are isomorphic in D.

  Context `(C : @Category objC).
  Context `(D : @Category objD).
  Variable F : Functor C D.

  Local Open Scope category_scope.
  Definition FIsomorphismOf
             (c c' : C)
             (Fc : D := F c)
             (Fc' : D := F c')
  : c c'Fc Fc'.
    subst Fc Fc'.
    intro i.
     (MorphismOf F i).
     (MorphismOf F (i -1));
      abstract (
          rewrite <- FCompositionOf;
          rewrite <- FIdentityOf;
          apply f_equal;
          destruct i as [ ? [] ];
          intuition
        ).
  Defined.
End Exercise_4_1_2_21.