# Library Exercise_4_4_1_1

Require Import Utf8.
Require Import FunctionalExtensionality JMeq EqdepFacts.
Require Import Graph PathsCategory ChainCategory UnderlyingGraph Graph PathsFunctor Morphism.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 4.4.1.1

## Problem

Note: This is an out-dated version of the problem statement, which requires that the maps be injective as graph homomorphisms, rather than just injective on edges.
Let [2] denote the linear order graph of length 2 (see Exercise 4.1.1.8 and Proposition 4.1.2.6), and let Loop denote the unique graph having one vertex and one arrow (pictured in Diagram (3.15)).
(a) Find an injective graph homomorphism f : [2] Paths(Loop).
(b) The graph [2] has 6 paths, so Paths([2]) has 6 arrows. What are the images of these arrows under the graph homomorphism Paths(f) : Paths([2]) Paths(Paths(Loop))?

Definition Loop : Graph := {| Vertex := unit; Edge := (fun _ _ unit) |}.
Inductive LinearOrder2Graph_Vertex := Zero | One | Two.
Inductive LinearOrder2Graph_Edge
: LinearOrder2Graph_VertexLinearOrder2Graph_VertexSet :=
| Zero_One : LinearOrder2Graph_Edge Zero One
| One_Two : LinearOrder2Graph_Edge One Two.
Definition LinearOrder2Graph : Graph
:= {| Vertex := LinearOrder2Graph_Vertex;
Edge := LinearOrder2Graph_Edge |}.
Fixpoint nth_edge_in_loop (n : ) : path (fun _ _unit) tt tt
:= match n with
| ONoEdges
| S n'AddEdge (nth_edge_in_loop n') tt
end.
Definition f (n m : ) : GraphHomomorphism LinearOrder2Graph (PathsFunctor Loop)
:= Build_GraphHomomorphism LinearOrder2Graph
(PathsFunctor Loop)
(fun _tt)
(fun src tgt
match src, tgt with
| Zero, One
(fun _nth_edge_in_loop n)
| One, Two
(fun _nth_edge_in_loop m)
| _, _fun xNoEdges
end).

Lemma Exercise_4_4_1_1_a_vert n m
: is_injective (OnVertices (f n m)) → False.
subst_body; clear; simpl.
intro H.
specialize (H One Two eq_refl).
inversion H.
Qed.
Lemma nth_edge_in_loop_injective
: is_injective nth_edge_in_loop.
intro x; induction x;
intro y; induction y;
intuition;
match goal with
| [ H : _ |- _ ] ⇒ try solve [ inversion H; firstorder ]
end.
Qed.
Definition f' n m := GraphHomomorphismToGraph'Homomorphism (f n m).
Lemma Exercise_4_4_1_1_a_edges n m
: m nis_injective (OnArrows' (f' n m)).
subst_body; clear; simpl.
intro.
assert (n m) by intuition.
intros x y.
simpl in *;
repeat intro;
try reflexivity;
repeat match goal with
| [ H : @eq (sigT _) _ _ |- _ ] ⇒
apply EqdepFacts.eq_sigT_eq_dep in H;
apply eq_dep_JMeq in H;
apply JMeq_eq in H
| [ H : _ = _ |- _ ] ⇒ apply nth_edge_in_loop_injective in H
end;
firstorder.
Qed.
Definition Paths2 := PathsFunctor LinearOrder2Graph.
Definition Paths2Path0 : Edge Paths2 Zero Zero
:= NoEdges.
Definition Paths2Path1 : Edge Paths2 One One
:= NoEdges.
Definition Paths2Path2 : Edge Paths2 Two Two
:= NoEdges.
Definition Paths2Path3 : Edge Paths2 Zero One
Definition Paths2Path4 : Edge Paths2 One Two
Definition Paths2Path5 : Edge Paths2 Zero Two

Section part_b.
Local Notation "[ a , .. , b ]" := (AddEdge .. (AddEdge NoEdges a) .. b).
Local Notation "[]" := NoEdges.

Variables n m : .

Local Notation "'Paths_f' a" := ((MorphismOf PathsFunctor (f n m)) a) (at level 10).
Local Notation "a ~> b" := (Edge _ a b).
Local Notation "a ~~> b" := (path _ a b).

Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path0.

Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path1.

Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path2.

Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path3.

Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path4.

Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path5.
End part_b.
End Exercise_4_4_1_1.