# Library Exercise_4_1_2_28

Require Import Utf8.
Require Import Omega JMeq.
Require Import Common DiscreteCategory NatCategory PathsCategory Graph ComputableCategory CategoryIsomorphisms ChainCategory.

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 4.1.2.28

## Problem

Let G be the graph depicted
```      v₀      e     v₁
o ----------> o
```
and let [1] : Ob Cat denote the free category on G (see Example 4.1.2.27). We call [1] the free arrow category. What are its objects? For every pair of objects in [1], write down the hom-set.
Lemma OneLeOne : 1 1. repeat constructor. Qed.
Lemma ZeroLeOne : 0 1. repeat constructor. Qed.
Lemma TwoNotLeOne n : S (S n) 1 → False. omega. Qed.

Inductive G_Vertex := G_v0 | G_v1.
Inductive G_Edge : G_VertexG_VertexSet := G_e : G_Edge G_v0 G_v1.

Definition G : Graph :=
{|
Vertex := G_Vertex;
Edge := G_Edge
|}.

Definition FreeArrowCategory := @PathsCategory (Vertex G) (Edge G).

Lemma E_4_1_2_28_Objects_G : Object FreeArrowCategory = Vertex G. reflexivity. Qed.

### Helper lemmas

Local Ltac t' tac :=
repeat match goal with
| _assumption
| _progress (repeat intro; hnf in *; subst_eq_refl; subst; trivial)
| _ ⇒ ( eq_refl)
| [ H : _ |- _ ] ⇒ solve [ inversion H; trivial ]
| [ H : _ |- _ ] ⇒ solve [ destruct H; trivial ]
| [ H : _ |- _ ] ⇒ specialize (H eq_refl)
| [ H : sigT _ |- _ ] ⇒ destruct H
| [ H : sig _ |- _ ] ⇒ destruct H
| [ H : context[match ?x with __ end] |- _ ] ⇒ destruct x
| _progress tac
end.

Lemma no_path'
: m (p : Morphism FreeArrowCategory G_v1 m),
{ Hm : G_v1 = m
| p = match Hm with
| eq_reflNoEdges
end }.
induction p; t' idtac.
Qed.
Lemma destruct_path v v' (p : Morphism FreeArrowCategory v v')
: { H : v = v' & match H
in (_ = y)
return (Morphism FreeArrowCategory v y Prop)
with
| eq_reflλ p0, p0 = NoEdges
end p }
+ { v'' : _ & { p' : path _ v v'' & { e : _ | p = AddEdge p' e } } }.
destruct p.
- left.
eq_refl.
reflexivity.
- right.
repeat esplit.
Defined.

Local Ltac t'' tac := t' ltac:(idtac;
match goal with
| [ H : _ |- _ ] ⇒ destruct (no_path' H)
end;
tac).

Local Ltac t :=
intros;
hnf in *;
match goal with
| [ p : path _ _ _ |- _ ] ⇒ induction p; solve [ t'' idtac ]
| [ p : path _ _ _ |- _ ] ⇒ destruct p; solve [ t'' idtac ]
| [ p : path _ _ _ |- _ ] ⇒ destruct (destruct_path p); solve [ t'' idtac ]
end.

Lemma one_path'
: m n (p : Morphism FreeArrowCategory n m)
(Hn : G_v0 = n)
(Hm : G_v1 = m),
p = match Hn with
| eq_reflmatch Hm with
end
end.
induction p;
repeat match goal with
| [ d : G_Vertex |- _ ] ⇒ destruct d
| _progress (t' idtac)
| _apply f_equal2
| _t
| [ d : G_Edge _ _ |- _ ] ⇒ try solve [ apply JMeq_eq; destruct d; reflexivity ]
end.
Qed.

Lemma E_4_1_2_28_Hom_v0_v0
: m : Morphism FreeArrowCategory G_v0 G_v0, m = NoEdges. Proof. t. Qed.
Lemma E_4_1_2_28_Hom_v1_v1
: m : Morphism FreeArrowCategory G_v1 G_v1, m = NoEdges. Proof. t. Qed.
Lemma E_4_1_2_28_Hom_v1_v0
: Morphism FreeArrowCategory G_v1 G_v0False. Proof. t. Qed.
Lemma E_4_1_2_28_Hom_v0_v1
: m : Morphism FreeArrowCategory G_v0 G_v1, m = AddEdge NoEdges G_e.
Proof. exact (fun m ⇒ @one_path' _ _ m eq_refl eq_refl). Qed.
End Exercise_4_1_2_28.