Set Implicit Arguments.
Unset Strict Implicit.


Require Export updateA.



Module Uple.
Export UpdateA.
Export Universe.



(** An uple is a list indexed by natural numbers, which we
view as a function whose domain is a natural number.
The domain is the length, and the valid indices are all
those which are strictly less than the length (starting with [0]).
*)


Definition axioms a :=
Function.axioms a &
inc (domain a) nat.

Definition length a := Bnat (domain a).

Definition create (f:nat -> E) (l:nat) :=
Function.create (R l) (fun x => f (Bnat x)).

Lemma domain_create : forall f l, domain (create f l) = R l.
Proof.
ir. 
uf create. 
rw Function.create_domain. tv. 
Qed.

Lemma length_create : forall f l, length (create f l) = l.
Proof.
ir. uf length. rw domain_create. rww Bnat_R. 
Qed.

Definition component (i:nat) a :=
V (R i) a.


Lemma component_create : forall f l i,
i < l -> component i (create f l) = f i.
Proof.
ir. uf component. wri inc_lt H. 
uf create. rw create_V_rewrite. 
rw Bnat_R. tv. am. 
Qed. 

Lemma create_axioms : forall f l, axioms (create f l).
Proof.
ir. uhg; ee. 
uf create. ap Function.create_axioms. 
rw domain_create. ap R_inc. 
Qed.

Lemma eq_create : forall a, axioms a ->
a = create (fun i => component i a) (length a).
Proof.
ir. 
cp H. uh H; ee. 
cp (Function.create_recovers H). 
transitivity (Function.create (domain a) (fun x : E => V x a)).
sy; am. uf create. 
uf length. rw R_Bnat. 
ap Function.create_extensionality. tv. ir. 
uf component. rw R_Bnat. tv. 
assert (sub (domain a) nat). 
assert (domain a = R (B H1)). rww B_eq. 
rw H5. ap sub_R_nat. app H5. am. 
Qed.

Lemma compare_create : forall f g l m,
l = m -> (forall i, Peano.lt i l -> f i = g i) ->
create f l = create g m.
Proof.
ir. wr H. uf create. 
ap Function.create_extensionality. tv. 
ir. ap H0. wr inc_lt. rww R_Bnat. 
ap inc_nat_from_inc_R. sh l. am. 
Qed. 

Lemma domain_emptyset : domain emptyset = emptyset.
Proof. 
uf domain;
ap extensionality; uhg; ir. 
rwi Image.inc_rw H. nin H. ee. 
nin H. elim x1. 
nin H. elim x0. 
Qed. 

Lemma empty_axioms : axioms emptyset.
Proof.
ir. uhg; ee. 
set (k:= Function.identity emptyset). 
apply sub_axioms with k. uf k. ap Function.identity_axioms. 
uhg; ir. nin H. elim x0. 
rw domain_emptyset. 
wr nat_zero_emptyset. ap R_inc. 
Qed.

Lemma length_emptyset : length emptyset = 0.
Proof.
uf length. rw domain_emptyset. 
wr nat_zero_emptyset. rw Bnat_R. tv. 
Qed.

Lemma create_length_zero : forall f ,
create f 0 = emptyset.
Proof.
ir. cp (eq_create empty_axioms). 
rw H. ap compare_create. rww length_emptyset. 
ir. cp lt_n_O. elim (H1 i H0). 
Qed. 



Lemma uple_extensionality : forall a b,
axioms a -> axioms b -> 
length a = length b ->
(forall i, i < (length a) -> component i a = component i b) ->
a=b.
Proof.
ir. cp (eq_create H). cp (eq_create H0). 
rw H3; rw H4. ap compare_create. am. am. 
Qed.


Definition concatenate a b :=
create (fun i => 
Y (i < (length a)) (component i a) 
(component (i - (length a)) b))
((length a) + (length b)).

Lemma length_concatenate : forall a b,
length (concatenate a b) = (length a) + (length b).
Proof.
ir. uf concatenate. rww length_create. 
Qed.

Lemma concatenate_axioms : forall a b,
axioms (concatenate a b).
Proof.
ir. uf concatenate. ap create_axioms. 
Qed. 

Lemma component_concatenate_first : forall a b i,
i < (length a) -> component i (concatenate a b) = component i a.
Proof.
ir. uf concatenate. 
rw component_create. 
rw Y_if_rw. tv. am. 
auto with arith. 
Qed.

Lemma component_concatenate_second : forall a b i,
i < (plus (length a) (length b)) ->
(length a) <= i ->
component i (concatenate a b) = component (i - (length a)) b.
Proof.
ir. uf concatenate. rw component_create. 
rw Y_if_not_rw. tv. auto with arith. am. 
Qed.

Lemma component_concatenate_plus : forall a b i,
i < (length b) -> 
component ((length a) + i ) (concatenate a b) = component i b.
Proof.
ir. rw component_concatenate_second. 
rw minus_plus. tv. 
assert (i+length a = length a + i). auto with arith. 
auto with arith. auto with arith. 
Qed.

Lemma concatenate_emptyset_left : forall a,
axioms a -> 
concatenate emptyset a = a.
Proof.
ir. ap uple_extensionality. 
ap concatenate_axioms. am. 
rw length_concatenate. rw length_emptyset. 
auto with arith. 

ir. rw component_concatenate_second. rw length_emptyset. 
assert (i- 0 = i). auto with arith. rww H1. 
rwi length_concatenate H0. am. 
rw length_emptyset. auto with arith. 
Qed.

Lemma concatenate_emptyset_right : forall a,
axioms a ->
concatenate a emptyset = a.
Proof.
ir. ap uple_extensionality. ap concatenate_axioms. 
am. rw length_concatenate. rw length_emptyset. 
auto with arith. 
ir. rw component_concatenate_first. tv. 
rwi length_concatenate H0. rwi length_emptyset H0. 
assert (length a + 0 = length a). auto with arith. 
wrr H1. 
Qed.





Lemma concatenate_assoc : forall a b c,
concatenate a (concatenate b c) = 
concatenate (concatenate a b) c.
Proof.
ir. ap uple_extensionality. 
ap concatenate_axioms. ap concatenate_axioms. 
rw length_concatenate. 
rw length_concatenate. 
rw length_concatenate. 
rw length_concatenate. 
auto with arith. 

ir. apply by_cases with (i < length a + length b); ir.
apply by_cases with (i<length a); ir. 
rw component_concatenate_first. rw component_concatenate_first. 
rw component_concatenate_first. tv. am. 
rww length_concatenate. am. 
assert (length a <= i). 
nin (le_or_lt (length a) i). tv. 
elim (H1 H2). 
rw component_concatenate_second. rw component_concatenate_first. 
rw component_concatenate_first. rw component_concatenate_second. 
tv. am. am. rww length_concatenate. 
om. 

rw length_concatenate. rw plus_assoc. 
auto with arith. am. 
assert (length a + length b <= i). om. 
rwi length_concatenate H.
rwi length_concatenate H. 
rw component_concatenate_second. 
rw component_concatenate_second. 
rw component_concatenate_second. 
rw length_concatenate. 
assert (i - length a - length b = i - (length a + length b)).
om. rw H2. tv. 
rw length_concatenate. om. 
rw length_concatenate. om. 
om. om. 
rw length_concatenate. om. 
om. 
Qed. 

Definition uple1 x :=
create (fun i:nat => x) 1.

Lemma uple1_axioms : forall x, 
axioms (uple1 x). 
Proof.
ir. uf uple1. ap create_axioms. 
Qed.

Lemma length_uple1 : forall x, length (uple1 x) = 1.
Proof.
ir. uf uple1. rww length_create. 
Qed. 

Lemma component_uple1 : forall x i, 
i < 1 -> component i (uple1 x) = x.
Proof.
ir. uf uple1. 
rw component_create. tv. am. 
Qed. 

Lemma eq_uple1 : forall a x,
axioms a -> length a = 1 -> x = component 0 a -> 
a = uple1 x.
Proof.
ir. rw H1. ap uple_extensionality. 
am. ap uple1_axioms. 
rw length_uple1. am. 
ir. rw component_uple1. assert (i=0).
om. rww H3. om. 
Qed. 

Definition utack x a :=
concatenate a (uple1 x).

Lemma utack_axioms : forall a x,
axioms a -> axioms (utack x a).
Proof.
ir. uf utack. ap concatenate_axioms. 
Qed.

Lemma length_utack : forall a x,
axioms a -> length (utack x a) = (length a) + 1.
Proof.
ir. uf utack. rw length_concatenate. 
rww length_uple1. 
Qed.

Lemma domain_R_length : forall a,
axioms a -> domain a = R (length a).
Proof.
ir. uf length. rw R_Bnat. tv. 
uh H; ee. am. 
Qed. 

Lemma inc_R_domain : forall a i,
axioms  a -> 
inc (R i) (domain a) = (i < (length a)).
Proof.
ir. 
rw domain_R_length. 
rw inc_lt. tv. am. 
Qed.

Lemma component_utack_old : forall a x i,
axioms a -> i < (length a) -> 
component i (utack x a) = component i a.
Proof.
ir. uf utack. 
rw component_concatenate_first. tv. am. 
Qed.

Lemma component_utack_new : forall a x i,
axioms a -> i = length a ->
component i (utack x a) = x.
Proof.
ir. uf utack. rw component_concatenate_second. 
rw H0. 
rw component_uple1. tv. 
wr minus_n_n. auto with arith. 
rw length_uple1. rw H0. 
assert (length a + 1 = S (length a)). 
rw plus_comm. auto with arith. rw H1. 
ap lt_n_Sn. rw H0. auto with arith. 
Qed.

Definition restrict a i :=
create (fun j => component j a) i.

Lemma length_restrict : forall a i,
length (restrict a i) = i.
Proof.
ir. uf restrict. 
rw length_create. tv. 
Qed.

Lemma component_restrict : forall a i j,
j < i -> component j (restrict a i) = component j a.
Proof.
ir. uf restrict. 
rw component_create. tv. am. 
Qed.

Lemma restrict_axioms : forall a i,
axioms (restrict a i).
Proof. 
ir. uf restrict. 
ap create_axioms. 
Qed.

Lemma eq_utack_restrict : forall a,
axioms a -> length a > 0 -> 
a = utack (component (length a - 1) a) (restrict a (length a -1)).
Proof.
ir. 
ap uple_extensionality. 
am. ap utack_axioms. ap restrict_axioms. 
rw length_utack. rw length_restrict. om. 
ap restrict_axioms. 

ir. 
assert (i = length a - 1 \/ i < length a -1).
om. nin H2. 
rw H2. rw component_utack_new. tv. 
ap restrict_axioms. 
rw length_restrict. tv. 
rw component_utack_old. rw component_restrict. 
tv. am. ap restrict_axioms. rw length_restrict. am. 
Qed. 


