# Library Exercise_4_1_1_13

Require Import Utf8.
Require Import CategoryIsomorphisms Graph Category GraphCategory SetCategory.

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 4.1.1.13

## Problem

Suppose that G = (V, A, src, tgt) and G' = (V', A', src', tgt') are graphs and that f : (f0, f1) : G G' is a graph homomorphism (as in Definition 3.3.3.1). If f is an isomorphism in Grph, does this imply that f0 : V V' and f1 : A A' are isomorphisms in Set? If so, why; and if not, show a counterexample (where f is an isomorphism but either f0 or f1 is not).

Let Grph := CategoryOfGraph's.

Lemma Exercise_4_1_1_13
(G G' : Grph)
(f : Morphism Grph G G')
(f0 := OnVertices' f)
(f1 := OnArrows' f)
: IsomorphismOf (C := Grph) fIsomorphismOf (C := CategoryOfTypes) f0 × IsomorphismOf (C := CategoryOfTypes) f1.
intro i.
split;
[ ( (OnVertices' (Inverse i)))
| ( (OnArrows' (Inverse i))) ];
abstract (
subst f0 f1;
destruct i as [ i_f i_inv i_left i_right ];
simpl;
inversion i_left;
inversion i_right;
subst i_f;
reflexivity
).
Defined.
End Exercise_4_1_1_13.