Definition uple_map (f:E ->E) u :=
Uple.create  (fun i => f (component i u)) (length u).

Lemma length_uple_map : forall f u,
length (uple_map f u) = length u.
Proof.
ir. uf uple_map. rw length_create. tv. 
Qed.

Lemma component_uple_map : forall f u i,
i < length u -> component i (uple_map f u) = f (component i u).
Proof.
ir. 
uf uple_map. rw component_create. tv. am. 
Qed. 

Lemma axioms_uple_map : forall f u, axioms (uple_map f u).
Proof.
ir. uf uple_map. ap create_axioms. 
Qed. 


Lemma uple_map_uple1 : forall f u,
uple_map f (uple1 u) = uple1 (f u).
Proof.
ir. ap uple_extensionality. 
ap axioms_uple_map. ap uple1_axioms. 
rww length_uple_map. rw length_uple1. 
rww length_uple1. 
ir. rwi length_uple_map H. 
rwi length_uple1 H. assert (i=0). om. 
rw H0. rw component_uple_map. 
rw component_uple1. rw component_uple1. tv. om. om. 
rw length_uple1. om. 
Qed. 

Lemma uple_map_emptyset : forall f,
uple_map f emptyset = emptyset.
Proof.
ir. ap uple_extensionality. 
ap axioms_uple_map. 
ap Uple.empty_axioms. rww length_uple_map. 
ir. rwi length_uple_map H. 
rwi length_emptyset H. assert (0=1).
om. discriminate H0. 
Qed. 

Lemma uple_map_concatenate : forall f u v,
uple_map f (concatenate u v) = concatenate (uple_map f u)
(uple_map f v).
Proof.
ir. ap uple_extensionality. 
ap axioms_uple_map. 
ap concatenate_axioms. rw length_uple_map. 
rw length_concatenate. rw length_concatenate. 
rw length_uple_map. rw length_uple_map. tv. 

ir. rwi length_uple_map H. rwi length_concatenate H. 
rw component_uple_map. assert (i < length u \/ 
length u <= i). om. nin H0. 
rw component_concatenate_first. rw component_concatenate_first.
rw component_uple_map. tv. am. rw length_uple_map. am. 
am. rw component_concatenate_second. rw component_concatenate_second. 
rw length_uple_map. 
rw component_uple_map. tv. om. 
rw length_uple_map. rw length_uple_map. am. rw length_uple_map.
am. am. am. rw length_concatenate. am. 
Qed. 

End Uple.

Module Graph.
Export Uple. 

Definition Vertices   := R (v_(r_(t_ DOT ))).
Definition Edges := R (e_(d_(g_ DOT))).

Definition vertices a := V Vertices a.
Definition edges a := V Edges a.

Definition create v e :=
denote Vertices v 
(denote Edges e stop).

Definition like a := a = create  (vertices a) (edges a).

Lemma vertices_create : forall v e, vertices (create v e) =v.
Proof.
ir; uf vertices; uf create. drw. 
Qed.

Lemma edges_create : forall v e, edges (create v e) = e.
Proof.
ir; uf edges; uf create. drw. 
Qed. 



Lemma create_like : forall v e, like (create v e).
Proof.
ir. uf like. 
rw vertices_create. rw edges_create. tv. 
Qed.

Lemma like_extensionality : forall a b,
like a -> like b -> vertices a = vertices b ->
edges a = edges b -> a = b.
Proof.
ir. uh H; uh H0. 
rw H ; rw H0. 
rw H1; rw H2. tv. 
Qed. 

Definition axioms a :=
like a &
(forall u, inc u (edges a) -> Arrow.like u) &
(forall u, inc u (edges a) -> inc (source u) (vertices a)) &
(forall u, inc u (edges a) -> inc (target u) (vertices a)).

Lemma axioms_extensionality : forall a b,
axioms a -> axioms b -> vertices a = vertices b ->
edges a = edges b -> a = b.
Proof.
ir. uh H; uh H0. ee. app like_extensionality. 
Qed. 


End Graph.

Module Free_Category.
Export Graph.

(** Now we define the free category on a graph. ***)

Definition segment (i:nat) u :=
component i (arrow u).

Definition seg_length u :=
length (arrow u).

Definition arrow_chain u :=
Arrow.like u &
Uple.axioms (arrow u) &
(0 < seg_length u -> source (segment 0 u) = source u) &
(0 < seg_length u -> 
target (segment (seg_length u -1) u) = target u) &
(forall i, i+1 < seg_length u ->
source (segment (i+1) u) = 
target (segment i u)) &
(seg_length u = 0 -> source u = target u).

Definition mor_freecat a u :=
axioms a & 
inc (source u) (vertices a) &
inc (target u) (vertices a) &
arrow_chain u &
(forall i, i < seg_length u ->
inc (segment i u) (edges a)).

Definition vertex_uple u :=
concatenate 
(Uple.create (fun i => source (segment i u)) (seg_length u))
(uple1 (target u)).

Definition vertex_uple' u := 
concatenate (uple1 (source u))
(Uple.create (fun i => target (segment i u)) (seg_length u)).

Lemma length_vertex_uple : forall u,
length (vertex_uple u) = seg_length u + 1.
Proof.
ir. uf vertex_uple. rw length_concatenate. 
rw length_create. rw length_uple1. tv. 
Qed.

Lemma length_vertex_uple' : forall u,
length (vertex_uple' u) = seg_length u + 1.
Proof.
ir. uf vertex_uple'. rw length_concatenate. 
rw length_create. rw length_uple1. tv. 
om. Qed.



Lemma vertex_uples_same : forall u,
arrow_chain u -> 
vertex_uple u = vertex_uple' u.
Proof.
ir. 
ap uple_extensionality. 
uf vertex_uple. 
ap concatenate_axioms. 
uf vertex_uple'. 
ap concatenate_axioms. 
rw length_vertex_uple. rww length_vertex_uple'. 

ir. 
apply by_cases with (0 < i); ir. 
apply by_cases with (i < seg_length u); ir.
uf vertex_uple. rw component_concatenate_first.
rw component_create. 
uf vertex_uple'. rw component_concatenate_second. 
rw component_create. rw length_uple1. 
uh H; ee. 
transitivity (source (segment ((i-1) + 1) u)).
assert (i-1+1 = i). om. 
rw H8. tv. ap H6. om. om. 
rw length_uple1. rw length_create. om. 
rw length_uple1. om. am. 
rw length_create. am. 


assert (i = seg_length u). 
rwi length_vertex_uple H0. om. rw H3. 
uf vertex_uple. rw component_concatenate_second.
rw length_create. rw component_uple1. 

uf vertex_uple'. rw component_concatenate_second. 
rw length_uple1. rw component_create. uh H; ee.
rw H6. tv. om. om. rw length_uple1. 
rw length_create. om. rw length_uple1. om.
om. rw length_create. rw length_uple1. 
om. rw length_create. om. 

assert (i=0). om. rw H2. 
apply by_cases with (0 < seg_length u); ir.
uf vertex_uple. rw component_concatenate_first. 
rw component_create. uf vertex_uple'. 
rw component_concatenate_first. rw component_uple1. 
uh H; ee. ap H5. am. 
om. rw length_uple1; om. am. 
rw length_create. am. 

assert (seg_length u = 0). om. 

uf vertex_uple. rw component_concatenate_second. 
rw length_create. rw component_uple1. 
uf vertex_uple'. 
rw component_concatenate_first. rw component_uple1. 
uh H; ee. sy; ap H9. am. om. 
rw length_uple1. om. om. 
rw length_create. rw length_uple1. 
om. rw length_create. om. 
Qed.


Definition freecat_comp u v :=
Arrow.create (source v) (target u)
(concatenate (arrow v) (arrow u)).

Lemma seg_length_freecat_comp : forall u v,
seg_length (freecat_comp u v) = seg_length u + seg_length v.
Proof.
ir. uf freecat_comp. 
uf seg_length. rw Arrow.arrow_create. rww length_concatenate. 
rww plus_comm. 
Qed. 

Lemma segment_freecat_comp_first : forall u v i,
i < seg_length v -> segment i (freecat_comp u v) 
= segment i v.
Proof.
ir. uf freecat_comp. uf segment. 
rw Arrow.arrow_create. 
rw component_concatenate_first. tv. 
am. 
Qed.

Lemma segment_freecat_comp_second : forall u v i,
seg_length v <= i -> i < seg_length u + seg_length v ->
segment i (freecat_comp u v) = 
segment (i -seg_length v) u.
Proof.
ir. uf freecat_comp. uf segment. 
rw Arrow.arrow_create. 
rw component_concatenate_second.
tv. ufi seg_length H0. om. 
am. 
Qed. 
 

Definition freecat_id x := 
Arrow.create x x emptyset.

Lemma seg_length_freecat_id : forall x, 
seg_length (freecat_id x) = 0.
Proof.
ir. uf freecat_id. 
uf seg_length. rw Arrow.arrow_create. 
rww length_emptyset. 
Qed. 

Lemma arrow_chain_extensionality : forall u v,
arrow_chain u -> arrow_chain v ->
seg_length u = seg_length v ->
source u = source v -> target u = target v -> 
(forall i, i< seg_length u -> segment i u = segment i v) ->
u = v.
Proof.
ir. 
assert (Arrow.like u). 
uh H; ee; am. 
assert (Arrow.like v). 
uh H0; ee; am. 
uh H5; uh H6. rw H5; rw H6.
rw H2. rw H3. ap uneq. 
ap uple_extensionality. 
uh H; ee; am. uh H0; ee; am. 
am. am. 
Qed. 

Definition freecat_edge b :=
Arrow.create (source b) (target b) (uple1 b).

Lemma seg_length_freecat_edge : forall b,
seg_length (freecat_edge b) = 1.
Proof.
ir. uf freecat_edge. 
uf seg_length. rw Arrow.arrow_create. 
rww length_uple1. 
Qed.

Lemma segment_freecat_edge : forall b i,
i = 0 -> segment i (freecat_edge b) = b.
Proof.
ir. uf freecat_edge; uf segment.
rw Arrow.arrow_create. 
rw component_uple1. tv. om. 
Qed.

Lemma source_first_segment : forall u i,
arrow_chain u -> 0 < seg_length u -> i = 0 ->
source (segment i u) = source u. 
Proof.
ir. 
uh H; ee. rw H1. ap H3. am. 
Qed.

Lemma target_last_segment : forall u i,
arrow_chain u -> 0 < seg_length u -> 
i = seg_length u - 1 -> 
target (segment i u) = target u.
Proof.
ir. uh H; ee. rw H1. ap H4. am. 
Qed. 

Lemma eq_freecat_edge : forall u x,
arrow_chain u -> seg_length u = 1 ->
x = (segment 0 u) ->
u = freecat_edge x.
Proof.
ir. 
rw H1. 
uf freecat_edge. 
uh H; ee. uh H. 
transitivity (Arrow.create (source u) (target u) (arrow u)).
am. rw source_first_segment. 
rw target_last_segment. 
ap uneq. ap eq_uple1. 
am. am. tv. uhg; ee; am. om. 
om. uhg; ee; am. om. tv. 
Qed.




Lemma source_freecat_id : forall x,
source (freecat_id x) = x.
Proof.
ir. uf freecat_id. 
rww Arrow.source_create. 
Qed.

Lemma target_freecat_id : forall x, 
target (freecat_id x) = x.
Proof.
ir. uf freecat_id. 
rww Arrow.target_create. 
Qed.

Lemma source_freecat_edge : forall b,
source (freecat_edge b) = source b.
Proof.
ir. uf freecat_edge. rww Arrow.source_create. 
Qed.

Lemma target_freecat_edge : forall b,
target (freecat_edge b) = target b.
Proof.
ir. uf freecat_edge. rww Arrow.target_create. 
Qed.

Lemma source_freecat_comp : forall u v,
source (freecat_comp u v) = source v.
Proof.
ir. 
uf freecat_comp. rww Arrow.source_create. 
Qed.

Lemma target_freecat_comp : forall u v,
target (freecat_comp u v) = target u.
Proof.
ir. 
uf freecat_comp. rww Arrow.target_create. 
Qed.


Lemma arrow_freecat_id : forall x, 
arrow (freecat_id x) = emptyset.
Proof.
ir. uf freecat_id. rw Arrow.arrow_create.
tv. 
Qed.

Lemma arrow_freecat_edge : forall b,
arrow (freecat_edge b) = uple1 b.
Proof.
ir. uf freecat_edge. rw Arrow.arrow_create.
tv. 
Qed.

Lemma arrow_freecat_comp : forall u v,
arrow (freecat_comp u v) = 
concatenate (arrow v) (arrow u). 
Proof.
ir. uf freecat_comp. rw Arrow.arrow_create.
tv. 
Qed.

Lemma arrow_chain_freecat_id : forall x,
arrow_chain (freecat_id x).
Proof.
ir. 
uhg; ee. 
uf freecat_id. rww Arrow.create_like. 
rw arrow_freecat_id. 
ap Uple.empty_axioms. 
ir. 
rwi seg_length_freecat_id H. 
elim (lt_irrefl _ H). 
ir. 
rwi seg_length_freecat_id H. 
elim (lt_irrefl _ H). 
ir. 
rwi seg_length_freecat_id H. 
assert (1 = 0). om. discriminate H0. 
ir. 
rw source_freecat_id. rww target_freecat_id. 
Qed. 

Lemma eq_freecat_id : forall u,
arrow_chain u -> seg_length u = 0 -> 
u = freecat_id (source u).
Proof.
ir. ap arrow_chain_extensionality. 
am. 
ap arrow_chain_freecat_id. 
rw seg_length_freecat_id. am. 
rw source_freecat_id. tv. 
rw target_freecat_id. 
uh H; ee. sy; au. 
ir. assert (0=1). om. 
discriminate H2. 
Qed. 


Lemma arrow_chain_freecat_edge : forall b,
arrow_chain (freecat_edge b).
Proof.
ir. 
uhg; ee. 
uf freecat_edge. 
rww Arrow.create_like. 
rw arrow_freecat_edge. 
ap uple1_axioms. 

ir. 
rw segment_freecat_edge. rww source_freecat_edge. 
tv. 

ir. rw seg_length_freecat_edge. 
rw segment_freecat_edge. rww target_freecat_edge. 
om. 

ir. rwi seg_length_freecat_edge H. 
assert (0 = 1). om. discriminate H0. 
ir. rwi seg_length_freecat_edge H. discriminate H. 
Qed. 

Lemma arrow_chain_freecat_comp : forall u v,
arrow_chain u -> arrow_chain v -> source u = target v ->
arrow_chain (freecat_comp u v).
Proof.
ir. 
uhg; ee. 
uf freecat_comp. 
rww Arrow.create_like. 
uf freecat_comp. rw Arrow.arrow_create. 
ap concatenate_axioms. 

ir. 
rwi seg_length_freecat_comp H2. 
assert ((seg_length v = 0 /\ 0 < seg_length u) \/ 0 < seg_length v).
om. nin H3. ee. 
rw segment_freecat_comp_second. rw H3. 
rw source_freecat_comp. 
uh H0; ee.
cp (H9 H3). rw H10. wr H1. 
uh H; ee. assert (0 -0 = 0). tv. rw H16. 
ap H12. am. om. am. 

rw segment_freecat_comp_first. 
rw source_freecat_comp. uh H0; ee.
au. am. 


ir. 
rwi seg_length_freecat_comp H2. 
assert (0 < seg_length u \/ (seg_length u = 0 /\ 0 < seg_length v)).
om. 
nin H3. rw seg_length_freecat_comp. 
rw segment_freecat_comp_second. 
rw target_freecat_comp. 
assert (seg_length u + seg_length v - 1 - seg_length v
= seg_length u - 1).
om. rw H4. uh H; ee. 
au. om. om. 

ee. rw seg_length_freecat_comp. rw segment_freecat_comp_first.
rw target_freecat_comp. 
uh H; ee. cp (H9 H3). wr H10. rw H1. 
rw H3. assert (0 + seg_length v - 1 = seg_length v - 1).
om. rw H11. uh H0; ee.
au. om. 

ir. rwi seg_length_freecat_comp H2. 
apply by_cases with (i+1 < seg_length v); ir. 
rw segment_freecat_comp_first. 
rw segment_freecat_comp_first. uh H0; ee; au. 
om. om. 
apply by_cases with (i + 1 = seg_length v); ir.
rw segment_freecat_comp_second; try om. 
rw segment_freecat_comp_first; try om. 
uh H; uh H0; ee.
assert (i + 1 - seg_length v = 0).
rw H4. 
auto with arith. 
rw H15. rw H11. 
assert (i = seg_length v - 1). 
wr H4. clear H1 H2 H3 H4 H5 H6 H7 H8 H9 H10.
clear H0 H11 H12 H13 H14 H15. 
om. rw H16. rw H7. am. 
clear H1 H2 H3 H5 H6 H7 H8 H9 H10
H0 H11 H12 H13 H14 H15. 
om. 
clear H1 H3 H5 H6 H7 H8 H9 H10
H0 H11 H12 H13 H14 H15. 
om. 

assert (seg_length v < i+1).
om. assert (seg_length v <= i). om. 
rw segment_freecat_comp_second; try om. 
rw segment_freecat_comp_second; try om. 
set (j:= i-seg_length v). 
assert (i + 1 - seg_length v = j +1). uf j; om. 
rw H7. uh H; ee. 
ap H11. om. 

ir. rwi seg_length_freecat_comp H2. 
assert (seg_length u = 0 /\ seg_length v = 0). 
om. ee. 
uh H; uh H0. 
ee. cp (H9 H4). 
cp (H14 H3). rw source_freecat_comp. 
rw target_freecat_comp. rw H15. wr H16. sy; am. 
Qed.

Lemma arrow_like_extensionality : forall a b,
Arrow.like a -> Arrow.like b ->
source a = source b -> target a = target b ->
arrow a = arrow b -> a = b.
Proof.
ir. uh H; uh H0; rw H; rw H0.
rw H1; rw H2; rw H3. reflexivity. 
Qed.


Lemma freecat_assoc : forall u v w,
freecat_comp u (freecat_comp v w) =
freecat_comp (freecat_comp u v) w.
Proof.
ir. 
ap arrow_like_extensionality. 
uf freecat_comp; rww Arrow.create_like. 
uf freecat_comp; rww Arrow.create_like. 
rw source_freecat_comp. 
rw source_freecat_comp. 
rw source_freecat_comp. tv. 
rw target_freecat_comp. 
rw target_freecat_comp. 
rw target_freecat_comp. tv. 
rw arrow_freecat_comp. 
rw arrow_freecat_comp. 
rw arrow_freecat_comp. 
rw arrow_freecat_comp. 
sy; ap concatenate_assoc. 
Qed.

Lemma freecat_left_id' : forall u x,
Arrow.like u -> x = target u -> Uple.axioms (arrow u) ->
freecat_comp (freecat_id x) u = u.
Proof.
ir. 
ap arrow_like_extensionality. 
uf freecat_comp; rww Arrow.create_like. am. 
rw source_freecat_comp. tv. 
rw target_freecat_comp. rw target_freecat_id. 
am. 
rw arrow_freecat_comp. 
rw arrow_freecat_id. rw concatenate_emptyset_right.
tv. am. 
Qed.

Lemma freecat_right_id' : forall u x,
Arrow.like u -> x = source u -> Uple.axioms (arrow u) ->
freecat_comp u (freecat_id x) = u.
Proof.
ir. 
ap arrow_like_extensionality. 
uf freecat_comp; rww Arrow.create_like. am. 
rw source_freecat_comp. tv. 
rw source_freecat_id. am. 
rw target_freecat_comp. tv. 
rw arrow_freecat_comp. 
rw arrow_freecat_id. rw concatenate_emptyset_left.
tv. am. 
Qed.

Lemma freecat_left_id : forall u x,
arrow_chain u -> x = target u ->
freecat_comp (freecat_id x) u = u.
Proof.
ir. ap freecat_left_id'. uh H; ee; am. 
am. uh H; ee; am. 
Qed.

Lemma freecat_right_id : forall u x,
arrow_chain u -> x = source u ->
freecat_comp u (freecat_id x) = u.
Proof.
ir. ap freecat_right_id'. uh H; ee; am. 
am. uh H; ee; am. 
Qed.

Lemma uples_contained : forall b u,
Uple.axioms u -> 
(forall i, i<length u -> inc (component i u) b) ->
inc u (powerset (Cartesian.product nat b)).
Proof.
ir. 
rw powerset_inc_rw. 
uhg; ir. 
assert (is_pair x).
uh H; ee. 
uh H; ee. cp (H _ H1).
wr H4. 
ap pair_is_pair. 
assert (inc (pr1 x) (domain u)).
uh H; ee. app Function.lem2. 
assert (inc (pr1 x) nat).
uh H; ee. assert (sub (domain u) nat).
assert (domain u = R (B H4)). rw B_eq. tv. 
rw H5. ap sub_R_nat. ap H5. am. 
assert (inc (pr2 x) b). 
assert (pr2 x = V (pr1 x) u). 
ap Function.pr2_V. uh H; ee; am. am. 
rw H5. set (j:= Bnat (pr1 x)). 
assert (pr1 x = R j). uf j. rww R_Bnat. rw H6. 
change (inc (component j u) b). ap H0. 
rwi H6 H3. wr inc_lt. uf length. rw R_Bnat. am. 
uh H; ee. am. 
ap product_inc. am. am. am. 
Qed.


Lemma mor_freecat_from_set : forall a u,
mor_freecat a u -> 
inc u (Image.create 
(product (product (vertices a) (vertices a))
(powerset (product nat (edges a))))
(fun x => Arrow.create (pr1 (pr1 x)) (pr2 (pr1 x)) (pr2 x))).
Proof.
ir. 
rw Image.inc_rw. 
sh (pair (pair (source u) (target u)) (arrow u)).
ee. 
ap product_pair_inc. 
ap product_pair_inc. uh H; ee. am. 
uh H; ee; am. 
ap uples_contained. 
uh H; ee. 
uh H2; ee; am. uh H; ee. am. 
rw pr1_pair. rw pr1_pair. rw pr2_pair. rw pr2_pair. 
uh H; ee. uh H2; ee; sy; am. 
Qed.


Lemma mor_freecat_bounded : forall a,
Bounded.axioms (mor_freecat a).
Proof.
ir. 
ap Bounded.criterion. sh
(Image.create 
(product (product (vertices a) (vertices a))
(powerset (product nat (edges a))))
(fun x => Arrow.create (pr1 (pr1 x)) (pr2 (pr1 x)) (pr2 x))). 
ir. app mor_freecat_from_set. 
Qed. 

Definition freecat_morphisms a :=
Bounded.create (mor_freecat a).

Lemma inc_freecat_morphisms : forall a u,
inc u (freecat_morphisms a) = mor_freecat a u.
Proof.
ir. 
uf freecat_morphisms. 
rw Bounded.inc_create. tv. ap mor_freecat_bounded. 
Qed. 

Definition freecat a :=
Category.Notations.create 
(vertices a) (freecat_morphisms a) freecat_comp freecat_id
emptyset.

Lemma is_mor_freecat : forall a u,
is_mor (freecat a) u =  mor_freecat a u.
Proof.
ir. 
uf freecat. 
rw is_mor_create. rww inc_freecat_morphisms. 
Qed.

Lemma is_ob_freecat : forall a x,
is_ob (freecat a) x = inc x (vertices a).
Proof.
ir. uf freecat. rww is_ob_create. 
Qed.

Lemma comp_freecat1 : forall a u v,
mor_freecat a u -> mor_freecat a v ->
source u = target v -> 
comp (freecat a) u v = freecat_comp u v.
Proof.
ir. uf freecat. rww comp_create. 
rww inc_freecat_morphisms. rww inc_freecat_morphisms.
Qed.

Lemma id_freecat1 : forall a x,
inc x (vertices a) -> 
id (freecat a) x = freecat_id x.
Proof.
ir. uf freecat. rww id_create. 
Qed.

Lemma structure_freecat : forall a,
structure (freecat a) = emptyset.
Proof.
ir. uf freecat. rww structure_create. 
Qed.

Lemma mor_freecat_id : forall a x,
inc x (vertices a) -> axioms a ->
mor_freecat a (freecat_id x).
Proof.
ir. uhg; ee. am. 
rw source_freecat_id. am. 
rww target_freecat_id. 
app arrow_chain_freecat_id. 
ir. rwi seg_length_freecat_id H1. 
assert (1=0). om. discriminate H2. 
Qed. 

Lemma mor_freecat_comp : forall a u v,
mor_freecat a u -> mor_freecat a v ->
source u = target v -> 
mor_freecat a (freecat_comp u v).
Proof.
ir. uhg; ee. 
uh H; ee; am. 
rw source_freecat_comp. uh H0; ee; am. 
rw target_freecat_comp. uh H; ee; am. 
uh H; uh H0; ee; app arrow_chain_freecat_comp.
ir. rwi seg_length_freecat_comp H2. 
apply by_cases with (i<seg_length v); ir. 
rw segment_freecat_comp_first. 
uh H0; ee; au. am. 
rw segment_freecat_comp_second. 
uh H; ee. ap H7. om. om. am. 
Qed. 

Lemma mor_freecat_edge : forall a u,
axioms a -> inc u (edges a) -> 
mor_freecat a (freecat_edge u).
Proof.
ir. uhg; ee. am. 
rww source_freecat_edge. 
uh H; ee. au. 
rw target_freecat_edge. uh H; ee; au. 
ap arrow_chain_freecat_edge. 

ir. rwi seg_length_freecat_edge H1. 
rw segment_freecat_edge. am. om. 
Qed. 

Lemma freecat_axioms : forall a,
axioms a -> Category.axioms (freecat a).
Proof.
ir. uf freecat. 
ap Category.create_axioms. 
uhg; ee. 
ir. ap iff_eq; ir. uhg; ee. am. 
rw inc_freecat_morphisms. app mor_freecat_id. 
rww source_freecat_id. rww target_freecat_id. 
uh H0; ee; am. 

ir. ap iff_eq; ir. 
rwi inc_freecat_morphisms H0.
uhg; ee. rww inc_freecat_morphisms.  
uh H0; ee; am. uh H0; ee; am. 
rw freecat_right_id. tv. 
uh H0; ee; am. tv. 
rww freecat_left_id. uh H0; ee; am. 
uh H0; ee. uh H3; ee; am. 
uh H0; ee; am. 

ir. cp H0; cp H1. 
rwi inc_freecat_morphisms H0. 
rwi inc_freecat_morphisms H1. 
uhg; ee; try am. 
rw inc_freecat_morphisms. 
app mor_freecat_comp. 
rww source_freecat_comp. 
rww target_freecat_comp. 

ir. 
rwi inc_freecat_morphisms H0. 
rwi inc_freecat_morphisms H1. 
rwi inc_freecat_morphisms H2.
rw freecat_assoc. 
tv. 
Qed. 


Lemma mor_freecat_rw : forall a u,
Graph.axioms a -> 
mor (freecat a) u = mor_freecat a u.
Proof.
ir. 
ap iff_eq; ir. uh H0; ee. rwi is_mor_freecat H1. am. 
ap is_mor_mor. ap freecat_axioms. am. 
rw is_mor_freecat. am. 
Qed. 

Lemma ob_freecat_rw : forall a x,
Graph.axioms a ->
ob (freecat a) x = inc x (vertices a).
Proof.
ir. 
ap iff_eq; ir. uh H0; ee. rwi is_ob_freecat H1. am. 
ap is_ob_ob. ap freecat_axioms. am. 
rw is_ob_freecat. am. 
Qed. 

Lemma id_freecat : forall a x,
Graph.axioms a -> ob (freecat a) x -> 
id (freecat a) x = freecat_id x.
Proof.
ir. rw id_freecat1. tv. 
rwi ob_freecat_rw H0. tv. am. 
Qed. 

Lemma comp_freecat : forall a u v,
Graph.axioms a -> mor (freecat a) u -> 
mor (freecat a) v -> source u = target v ->
comp (freecat a) u v = freecat_comp u v.
Proof.
ir. rww comp_freecat1. 
wrr mor_freecat_rw. wrr mor_freecat_rw. 
Qed. 







Definition mor_chain a u :=
arrow_chain u &
Category.axioms a &
ob a (source u) & ob a (target u) &
(forall i, i< (seg_length u) -> mor a (segment i u)).

Lemma mor_chain_freecat_id : forall a x,
ob a x -> mor_chain a (freecat_id x).
Proof.
ir. uhg. ee. 
ap arrow_chain_freecat_id. uh H; ee; am. 

rww source_freecat_id. 
rww target_freecat_id. 
ir. 
rwi seg_length_freecat_id H0. 
assert (0=1). om. discriminate H1. 
Qed. 

Lemma mor_chain_freecat_comp : forall a u v,
mor_chain a u -> mor_chain a v ->
source u = target v -> mor_chain a (freecat_comp u v).
Proof.
ir. uhg; ee. 
ap arrow_chain_freecat_comp. uh H; ee; am. 
uh H0; ee; am. am. uh H; ee. am. 

rw source_freecat_comp. lu. 
rw target_freecat_comp. lu. 

ir. rwi seg_length_freecat_comp H2. 
assert (i < seg_length v \/ 
(i-seg_length v < seg_length u /\ 
seg_length v <= i)).
om. nin H3. 
rw segment_freecat_comp_first. uh H0; ee.
ap H7. am. am. 
ee. rw segment_freecat_comp_second. 
uh H; ee. ap H8. am. am. am. 
Qed.

Lemma mor_chain_freecat_edge : forall a u,
mor a u -> mor_chain a (freecat_edge u).
Proof.
ir. uhg; ee.
ap arrow_chain_freecat_edge. uh H; ee; am. 
rw source_freecat_edge. rww ob_source. 
rw target_freecat_edge; rww ob_target. 
ir. rw segment_freecat_edge. am. 
rwi seg_length_freecat_edge H0. om. 
Qed. 

Definition chain_tack u v :=
freecat_comp (freecat_edge u) v.

Lemma arrow_chain_chain_tack : forall u v,
arrow_chain v -> 
source u = target v -> arrow_chain (chain_tack u v).
Proof.
ir. uf chain_tack. 
ap arrow_chain_freecat_comp. ap arrow_chain_freecat_edge.
am. rww source_freecat_edge. 
Qed. 

Lemma source_chain_tack : forall u v,
source (chain_tack u v) = source v.
Proof.
ir. uf chain_tack. rw source_freecat_comp. tv. 
Qed.

Lemma target_chain_tack : forall u v,
target (chain_tack u v) = target u.
Proof.
ir. uf chain_tack. rw target_freecat_comp.
rww target_freecat_edge. 
Qed. 

Lemma arrow_chain_tack : forall u v,
arrow (chain_tack u v) = utack u (arrow v).
Proof.
ir. uf chain_tack. 
rw arrow_freecat_comp. 
rw arrow_freecat_edge. tv. 
Qed. 

Lemma seg_length_chain_tack : forall u v,
seg_length (chain_tack u v) = seg_length v + 1.
Proof.
ir. uf chain_tack. 
rw seg_length_freecat_comp. rw seg_length_freecat_edge.
om. 
Qed. 

Lemma segment_chain_tack_old : forall u v i,
i < seg_length v ->
segment i (chain_tack u v) = segment i v.
Proof.
ir. uf chain_tack. 
rw segment_freecat_comp_first. tv. am. 
Qed.

Lemma segment_chain_tack_new : forall u v i,
i = seg_length v ->
segment i (chain_tack u v) = u.
Proof.
ir. uf chain_tack. 
rw segment_freecat_comp_second. 
rw segment_freecat_edge. tv. om. 
om. 
rw seg_length_freecat_edge. om. 
Qed. 

Lemma mor_chain_chain_tack : forall a u v,
mor_chain a v -> mor a u ->
source u = target v -> mor_chain a (chain_tack u v).
Proof.
ir. uhg; ee. 
ap arrow_chain_chain_tack. uh H; ee; am. 
am. uh H0; ee; am. 

rw source_chain_tack. lu. 
rw target_chain_tack. rww ob_target. 

ir. assert (i < seg_length v \/ i = seg_length v).
rwi seg_length_chain_tack H2. om. 
nin H3. rw segment_chain_tack_old. 
uh H; ee; au. am. 
rw segment_chain_tack_new. am. am. 
Qed. 


Definition object_number i u :=
Y (i< seg_length u) (source (segment i u)) (target u).

Lemma object_number_zero : forall u,
arrow_chain u -> object_number 0 u = source u.
Proof.
ir. uf object_number. 
assert (0<seg_length u \/ seg_length u = 0).
om. nin H0. 

rw Y_if_rw. uh H; ee. au. am. 
rw Y_if_not_rw. uh H; ee. sy; au. rw H0; om. 
Qed.

Lemma object_number_seg_length : forall u ,
arrow_chain u -> object_number (seg_length u) u = target u.
Proof.
ir. uf object_number. 
rw Y_if_not_rw. tv. om. 
Qed.

Lemma source_segment : forall i u,
arrow_chain u -> i < seg_length u -> 
source (segment i u) = object_number i u.
Proof.
ir. uf object_number. 
rww Y_if_rw. 
Qed.

Lemma target_segment : forall i u,
arrow_chain u -> i < seg_length u ->
target (segment i u) = object_number (i+1) u.
Proof.
ir. 
uf object_number. 
assert (i+1 < seg_length u \/ i +1 = seg_length u).
om. nin H1. 
rw Y_if_rw. uh H; ee. sy; au. am. 
rw Y_if_not_rw. uh H; ee. wr H4. 
assert (i = seg_length u -1). om. 
rww H7. om. om. 
Qed. 

Definition chain_restrict i u :=
Arrow.create (source u) (object_number i u) 
(restrict (arrow u) i).

Lemma source_chain_restrict : forall i u,
source (chain_restrict i u) = source u.
Proof.
ir. uf chain_restrict. 
rw Arrow.source_create. tv. 
Qed.

Lemma target_chain_restrict : forall i u,
target (chain_restrict i u) = object_number i u.
Proof.
ir. uf chain_restrict. 
rw Arrow.target_create. tv. 
Qed.

Lemma seg_length_chain_restrict : forall i u,
seg_length (chain_restrict i u) = i.
Proof.
ir. uf chain_restrict. 
uf seg_length. 
rw Arrow.arrow_create. 
rw length_restrict. tv. 
Qed. 

Lemma segment_chain_restrict : forall i j u,
j < i -> 
segment j (chain_restrict i u) = segment j u.
Proof.
ir. uf chain_restrict. 
uf segment. rw Arrow.arrow_create. 
rw component_restrict. tv. am. 
Qed. 

Lemma arrow_chain_chain_restrict : forall i u,
arrow_chain u ->  i <= seg_length u ->
arrow_chain (chain_restrict i u).
Proof.
ir. uhg; ee. 
uf chain_restrict. rww Arrow.create_like. 
uf chain_restrict. 
rw Arrow.arrow_create. 
uf restrict. 
ap create_axioms. 

ir. rw segment_chain_restrict. 
rw source_chain_restrict. uh H; ee. ap H3.
rwi seg_length_chain_restrict H1. om. 
rwi seg_length_chain_restrict H1; am. 

ir. rwi seg_length_chain_restrict H1. 
rw seg_length_chain_restrict. 
rw segment_chain_restrict. 
rw target_chain_restrict. 
rw target_segment. assert (i-1+1=i).
om. rww H2. am. om. om. 

ir. rwi seg_length_chain_restrict H1. 
rw segment_chain_restrict. 
rw segment_chain_restrict. rw source_segment.
rw target_segment. tv. am. om. am. 
om. om. om. 

ir. 
rwi seg_length_chain_restrict H1. rw H1. 
rw source_chain_restrict. 
rw target_chain_restrict. rw object_number_zero. tv. 
am. 
Qed. 

Lemma chain_restrict_refl : forall u,
arrow_chain u ->
chain_restrict (seg_length u) u = u.
Proof.
ir. ap arrow_chain_extensionality. 
ap arrow_chain_chain_restrict. am. 
om. am. 
rw seg_length_chain_restrict. tv. 
rw source_chain_restrict. tv. 
rw target_chain_restrict. rw object_number_seg_length. 
tv. am. 

ir. rwi seg_length_chain_restrict H0. 
rw segment_chain_restrict. tv. am. 
Qed.

Lemma eq_chain_tack_restrict : forall u,
arrow_chain u -> seg_length u > 0 ->
u = chain_tack (segment (seg_length u - 1) u) 
(chain_restrict (seg_length u - 1) u).
Proof.
ir. 
ap arrow_chain_extensionality. am. 
ap arrow_chain_chain_tack. 
ap arrow_chain_chain_restrict. am. 
om. cp H. 
uh H; ee. 
rw source_segment. 
rw target_chain_restrict. 
tv. am. om. 

rw seg_length_chain_tack. 
rw seg_length_chain_restrict. om. 
rw source_chain_tack. rw source_chain_restrict. 
tv. rw target_chain_tack. 
rw target_segment. 
assert (seg_length u - 1 + 1 = seg_length u).
om. rw H1. rw object_number_seg_length. tv.
am. am. om. 

ir. 
assert (i < seg_length u - 1 \/ i = seg_length u - 1).
om. nin H2. 
rw segment_chain_tack_old. 
rw segment_chain_restrict. tv. am. 
rw seg_length_chain_restrict. am. 

rw segment_chain_tack_new. rww H2. 
rw seg_length_chain_restrict. am. 
Qed.

Lemma arrow_chain_induction : forall (P:E->Prop),
(forall x, P (freecat_id x)) ->
(forall u v, arrow_chain v -> source u = target v ->
P v -> P (chain_tack u v)) ->
(forall y, arrow_chain y -> P y).
Proof.
intros P H H0. 
assert (forall n y, seg_length y <= n -> arrow_chain y -> P y).
intro n. 
nin n. 

ir. assert (seg_length y = 0). om. 
assert (y = freecat_id (source  y)). ap eq_freecat_id. 
am. am. rw H4. ap H. 

ir. 
assert (seg_length y = S n \/ seg_length y < S n).
om. nin H3. 
util (eq_chain_tack_restrict (u:=y)). 
am. om. rw H4. ap H0. 
ap arrow_chain_chain_restrict. am. om. 
rw target_chain_restrict. 
rw source_segment. tv. am. om. 
ap IHn. 
rw seg_length_chain_restrict. om. 
ap arrow_chain_chain_restrict. am. om. 

ap IHn. om. am. 

ir. 
ap (H1 (seg_length y)). om. am. 
Qed. 

Lemma mor_chain_chain_restrict : forall a u i,
mor_chain a u -> i <= seg_length u ->
mor_chain a (chain_restrict i u).
Proof.
ir. uhg; ee. 
ap arrow_chain_chain_restrict. uh H; ee; am. 
am. uh H; ee; am. 
rw source_chain_restrict. lu. 
rw target_chain_restrict. 
assert (i < seg_length u \/ i = seg_length u).
om. nin H1. 
assert (object_number i u = source (segment i u)). 
rww source_segment. lu. 
rw H2. uh H; ee. 
rww ob_source. au. 
assert (object_number i u = target u).
rw H1. rw object_number_seg_length. tv. lu. 
rw H2. lu. 
ir. uh H; ee. 
rw segment_chain_restrict. ap H5. 
rwi seg_length_chain_restrict H1. om. 
rwi seg_length_chain_restrict H1. am. 
Qed. 

Lemma chain_restrict_chain_tack : forall u v i,
i = seg_length v -> arrow_chain v -> 
source u = target v -> 
chain_restrict i (chain_tack u v) = v.
Proof.
ir. ap arrow_chain_extensionality.
ap arrow_chain_chain_restrict. 
app arrow_chain_chain_tack. 
rw seg_length_chain_tack. om. 
am. 
rw seg_length_chain_restrict. am. 
rw source_chain_restrict. rww source_chain_tack.
rw target_chain_restrict. 
transitivity (source (segment i (chain_tack u v))).
rw source_segment. tv. 
app arrow_chain_chain_tack. rw seg_length_chain_tack.
om. 
rw segment_chain_tack_new. am. am. 

ir. rwi seg_length_chain_restrict H2. 
rw segment_chain_restrict. rw segment_chain_tack_old. 
tv. om. am. 
Qed. 



Lemma mor_chain_induction : forall a (P:E->Prop),
(forall x, ob a x -> P (freecat_id x)) ->
(forall u v, mor_chain a v -> mor a u ->
source u = target v -> P v -> P (chain_tack u v)) ->
(forall y, mor_chain a y -> P y).
Proof.
ir. generalize H1. 

apply arrow_chain_induction with (P:=fun z => (mor_chain a z -> P z)).
ir. 
ap H. 
uh H2. ee. rwi source_freecat_id H4. am. 

ir. 
assert (lem1 : mor_chain a v).
assert (v = chain_restrict (seg_length v) (chain_tack u v)).
rw chain_restrict_chain_tack. tv. tv. am. 
am. rw H6. 
ap mor_chain_chain_restrict. am. 
rw seg_length_chain_tack. om. 



assert (lem2 : mor a u).
assert  (u = segment (seg_length v) (chain_tack u v)).
rw segment_chain_tack_new. tv. tv. 
rw H6. uh H5; ee. ap H10. 
rw seg_length_chain_tack. om. 

ap H0. am. am. am. ap H4; am. 
lu. 
Qed.



Definition compose_chain a u :=
iterate (seg_length u) (fun i v => comp a (segment i u) v) 
(id a (source u)).

Lemma compose_chain_freecat_id : forall a x,
compose_chain a (freecat_id x) = id a x.
Proof.
ir. uf compose_chain. 
rw seg_length_freecat_id. 
rw iterate_0. rw source_freecat_id. tv. 
Qed.

Lemma compose_chain_chain_tack : forall a u v,
compose_chain a (chain_tack u v) =
comp a u (compose_chain a v).
Proof.
ir. 
set (k:= compose_chain a v). 
uf compose_chain. 
rw seg_length_chain_tack. 
rw iterate_nplus1. 
rww segment_chain_tack_new. 
uf k. uf compose_chain. ap uneq. 
apply iterate_same with (P:= fun (x:E) => True). 
tv. 
rw source_chain_tack. tv. tv. 
ir. tv. 
ir. 
rw segment_chain_tack_old. tv. tv. 
Qed.

Lemma compose_chain_freecat_edge : forall a u,
mor a u -> compose_chain a (freecat_edge u) = u.
Proof.
ir. assert (freecat_edge u = chain_tack u (freecat_id (source u))).
uf chain_tack. 
rw freecat_right_id. tv. 
ap arrow_chain_freecat_edge. rww source_freecat_edge. 
rw H0. 
rw compose_chain_chain_tack. rw compose_chain_freecat_id. 
rw right_id. tv. rww ob_source. am. tv. tv. 
Qed. 

Definition compose_chain_facts a u :=
mor_chain a u &
source (compose_chain a u) = source u &
target (compose_chain a u) = target u &
mor a (compose_chain a u).

Lemma compose_chain_facts_compose_chain : forall a u,
mor_chain a u -> compose_chain_facts a u.
Proof.
ir. apply mor_chain_induction with (a:= a)
(P:= fun u => compose_chain_facts a u). 
ir. uhg; ee. 
ap mor_chain_freecat_id. am. 
rw compose_chain_freecat_id. rw source_freecat_id. 
rww source_id. 
rw compose_chain_freecat_id. 
rw target_freecat_id. rww target_id. 
rw compose_chain_freecat_id. app mor_id. 

ir. uhg; ee. 
ap mor_chain_chain_tack. am. am. am. 
rw compose_chain_chain_tack. 
rw source_comp. uh H3; ee. 
rw H4. rw source_chain_tack. tv. am. 
uh H3; ee; am. 
uh H3; ee. rw H5. am. 

rw compose_chain_chain_tack. rw target_comp.
rw target_chain_tack. tv. am. 
uh H3; ee; am. 
uh H3; ee. rw H5. am. 
rw compose_chain_chain_tack. 
rw mor_comp. tv. am. 
uh H3; ee; am. 
uh H3; ee. rw H5. am. tv. am. 
Qed. 

Lemma source_compose_chain : forall a u,
mor_chain a u -> source (compose_chain a u) = source u.
Proof.
ir. cp (compose_chain_facts_compose_chain H). 
uh H0; ee; am. 
Qed.

Lemma target_compose_chain : forall a u,
mor_chain a u -> target (compose_chain a u) = target u.
Proof.
ir. cp (compose_chain_facts_compose_chain H). 
uh H0; ee; am. 
Qed. 



Lemma mor_compose_chain : forall a u, mor_chain a u ->
mor a (compose_chain a u).
Proof.
ir. cp (compose_chain_facts_compose_chain H). 
uh H0; ee; am. 
Qed. 

Lemma freecat_comp_chain_tack : forall y u v,
freecat_comp (chain_tack y u) v =
chain_tack y (freecat_comp u v).
Proof.
ir. uf chain_tack. rw freecat_assoc. tv. 
Qed. 

Lemma compose_chain_freecat_comp : forall a u v,
mor_chain a u -> mor_chain a v ->
source u = target v -> 
compose_chain a (freecat_comp u v) = 
comp a (compose_chain a u) (compose_chain a v).
Proof.
ir. 
assert (forall z, mor_chain a z -> source z = target v ->
compose_chain a (freecat_comp z v) =
comp a (compose_chain a z) (compose_chain a v)).
intros z H2. 
apply mor_chain_induction with (a:=a) 
(P:= fun w => source w = target v ->
compose_chain a (freecat_comp w v) =
comp a (compose_chain a w) (compose_chain a v)).

ir. 
rw freecat_left_id. 
rw compose_chain_freecat_id. 
rw left_id. tv. am. 
ap mor_compose_chain. am. 
rw target_compose_chain. rwi source_freecat_id H4. 
sy; am. am. tv. uh H0; ee; am. 
rwi source_freecat_id H4. am. 

ir. 
rw freecat_comp_chain_tack.

rw compose_chain_chain_tack. 
sy. rw compose_chain_chain_tack. 
rw assoc. wr H6. tv. 
rwi source_chain_tack H7. am. am. 
app mor_compose_chain. app mor_compose_chain. 
rww target_compose_chain. 
rww source_compose_chain. 
rww target_compose_chain. 
rwi source_chain_tack H7. am. tv. 
am. 
ap H2. am. am. 
Qed.



Definition chain_map (fo : E -> E) (fa:E -> E) u :=
Arrow.create 
(fo (source u)) (fo (target u)) (uple_map fa (arrow u)).

Lemma source_chain_map : forall fo fa u,
source (chain_map fo fa u) = fo (source u).
Proof.
ir. uf chain_map. 
rw Arrow.source_create. tv. 
Qed.

Lemma target_chain_map : forall fo fa u,
target (chain_map fo fa u) = fo (target u).
Proof.
ir. uf chain_map. 
rw Arrow.target_create. tv. 
Qed.

Lemma arrow_chain_map : forall fo fa u,
arrow (chain_map fo fa u) = uple_map fa (arrow u).
Proof.
ir. uf chain_map. 
rw Arrow.arrow_create. tv. 
Qed.

Lemma seg_length_chain_map : forall fo fa u,
seg_length (chain_map fo fa u) = seg_length u.
Proof.
ir. uf seg_length. 
rw arrow_chain_map. rw length_uple_map. tv. 
Qed.


Lemma segment_chain_map : forall fo fa u i,
i < seg_length u -> segment i (chain_map fo fa u) 
= fa (segment i u).
Proof.
ir. uf segment. 
rw arrow_chain_map. rw component_uple_map. 
tv. am. 
Qed. 

Lemma arrow_chain_chain_map : forall fo fa u,
arrow_chain u -> 
(forall i, i<seg_length u -> fo (source (segment i u)) =
source (fa (segment i u))) ->
(forall i, i<seg_length u -> fo (target (segment i u)) =
target (fa (segment i u))) ->
arrow_chain (chain_map fo fa u).
Proof.
ir. 
uhg; ee. uf chain_map. rww Arrow.create_like. 
rw arrow_chain_map. ap axioms_uple_map. 
ir. rwi seg_length_chain_map H2. 

rww segment_chain_map. 
rww source_chain_map. wrr H0. rww source_segment. 
rww object_number_zero. 


ir. rwi seg_length_chain_map H2. 

rww segment_chain_map. 
rww target_chain_map. wrr H1. rww target_segment. 
rw seg_length_chain_map. 
assert (seg_length u - 1 + 1 = seg_length u).
om. rw H3. rww object_number_seg_length. 

rw seg_length_chain_map. om. 
rw seg_length_chain_map. om. 
rw seg_length_chain_map. om. 


ir. rwi seg_length_chain_map H2. 
rw segment_chain_map. 
rw segment_chain_map. wr H0. wr H1. 
uh H; ee. rw H6. tv. am. om. 
om. om. om. 


rw seg_length_chain_map. ir. 
rw source_chain_map. rw target_chain_map. uh H; ee. 
rww H7. 
Qed. 



Lemma chain_map_freecat_id : forall fo fm x,
chain_map fo fm (freecat_id x) = freecat_id (fo x).
Proof.
ir. uf chain_map. 
rw source_freecat_id. rw target_freecat_id. 
rw arrow_freecat_id. rw uple_map_emptyset. 
tv. 
Qed.  



Lemma chain_map_freecat_edge : forall fo fm u,
source (fm u) = fo (source u) ->
target (fm u) = fo (target u) ->
chain_map fo fm (freecat_edge u) = freecat_edge (fm u).
Proof.
ir. 
uf chain_map. rw source_freecat_edge. 
rw target_freecat_edge. rw arrow_freecat_edge. 
rw uple_map_uple1. wr H. wr H0. tv. 
Qed.




Lemma chain_map_freecat_comp : forall fo fm u v,
chain_map fo fm (freecat_comp u v) =
freecat_comp (chain_map fo fm u) (chain_map fo fm v).
Proof.
ir. uf chain_map. 
rw source_freecat_comp. 
rw target_freecat_comp. 
rw arrow_freecat_comp. rw uple_map_concatenate. 
uf freecat_comp. 
rw Arrow.source_create. rw Arrow.target_create. 
rw Arrow.arrow_create. rw Arrow.arrow_create. tv. 
Qed.

Lemma chain_map_chain_tack : forall fo fm u v,
target (fm u) = fo (target u) ->
chain_map fo fm (chain_tack u v) = 
chain_tack (fm u) (chain_map fo fm v).
Proof.
ir. 
uf chain_map. rw source_chain_tack. rw target_chain_tack.
rw arrow_chain_tack. uf utack. 
rw uple_map_concatenate. 
rw uple_map_uple1. 
uf chain_tack. uf freecat_comp. 
rw Arrow.source_create. rw Arrow.arrow_create. 
rw target_freecat_edge. rw H. 
rw arrow_freecat_edge. tv. 
Qed. 




Definition free_functor g a fo fm :=
Functor.create (freecat g) a (fun u => 
(compose_chain a (chain_map fo fm u))).


Definition free_functor_property g a fo fm :=
Graph.axioms g &
Category.axioms a & 
(forall x, inc x (vertices g) -> ob a (fo x)) &
(forall u, inc u (edges g) -> mor a (fm u)) &
(forall u, inc u (edges g) -> source (fm u) = fo (source u)) &
(forall u, inc u (edges g) -> target (fm u) = fo (target u)).



Lemma source_free_functor : forall g a fo fm,
source (free_functor g a fo fm) = freecat g.
Proof.
ir. uf free_functor. rw Functor.source_create. tv. 
Qed.

Lemma target_free_functor : forall g a fo fm,
target (free_functor g a fo fm) = a.
Proof.
ir. uf free_functor. rw Functor.target_create. tv. 
Qed.

Lemma fmor_free_functor : forall g a fo fm u,
Graph.axioms g -> 
mor_freecat g u -> fmor (free_functor g a fo fm) u =
(compose_chain a (chain_map fo fm u)).
Proof.
ir. uf free_functor. 
rw fmor_create. tv. rw mor_freecat_rw.  am. am. 
Qed. 

Lemma mor_chain_chain_map : forall g a fo fm u,
free_functor_property g a fo fm ->
mor_freecat g u ->  
mor_chain a (chain_map fo fm u).
Proof.
ir. uhg; ee. 
ap arrow_chain_chain_map. uh H0; ee. am. 
ir. uh H; ee. sy; ap H5. uh H0; ee. 
ap H10. am. 

ir. uh H; uh H0; ee. sy; ap H10. ap H5. am. 
uh H; ee; am. rw source_chain_map. uh H; uh H0; ee. 
ap H6. am. 
rw target_chain_map. uh H; uh H0; ee. app H6. 

ir. rwi seg_length_chain_map H1. 
rww segment_chain_map. uh H; uh H0; ee.
ap H8. ap H5. am. 
Qed. 





Lemma fob_free_functor : forall g a fo fm x,
free_functor_property g a fo fm -> 
inc x (vertices g) ->
fob (free_functor g a fo fm) x = fo x.
Proof.
ir. uf fob. 
rw source_free_functor. rw id_freecat. 
rw fmor_free_functor. 
rw source_compose_chain. 
rw source_chain_map. rw source_freecat_id. tv. 
apply mor_chain_chain_map with g. am. 
ap mor_freecat_id. am. 
uh H; ee; am. uh H; ee; am. 
ap mor_freecat_id. am. uh H; ee; am. uh H; ee; am. 
rww ob_freecat_rw. uh H; ee; am. 
Qed. 

Lemma free_functor_axioms : forall g a fo fm,
free_functor_property g a fo fm -> 
Functor.axioms (free_functor g a fo fm).
Proof.
ir. 
cp H. 
uh H; ee. 
uhg; ee. uf free_functor. 
uf Functor.create. 
ap Umorphism.create_like. 
rw source_free_functor. 
app freecat_axioms. 
rw target_free_functor. 
am. 

ir. rwi source_free_functor H6. 
cp H6. rwi ob_freecat_rw H7. 
rw target_free_functor. rww fob_free_functor. 
ap H2. am. am. 

ir. rwi source_free_functor H6. cp H6. 
rwi ob_freecat_rw H7; try am. 
rw target_free_functor. rww fob_free_functor. 
rww fmor_free_functor. 
rw source_free_functor. rww id_freecat. 

rw chain_map_freecat_id. rw compose_chain_freecat_id. 
tv. 
rw source_free_functor. rw id_freecat. 
ap  mor_freecat_id. am. am. am. 
am. 

ir. rwi source_free_functor H6. 
rw target_free_functor. rw fmor_free_functor. 
ap mor_compose_chain. 
apply mor_chain_chain_map with g. am. 
wrr mor_freecat_rw. am. wrr mor_freecat_rw. 

ir. rwi source_free_functor H6. 
rw fmor_free_functor. rw source_compose_chain.

rw fob_free_functor. rw source_chain_map. tv. am. 
rwi mor_freecat_rw H6. 
uh H6; ee. am. am. 
apply mor_chain_chain_map with g. am. wrr mor_freecat_rw. 
am. wrr mor_freecat_rw. 

ir. rwi source_free_functor H6. 
rw fmor_free_functor. rw target_compose_chain.

rw fob_free_functor. rw target_chain_map. tv. am. 
rwi mor_freecat_rw H6. 
uh H6; ee. am. am. 
apply mor_chain_chain_map with g. am. wrr mor_freecat_rw. 
am. wrr mor_freecat_rw. 

ir. rwi source_free_functor H6.
rwi source_free_functor H7.
rw target_free_functor. 
rw fmor_free_functor. rw fmor_free_functor.
rw fmor_free_functor. rw source_free_functor. 
rw comp_freecat. 
rw chain_map_freecat_comp. 
rw compose_chain_freecat_comp. tv. 

apply mor_chain_chain_map with g. am. 
wrr mor_freecat_rw. 
apply mor_chain_chain_map with g. am. 
wrr mor_freecat_rw. 
rw source_chain_map. rw target_chain_map. rww H8. 
am. am. am. am. am. 
rw source_free_functor. rw comp_freecat. 
ap mor_freecat_comp. 
wrr mor_freecat_rw. 
wrr mor_freecat_rw. am. am. am. am. am. 
am. 
wrr mor_freecat_rw. am. wrr mor_freecat_rw.
Qed. 


Lemma fmor_ff_freecat_id : forall g a fo fm x,
free_functor_property g a fo fm ->
inc x (vertices g) ->
fmor (free_functor g a fo fm) (freecat_id x) = id a (fo x).
Proof.
ir. rewrite <- id_freecat with g x. 
rw fmor_id. rw target_free_functor. 
rw fob_free_functor. tv. am. am. 
app free_functor_axioms. rww source_free_functor. 
rww ob_freecat_rw. uh H; ee; am. uh H; ee; am.
rww ob_freecat_rw. uh H; ee; am. 
Qed.

Lemma fmor_ff_freecat_edge : forall g a fo fm u,
free_functor_property g a fo fm ->
inc u (edges g) ->
fmor (free_functor g a fo fm) (freecat_edge u) = fm u.
Proof.
ir. 
rw fmor_free_functor. 
rw chain_map_freecat_edge. rw compose_chain_freecat_edge.
tv. 
uh H; ee. au. 
uh H; ee. au. uh H; ee; au. uh H; ee; am. 
ap mor_freecat_edge. uh H; ee; am. am. 
Qed.

Lemma fmor_comp : forall a f u v,
Functor.axioms f -> source f = a ->
mor a u -> mor a v -> 
source u = target v ->
fmor f (comp a u v) = comp (target f) (fmor f u) (fmor f v).
Proof.
ir. wr H0. 
rww comp_fmor. rww H0. rww H0. 
Qed. 

Lemma fmor_ff_freecat_comp : forall g a fo fm u v,
free_functor_property g a fo fm ->
mor (freecat g) u ->
mor (freecat g) v ->
source u = target v ->
fmor (free_functor g a fo fm) (freecat_comp u v) =
comp a (fmor (free_functor g a fo fm) u) 
(fmor (free_functor g a fo fm) v).
Proof.
ir. cp H. uh H; ee. 
assert (freecat_comp u v = comp (freecat g) u v).
rww comp_freecat. 
rw H9. rw fmor_comp. 
rw target_free_functor. tv. 
app free_functor_axioms. rww source_free_functor. 
am. am. am.  
Qed. 

Lemma fmor_ff_chain_tack : forall g a fo fm u v,
free_functor_property g a fo fm ->
inc u (edges g) -> 
mor (freecat g) v -> source u = target v -> 
fmor (free_functor g a fo fm) (chain_tack u v) =
comp a (fm u) (fmor (free_functor g a fo fm) v).
Proof.
ir. uf chain_tack. 
rw fmor_ff_freecat_comp. rw fmor_ff_freecat_edge. 
tv. am. am. am. 
rww mor_freecat_rw. app mor_freecat_edge. uh H; ee; am.
uh H; ee; am. am. rww source_freecat_edge. 
Qed. 


Lemma free_functor_property_fob_fmor : forall g a f,
Functor.axioms f -> Graph.axioms g ->
source f = freecat g -> target f = a ->
free_functor_property g a (fob f) (fun u => fmor f (freecat_edge u)).
Proof.
ir. 
uhg; ee. 
am. wr H2. rww category_axioms_target. 
ir. wr H2. ap ob_fob. am. 
rw H1. rww ob_freecat_rw. 

ir. wr H2. ap mor_fmor. 
am. rw H1. rww mor_freecat_rw. 
app mor_freecat_edge. 

ir. rw source_fmor. rww source_freecat_edge. am. 
rw H1. rww mor_freecat_rw. 
app mor_freecat_edge. 

ir. rw target_fmor. rww target_freecat_edge. am. 
rw H1. rww mor_freecat_rw. 
app mor_freecat_edge. 
Qed.


Definition graph_fmor g f y := 
fmor (free_functor g (target f) (fob f) 
(fun u => fmor f (freecat_edge u))) y.

Lemma graph_fob : forall g f x,
Graph.axioms g -> source f = freecat g -> 
Functor.axioms f -> inc x (vertices g) ->
fob (free_functor g (target f) (fob f) 
(fun u => fmor f (freecat_edge u))) x = fob f x.
Proof.
ir. rw fob_free_functor. tv. 
ap free_functor_property_fob_fmor. am. am. 
am. tv. am. 
Qed. 

Definition graph_fmor_recovers g f y :=
graph_fmor g f y = fmor f y.

Lemma graph_fmor_recovers_freecat_id : forall g f x,
Graph.axioms g -> source f = freecat g -> 
Functor.axioms f -> inc x (vertices g) ->
graph_fmor_recovers g f (freecat_id x). 
Proof.
ir. uhg. uf graph_fmor. rw fmor_free_functor.
rw chain_map_freecat_id. rw compose_chain_freecat_id. 
assert (freecat_id x = id (source f) x).
rw H0. rww id_freecat. rww ob_freecat_rw. 
rw H3. rww fmor_id. 
rw H0. rww ob_freecat_rw. am. 
app mor_freecat_id. 
Qed. 

Lemma graph_fmor_recovers_freecat_edge : forall g f u,
Graph.axioms g -> source f = freecat g -> 
Functor.axioms f -> inc u (edges g) ->
graph_fmor_recovers g f (freecat_edge u).
Proof.
ir. uhg. uf graph_fmor. rw fmor_free_functor.
rw chain_map_freecat_edge. rw compose_chain_freecat_edge. 
tv. app mor_fmor. rw H0. 
rww mor_freecat_rw. app mor_freecat_edge. 
rww source_fmor. rww source_freecat_edge. 
rw H0. rww mor_freecat_rw. app mor_freecat_edge. 
rww target_fmor. rww target_freecat_edge. 
rw H0. rww mor_freecat_rw. app mor_freecat_edge. 
am. app mor_freecat_edge. 
Qed. 

Lemma graph_fmor_recovers_freecat_comp : forall g f u v,
Graph.axioms g -> source f = freecat g -> 
Functor.axioms f -> mor_freecat g u -> mor_freecat g v ->
source u = target v -> 
graph_fmor_recovers g f u -> graph_fmor_recovers g f v -> 
graph_fmor_recovers g f (freecat_comp u v).
Proof.
ir. uhg. uf graph_fmor. rw fmor_free_functor.
rw chain_map_freecat_comp. rw compose_chain_freecat_comp.

assert (freecat_comp u v = comp (source f) u v).
rw H0. rww comp_freecat. rww mor_freecat_rw. 
rww mor_freecat_rw. rw H7. 
rw fmor_comp. uh H5. uh H6. wr H5; wr H6. 
uf graph_fmor. rww fmor_free_functor. 
rww fmor_free_functor. am. tv. 
rw H0; rww mor_freecat_rw. 
rw H0; rww mor_freecat_rw. am. 
apply mor_chain_chain_map with g. 
app free_functor_property_fob_fmor. 
am. 
apply mor_chain_chain_map with g. 
app free_functor_property_fob_fmor. 
am. 
rw source_chain_map. rw target_chain_map. rww H4. 
am. app mor_freecat_comp. 
Qed. 

Lemma graph_fmor_recovers_chain_tack : forall g f u v,
Graph.axioms g -> source f = freecat g -> 
Functor.axioms f -> inc u (edges g) -> mor_freecat g v ->
source u = target v -> 
graph_fmor_recovers g f v -> 
graph_fmor_recovers g f (chain_tack u v).
Proof.
ir. uf chain_tack. 
app graph_fmor_recovers_freecat_comp. 
app mor_freecat_edge. rww source_freecat_edge. 
app graph_fmor_recovers_freecat_edge. 
Qed. 

Lemma inc_object_number_vertices : forall g u i,
Graph.axioms g -> mor_freecat g u ->
i <= seg_length u -> inc (object_number i u) (vertices g).
Proof.
ir. 
assert (i < seg_length u \/ i = seg_length u). om.
nin H2. assert (object_number i u = source (segment i u)).
rww source_segment. uh H0; ee; am. 
rw H3. uh H0; ee. 
uh H; ee. ap H9. ap H7. am. 
rw H2. rw object_number_seg_length. uh H0; ee. am. 
uh H0; ee; am.  
Qed. 

Lemma mor_freecat_chain_restrict : forall g u i,
Graph.axioms g -> mor_freecat g u ->
i <= seg_length u -> mor_freecat g (chain_restrict i u).
Proof.
ir. 
cp H0; uh H0; ee. 
uhg; ee. am. 
rww source_chain_restrict. 
rww target_chain_restrict. 
app inc_object_number_vertices. 
app arrow_chain_chain_restrict. 

ir. 
rwi seg_length_chain_restrict H7. 
rw segment_chain_restrict. ap H6. om. am. 
Qed. 

Lemma mor_freecat_induction : forall g (P : E -> Prop),
Graph.axioms g -> 
(forall x, inc x (vertices g) -> P (freecat_id x)) ->
(forall u v, inc u (edges g) ->  mor_freecat g v -> 
source u = target v -> P v -> P (chain_tack u v)) ->
(forall u, mor_freecat g u -> P u).
Proof.
ir. 
generalize H2. 
apply arrow_chain_induction with (P:=fun u => mor_freecat g u -> P u).
ir. 
ap H0. uh H3; ee. rwi source_freecat_id H4. am. 

ir. ap H1. assert (u0 = segment (seg_length v) (chain_tack u0 v)).
rww segment_chain_tack_new. rw H7. 
uh H6; ee. ap H11. rw seg_length_chain_tack; om. 
assert (v = chain_restrict (seg_length v) (chain_tack u0 v)).
rw chain_restrict_chain_tack. tv. tv. am. am. 
rw H7. 
ap mor_freecat_chain_restrict. 
am. am. 
rw seg_length_chain_tack. om. am. ap H5. 
assert (v = chain_restrict (seg_length v) (chain_tack u0 v)).
rw chain_restrict_chain_tack. tv. tv. am. am. 
rw H7. 
ap mor_freecat_chain_restrict. 
am. am. 
rw seg_length_chain_tack. om. uh H2; ee; am. 
Qed. 

Lemma graph_fmor_recovers_all : forall g f u,
Graph.axioms g -> source f = freecat g -> 
Functor.axioms f -> mor_freecat g u -> 
graph_fmor_recovers g f u.
Proof.
ir. 
apply mor_freecat_induction with (g:=g)
(P:= graph_fmor_recovers g f).
am. ir. app graph_fmor_recovers_freecat_id. 
ir. app graph_fmor_recovers_chain_tack. 
am.  
Qed. 

Lemma eq_free_functor_fob_fmor : forall g f,
Graph.axioms g -> source f = freecat g -> 
Functor.axioms f ->
f = free_functor g (target f) (fob f) 
(fun u => fmor f (freecat_edge u)).
Proof.
ir. 
ap Functor.axioms_extensionality. 
am. ap free_functor_axioms. 
app free_functor_property_fob_fmor. 
rww source_free_functor. rww target_free_functor.
ir. 
assert (mor_freecat g u). 
wr mor_freecat_rw. wrr H0. am. 
assert (graph_fmor_recovers g f u).
app graph_fmor_recovers_all. 
uh H4; ee. sy; am. 
Qed. 

(** Up to now we have classified functors whose source
is of the form (freecat g). We need to discuss natural
transformations. ***)

Definition free_nt_property g a b (t:E -> E) :=
Graph.axioms g & Functor.axioms a & Functor.axioms b
& source a = freecat g  
& source b = freecat g 
& target a = target b &
(forall x, inc x (vertices g) ->  mor (target a) (t x)) &
(forall x, inc x (vertices g) -> source (t x) = fob a x) &
(forall x, inc x (vertices g) -> target (t x) = fob b x) &
(forall u, inc u (edges g) -> 
comp (target a) (t (target u)) (fmor a (freecat_edge u)) =
comp (target a) (fmor b (freecat_edge u)) (t (source u))).

Definition free_nt_respects a b (t:E->E) u :=
comp (target a) (t (target u)) (fmor a u) =
comp (target a) (fmor b u) (t (source u)).

Lemma free_nt_respects_freecat_id : forall g a b t x,
free_nt_property g a b t -> 
inc x (vertices g) -> 
free_nt_respects a b t (freecat_id x).
Proof.
ir. uh H; ee. uhg. 
assert (freecat_id x = id (source a) x). 
rw H3. rww id_freecat. rww ob_freecat_rw. 

rw H10. rww fmor_id. rww source_id. 
rww target_id. rww right_id. 
rw H3; wr H4. rww fmor_id. 
rw H5. rww left_id. 
app ob_fob. 
rw H4. rww ob_freecat_rw. wr H5; au. 
au. rw H4. rww ob_freecat_rw. 
app ob_fob. rw H3. rww ob_freecat_rw. au. 
au. rw H3. rww ob_freecat_rw.
 rw H3. rww ob_freecat_rw.
 rw H3. rww ob_freecat_rw.
Qed. 

Lemma free_nt_respects_freecat_edge : forall g a b t u,
free_nt_property g a b t -> 
inc u (edges g) -> 
free_nt_respects a b t (freecat_edge u).
Proof.
ir. uh H; ee. 
uhg. 
rw target_freecat_edge. rw source_freecat_edge.
au. 
Qed. 

Lemma free_nt_respects_freecat_comp : forall g a b t u v,
free_nt_property g a b t -> 
mor_freecat g u -> mor_freecat g v -> source u = target v ->
free_nt_respects a b t u -> 
free_nt_respects a b t v -> 
free_nt_respects a b t (freecat_comp u v).
Proof.
ir. uh H; ee. 
uh H3; uh H4. 
assert (freecat_comp u v = comp (source a) u v).
rw H7. rww comp_freecat. 
rww mor_freecat_rw. rww mor_freecat_rw. 
rw H14. 
uhg. 

assert (mor (freecat g) u). 
rww mor_freecat_rw. 
assert (mor (freecat g) v). 
rww mor_freecat_rw. 
assert (mor (source a) u).
rww H7. 
assert (mor (source a) v). 
rww H7. 
assert (mor (source b) u). rww H8. 
assert (mor (source b) v). rww H8. 

assert (inc (target u) (vertices g)).
wr ob_freecat_rw. wr H7. rww ob_target. am. 

assert (inc (target v) (vertices g)).
wr ob_freecat_rw. wr H7. rww ob_target. am. 

assert (inc (source u) (vertices g)).
wr ob_freecat_rw. wr H7. rww ob_source. am. 

assert (inc (source v) (vertices g)).
wr ob_freecat_rw. wr H7. rww ob_source. am. 



rw fmor_comp. 
assert (fmor b (comp (source a) u v) =
fmor b (comp (source b) u v)). 
rw H7; wrr H8. rw H25. 
rww fmor_comp. wr H9. 
rww target_comp. 
rww source_comp. 
rww assoc. 

wr H4. 

wrr assoc. rw H3. 
rw H2. app assoc. 

(** The main step is done but there are 20 subgoals! **)

rw H9. app mor_fmor. 
app H10. app mor_fmor. 
rww source_fmor. rw H2. 
sy; au. rww target_fmor. au. 

au. app mor_fmor. app mor_fmor. 
rww target_fmor. au. rww target_fmor. 
rww source_fmor. rww H2. 
rw H9. app mor_fmor. 
rw H9. app mor_fmor. 
au. rww source_fmor. rww target_fmor. rww H2. 
rww source_fmor. sy; au. am. tv. 
am. am. am. 
Qed.  


Lemma free_nt_respects_chain_tack : forall g a b t u v,
free_nt_property g a b t -> inc u (edges g) -> 
mor_freecat g v -> source u = target v ->
free_nt_respects a b t v -> 
free_nt_respects a b t (chain_tack u v).
Proof.
ir. uf chain_tack. 
apply free_nt_respects_freecat_comp with (g:=g).
am. app mor_freecat_edge. uh H; ee; am. 
am. 
rww source_freecat_edge. 
apply free_nt_respects_freecat_edge with (g:=g).
am. am. am. 
Qed.  

Lemma free_nt_respects_all : forall g a b t u,
free_nt_property g a b t -> 
mor_freecat g u -> 
free_nt_respects a b t u.
Proof.
ir. 
apply mor_freecat_induction with 
(g:=g) (P:= free_nt_respects a b t).
uh H; ee; am. 
ir. apply free_nt_respects_freecat_id with g. am. 
am. 

ir. apply free_nt_respects_chain_tack with g. am. 
am. am. am. am. am. 
Qed. 

Lemma free_nt_nat_trans_property : forall g a b t,
free_nt_property g a b t -> Nat_Trans.property a b t.
Proof.
ir. 
cp H; uh H; ee. 
uhg; ee. 
am. am. rww H4. am. 
ir. wr H5. ap H6. 
wr ob_freecat_rw. wrr H3. am. 
ir. ap H7.  
wr ob_freecat_rw. wrr H3. am. 
ir. ap H8.  
wr ob_freecat_rw. wrr H3. am. 

ir. assert (free_nt_respects a b t u). 
apply free_nt_respects_all with g. 
am. wr mor_freecat_rw. wrr H3. am. 
uh H11. 
wrr H5. 
Qed. 

Lemma free_nt_prop_eq_nat_trans_prop : forall g a b t,
Graph.axioms g -> source a = freecat g -> 
free_nt_property g a b t = Nat_Trans.property a b t.
Proof.
ir. ap iff_eq; ir. 
apply free_nt_nat_trans_property with g.
am. 
uh H1; uhg; ee.
am. am. am. am. wrr H3. am. 
ir. rw H4. ap H5. rw H0. 
rww ob_freecat_rw. 
ir. ap H6. rw H0. 
rww ob_freecat_rw. 
ir. ap H7. rw H0. 
rww ob_freecat_rw. 

ir. rw H4. 
assert (target u = target (freecat_edge u)).
rww target_freecat_edge. 
assert (source u = source (freecat_edge u)). 
rww source_freecat_edge. 
rw H10. rw H11. 
ap H8. rw H0. 
rw mor_freecat_rw. 
app mor_freecat_edge. am. 
Qed. 

Lemma free_nt_property_ntrans : forall g r,
Graph.axioms g -> Nat_Trans.axioms r -> 
osource r = freecat g -> 
free_nt_property g (source r) (target r) (ntrans r).
Proof.
ir. rw free_nt_prop_eq_nat_trans_prop. 
ap Nat_Trans.axioms_property. am. am. 
am.  
Qed. 


(** Note the following lemma which is general for any
natural transformation; in our context it means
that we don't need a specific reconstruction process for
natural transformations from (freecat g) **)

Lemma nat_trans_create_recovers : forall r,
Nat_Trans.axioms r -> 
r = Nat_Trans.create (source r) (target r) (ntrans r).
Proof.
ir. uh H; ee. uh H. sy; am. 
Qed. 

End Free_Category.