Set Implicit Arguments.
Unset Strict Implicit.


Require Export gzdef.



Module Left_Fractions.
Export GZ_Def. 

Definition lf_symbol f t :=
Arrow.create (source f) (source t) (pair f t).

Definition lf_forward v := pr1 (arrow v).
Definition lf_backward v := pr2 (arrow v).

Lemma source_lf_symbol : forall f t, source (lf_symbol f t) 
= source f.
Proof.
ir. uf lf_symbol. rww Arrow.source_create. 
Qed.

Lemma target_lf_symbol : forall f t, target (lf_symbol f t)
= source t.
Proof.
ir. uf lf_symbol. rww Arrow.target_create. 
Qed.

Lemma lf_forward_lf_symbol : forall f t, lf_forward
(lf_symbol f t) = f.
Proof.
ir. uf lf_symbol. uf lf_forward. 
rw Arrow.arrow_create. rww pr1_pair. 
Qed.

Lemma lf_backward_lf_symbol : forall f t, lf_backward 
(lf_symbol f t) = t.
Proof.
ir. uf lf_symbol. uf lf_backward. 
rw Arrow.arrow_create. rww pr2_pair. 
Qed. 

Definition lf_symbol_like v :=
v = lf_symbol (lf_forward v) (lf_backward v).

Lemma lf_symbol_like_lf_symbol : forall f t,
lf_symbol_like (lf_symbol f t).
Proof.
ir. uf lf_symbol_like. 
rw lf_forward_lf_symbol. rw lf_backward_lf_symbol. tv. 
Qed. 

Definition lf_symbol_property a s f t :=
localizing_system a s &
mor a f & inc t s & target f = target t.

Definition is_lf_symbol a s v :=
lf_symbol_like v & lf_symbol_property a s (lf_forward v)
(lf_backward v).

Lemma is_lf_symbol_lf_symbol : forall a s f t,
lf_symbol_property a s f t ->
is_lf_symbol a s (lf_symbol f t).
Proof.
ir. uhg; ee. ap lf_symbol_like_lf_symbol. 
rw lf_forward_lf_symbol. rw lf_backward_lf_symbol. 
am. 
Qed. 

Definition multiplicative_system a s :=
localizing_system a s &
(forall y z, inc y s -> inc z s -> 
source y = target z -> inc (comp a y z) s).

Definition has_left_fractions a s :=
multiplicative_system a s 
&
(forall x, ob a x -> inc (id a x) s) 
&
(forall r g, inc r s -> mor a g -> source r = source g ->
exists u, (is_lf_symbol a s u & source u = target r
& target u = target g & comp a (lf_backward u) g =
comp a (lf_forward u) r)) 
&
(forall v r t, inc v s -> mor a r -> mor a t ->
source r = target v -> source t = target v ->
comp a r v = comp a t v -> 
exists w, (inc w s & source w = target r & source w = target t
& comp a w r = comp a w t)).

Definition lf_choice a s r g :=
choose (fun u => (is_lf_symbol a s u & source u = target r
& target u = target g & comp a (lf_backward u) g =
comp a (lf_forward u) r)).

Lemma is_lf_symbol_lf_choice : forall a s r g,
has_left_fractions a s ->
inc r s -> mor a g -> source r = source g ->
is_lf_symbol a s (lf_choice a s r g).
Proof.
ir. 
assert ((fun u : E =>
      is_lf_symbol a s u &
      source u = target r &
      target u = target g &
      comp a (lf_backward u) g = comp a (lf_forward u) r) 
(lf_choice a s r g)). 
uf lf_choice. ap choose_pr. 
uh H; ee. au. 
cbv beta in H3. ee. am. 
Qed.

Lemma source_lf_choice : forall a s r g,
has_left_fractions a s ->
inc r s -> mor a g -> source r = source g ->
source (lf_choice a s r g) = target r.
Proof.
ir. 
assert ((fun u : E =>
      is_lf_symbol a s u &
      source u = target r &
      target u = target g &
      comp a (lf_backward u) g = comp a (lf_forward u) r) 
(lf_choice a s r g)). 
uf lf_choice. ap choose_pr. 
uh H; ee. au. 
cbv beta in H3. ee. am. 
Qed.

Lemma target_lf_choice : forall a s r g,
has_left_fractions a s ->
inc r s -> mor a g -> source r = source g ->
target (lf_choice a s r g) = target g.
Proof.
ir. 
assert ((fun u : E =>
      is_lf_symbol a s u &
      source u = target r &
      target u = target g &
      comp a (lf_backward u) g = comp a (lf_forward u) r) 
(lf_choice a s r g)). 
uf lf_choice. ap choose_pr. 
uh H; ee. au. 
cbv beta in H3. ee. am. 
Qed.

Lemma comp_lf_backward_lf_choice : forall a s r g,
has_left_fractions a s ->
inc r s -> mor a g -> source r = source g ->
comp a (lf_backward (lf_choice a s r g)) g
 = comp a (lf_forward (lf_choice a s r g)) r.
Proof.
ir. 
assert ((fun u : E =>
      is_lf_symbol a s u &
      source u = target r &
      target u = target g &
      comp a (lf_backward u) g = comp a (lf_forward u) r) 
(lf_choice a s r g)). 
uf lf_choice. ap choose_pr. 
uh H; ee. au. 
cbv beta in H3. ee. am. 
Qed.




Lemma source_lf_forward : forall v,
lf_symbol_like v -> source (lf_forward v) = source v.
Proof.
ir. uh H; ee. rw H. rw lf_forward_lf_symbol. 
rw source_lf_symbol. tv. 
Qed.

Lemma source_lf_backward : forall v,
lf_symbol_like v -> source (lf_backward v) = target v.
Proof.
ir. uh H; ee. rw H. rw lf_backward_lf_symbol. 
rw target_lf_symbol. tv. 
Qed. 


Lemma inc_ms_mor : forall a u,
(exists s, (localizing_system a s & inc u s)) ->
mor a u.
Proof.
ir. nin H. ee. 
uh H; ee. ap H1; am. 
Qed. 

Lemma inc_hlf_mor : forall a u,
(exists s, (has_left_fractions a s & inc u s)) ->
mor a u.
Proof.
ir. nin H. ee. 
ap inc_ms_mor. sh x. ee. lu. am. 
Qed. 



Definition lf_id_rep a x :=
lf_symbol (id a x) (id a x).

Lemma source_lf_id_rep : forall a x, 
ob a x -> source (lf_id_rep a x) = x.
Proof.
ir. uf lf_id_rep. rww source_lf_symbol. 
rww source_id. 
Qed.

Lemma target_lf_id_rep : forall a x, 
ob a x -> target (lf_id_rep a x) = x.
Proof.
ir. uf lf_id_rep. rww target_lf_symbol. 
rww source_id. 
Qed.

Lemma is_lf_symbol_lf_id_rep : forall a s x,
has_left_fractions a s -> ob a x ->
is_lf_symbol a s (lf_id_rep a x).
Proof.
ir. uf lf_id_rep. 
ap is_lf_symbol_lf_symbol. uhg; ee. 
lu. app mor_id. uh H; ee. uh H; ee. 
au. tv. 
Qed.

Definition lf_vertex v :=
target (lf_backward v).

Lemma target_lf_forward : forall u,
(exists a, exists s, (is_lf_symbol a s u)) ->
target (lf_forward u) = lf_vertex u.
Proof.
ir. nin H. nin H. uh H; ee. 
uf lf_vertex. uh H0; ee; am. 
Qed.

Lemma target_lf_backward : forall u,
target (lf_backward u) = lf_vertex u.
Proof.
ir. tv. 
Qed. 

Definition lf_extend a (s:E) p u :=
lf_symbol (comp a p (lf_forward u)) (comp a p (lf_backward u)).

Lemma mor_lf_forward : forall a u,
(exists s, is_lf_symbol a s u) -> 
mor a (lf_forward u).
Proof.
ir. nin H. uh H; ee. uh H0; ee; am. 
Qed.

Lemma inc_lf_backward : forall s u,
(exists a, is_lf_symbol a s u) ->
inc (lf_backward u) s.
Proof.
ir. nin H. uh H; ee. uh H0; ee; am. 
Qed. 



Lemma mor_lf_backward : forall a u,
(exists s, is_lf_symbol a s u) -> 
mor a (lf_backward u).
Proof.
ir. nin H. uh H; ee. uh H0; ee. 
ap inc_ms_mor. sh x. ee. am. 
am. 
Qed. 

Lemma is_lf_symbol_lf_extend : forall a s p u,
has_left_fractions a s -> 
is_lf_symbol a s u -> 
mor a p -> source p = lf_vertex u ->
inc (comp a p (lf_backward u)) s -> 
is_lf_symbol a s (lf_extend a s p u).
Proof.
ir. 

uf lf_extend. 
ap is_lf_symbol_lf_symbol. uhg; ee. 
lu. rw mor_comp. tv. am. ap mor_lf_forward.
sh s; am. 
rw target_lf_forward. am. 
sh a. sh s. am. tv. 
uh H; ee. uh H; ee. am.  
rw target_comp. rw target_comp. tv. am. 
ap mor_lf_backward. sh s; am. am. am. 
ap mor_lf_forward. sh s; am. rw target_lf_forward.
am. sh a. sh s; am. 
Qed.

Lemma source_lf_extend : forall a s p u,
is_lf_symbol a s u ->
mor a p -> source p = lf_vertex u -> 
source (lf_extend a s p u) = source u.
Proof.
ir. 

uf lf_extend. 
rw source_lf_symbol. rw source_comp. 
rw source_lf_forward. tv. lu. 
am. ap mor_lf_forward. sh s; am. 
rw target_lf_forward. am. 
sh a. sh s; am. 
Qed.

Lemma target_lf_extend : forall a s p u,
is_lf_symbol a s u ->
mor a p -> source p = lf_vertex u -> 
target (lf_extend a s p u) = target u.
Proof.
ir. 

uf lf_extend. 
rw target_lf_symbol. rw source_comp. 
rw source_lf_backward. tv. lu. 
am. ap mor_lf_backward. sh s; am. 
rw target_lf_backward. am. 
Qed.

Lemma lf_forward_lf_extend : forall a s p u,
lf_forward (lf_extend a s p u) = comp a p (lf_forward u).
Proof.
ir. uf lf_extend. 
rw lf_forward_lf_symbol. tv. 
Qed.

Lemma lf_backward_lf_extend : forall a s p u,
lf_backward (lf_extend a s p u) = comp a p (lf_backward u).
Proof.
ir. uf lf_extend. 
rw lf_backward_lf_symbol. tv. 
Qed. 

Lemma lf_vertex_lf_extend : forall a s p u,
has_left_fractions a s ->
is_lf_symbol a s u -> mor a p -> source p = lf_vertex u ->
lf_vertex (lf_extend a s p u) = target p.
Proof.
ir. uf lf_vertex. 
rw lf_backward_lf_extend. 
rw target_comp. tv. am. 
ap mor_lf_backward. sh s; am. am. 
Qed.

(** Gabriel-Zisman don't explain this very well but we
need two notions which are slightly different. The
weaker notion which we call [lf_beyond] means that
there is just an arrow going from the vertex of [u]
to the vertex of [v] (making everything 
commute). The stronger notion which we call
[lf_under] means that there is such an arrow which is
in [s]. Of course if [s] satisfied 3 for the price of 2
then these would be equivalent but Gabriel-Zisman
claim to do the theory without this condition and we 
try to follow. *)

Definition lf_beyond a s u v :=
has_left_fractions a s &
is_lf_symbol a s u & is_lf_symbol a s v &
source u = source v & target u = target v &
(exists p, (mor a p & source p = lf_vertex u &
lf_extend a s p u = v)).

Definition lf_under a s u v :=
has_left_fractions a s &
is_lf_symbol a s u & is_lf_symbol a s v &
source u = source v & target u = target v &
(exists p, (inc p s & source p = lf_vertex u &
lf_extend a s p u = v)).

Lemma lf_under_lf_beyond : forall a s u v,
lf_under a s u v -> lf_beyond a s u v.
Proof.
ir. uh H; uhg; ee; try am. 
nin H4. ee.
sh x. ee; try am. ap inc_hlf_mor. 
sh s; ee; am. 
Qed.



Lemma lf_beyond_lf_extend : forall a s p u,
has_left_fractions a s -> 
is_lf_symbol a s u -> mor a p ->
source p = lf_vertex u ->
inc (comp a p (lf_backward u)) s -> 
lf_beyond a s u (lf_extend a s p u).
Proof.
ir. 
uhg; ee. am. am. 
app is_lf_symbol_lf_extend. 
rww source_lf_extend. rww target_lf_extend. 
sh p. ee; try am. tv. 
Qed. 

Lemma inc_comp : forall a s u v,
multiplicative_system a s ->
inc u s ->  inc v s -> source u = target v ->
inc (comp a u v) s.
Proof.
ir. uh H; ee; au. 
Qed. 

Lemma lf_under_lf_extend : forall a s p u,
has_left_fractions a s -> 
is_lf_symbol a s u -> inc p s ->
source p = lf_vertex u ->
lf_under a s u (lf_extend a s p u).
Proof.
ir. 
uhg; ee. am. am. 
app is_lf_symbol_lf_extend. 
ap inc_hlf_mor. sh s; ee; am. 
ap inc_comp. lu. 
am. 
ap inc_lf_backward. 
sh a; am. 
rw target_lf_backward. am. 
rww source_lf_extend. 
ap inc_hlf_mor. sh s; ee; am. 
rww target_lf_extend. ap inc_hlf_mor. sh s; ee; am. 
sh p. ee; try am. tv. 
Qed. 

Lemma lf_symbol_like_extens : forall u v,
lf_symbol_like u -> lf_symbol_like v ->
lf_forward u = lf_forward v -> lf_backward u = lf_backward v ->
u = v.
Proof.
ir. uh H; uh H0; ee. 
rw H; rw H0. rw H1; rw H2. reflexivity. 
Qed.

Lemma lf_symbol_like_lf_extend : forall a s p u,
lf_symbol_like (lf_extend a s p u).
Proof.
ir. uf lf_extend. 
ap  lf_symbol_like_lf_symbol. 
Qed. 

Lemma lf_extend_comp : forall a s u p q,
is_lf_symbol a s u ->
mor a p -> mor a q -> 
source q = lf_vertex u -> 
source p = target q ->
lf_extend a s (comp a p q) u =
lf_extend a s p (lf_extend a s q u).
Proof.
ir. 
ap lf_symbol_like_extens.
ap lf_symbol_like_lf_extend.
ap lf_symbol_like_lf_extend.
rw lf_forward_lf_extend. rw lf_forward_lf_extend.
rw lf_forward_lf_extend. 
rww assoc. uh H; ee. uh H4; ee; am. 
rw target_lf_forward. am. 
sh a. sh s. am. 
rw lf_backward_lf_extend. rw lf_backward_lf_extend.
rw lf_backward_lf_extend. 
rww assoc. uh H; ee. uh H4; ee. 
ap inc_ms_mor. sh s. ee; am. 
Qed.



Lemma lf_beyond_trans : forall a s u v w,
lf_beyond a s u v -> lf_beyond a s v w ->
lf_beyond a s u w.
Proof.
ir. 
uh H; uh H0; ee. nin H10; nin H5; ee.
uhg; ee; try am. 
rww H8. rww H9. 
assert (source x0 = target x).
transitivity (lf_vertex v).
am. wr H14. 
rw lf_vertex_lf_extend. 
tv. am. am. am. am. 

sh (comp a x0 x).
ee. 
rww  mor_comp. 
rww source_comp. 
rw lf_extend_comp. 
rw H14. rw H12. tv. 
am. am. am. am. am. 
Qed. 

Lemma exists_lf_under : forall a s u v,
lf_beyond a s u v -> exists w,
(lf_beyond a s v w & lf_under a s u w).
Proof.
ir. 
assert (lem1 : has_left_fractions a s).
lu. 
uh lem1; ee. 
util (H2 (lf_backward v) (lf_backward u)).
ap inc_lf_backward. sh a; lu. 
ap mor_lf_backward. sh s; lu. 
rw source_lf_backward. rw source_lf_backward.
uh H; ee. sy; am. uh H; ee. uh H4; ee; am. 
uh H; ee. uh H5; ee; am. 

nin H4. ee. 
uh H; ee. 
nin H12. ee. 

assert (source x = target x0).
transitivity (lf_vertex v).
am. wr H14. 
rw lf_vertex_lf_extend. tv. am. 
am. am. am. 

assert (lem2 : source x0 = target x).
rw H6. am. 



util (H3 
(lf_backward u) (lf_backward x) (comp a (lf_forward x) x0)).

ap inc_lf_backward. sh a; am. 
ap mor_lf_backward. sh s; am. 
rw mor_comp. tv. 
ap mor_lf_forward. sh s; am. 
am. rw source_lf_forward. 
am. 
uh H4; ee; am. 
tv. 
rw source_lf_backward. tv. 
uh H4; ee; am. 
rw source_comp. rw H13. tv. 
ap mor_lf_forward. sh s; am. am. 
rw source_lf_forward. am. 
uh H4; ee; am. 

util H16. rw assoc. 
assert (comp a x0 (lf_backward u) = 
lf_backward v). 
wr H14. rw lf_backward_lf_extend. tv. 
rw H17. am. 
ap mor_lf_forward. sh s; am. 
am. ap mor_lf_backward. sh s; am. 
rw source_lf_forward. am. 
uh H4; ee; am. 
wr H6. am.   
tv. clear H16. 
nin H17. 
ee. 

assert (mor a x1).
ap inc_hlf_mor. sh s; ee; am. 

assert (mor a (lf_forward x)).
ap mor_lf_forward. sh s; am. 

assert (mor a (lf_backward x)).
ap mor_lf_backward. sh s; am. 

assert (source x1 = target (lf_forward x)).
rw target_lf_forward. am. 
sh a; sh s; am. 


assert (lem3 : 
lf_extend a s (comp a x1 (lf_backward x)) u =
lf_extend a s (comp a x1 (lf_forward x)) v).
rw H19. 
wr assoc. 
rw lf_extend_comp. 
rw H14. reflexivity. 
am. 
rw mor_comp. tv. am. 
am. 
am. tv. 
am. am. 
rw source_comp. rw source_lf_forward. am. 
uh H4; ee; am. am. am. 
am. 
am. am. 
am. am. 
rww source_lf_forward. uh H4; ee; am. tv. 


sh (lf_extend a s (comp a x1 (lf_backward x)) u).
ee. 
rw lem3. 
ap lf_beyond_lf_extend. am. 
am. rww mor_comp. 
rww source_comp. 
rw source_lf_forward. am. uh H4; ee; am. 

rw assoc. wr H7. 
ap inc_comp. uh H; ee; am. am. 
ap  inc_comp. uh H; ee; am. 
ap inc_lf_backward. sh a; am. 
ap inc_lf_backward. sh a; am. 
wr H6. 
rw source_lf_backward. tv. uh H4; ee; am. 
rw target_comp. am. 
am. 
ap mor_lf_backward. sh s; am.  
rw source_lf_backward. rw target_lf_backward. 
am. uh H4; ee; am. am. 
am. ap mor_lf_backward. sh s; am. 
rw target_lf_forward. am. 
sh a; sh s; am. 

rw source_lf_forward. rw target_lf_backward. 
am. uh H4; ee; am. tv. 

ap  lf_under_lf_extend. 
am. am. ap inc_comp. 
uh H; ee; am. am. 
ap inc_lf_backward. sh a; am. 
am. 
rw source_comp. rw source_lf_backward. am. uh H4; ee; am. 
am. am. 
am. 
Qed. 

Definition lf_equiv a s u v :=
(exists w, (lf_beyond a s u w & lf_beyond a s v w)).


Lemma lf_equiv_symm : forall a s u v,
lf_equiv a s u v -> lf_equiv a s v u.
Proof.
ir. uh H; uhg. nin H. sh x. xd. 
Qed.

Lemma  lf_extend_id : forall a s u,
is_lf_symbol a s u -> 
lf_extend a s (id a (lf_vertex u)) u = u.
Proof.
ir. 
assert (ob a (lf_vertex u)). 
uf lf_vertex. rw ob_target. tv. 
ap mor_lf_backward. sh s; am. 

ap lf_symbol_like_extens. 
ap lf_symbol_like_lf_extend. 
uh H; ee; am. 
rw lf_forward_lf_extend. 
rw left_id. tv. am. 
ap  mor_lf_forward. sh s; am. 
rw target_lf_forward. tv. sh a; sh s; am. tv. 

rw lf_backward_lf_extend. rw left_id. 
tv. am. ap mor_lf_backward. sh s; am. 
rw target_lf_backward. tv. tv. 
Qed. 

Lemma lf_equiv_refl : forall a s u,
has_left_fractions a s -> 
is_lf_symbol a s u -> lf_equiv a s u u.
Proof.
ir. uhg. sh u. 
assert (ob a (lf_vertex u)).
uf lf_vertex. rw ob_target. tv. 
ap mor_lf_backward. sh s; am. 

dj. uhg; ee. 
am. am. am. tv. tv. 
sh (id a (lf_vertex u)). 
ee. ap mor_id. am. 
rww source_id. 
rw lf_extend_id. tv. am. am. 
Qed.

Lemma lf_beyond_refl : forall a s u,
has_left_fractions a s -> 
is_lf_symbol a s u -> lf_beyond a s u u.
Proof.
ir. assert (ob a (lf_vertex u)).
uf lf_vertex. rw ob_target. tv. 
ap mor_lf_backward. sh s; am. 

dj. uhg; ee. 
am. am. am. tv. tv. 
sh (id a (lf_vertex u)). 
ee. ap mor_id. am. 
rww source_id. 
rw lf_extend_id. tv. am. 
Qed. 



Lemma lf_equiv_beyond_under : forall a s u v,
lf_equiv a s u v -> exists w,
(lf_beyond a s u w & lf_under a s v w).
Proof.
ir. 
uh H. nin H. 
ee. 
cp (exists_lf_under H0). nin H1. 
ee. sh x0. ee. 
apply lf_beyond_trans with x. am. am. am. 
Qed.


Lemma exists_lf_further : forall a s u v w,
lf_beyond a s u v -> lf_under a s u w ->
exists z, (lf_beyond a s v z & lf_beyond a s w z).
Proof.
ir. uh H; uh H0; nin H; nin H0; ee.
nin H6; nin H10; ee. 
set (p:= lf_choice a s x x0).
set (e:= lf_backward p).
set (f:= lf_forward p).

assert (source x = source x0). 
rw H13. am. 

assert (is_lf_symbol a s p).
uf p. ap is_lf_symbol_lf_choice. 
am. am. am. am. 

assert (mor a e). 
uf e. ap mor_lf_backward. sh s; am.

assert (mor a f).
uf f. ap mor_lf_forward. sh s; am. 

assert (inc e s).
uf e. ap inc_lf_backward. sh a; am. 

assert (mor a x).
ap inc_hlf_mor. sh s; ee; am. 

assert (target x = lf_vertex w).
wr H12. rw lf_vertex_lf_extend. tv. 
am. am. am. am. 

assert (target x0 = lf_vertex v). 
wr H14. rw lf_vertex_lf_extend. tv. 
am. am. am. wrr H15. 

assert (target p = lf_vertex v). 
uf p. rww target_lf_choice. 

assert (source p = lf_vertex w). 
uf p. rww source_lf_choice. 

assert (source e = target x0).
rww H22. uf e. rww source_lf_backward.
uh H16; ee; am. 

assert (lf_vertex p = target f).
uf f. rww target_lf_forward. 
sh a; sh s; am. 

assert (target e = target f).
uf e. rww target_lf_backward. 

assert (source f = target x).
uf f. rww source_lf_forward. 
rww H24. sy; am. uh H16; ee; am. 

assert (source e = lf_vertex v).
rww H25. 

assert (source f = lf_vertex w).
rww H28. 

assert (comp a f x = comp a e x0).
uf f. uf e. 
uf p. sy. 
ap comp_lf_backward_lf_choice. am. 
am. am. am. 

assert (lf_extend a s e v = lf_extend a s f w).
transitivity (lf_extend a s (comp a e x0) u).
rw lf_extend_comp. rw H14. tv. 
am. am. am. am. am. 
wr H31. rw lf_extend_comp. 
rw H12. tv. am. am. am. am. am. 

sh (lf_extend a s e v). 
dj. ap lf_under_lf_beyond. 
ap lf_under_lf_extend. am. am. am. am. 

assert (localizing_system a s).
lu. 

rw H32. ap lf_beyond_lf_extend. 
am. am. am. am. 
rewrite <- lf_backward_lf_extend with (s:=s). 
wr H32. uh H33. ee. uh H36; ee. 
uh H40; ee. am. 
Qed. 








Lemma lf_equiv_trans : forall a s u w,
has_left_fractions a s -> 
(exists v, (lf_equiv a s u v & lf_equiv a s v w)) ->
lf_equiv a s u w.
Proof.
ir. nin H0. 
ee. cp (lf_equiv_beyond_under H0). 
cp (lf_equiv_beyond_under H1). 
nin H2. nin H3. ee. 
cp (exists_lf_further H3 H5). 
nin H6. ee. 

uhg. sh x2. ee. 
apply lf_beyond_trans with x0. am. 
am. 
apply lf_beyond_trans with x1. 
ap lf_under_lf_beyond. am. am. 
Qed.



(** Now we come to the definition of the composition
representative, and the proof that equivalent [lf_symbol]'s
give equivalent [lf_comp_rep]'s. ********************)

Definition fills_in a s u v w :=
has_left_fractions a s &
is_lf_symbol a s u & is_lf_symbol a s v & is_lf_symbol a s w
& source u = target v & source w = lf_vertex v &
target w = lf_vertex u & 
comp a (lf_forward w) (lf_backward v) =
comp a (lf_backward w) (lf_forward u).

Definition lf_filler a s u v := 
lf_choice a s (lf_backward v) (lf_forward u). 

Definition lf_make_comp a (s:E) u v w :=
lf_symbol (comp a (lf_forward w) (lf_forward v))
(comp a (lf_backward w) (lf_backward u)).

Definition lf_comp_rep a s u v := 
lf_make_comp a s u v (lf_filler a s u v).


Lemma fills_in_lf_filler : forall a s u v,
has_left_fractions a s ->
is_lf_symbol a s u -> is_lf_symbol a s v ->
source u = target v ->
fills_in a s u v (lf_filler a s u v).
Proof.
ir. uf lf_filler. 
uhg; ee. 
am. am. am. 
ap is_lf_symbol_lf_choice. am. 
uh H1; ee. uh H3; ee; am. 
uh H0; ee. uh H3; ee; am. 
rw source_lf_backward. rw source_lf_forward. 
sy; am. uh H0; ee; am. uh H1; ee; am. 
am. 
rw source_lf_choice. 
tv. am. uh H1; ee. uh H3; ee; am. 
uh H0; ee. uh H3; ee; am. 
rw source_lf_backward. 
rw source_lf_forward. sy; am. 
uh H0; ee; am. uh H1; ee; am. 

rw target_lf_choice. rw target_lf_forward. 
tv. sh a; sh s; am. am. 
uh H1; ee; uh H3; ee; am. 
uh H0; ee;  uh H3; ee; am. 
rw source_lf_backward. rw source_lf_forward. 
sy; am. uh H0; ee; am. 
uh H1; ee; am. 
rw comp_lf_backward_lf_choice. tv. 
am. uh H1; ee; uh H3; ee; am. 
uh H0; ee; uh H3; ee; am. 
rw source_lf_backward. rw source_lf_forward. 
sy; am. uh H0; ee; am. uh H1; ee; am. 
Qed.

Lemma source_lf_make_comp : forall a s u v w,
fills_in a s u v w -> 
source (lf_make_comp a s u v w) = source v.
Proof.
ir. 
uh H; ee. 
uf lf_make_comp. 
rw source_lf_symbol. 
rw source_comp. 
rw source_lf_forward. tv. 
uh H1; ee; am. 
uh H2; ee. uh H7; ee; am. 
uh H1; ee; uh H7; ee; am. 
rw source_lf_forward. 
rw target_lf_forward. am. sh a; sh s; am. 
uh H2; ee; am. 
Qed.

Lemma target_lf_make_comp : forall a s u v w,
fills_in a s u v w ->
target (lf_make_comp a s u v w) = target u.
Proof.
ir. 
uh H; ee. 
uh H0; uh H1; uh H2; ee.
uh H7; uh H8; uh H9; ee. 
uf lf_make_comp. 
rw target_lf_symbol. 
rww source_comp. 
rw source_lf_backward. tv. 
am. ap inc_hlf_mor. sh s; ee; am. 
ap inc_hlf_mor; sh s; ee; am. 
rww source_lf_backward. 
Qed.

Lemma lf_vertex_lf_make_comp : forall a s u v w,
fills_in a s u v w -> 
lf_vertex (lf_make_comp a s u v w) =
lf_vertex w. 
Proof.
ir. 
uf lf_vertex. 
uf lf_make_comp.
rw lf_backward_lf_symbol. 
uh H; ee. 
rw target_comp. tv. 
ap mor_lf_backward. 
sh s. am. 
ap mor_lf_backward. 
sh s. am. 
rw source_lf_backward. rw target_lf_backward. 
am. uh H2; ee; am. 
Qed.


Lemma is_lf_symbol_lf_make_comp : forall a s u v w,
fills_in a s u v w -> 
is_lf_symbol a s (lf_make_comp a s u v w).
Proof.
ir. uh H; ee. 
uh H0; uh H1; uh H2; ee.
uh H7; uh H8; uh H9; ee. 
uf lf_make_comp. 
ap is_lf_symbol_lf_symbol. 
uhg; ee. lu. 
rww mor_comp. 
rww source_lf_forward. rww target_lf_forward. 
sh a; sh s.
uhg; ee; try am. uhg; ee; try am. 
app inc_comp. uh H; ee; am. 
rww source_lf_backward. rww target_comp. 
rww target_lf_forward. 
rww target_comp. ap inc_hlf_mor.
sh s; ee; am. ap inc_hlf_mor; sh s; ee; am. 
rww source_lf_backward. sh a; sh s.
uhg; ee; try am. uhg; ee; am. 
rww source_lf_forward. rww target_lf_forward.
sh a; sh s. uhg; ee; try am. 
uhg; ee; am.  
Qed. 

Lemma lf_forward_lf_make_comp : forall a s u v w,
lf_forward (lf_make_comp a s u v w) = 
comp a (lf_forward w) (lf_forward v).
Proof.
ir. 
uf lf_make_comp. rww lf_forward_lf_symbol. 
Qed. 

Lemma lf_backward_lf_make_comp : forall a s u v w,
lf_backward (lf_make_comp a s u v w) = 
comp a (lf_backward w) (lf_backward u).
Proof.
ir. 
uf lf_make_comp. rww lf_backward_lf_symbol. 
Qed. 


Lemma lf_beyond_fills_in : forall a s u v w,
(exists y, (fills_in a s u v y & 
lf_beyond a s y w)) -> 
fills_in a s u v w.
Proof.
ir. nin H. 
ee. 
uh H; ee. 
uh H0. ee. nin H12. 
ee. 
uhg; ee; try am. 
wrr H10.  wrr H11. 
wr H14. 
rw lf_forward_lf_extend. 
rw lf_backward_lf_extend. 

assert (mor a (lf_forward x)).
uh H3; ee. uh H15; ee; am. 
assert (mor a (lf_forward u)).
uh H1; ee. uh H16; ee; am. 
assert (mor a (lf_backward x)).
ap mor_lf_backward. sh s; am. 
assert (mor a (lf_backward v)).
ap mor_lf_backward. sh s; am. 

rw assoc. rw H7. 
rww assoc. 
rw source_lf_backward. rw target_lf_forward.
am. sh a; sh s; am. uh H3; ee; am. 
am. am. am. 
rww target_lf_forward. 
sh a; sh s; am. 
rw source_lf_forward. rw target_lf_backward.
am. uh H3; ee; am. tv. 
Qed.

Lemma lf_beyond_lf_make_comp : forall a s u v w y,
fills_in a s u v w ->
lf_beyond a s w y ->
lf_beyond a s (lf_make_comp a s u v w) (lf_make_comp a s u v y).
Proof.
ir. 
cp H; cp H0. uh H1; uh H2; ee. 
nin H7; ee. 
assert (fills_in a s u v y).
ap lf_beyond_fills_in. sh w; ee; am. 
uhg; ee.
am. app is_lf_symbol_lf_make_comp.
app is_lf_symbol_lf_make_comp. 
rww source_lf_make_comp. rww source_lf_make_comp.
rww target_lf_make_comp. rww target_lf_make_comp.

sh x. ee. am. 
rww lf_vertex_lf_make_comp. 

ap lf_symbol_like_extens. 
ap lf_symbol_like_lf_extend. 
uf lf_make_comp. 
ap lf_symbol_like_lf_symbol. 
rw lf_forward_lf_extend. 
rw lf_forward_lf_make_comp. 
rw lf_forward_lf_make_comp. 
wr H16. 
rw lf_forward_lf_extend. 
sy; ap assoc. am. ap mor_lf_forward.
sh s; am. ap mor_lf_forward. 
sh s; am. rw target_lf_forward. am. 
sh a; sh s; am. rw source_lf_forward.
rw target_lf_forward. am. sh a; sh s; am.
uh H10; ee; am. tv. 

rw lf_backward_lf_extend. 
rw lf_backward_lf_make_comp.
rw lf_backward_lf_make_comp.
wr H16. rw lf_backward_lf_extend. 
sy; ap assoc. am. 
ap mor_lf_backward. sh s; am. 
ap mor_lf_backward. sh s; am. 
rw target_lf_backward. am. 
rw source_lf_backward. rw target_lf_backward. 
am. uh H10; ee; am. tv. 
Qed.

Definition lf_lean_to a s e f g h i j :=
has_left_fractions a s &
mor a e & mor a f & mor a g & mor a h & mor a i & mor a j &
inc e s & inc h s & 
source e = source f & source g = target e & source h = target f
& target g = target h & source i = target e & source j = target f
& target i = target j & 
comp a g e = comp a h f & comp a i e = comp a j f.

Lemma show_lf_lean_to : forall a s e f g h i j,
has_left_fractions a s ->
mor a f -> mor a g -> mor a i -> mor a j ->
inc e s -> inc h s ->
source e = source f -> source g = target e -> source h = target f
-> source i = target e -> source j = target f ->
comp a g e = comp a h f -> comp a i e = comp a j f->
lf_lean_to a s e f g h i j.
Proof.
ir. 
assert (mor a e).
ap inc_hlf_mor. sh s; ee; am. 
assert (mor a h).
ap inc_hlf_mor. sh s; ee; am. 
uhg; ee; try am.
transitivity (target (comp a g e)).
rww target_comp. rw H11. 
rww target_comp. 
transitivity (target (comp a i e)).
rww target_comp. rw H12. 
rww target_comp. 
Qed.

Definition closes_lf_lean_to a s e f g h i j k l :=
lf_lean_to a s e f g h i j &
mor a k & mor a l & inc l s & 
source k = target g & source l = target i &
target k = target l &
comp a k g = comp a l i & comp a k h = comp a l j.

(*** The following is one of the key arguments.
It uses both existence conditions in the [has_left_fractions] 
condition.
*************************************************)

Lemma lf_lean_to_closure : forall a s e f g h i j,
lf_lean_to a s e f g h i j -> 
(exists k, exists l,(closes_lf_lean_to a s e f g h i j k l)).
Proof.
ir. 
uh H; ee. 

assert (source h = source j). 
rww H13. 


set (w := lf_choice a s h j). 
assert (is_lf_symbol a s w). 
uf w. app is_lf_symbol_lf_choice. 

assert (source w = target h).
uf w. rww source_lf_choice. 

assert (target w = target j).
uf w. rww target_lf_choice. 

set (p:= lf_forward w).
set (q:= lf_backward w).

assert  (mor a p).
uf p. ap mor_lf_forward. sh s; am. 

assert (mor a q).
uf q. ap mor_lf_backward. sh s; am. 

assert (inc q s).
uf q. ap inc_lf_backward. sh a; am. 

assert (source p = target h).
uf p. rww source_lf_forward. uh H18; ee; am. 

assert (source p = target g).
rww H11. 

assert (source q = target j).
uf q. rww source_lf_backward. uh H18; ee; am. 

assert (source q = target i).
rww H14. 

assert (target p = target q).
uf p; uf q. rww target_lf_forward. 
sh a; sh s; am. 

assert (comp a p h = comp a q j).
uf p; uf q. sy. uf w. 
app comp_lf_backward_lf_choice. 

set (r:= comp a p g).
set (t:= comp a q i).

assert (mor a r).
uf r. rww mor_comp. 

assert (mor a t).
uf t. rww mor_comp.

assert (source r = target e).
uf r. rww source_comp. 

assert (source t = target e).
uf t. rww source_comp.

assert (target r = target p).
uf r. rww target_comp. 

assert (target t = target p).
uf t. rww target_comp.
sy; am. 

assert (target r = target t).
rww H35. 

(** Now is where we do the first diagram-chase **)

assert (comp a r e = comp a t e).
uf r. uf t. 
rww assoc. rw H15. 
wr assoc. rw H29. rww assoc. 
wr H16. rww assoc. am. am. am. 
am. am. tv. 


(** Now apply the hlf condition to get an 
arrow [x] which equalizes [r] and [t] on the left **)

cp H. uh H38. ee. 
util (H41 e r t). am. am. am. am. 
am. cp (H42 H37). clear H38 H39 H40 H41 H42. 
nin H43. ee. 

assert (mor a x).
ap inc_hlf_mor. sh s; ee; am. 
assert (source x = target p).
rww H39. 
assert (source x = target q).
rww H39. wrr H28. 

(** Now to finish the answer is the pair of arrows obtained
from [p] and [q] by composing with [x]. ***)

sh (comp a x p).
sh (comp a x q).
uhg; ee. 
uhg; ee; am. 
rww mor_comp. 
rww mor_comp. 
app inc_comp. uh H; ee; am. 
rww source_comp. rww source_comp. 
rww target_comp. rww target_comp. 


rww assoc. 
rww assoc. 

rww assoc. rww assoc. 
rww H29.  
Qed. 

(**** Hopefully we will be able to take this out 
Lemma fills_in_equiv : forall a s w y,
(exists u, exists v, (fills_in a s u v w &
fills_in a s u v y)) ->
lf_equiv a s w y.
Proof.
(** Ideally we should use the previous lemma, added later;
for now to save time we include the old proof which basically
redoes the same thing more clumsily **)
ir. nin H. nin H. 
ee. cp H; cp H0; uh H; uh H0; ee.
set (p:= lf_backward x0).
set (q:= lf_forward x).
assert (mor a q).
uf q. ap mor_lf_forward. sh s; am. 

assert (inc p s).
uf p. ap inc_lf_backward. sh a; am. 

assert (mor a p).
uf p. ap mor_lf_backward. sh s; am. 

assert (source p = source q).
uf p; uf q. rw source_lf_backward. 
rw source_lf_forward. sy; am. 
uh H3; ee; am. uh H4; ee; am. 

assert (target p = source w).
uf p. rw target_lf_backward. 
sy; am. 

assert (target p = source y).
uf p. rw target_lf_backward. sy; am. 

assert (target q = target w).
uf q. rw target_lf_forward. sy; am. 
sh a; sh s; am. 

assert (target q = target y).
uf q. rw target_lf_forward. sy; am. 
sh a; sh s; am. 

assert (comp a (lf_forward w) p = comp a (lf_backward w) q).
am. 

assert (comp a (lf_forward y) p = comp a (lf_backward y) q).
am. 

set (b:= lf_choice a s (lf_backward y) (lf_backward w)).

assert (is_lf_symbol a s b).
uf b. ap is_lf_symbol_lf_choice. 
am. ap inc_lf_backward. sh a; am. 
ap mor_lf_backward. sh s; am. 
rw source_lf_backward. rw source_lf_backward. 
rww H15. uh H12; ee; am. uh H5; ee; am. 

assert (source b = lf_vertex y).
uf b. rw source_lf_choice. 
rw target_lf_backward. tv. 
am. ap inc_lf_backward. sh a; am. 
ap mor_lf_backward. sh s; am. 
rw source_lf_backward. rw source_lf_backward. 
rww H15. uh H12; ee; am. uh H5; ee; am. 

assert (target b = lf_vertex w).
uf b. rw target_lf_choice. 
tv. 
am. ap inc_lf_backward. sh a; am. 
ap mor_lf_backward. sh s; am. 
rw source_lf_backward. rw source_lf_backward. 
rww H15. uh H12; ee; am. uh H5; ee; am. 


assert (comp a (lf_forward b) (lf_backward y) = 
comp a (lf_backward b) (lf_backward w)). 
uf b. sy. 
ap comp_lf_backward_lf_choice. 
am. ap inc_lf_backward. sh a; am. 
ap mor_lf_backward. sh s; am. 
rw source_lf_backward. rw source_lf_backward. 
rww H15. uh H12; ee; am. uh H5; ee; am. 

set (r:= comp a (lf_forward b) (lf_forward y)).
set (t:= comp a (lf_backward b) (lf_forward w)).

assert (mor a (lf_forward b)). 
ap mor_lf_forward. sh s; am.

assert (mor a (lf_forward y)).
ap mor_lf_forward. sh s; am.

assert (mor a (lf_backward b)).
ap mor_lf_backward. sh s; am. 

assert (mor a (lf_forward w)).
ap mor_lf_forward. sh s; am.

assert (source (lf_forward b) = target (lf_forward y)).
rw source_lf_forward. rw target_lf_forward. am. 
sh a; sh s; am. uh H27; ee; am. 

assert (source (lf_backward b) = target (lf_forward w)).
rw source_lf_backward. rw target_lf_forward. am. 
sh a; sh s; am. uh H27; ee; am. 

assert (source r = target p).
uf r. rww source_comp.
rw source_lf_forward. am. uh H5; ee; am. 

assert (source t = target p).
uf t. rww source_comp.
rw source_lf_forward. am. uh H12; ee; am. 

assert (mor a r).
uf r. rww mor_comp. 


assert (mor a t).
uf t. rww mor_comp. 

assert (comp a r p = comp a t p).
uf r; uf t. 
rww assoc. rw H26. 
sy. rww assoc. rw H25. 
wrr assoc. sy. wr assoc. 
rw H30. reflexivity. 
am. ap mor_lf_backward. sh s; am. 
am. rw H35. rww target_lf_forward.
sh a; sh s; am. 
rw source_lf_backward. sy; am. 
uh H5; ee; am. tv. 
ap mor_lf_backward. sh s; am. 
rw H36. 
rw target_lf_forward. tv. 
sh a; sh s; am. rw source_lf_backward.
sy; am. uh H12; ee; am. rw source_lf_forward.
sy; am. uh H12; ee; am. 
rw source_lf_forward. sy; am. uh H5; ee; am. 


cp H0. uh H42. ee. clear H42 H43 H44. 
util (H45 p r t).
am. am. am. am. am. 
cp (H42 H41). nin H43. 
ee. 


uhg. 
sh (lf_extend a s (comp a x1 (lf_backward b)) w).
dj. 
ap lf_under_lf_beyond. 
ap lf_under_lf_extend. 
am. am. 
ap inc_comp. uh H0; ee; am. am. 
ap inc_lf_backward. sh a; am. 
rw target_lf_backward. rw H44. 
uf r. rww target_comp. 
rw target_lf_forward. tv. 
sh a; sh s; am. 

rw source_comp. 
rw source_lf_backward. am. 
uh H27; ee; am. 
ap inc_hlf_mor. sh s; ee; am. 
am. 
rw target_lf_backward. rw H44. 
uf r. rww target_comp. 
rw target_lf_forward. tv. 
sh a; sh s; am. 

assert (lf_symbol_like y).
uh H5; ee; am. 
assert (lf_symbol_like w).
uh H12; ee; am. 
assert (lf_symbol_like b). 
uh H27; ee; am. 

assert (mor a x1).
ap inc_hlf_mor. sh s; ee; am. 

assert (mor a (lf_backward y)).
ap mor_lf_backward. sh s; am. 

assert (mor a (lf_backward w)).
ap mor_lf_backward. sh s; am. 

assert (target r = lf_vertex b).
uf r. rww target_comp.
rww target_lf_forward. 
sh a; sh s; am. 

assert (target t = lf_vertex b). 
uf t. rww target_comp. 


assert (lf_extend a s (comp a x1 (lf_backward b)) w
= lf_extend a s (comp a x1 (lf_forward b)) y).
ap lf_symbol_like_extens. 
ap  lf_symbol_like_lf_extend.
 ap  lf_symbol_like_lf_extend.
rw lf_forward_lf_extend. 
rw lf_forward_lf_extend.

rw assoc. rw assoc. sy; am. 
am. am. am. 
rw target_lf_forward. rw H44. 
am. sh a; sh s; am. 
rw source_lf_forward. rw target_lf_forward.
am. sh a; sh s; am. am. tv. 
am. am. am. 
rw target_lf_backward. rw H44. am. 
rw source_lf_backward. 
rw target_lf_forward. am. 
sh a; sh s; am. 
am. tv. 

rw lf_backward_lf_extend. 
rw lf_backward_lf_extend. 
rw assoc. 
rw assoc. ap uneq. 
uf b. 
ap comp_lf_backward_lf_choice. 
am. ap inc_lf_backward. sh a; am. 
am. rww source_lf_backward. rww source_lf_backward.
rww H15. am. am. am. 
rww target_lf_forward. rw H44. am. 
sh a; sh s; am. 
rw source_lf_forward. 
rw target_lf_backward. 
am. am. tv. am. 
am. am. rww target_lf_backward. rw H44. am. 
rw source_lf_backward. rw target_lf_backward. 
am. am. tv. 

rw H57. 

ap lf_beyond_lf_extend. 
am. am. 
rww mor_comp. 
rww target_lf_forward. rww H44. 
sh a; sh s; am. 

rww source_comp. 
rww source_lf_forward. 
rw target_lf_forward. rww H44. 
sh a; sh s; am. 
rw assoc. 
rw H30. 

ap inc_comp. uh H0; ee; am. 
am. 
ap inc_comp. uh H0; ee; am. 
ap inc_lf_backward. sh a; am. 
ap inc_lf_backward. sh a; am. 
rw source_lf_backward. rw target_lf_backward. 
am. am. 
rww target_comp. 
rww target_lf_backward. rww H44. 
rww source_lf_backward. am. 
am. am. 
rww target_lf_forward. 
rww H44. sh a; sh s; am. 
rww source_lf_forward. 
tv. 
Qed.

********************)

(** The following redefinition
 is somewhat similar to the difference between [lf_beyond]
and [lf_under]. It seems that we need both stronger and
weaker versions of this type of notion, asking or not
that the filler arrow be in [s]. *****************)

Definition weakly_reps_lf_comp a s u v w :=
has_left_fractions a s &
is_lf_symbol a s u & is_lf_symbol a s v & is_lf_symbol a s w
& source u = target v & source w = source v &
target w = target u & 
(exists p, exists q,( mor a p & mor a q &
source p = lf_vertex v & source q = lf_vertex u &
target p = lf_vertex w & target q = lf_vertex w &
comp a p (lf_backward v) = comp a q (lf_forward u) &
comp a p (lf_forward v) = lf_forward w &
comp a q (lf_backward u) = lf_backward w)).


Lemma weak_rep_lf_equiv : forall a s u v w y,
fills_in a s u v y -> 
weakly_reps_lf_comp a s u v w ->
lf_equiv a s w (lf_make_comp a s u v y).
Proof.
ir.
uh H0; ee. 
nin H7; nin H7; ee.
assert (lf_lean_to a s (lf_backward v) (lf_forward u)
(lf_forward y) (lf_backward y) x x0).

cp H. uh H16; ee. 

ap show_lf_lean_to. 
am. ap mor_lf_forward. sh s; am. 
ap mor_lf_forward. sh s; am. 
am. am. 
ap inc_lf_backward. sh a. am. 
ap inc_lf_backward. sh a; am. 
rww source_lf_backward. rww source_lf_forward. 
sy; am. uh H17; ee; am. uh H18; ee; am. 
rww source_lf_forward. uh H19; ee; am.

rww source_lf_backward. rww target_lf_forward. 
sh a; sh s; am. uh H19; ee; am. 
rww target_lf_backward. rww target_lf_forward. 
sh a; sh s; am. 
am. am. 

cp (lf_lean_to_closure H16).
nin H17; nin H17. 
uh H17; ee. 

cp H. uh H26; ee. 

uhg. 
sh (lf_extend a s x2 w). 
dj. 

ap lf_under_lf_beyond. 
ap lf_under_lf_extend. am. 
am. am. rww H22. 

uhg; ee. am. 
app  is_lf_symbol_lf_make_comp. 
uh H34; ee; am. 
rw source_lf_make_comp. rw source_lf_extend.
sy; am. am. am. 
rww H22. am. 

rw target_lf_make_comp. rw target_lf_extend. 
sy; am. am. am. rww H22. am. 

sh x1. ee. am. 
rw lf_vertex_lf_make_comp. wr target_lf_forward. 
am. sh a; sh s; am. am. 

ap lf_symbol_like_extens. ap lf_symbol_like_lf_extend.
ap lf_symbol_like_lf_extend. 

rw lf_forward_lf_extend. rw lf_forward_lf_make_comp.
rw lf_forward_lf_extend. 
wr assoc. rw H24. rw assoc. wr H14. tv. 
am. am. ap mor_lf_forward. sh s; am. 
am. rww target_lf_forward. sh a; sh s; am. 
tv. am. ap mor_lf_forward. sh s; am. 
ap mor_lf_forward. sh s; am. 
am. 
rww source_lf_forward. rww target_lf_forward. 
sh a; sh s; am. uh H29; ee; am. tv. 


rw lf_backward_lf_extend. rw lf_backward_lf_make_comp.
rw lf_backward_lf_extend. wr assoc. rw H25. 
rw assoc. rw H15. tv. 
am. am. ap mor_lf_backward. sh s; am. 
rw H22. rww H12. 
rww target_lf_backward. tv. 
am. ap mor_lf_backward. sh s; am. 
ap mor_lf_backward. sh s; am. 
rw target_lf_backward. wr target_lf_forward. 
am. sh a; sh s; am. 
rw source_lf_backward. rw target_lf_backward. 
am. uh H29; ee; am. tv.   
Qed.

Lemma lf_beyond_weakly_reps_make_comp : forall a s u v w y,
lf_beyond a s u w -> fills_in a s w v y ->
weakly_reps_lf_comp a s u v (lf_make_comp a s w v y).
Proof.
ir. 
cp H; cp H0. 
uh H1; uh H2; nin H1; ee. nin H14; ee. 

uhg; ee. 
am. am. am. 
app is_lf_symbol_lf_make_comp. 
rww H12. 
rww source_lf_make_comp. rww target_lf_make_comp. 
sy; am. 
sh (lf_forward y).
sh (comp a (lf_backward y) x).

assert (target x = lf_vertex w).
wr H16. rww lf_vertex_lf_extend. 

assert (lf_symbol_like u).
uh H3; ee; am. 
assert (lf_symbol_like v).
uh H5; ee; am. 
assert (lf_symbol_like w).
uh H4; ee; am. 
assert (lf_symbol_like y).
uh H6; ee; am. 

assert (mor a (lf_backward y)). 
ap mor_lf_backward. sh s; am. 

assert (mor a (lf_forward y)). 
ap mor_lf_forward. sh s; am. 

(*** a lot of verifications but basically they are standard **)
ee. 
ap mor_lf_forward. sh s; am. 
rww mor_comp.  
rw source_lf_backward. rww H17. 
am. rww source_lf_forward. 

rw source_comp. am. am. am. 
rww source_lf_backward. rww H17. 
rww target_lf_forward. rww lf_vertex_lf_make_comp.
sh a; sh s; am. 
rww target_comp. rww target_lf_backward. 
rww lf_vertex_lf_make_comp. rww source_lf_backward.
rww H17. 
rw H10. sy. rw assoc. ap uneq. wr H16. 
rww lf_forward_lf_extend. am. am. 
ap mor_lf_forward. sh s; am. 
rww source_lf_backward. rww H17. rww target_lf_forward.
sh a; sh s; am. tv. 
rww lf_forward_lf_make_comp. 
rww lf_backward_lf_make_comp. 
wr H16. rw lf_backward_lf_extend. 
ap assoc. am. am. ap mor_lf_backward. sh s; am. 
rww source_lf_backward. rww H17. 
rww target_lf_backward. tv.  
Qed. 

Lemma weakly_reps_make_comp : forall a s u v y,
fills_in a s u v y -> 
weakly_reps_lf_comp a s u v (lf_make_comp a s u v y).
Proof.
ir. 
cp H. uh H0; ee. 
uhg; ee; try am. 
app is_lf_symbol_lf_make_comp. 
rww source_lf_make_comp. 
rww target_lf_make_comp. 

assert (lf_symbol_like y).
uh H3; ee; am. 

sh (lf_forward y).
sh (lf_backward y).
dj. 
ap mor_lf_forward. sh s. am. 
ap mor_lf_backward. sh s; am. 
rww source_lf_forward. 
rww source_lf_backward. 
rww target_lf_forward. 
rww lf_vertex_lf_make_comp. sh a; sh s; am. 
rww target_lf_backward. 
rww lf_vertex_lf_make_comp. am. 
rww lf_forward_lf_make_comp. 
rww lf_backward_lf_make_comp. 
Qed. 


Lemma source_lf_comp_rep : forall a s u v,
has_left_fractions a s -> 
is_lf_symbol a s u -> is_lf_symbol a s v ->
source u = target v -> 
source (lf_comp_rep a s u v) = source v.
Proof.
ir.
assert (fills_in a s u v (lf_filler a s u v)).
app fills_in_lf_filler. 

uf lf_comp_rep.  
rww source_lf_make_comp. 
Qed.

Lemma target_lf_comp_rep : forall a s u v,
has_left_fractions a s -> 
is_lf_symbol a s u -> is_lf_symbol a s v ->
source u = target v -> 
target (lf_comp_rep a s u v) = target u.
Proof.
ir.
assert (fills_in a s u v (lf_filler a s u v)).
app fills_in_lf_filler. 

uf lf_comp_rep.  
rww target_lf_make_comp. 
Qed.

Lemma is_lf_symbol_lf_comp_rep : forall a s u v,
has_left_fractions a s -> 
is_lf_symbol a s u -> is_lf_symbol a s v ->
source u = target v -> 
is_lf_symbol a s (lf_comp_rep a s u v).
Proof.
ir.
assert (fills_in a s u v (lf_filler a s u v)).
app fills_in_lf_filler. 

uf lf_comp_rep.
app is_lf_symbol_lf_make_comp.
Qed.

Lemma weakly_reps_lf_comp_lf_comp_rep : forall a s u v,
has_left_fractions a s -> is_lf_symbol a s u ->
is_lf_symbol a s v -> source u = target v ->
weakly_reps_lf_comp a s u v (lf_comp_rep a s u v).
Proof.
ir.
assert (fills_in a s u v (lf_filler a s u v)).
app fills_in_lf_filler. 

uf lf_comp_rep. app weakly_reps_make_comp. 
Qed.
 

Lemma lf_equiv_lf_comp_rep : forall a s u v w,
weakly_reps_lf_comp a s u v w ->
lf_equiv a s w (lf_comp_rep a s u v).
Proof.
ir.
cp H. 
uh H0; ee. 
assert (fills_in a s u v (lf_filler a s u v)).
app fills_in_lf_filler. 

uf lf_comp_rep. app weak_rep_lf_equiv. 
Qed.

Lemma weakly_reps_lf_comp_equiv : forall a s w1 w2,
(exists u, exists v, (weakly_reps_lf_comp a s u v w1 & 
weakly_reps_lf_comp a s u v w2)) ->
lf_equiv a s w1 w2.
Proof.
ir. 
nin H. nin H. ee. 
ap lf_equiv_trans. uh H; ee; am. 
sh (lf_comp_rep a s x x0).
ee. 
ap lf_equiv_lf_comp_rep. am. ap lf_equiv_symm. 
ap lf_equiv_lf_comp_rep. am. 
Qed.


Lemma weakly_reps_make_comp_beyond : forall a s u v u1 v1 y,
has_left_fractions a s -> lf_beyond a s u u1 -> 
lf_beyond a s v v1 -> source u = target v -> 
fills_in a s u1 v1 y -> 
weakly_reps_lf_comp a s u v (lf_make_comp a s u1 v1 y).
Proof.
ir. 
cp H0; cp H1; cp H3. 
uh H4; uh H5; uh H6; ee. 
nin H23; nin H18; ee. 

uhg; ee; try am. 
app is_lf_symbol_lf_make_comp. 
rww source_lf_make_comp. wr H25. 
rww source_lf_extend. 
rww target_lf_make_comp. 
wrr H27. rww target_lf_extend. 

assert (mor a (lf_forward y)).
app mor_lf_forward. sh s; am. 

assert (mor a (lf_backward y)).
ap mor_lf_backward. sh s; am. 

assert (source (lf_forward y) = target x0).
rw source_lf_forward. rw H11. 
wr H25. rww lf_vertex_lf_extend. uh H9; ee; am.

assert (source (lf_backward y) = target x).
rw source_lf_backward. rw H12. wr H27. 
rww lf_vertex_lf_extend. uh H9; ee; am. 

assert (source x0 = target (lf_forward v)).
rww target_lf_forward. sh a; sh s; am. 

assert (source x0 = target (lf_backward v)).
rww target_lf_backward. 

assert (source x = target (lf_forward u)).
rww target_lf_forward. sh a; sh s; am. 

assert (source x = target (lf_backward u)).
rww target_lf_backward. 


sh (comp a (lf_forward y) x0).
sh (comp a (lf_backward y) x).
ee. 

rww mor_comp. rww mor_comp. 
rww source_comp. rww source_comp. 
rww target_comp. rww lf_vertex_lf_make_comp.
rww target_lf_forward. sh a; sh s; am. 
rww target_comp. rww lf_vertex_lf_make_comp.

assert (comp a x0 (lf_backward v) = lf_backward v1).
wr H25. rww lf_backward_lf_extend. 

assert (comp a x (lf_forward u) = lf_forward u1).
wr H27. rww lf_forward_lf_extend. 

rww assoc. rw H36. rww assoc. rww H37. 

ap mor_lf_forward. sh s; am. 
ap mor_lf_backward. sh s; am. 

rww lf_forward_lf_make_comp. 
rww assoc. ap uneq. wr H25. 
rww lf_forward_lf_extend. 
ap mor_lf_forward. sh s; am. 

rww lf_backward_lf_make_comp. 
rww assoc. ap uneq. 
wr H27. 
rww lf_backward_lf_extend. 
ap mor_lf_backward. sh s; am. 
Qed. 

Lemma weakly_reps_comp_rep_beyond : forall a s u v u1 v1,
has_left_fractions a s -> lf_beyond a s u u1 -> 
lf_beyond a s v v1 -> source u = target v -> 
weakly_reps_lf_comp a s u v (lf_comp_rep a s u1 v1).
Proof.
ir.
uf lf_comp_rep. 
app weakly_reps_make_comp_beyond. 
uh H0; uh H1; ee. app fills_in_lf_filler. 
wrr H10. wrr H6. 
Qed. 

(** The following is the statement that equivalent
symbols give equivalent composition representatives
(i.e. well-definedness of the composition up to
equivalence). This was a small piece of a phrase
in GZ. *******************************************)

Lemma lf_comp_indep : forall a s u v u1 v1,
has_left_fractions a s -> lf_equiv a s u u1 ->
lf_equiv a s v v1 -> source u = target v -> 
lf_equiv a s (lf_comp_rep a s u v) (lf_comp_rep a s u1 v1).
Proof.
ir. 
uh H0; uh H1. nin H0; nin H1; ee.
assert (source u = source u1).
uh H0; uh H4. ee. rww H7. 
assert (target v = target v1).
uh H1; uh H3. ee. rww H14. sy; am. 

ap lf_equiv_trans. am. 
sh (lf_comp_rep a s x x0).
ee.

ap weakly_reps_lf_comp_equiv. 
sh u; sh v. ee. app weakly_reps_lf_comp_lf_comp_rep.
uh H0; ee; am. 
uh H1; ee; am. 
app weakly_reps_comp_rep_beyond. 

ap weakly_reps_lf_comp_equiv. 
sh u1; sh v1. ee. 
app weakly_reps_comp_rep_beyond. 
wr H5; wr H6; am. 
app weakly_reps_lf_comp_lf_comp_rep.
uh H4; ee; am. uh H3; ee; am. 
wr H5; wr H6; am. 
Qed. 


(** The following is useful in practice. **)
Lemma lf_equiv_make_comp_comp_rep : forall a s u v y,
fills_in a s u v y ->
lf_equiv a s (lf_make_comp a s u v y) (lf_comp_rep a s u v).
Proof.
ir. ap lf_equiv_lf_comp_rep. 
ap weakly_reps_make_comp. am. 
Qed.

(** Next we do the associativity of composition up to
equivalence. This is relatively easy compared to what
we had to do for transitivity and well-definedness. ***)


(*** The definition [assoc_board]
corresponds to the following
 diagram: it is a sort of diagonal checkerboard. 

  \ w // \ v // \ u //
   \ //   \ //   \ //
      \ y // \ x //
       \ //   \ //
          \ z //
           \ //
 
********************************************)

Definition assoc_board a s u v w x y z :=
fills_in a s u v x &
fills_in a s v w y &
fills_in a s x y z.

(** The combination of [y] and [z]. **)

Definition ffb_symbol a (s:E) y z := 
(lf_symbol (comp a (lf_forward z) (lf_forward y)) (lf_backward z)).

(** The combination of [x] and [z]. **) 

Definition fbb_symbol a (s:E) x z :=
(lf_symbol (lf_forward z) (comp a (lf_backward z) (lf_backward x))).
 
Definition ffb_symbol_facts (a s u v w x y z k:E) := 
lf_forward k = comp a (lf_forward z) (lf_forward y) &
lf_backward k = lf_backward z &
source k = lf_vertex w &
target k = lf_vertex x &
target (lf_forward k) = lf_vertex z &
target (lf_backward k) = lf_vertex z &
lf_symbol_like k &
mor a (lf_forward k) &
mor a (lf_backward k) &
inc (lf_backward k) s &
is_lf_symbol a s k &
fills_in a s (lf_make_comp a s u v x) w k.

Lemma get_ffb_symbol_facts : forall a s u v w x y z,
assoc_board a s u v w x y z -> 
ffb_symbol_facts a s u v w x y z (ffb_symbol a s y z). 
Proof.
ir. 
set (k:= ffb_symbol a s y z).
cp H. uh H0; ee. uh H; ee. 
uh H0; uh H1; uh H2; ee.

assert (mor a (lf_forward z)).
ap mor_lf_forward. sh s; am. 
assert (mor a (lf_forward y)).
ap mor_lf_forward. sh s; am. 
assert (source (lf_forward z) = target (lf_forward y)).
rw source_lf_forward. rw target_lf_forward. 
am. sh a; sh s; am. uh H7; ee; am. 

uhg; dj. 

uf k. uf ffb_symbol. 
rww lf_forward_lf_symbol.

uf k. uf ffb_symbol. 
rww lf_backward_lf_symbol.  

uf k. uf ffb_symbol. 
rw source_lf_symbol. 
rww source_comp. rw source_lf_forward. 
am. uh H6; ee; am. 


uf k; uf ffb_symbol. 
rw target_lf_symbol. rw source_lf_backward. 
am. uh H7; ee; am. 

rw H29. rww target_comp. 
rww target_lf_forward. sh a; sh s; am. 
rw H30. rww target_lf_backward. 
uf k; uf ffb_symbol; ap lf_symbol_like_lf_symbol.

rw H29. rww mor_comp. 
rw H30. ap mor_lf_backward. sh s; am. 
rw H30. ap inc_lf_backward. sh a; am. 


uhg; ee. am. 
uhg; ee. uh H0; ee. 
uh H0; ee; am. 
am. am. rww H34. 

uhg; ee. am. ap is_lf_symbol_lf_make_comp. 
am. am. am. 
rww source_lf_make_comp. am. 
rww lf_vertex_lf_make_comp. 
rw H29. rw H30. 
rw lf_forward_lf_make_comp. 

assert (mor a (lf_backward w)).
ap mor_lf_backward. sh s; am. 

assert (mor a (lf_forward v)).
ap mor_lf_forward. sh s; am. 

assert (mor a (lf_backward y)).
ap mor_lf_backward. sh s; am. 

assert (mor a (lf_forward x)).
ap mor_lf_forward. sh s; am. 

assert (mor a (lf_backward z)).
ap mor_lf_backward. sh s; am. 


assert (source (lf_forward y) = target (lf_backward w)).
rw source_lf_forward. rww target_lf_backward. 
uh H6; ee; am. 

assert (source (lf_backward y) = target (lf_forward v)).
rw source_lf_backward. rww target_lf_forward. 
sh a; sh s; am. uh H6; ee; am. 

assert (source (lf_forward x) = target (lf_forward v)).
rw source_lf_forward. rww target_lf_forward. 
sh a; sh s; am. uh H5; ee; am. 

assert (source (lf_forward z) = target (lf_backward y)).
rw source_lf_forward. rww target_lf_backward. 
uh H7; ee; am. 

assert (source (lf_backward z) = target (lf_forward x)).
rw source_lf_backward. rww target_lf_forward. 
sh a; sh s; am. uh H7; ee; am. 

(** Now for the actual chase! **)

rww assoc. rw H18. 
wrr assoc. rw H11. 
rww assoc. 
Qed. 

Definition fbb_symbol_facts (a s u v w x y z k:E) := 
lf_forward k = lf_forward z &
lf_backward k = comp a (lf_backward z) (lf_backward x) &
source k = lf_vertex y &
target k = lf_vertex u &
target (lf_forward k) = lf_vertex z &
target (lf_backward k) = lf_vertex z &
lf_symbol_like k &
mor a (lf_forward k) &
mor a (lf_backward k) &
inc (lf_backward k) s &
is_lf_symbol a s k &
fills_in a s u (lf_make_comp a s v w y) k.

Lemma get_fbb_symbol_facts : forall a s u v w x y z,
assoc_board a s u v w x y z -> 
fbb_symbol_facts a s u v w x y z (fbb_symbol a s x z).
Proof.
ir. 
cp H. uh H; uh H0. ee. 
uh H0; uh H1; uh H2; ee. 

assert (lf_symbol_like y).
uh H14; ee; am.

assert (lf_symbol_like v).
uh H12; ee; am.

assert (lf_symbol_like z).
uh H7; ee; am.

assert (lf_symbol_like x).
uh H5; ee; am.

assert  (lf_symbol_like u).
uh H19; ee; am.

assert (mor a (lf_forward z)).
ap mor_lf_forward. sh s; am. 

assert (mor a (lf_backward z)).
ap mor_lf_backward. sh s; am. 

assert  (inc (lf_backward z) s).
ap inc_lf_backward. sh a; am. 

assert (mor a (lf_forward x)).
ap mor_lf_forward. sh s; am. 

assert (mor a (lf_backward x)).
ap mor_lf_backward. sh s; am. 

assert (inc (lf_backward x) s).
ap inc_lf_backward. sh a; am. 

assert (mor a (lf_backward y)).
ap mor_lf_backward. sh s; am. 

assert (mor a (lf_backward v)).
ap mor_lf_backward. sh s; am. 

assert (mor a (lf_forward u)).
ap mor_lf_forward. sh s; am. 

assert (source (lf_backward x) = target (lf_forward u)).
rww source_lf_backward. rww target_lf_forward. 
sh a; sh s; am. 

assert (source (lf_forward x) = target (lf_backward v)).
rww source_lf_forward. 

assert (source (lf_backward y) = target (lf_backward v)).
rww source_lf_backward. 

assert (source (lf_backward z) = target (lf_forward x)).
rww source_lf_backward. rww target_lf_forward. 
sh a; sh s; am. 

assert (source (lf_backward z) = target (lf_backward x)).
rww source_lf_backward. 

assert (source (lf_forward z) = target (lf_backward y)).
rww source_lf_forward. 

set (k:= fbb_symbol a s x z). 

uhg; dj. 

uf k. uf fbb_symbol. rww lf_forward_lf_symbol. 

uf k. uf fbb_symbol. rww lf_backward_lf_symbol. 

uf k. uf fbb_symbol. rww source_lf_symbol. 

uf k. uf fbb_symbol. rww target_lf_symbol. 
rww source_comp. rw H40. 
rww target_lf_forward. sh a; sh s; am. 
rw H46. rww target_lf_forward. sh a; sh s; am. 
rw H47. rww target_comp. 
uf k; uf fbb_symbol; ap lf_symbol_like_lf_symbol.
rww H46. rw H47. rww mor_comp. 
rw H47. app inc_comp. uh H0; ee; am. 

uhg; ee. am. uhg; ee. 
uh H0; ee; uh H0; ee; am. am. am. 
rw H50; rww H51. 

uhg; ee. am. am. 
app is_lf_symbol_lf_make_comp. 
am. rww target_lf_make_comp. 
rww lf_vertex_lf_make_comp. am. 

rw lf_backward_lf_make_comp. 
rw H46; rw H47. 

sy. rww assoc. wr H25. 
wrr assoc. wr H11. 
app assoc. 
Qed.  



Lemma make_comp_assoc_board : forall a s u v w x y z,
assoc_board a s u v w x y z ->
lf_make_comp a s (lf_make_comp a s u v x) w (ffb_symbol a s y z) =
lf_make_comp a s u (lf_make_comp a s v w y) (fbb_symbol a s x z).
Proof.
ir. 
cp H. uh H; uh H0. 
ee. uh H0; uh H1; uh H2; ee. 


assert (mor a (lf_forward w)).
ap mor_lf_forward. sh s; am. 

assert (mor a (lf_forward y)).
ap mor_lf_forward. sh s; am. 

assert (mor a (lf_forward z)).
ap mor_lf_forward. sh s; am. 

assert (mor a (lf_backward u)).
ap mor_lf_backward. sh s; am. 

assert (mor a (lf_backward x)).
ap mor_lf_backward. sh s; am. 

assert (mor a (lf_backward z)).
ap mor_lf_backward. sh s; am. 

assert (source (lf_forward y) = target (lf_forward w)).
rw source_lf_forward. rww target_lf_forward.
sh a; sh s; am. uh H6; ee; am. 

assert (source (lf_forward z) = target (lf_forward y)).
rw source_lf_forward. rww target_lf_forward.
sh a; sh s; am. uh H7; ee; am. 

assert (source (lf_backward x) = target (lf_backward u)).
rww source_lf_backward. uh H5; ee; am. 

assert (source (lf_backward z) = target (lf_backward x)). 
rww source_lf_backward. uh H7; ee; am. 


ap lf_symbol_like_extens. 
uf lf_make_comp. ap lf_symbol_like_lf_symbol. 
uf lf_make_comp. ap lf_symbol_like_lf_symbol. 

rw lf_forward_lf_make_comp. 
uf ffb_symbol. rw lf_forward_lf_symbol. 
rw lf_forward_lf_make_comp. 
uf fbb_symbol; rw lf_forward_lf_symbol. 
rw lf_forward_lf_make_comp. 
app assoc. 



rw lf_backward_lf_make_comp. 
uf ffb_symbol. rw lf_backward_lf_symbol. 
rw lf_backward_lf_make_comp. 
rw lf_backward_lf_make_comp. 
uf fbb_symbol; rw lf_backward_lf_symbol. 
sy; app assoc. 
Qed.

Lemma lf_comp_rep_assoc : forall a s u v w,
has_left_fractions a s -> 
is_lf_symbol a s u -> is_lf_symbol a s v -> 
is_lf_symbol a s w -> 
source u = target v -> source v = target w ->
lf_equiv a s (lf_comp_rep a s (lf_comp_rep a s u v) w)
(lf_comp_rep a s u (lf_comp_rep a s v w)).
Proof.
ir. 
set (x:= lf_filler a s u v).
set (y:= lf_filler a s v w).
set (z:= lf_filler a s x y).

assert (assoc_board a s u v w x y z).
uhg; dj. 
uf x. app fills_in_lf_filler. 
uf y. app fills_in_lf_filler. 
uh H5; uh H6; ee. 
uf z. app fills_in_lf_filler. 
rww H12. 

cp H5. uh H6; ee. 
cp (get_ffb_symbol_facts H5). 
cp (get_fbb_symbol_facts H5).

cp (make_comp_assoc_board H5). 
generalize H9 H10 H11. clear H9 H10 H11. 
set (k:= ffb_symbol a s y z). 
set (l:= fbb_symbol a s x z). 
ir. 

uh H9; uh H10; ee.

assert (lf_make_comp a s v w y = lf_comp_rep a s v w).
reflexivity. 

assert (lf_make_comp a s u v x = lf_comp_rep a s u v).
reflexivity. 

rwi H34 H22. 
rwi H35 H33. rwi H34 H11. rwi H35 H11. 

cp (lf_equiv_make_comp_comp_rep H33). 
cp (lf_equiv_make_comp_comp_rep H22). 

ap lf_equiv_trans. 
am. sh (lf_make_comp a s (lf_comp_rep a s u v) w k).
ee.

app lf_equiv_symm. 
rww H11.  
Qed. 

Definition left_id_filler a (s:E) u := 
lf_symbol (id a (lf_vertex u)) (lf_backward u).

Definition right_id_filler a (s:E) u :=
lf_symbol (lf_forward u) (id a (lf_vertex u)).

Lemma ob_lf_vertex : forall a u,
(exists s,(is_lf_symbol a s u)) ->
ob a (lf_vertex u).
Proof.
ir. uf lf_vertex. rww ob_target. 
app mor_lf_backward. 
Qed. 

Lemma source_left_id_filler : forall a s u,
is_lf_symbol a s u -> 
source (left_id_filler a s u) = lf_vertex u.
Proof.
ir. uf left_id_filler. rw source_lf_symbol. 
rww source_id. 
ap ob_lf_vertex. sh s; am. 
Qed.

Lemma target_left_id_filler : forall a s u,
is_lf_symbol a s u -> 
target (left_id_filler a s u) = target u.
Proof.
ir. uf left_id_filler. rw target_lf_symbol. 
rw source_lf_backward. tv. uh H; ee; am. 
Qed.

Lemma source_right_id_filler : forall a s u,
is_lf_symbol a s u -> 
source (right_id_filler a s u) = source u.
Proof.
ir. uf right_id_filler. rw source_lf_symbol. 
rw source_lf_forward. tv. uh H; ee; am.   
Qed.

Lemma target_right_id_filler : forall a s u,
is_lf_symbol a s u -> 
target (right_id_filler a s u) = lf_vertex u.
Proof.
ir. uf right_id_filler. rw target_lf_symbol. 
uf lf_vertex. ap source_id. 
rww ob_target. ap mor_lf_backward. sh s; am. 
Qed.

Lemma lf_forward_left_id_filler : forall a s u,
is_lf_symbol a s u -> 
lf_forward (left_id_filler a s u) = id a (lf_vertex u).
Proof.
ir. uf left_id_filler. rww lf_forward_lf_symbol. 
Qed. 

Lemma lf_backward_left_id_filler : forall a s u,
is_lf_symbol a s u -> 
lf_backward (left_id_filler a s u) = lf_backward u.
Proof.
ir. uf left_id_filler. rww lf_backward_lf_symbol. 
Qed. 

Lemma lf_forward_right_id_filler : forall a s u,
is_lf_symbol a s u -> 
lf_forward (right_id_filler a s u) = lf_forward u.
Proof.
ir. uf right_id_filler. rww lf_forward_lf_symbol. 
Qed. 

Lemma lf_backward_right_id_filler : forall a s u,
is_lf_symbol a s u -> 
lf_backward (right_id_filler a s u) = id a (lf_vertex u).
Proof.
ir. uf right_id_filler. rww lf_backward_lf_symbol. 
Qed. 

Lemma lf_vertex_left_id_filler : forall a s u,
is_lf_symbol a s u -> 
lf_vertex (left_id_filler a s u) = lf_vertex u.
Proof.
ir. uf lf_vertex. 
rww lf_backward_left_id_filler. 
Qed.

Lemma lf_vertex_right_id_filler : forall a s u,
is_lf_symbol a s u -> 
lf_vertex (right_id_filler a s u) = lf_vertex u.
Proof.
ir. uf lf_vertex.   
rww lf_backward_right_id_filler. 
rww target_id. 
ap ob_lf_vertex. sh s; am.  
Qed.

Lemma is_lf_symbol_left_id_filler : forall a s u,
is_lf_symbol a s u -> 
is_lf_symbol a s (left_id_filler a s u).
Proof.
ir. uhg; ee. 
uf left_id_filler. ap lf_symbol_like_lf_symbol. 
uhg; ee. 
lu. rww lf_forward_left_id_filler. 
app mor_id. 
ap ob_lf_vertex. sh s; am. 
rw lf_backward_left_id_filler. 
ap inc_lf_backward. sh a; am. 
am. 
rww lf_forward_left_id_filler. 
rww lf_backward_left_id_filler. 
rww target_id. ap ob_lf_vertex. sh s; am.  
Qed.


Lemma is_lf_symbol_right_id_filler : forall a s u,
has_left_fractions a s -> is_lf_symbol a s u -> 
is_lf_symbol a s (right_id_filler a s u).
Proof.
ir. uhg; ee. 
uf right_id_filler. ap lf_symbol_like_lf_symbol. 
uhg; ee. 
lu. rww lf_forward_right_id_filler. 
ap mor_lf_forward. sh s; am. 
rw lf_backward_right_id_filler. 
uh H; ee. ap H1. ap ob_lf_vertex. sh s; am. am. 

rww lf_forward_right_id_filler. 
rww lf_backward_right_id_filler. 
rww target_id. rww target_lf_forward. 
sh a; sh s; am. ap ob_lf_vertex. sh s; am.  
Qed.


Lemma lf_forward_lf_id_rep : forall a x,
lf_forward (lf_id_rep a x) = id a x.
Proof.
ir. uf lf_id_rep. rww lf_forward_lf_symbol. 
Qed.

Lemma lf_backward_lf_id_rep : forall a x,
lf_backward (lf_id_rep a x) = id a x.
Proof.
ir. uf lf_id_rep. rww lf_backward_lf_symbol. 
Qed.


Lemma fills_in_left_id_filler : forall a s u,
has_left_fractions a s -> is_lf_symbol a s u ->
fills_in a s (lf_id_rep a (target u)) u (left_id_filler a s u).
Proof.
ir. 
assert (target u = source (lf_backward u)).
rww source_lf_backward. uh H0; ee; am. 
assert (ob a (target u)).
rw H1. rww ob_source. ap mor_lf_backward. 
sh s; am. 

assert (mor a (lf_backward u)).
ap mor_lf_backward. sh s; am. 


uhg; ee. 
am. ap is_lf_symbol_lf_id_rep. am. 
am. am. 
ap is_lf_symbol_left_id_filler. am. 
rww source_lf_id_rep. 
rww source_left_id_filler. 
rww target_left_id_filler. 
uf lf_vertex. 
rw lf_backward_lf_id_rep. 
rww target_id. 

rww lf_forward_left_id_filler. rw lf_backward_left_id_filler.
rw lf_forward_lf_id_rep. 
assert (lf_vertex u = target (lf_backward u)).
tv. rw H4. 
rww left_id. 
rw H1. 
rww right_id. rww ob_source. 
rww ob_target. am.  
Qed.

Lemma fills_in_right_id_filler : forall a s u,
has_left_fractions a s -> is_lf_symbol a s u ->
fills_in a s u (lf_id_rep a (source u)) (right_id_filler a s u).
Proof.
ir. 
assert (source u = source (lf_forward u)).
rww source_lf_forward. uh H0; ee; am. 
assert (ob a (source u)).
rw H1. rww ob_source. ap mor_lf_forward. 
sh s; am. 

assert (mor a (lf_forward u)).
ap mor_lf_forward. sh s; am. 


uhg; ee. 
am. am. ap is_lf_symbol_lf_id_rep. am. 
am. 
ap is_lf_symbol_right_id_filler. am. 
am. rww target_lf_id_rep. 
rww source_right_id_filler. 
uf lf_vertex. 
rw lf_backward_lf_id_rep. 
rww target_id. 

rww target_right_id_filler. 

rww lf_forward_right_id_filler. rw lf_backward_right_id_filler.
rw lf_backward_lf_id_rep. 
assert (lf_vertex u = target (lf_forward u)).
rw target_lf_forward. tv. sh a; sh s; am.  rw H4. 
rww right_id. 
rww left_id. rww ob_target. 
rww source_lf_forward. uh H0; ee; am. am. 
Qed.

Lemma lf_make_comp_left_id_filler : forall a s u,
is_lf_symbol a s u -> 
lf_make_comp a s (lf_id_rep a (target u)) u 
(left_id_filler a s u) = u.
Proof.
ir. 

ap lf_symbol_like_extens. 
uf lf_make_comp. ap lf_symbol_like_lf_symbol. 
uh H; ee; am. 
rw lf_forward_lf_make_comp. 
rw lf_forward_left_id_filler. 
assert (lf_vertex u = target (lf_forward u)).
rw target_lf_forward. tv. sh a; sh s; am. 
rw H0. 
rww left_id. rww ob_target. 
ap mor_lf_forward. sh s; am. 
ap mor_lf_forward. sh s; am. am. 

rw lf_backward_lf_make_comp. 
rw lf_backward_left_id_filler. 
rw lf_backward_lf_id_rep. 
assert (target u = source (lf_backward u)).
rww source_lf_backward. uh H; ee; am. 
rw H0. rww right_id. 
rww ob_source. 
ap mor_lf_backward. sh s; am. 
ap mor_lf_backward. sh s; am. am. 
Qed.

Lemma lf_make_comp_right_id_filler : forall a s u,
is_lf_symbol a s u -> 
lf_make_comp a s u (lf_id_rep a (source u)) 
(right_id_filler a s u) = u.
Proof.
ir. 
assert (mor a (lf_forward u)).
ap mor_lf_forward. sh s; am.

assert (mor a (lf_backward u)).
ap mor_lf_backward. sh s; am.

ap lf_symbol_like_extens. 
uf lf_make_comp. ap lf_symbol_like_lf_symbol. 
uh H; ee; am. 

rw lf_forward_lf_make_comp. 
rw lf_forward_right_id_filler. 
rw lf_forward_lf_id_rep. 
assert (source u = source (lf_forward u)).
rww source_lf_forward. uh H; ee; am. 
rw H2. 
rww right_id. rww ob_source. am. 

rw lf_backward_lf_make_comp. 
rw lf_backward_right_id_filler. 
assert (lf_vertex u = target (lf_backward u)).
rww target_lf_backward. rw H2. 
rww left_id. rww ob_target. am. 
Qed.

(** putting together the above with previous stuff
we get the left and right identity properties **)

Lemma lf_left_id : forall a s u,
has_left_fractions a s ->
is_lf_symbol a s u -> 
lf_equiv a s (lf_comp_rep a s (lf_id_rep a (target u)) u) u.
Proof.
ir. 
cp (fills_in_left_id_filler H H0). 
cp (lf_equiv_make_comp_comp_rep H1).
rwi lf_make_comp_left_id_filler H2. 
app lf_equiv_symm. am. 
Qed.

Lemma lf_right_id : forall a s u,
has_left_fractions a s ->
is_lf_symbol a s u -> 
lf_equiv a s (lf_comp_rep a s u (lf_id_rep a (source u))) u.
Proof.
ir. 
cp (fills_in_right_id_filler H H0). 
cp (lf_equiv_make_comp_comp_rep H1).
rwi lf_make_comp_right_id_filler H2. 
app lf_equiv_symm. am. 
Qed.

(** Now we define the [taut_lf_symbol]'s which will 
give the functor from [a] to the fraction category. **) 


Definition taut_lf_symbol a y :=
lf_symbol y (id a (target y)).


Lemma source_taut_lf_symbol : forall a y,
source (taut_lf_symbol a y) = source y.
Proof.
ir. uf taut_lf_symbol. rww source_lf_symbol.
Qed.

Lemma target_taut_lf_symbol : forall a y,
mor a y -> 
target (taut_lf_symbol a y) = target y.
Proof.
ir. uf taut_lf_symbol. rww target_lf_symbol.
rww source_id. rww ob_target. 
Qed.

Lemma lf_forward_taut_lf_symbol : forall a y,
lf_forward (taut_lf_symbol a y) = y.
Proof.
ir. uf taut_lf_symbol. 
rww lf_forward_lf_symbol. 
Qed.

Lemma lf_backward_taut_lf_symbol : forall a y,
lf_backward (taut_lf_symbol a y) = id a (target y).
Proof.
ir. uf taut_lf_symbol. 
rww lf_backward_lf_symbol. 
Qed.

Lemma lf_vertex_taut_lf_symbol : forall a y,
mor a y -> 
lf_vertex (taut_lf_symbol a y) = target y.
Proof.
ir. uf lf_vertex. rw lf_backward_taut_lf_symbol.
rww target_id. rww ob_target. 
Qed.

Lemma is_lf_symbol_taut_lf_symbol : forall a s y,
has_left_fractions a s -> mor a y ->
is_lf_symbol a s (taut_lf_symbol a y).
Proof.
ir. 
uhg; ee. uf taut_lf_symbol. 
ap lf_symbol_like_lf_symbol. 
uhg; ee. 
lu. 
rww lf_forward_taut_lf_symbol. 
rww lf_backward_taut_lf_symbol. 
uh H; ee.
ap H1. rww ob_target. 
rw lf_forward_taut_lf_symbol. 
rw lf_backward_taut_lf_symbol. 
rww target_id. rww ob_target. 
Qed.

Lemma taut_lf_symbol_id : forall a x,
ob a x -> 
taut_lf_symbol a (id a x) = lf_id_rep a x.
Proof.
ir. uf taut_lf_symbol. 
rww target_id. 
Qed. 

Lemma fills_in_taut_lf_symbol : forall a s y z,
has_left_fractions a s -> 
mor a y -> mor a z -> source y = target z ->
fills_in a s (taut_lf_symbol a y) 
(taut_lf_symbol a z) (taut_lf_symbol a y).
Proof.
ir. 

uhg; ee. 
am. 
app is_lf_symbol_taut_lf_symbol. 
app is_lf_symbol_taut_lf_symbol. 
app is_lf_symbol_taut_lf_symbol. 
rww source_taut_lf_symbol. 
rww target_taut_lf_symbol. 
rww source_taut_lf_symbol. 
rww lf_vertex_taut_lf_symbol. 
rww target_taut_lf_symbol. 
rww lf_vertex_taut_lf_symbol. 

rww lf_forward_taut_lf_symbol. 
rww lf_backward_taut_lf_symbol. 
rww lf_backward_taut_lf_symbol. 
wr H2. rww left_id. rww right_id. 
rww ob_source. rww ob_target. 
Qed.

Lemma comp_taut_lf_symbol : forall a s y z,
has_left_fractions a s -> 
mor a y -> mor a z -> source y = target z ->
lf_equiv a s 
(lf_comp_rep a s (taut_lf_symbol a y) (taut_lf_symbol a z))
(taut_lf_symbol a (comp a y z)).
Proof.
ir. 
cp (fills_in_taut_lf_symbol H H0 H1 H2). 
cp (lf_equiv_make_comp_comp_rep H3).

assert (lf_make_comp a s (taut_lf_symbol a y) (taut_lf_symbol a z)
          (taut_lf_symbol a y) = taut_lf_symbol a (comp a y z)).
ap lf_symbol_like_extens. 
uf lf_make_comp. ap lf_symbol_like_lf_symbol. 
uf taut_lf_symbol. ap lf_symbol_like_lf_symbol. 

rww lf_forward_lf_make_comp. 
rww lf_forward_taut_lf_symbol. 
rww lf_forward_taut_lf_symbol. 
rww lf_forward_taut_lf_symbol. 

rww lf_backward_lf_make_comp. 
rww lf_backward_taut_lf_symbol. 
rww lf_backward_taut_lf_symbol. 
rww left_id. 
rww target_comp. rww ob_target. app mor_id. 
rww ob_target. rww target_id. 
rww ob_target. 

rwi H5 H4. app lf_equiv_symm. 
Qed.

 

(** Next are the inverses for morphisms in [s]. **)

Definition inverse_lf_symbol a y :=
lf_symbol (id a (target y)) y.

Lemma source_inverse_lf_symbol : forall a y,
mor a y -> 
source (inverse_lf_symbol a y) = target y.
Proof.
ir. uf inverse_lf_symbol. rww source_lf_symbol.
rww source_id. rww ob_target. 
Qed.

Lemma target_inverse_lf_symbol : forall a y,
mor a y -> 
target (inverse_lf_symbol a y) = source y.
Proof.
ir. uf inverse_lf_symbol. rww target_lf_symbol.
Qed.

Lemma lf_forward_inverse_lf_symbol : forall a y,
lf_forward (inverse_lf_symbol a y) = id a (target y).
Proof.
ir. uf inverse_lf_symbol. 
rww lf_forward_lf_symbol. 
Qed.

Lemma lf_backward_inverse_lf_symbol : forall a y,
lf_backward (inverse_lf_symbol a y) = y.
Proof.
ir. uf inverse_lf_symbol. 
rww lf_backward_lf_symbol. 
Qed.

Lemma lf_vertex_inverse_lf_symbol : forall a y,
lf_vertex (inverse_lf_symbol a y) = target y.
Proof.
ir. uf lf_vertex. rw lf_backward_inverse_lf_symbol.
tv. 
Qed.

Lemma is_lf_symbol_inverse_lf_symbol : forall a s y,
has_left_fractions a s -> inc y s ->
is_lf_symbol a s (inverse_lf_symbol a y).
Proof.
ir. 
assert (mor a y).
ap inc_hlf_mor. sh s; ee; am. 
uhg; ee. uf inverse_lf_symbol. 
ap lf_symbol_like_lf_symbol. 
uhg; ee. 
lu. 
rww lf_forward_inverse_lf_symbol. 
app mor_id. rww ob_target. 
rww lf_backward_inverse_lf_symbol. 
rw lf_forward_inverse_lf_symbol. 
rw lf_backward_inverse_lf_symbol. 
rww target_id. rww ob_target. 
Qed.

Lemma fills_in_left_lf_inverse : forall a s y,
has_left_fractions a s -> inc y s ->
fills_in a s (inverse_lf_symbol a y) (taut_lf_symbol a y)
(lf_id_rep a (target y)).
Proof.
ir. 
assert (mor a y).
ap inc_hlf_mor. sh s; ee; am. 
assert (ob a (source y)).
rww ob_source. 
assert (ob a (target y)).
rww ob_target. 

uhg; ee. am. 
app is_lf_symbol_inverse_lf_symbol. 
app is_lf_symbol_taut_lf_symbol. 
app is_lf_symbol_lf_id_rep. 

rww source_inverse_lf_symbol. rww target_taut_lf_symbol.
rww source_lf_id_rep. rww lf_vertex_taut_lf_symbol. 
rww target_lf_id_rep. rww lf_vertex_inverse_lf_symbol. 

rww lf_forward_lf_id_rep. 
rww lf_backward_taut_lf_symbol. 
rww lf_backward_lf_id_rep. 
rww lf_forward_inverse_lf_symbol. 
Qed.

Lemma fills_in_right_lf_inverse : forall a s y,
has_left_fractions a s -> inc y s ->
fills_in a s (taut_lf_symbol a y) (inverse_lf_symbol a y)
(lf_id_rep a (target y)).
Proof.
ir. 
assert (mor a y).
ap inc_hlf_mor. sh s; ee; am. 
assert (ob a (source y)).
rww ob_source. 
assert (ob a (target y)).
rww ob_target. 

uhg; ee. am. 
app is_lf_symbol_taut_lf_symbol. 
app is_lf_symbol_inverse_lf_symbol. 
app is_lf_symbol_lf_id_rep. 

rww target_inverse_lf_symbol. rww source_taut_lf_symbol.
rww source_lf_id_rep. rww lf_vertex_inverse_lf_symbol. 
rww target_lf_id_rep. rww lf_vertex_taut_lf_symbol. 

rww lf_forward_lf_id_rep. 
rww lf_backward_inverse_lf_symbol. 
rww lf_backward_lf_id_rep. 
rww lf_forward_taut_lf_symbol. 
Qed.


Lemma lf_left_inverse : forall a s y,
has_left_fractions a s -> inc y s ->
lf_equiv a s 
(lf_comp_rep a s (inverse_lf_symbol a y) (taut_lf_symbol a y))
(lf_id_rep a (source y)).
Proof.
ir. 
assert (mor a y).
ap inc_hlf_mor. sh s; ee; am. 
assert (ob a (source y)).
rww ob_source. 
assert (ob a (target y)).
rww ob_target. 

cp (fills_in_left_lf_inverse H H0). 
cp (lf_equiv_make_comp_comp_rep H4).
assert (lf_make_comp a s 
(inverse_lf_symbol a y) (taut_lf_symbol a y)
(lf_id_rep a (target y)) = lf_symbol y y).
ap lf_symbol_like_extens. 
uf lf_make_comp. ap lf_symbol_like_lf_symbol.
ap lf_symbol_like_lf_symbol.

rww lf_forward_lf_make_comp. 
rww lf_forward_lf_id_rep. 
rww lf_forward_taut_lf_symbol. 
rww lf_forward_lf_symbol. 
rww left_id. 

rww lf_backward_lf_make_comp. 
rww lf_backward_lf_id_rep. 
rww lf_backward_inverse_lf_symbol. 
rww lf_backward_lf_symbol. 
rww left_id. 

rwi H6 H5. 
clear H6. 

apply lf_equiv_trans. am. 
sh (lf_symbol y y). 
ee. 
app lf_equiv_symm. 

assert (is_lf_symbol a s (lf_symbol y y)).
uhg; ee. ap lf_symbol_like_lf_symbol. 
uhg; ee. uh H; ee; uh H; ee; am. 
rww lf_forward_lf_symbol. 
rww lf_backward_lf_symbol. 
rww lf_forward_lf_symbol. 
rww lf_backward_lf_symbol. 

uhg; ee. 

sh (lf_symbol y y).
ee. 
ap lf_beyond_refl. am. am. 

uhg; ee. 
am. app is_lf_symbol_lf_id_rep. 
am. 
rww source_lf_id_rep. rww source_lf_symbol. 
rww target_lf_id_rep. rww target_lf_symbol.
sh y. ee. am. 
uf lf_vertex. rww lf_backward_lf_id_rep. 
rww target_id. 
uf lf_extend. 
rw lf_forward_lf_id_rep. 
rw right_id. 
rw lf_backward_lf_id_rep. 
rw right_id. tv. am. am. tv. tv. 
am. am. tv. tv. 
Qed.


Lemma lf_right_inverse : forall a s y,
has_left_fractions a s -> inc y s ->
lf_equiv a s 
(lf_comp_rep a s (taut_lf_symbol a y) (inverse_lf_symbol a y))
(lf_id_rep a (target y)).
Proof.
ir. 
assert (mor a y).
ap inc_hlf_mor. sh s; ee; am. 
assert (ob a (source y)).
rww ob_source. 
assert (ob a (target y)).
rww ob_target. 

cp (fills_in_right_lf_inverse H H0). 
cp (lf_equiv_make_comp_comp_rep H4).
assert (lf_make_comp a s 
(taut_lf_symbol a y) (inverse_lf_symbol a y)
(lf_id_rep a (target y)) = lf_id_rep a (target y)).
ap lf_symbol_like_extens. 
uf lf_make_comp. ap lf_symbol_like_lf_symbol.
uf lf_id_rep. ap lf_symbol_like_lf_symbol.

rww lf_forward_lf_make_comp. 
rww lf_forward_lf_id_rep. 
rww lf_forward_inverse_lf_symbol. 
rww left_id. app mor_id. 
rww target_id. 

rww lf_backward_lf_make_comp. 
rww lf_backward_lf_id_rep. 
rww lf_backward_taut_lf_symbol. 
rww left_id. 
app mor_id. rww target_id. 

rwi H6 H5. app lf_equiv_symm. 
Qed.

Lemma lf_symbol_equiv : forall a s u,
has_left_fractions a s -> is_lf_symbol a s u ->
lf_equiv a s u 
(lf_comp_rep a s 
(inverse_lf_symbol a (lf_backward u))
(taut_lf_symbol a (lf_forward u))).
Proof.
ir. 
assert (exists s0, is_lf_symbol a s0 u).
sh s; am. 
assert (exists a0, is_lf_symbol a0 s u).
sh a; am. 
assert (exists a0, exists s0, is_lf_symbol a0 s0 u).
sh a; sh s; am. 
assert (mor a (lf_forward u)).
app mor_lf_forward. 
assert (mor a (lf_backward u)).
app mor_lf_backward. 
assert (inc (lf_backward u) s).
app inc_lf_backward. 
assert (ob a (lf_vertex u)).
app ob_lf_vertex.  


assert (fills_in a s (inverse_lf_symbol a (lf_backward u))
(taut_lf_symbol a (lf_forward u)) (lf_id_rep a (lf_vertex u))).

uhg; ee. am. 
app is_lf_symbol_inverse_lf_symbol. 
app is_lf_symbol_taut_lf_symbol. 
app is_lf_symbol_lf_id_rep. 

rww source_inverse_lf_symbol. 
rww target_taut_lf_symbol. rww target_lf_forward. 
rww source_lf_id_rep. rww lf_vertex_taut_lf_symbol. 
rww target_lf_forward. 
rww target_lf_id_rep. rww lf_vertex_inverse_lf_symbol.

rww lf_forward_lf_id_rep. 
rww lf_backward_taut_lf_symbol. rww target_lf_forward.
rww lf_backward_lf_id_rep. rww lf_forward_inverse_lf_symbol.

cp (lf_equiv_make_comp_comp_rep H8). 

assert (lf_make_comp a s (inverse_lf_symbol a (lf_backward u))
(taut_lf_symbol a (lf_forward u)) (lf_id_rep a (lf_vertex u)) = u).
ap lf_symbol_like_extens. 
uf lf_make_comp. ap lf_symbol_like_lf_symbol. 
uh H0; ee. am. 

rww lf_forward_lf_make_comp. 
rww lf_forward_lf_id_rep. 
rww lf_forward_taut_lf_symbol. 
assert (lf_vertex u = target (lf_forward u)). 
rww target_lf_forward. rw H10. app left_id. 
rww ob_target. 

rww lf_backward_lf_make_comp. rww lf_backward_lf_id_rep.
rww lf_backward_inverse_lf_symbol. 
assert  (lf_vertex u = target (lf_backward u)).
tv. rw H10. rww left_id. 

rwi H10 H9. am. 
Qed.


End Left_Fractions.

(** Now we combine everything together to define
the quotient by lf_equiv which is our category of
left fractions. ***)

Module Left_Fraction_Category.
Export Left_Fractions.
Export Associating_Quotient.

Definition lf_symbol_container a s :=
Image.create (Cartesian.product (morphisms a) s)
(fun z => lf_symbol (pr1 z) (pr2 z)).

Lemma inc_lf_symbol_container : forall a s u,
is_lf_symbol a s u -> 
inc u (lf_symbol_container a s).
Proof.
ir. 
uf lf_symbol_container. 
rw Image.inc_rw. 
sh (pair (lf_forward u) (lf_backward u)). 
ee. 
ap product_pair_inc. 
change (is_mor a (lf_forward u)).
ap mor_is_mor. ap mor_lf_forward. 
sh s; am. ap inc_lf_backward. 
sh a; am. 
rw pr1_pair. rw pr2_pair. 
uh H; ee. uh H; ee. sy; am. 
Qed. 

Definition lf_symbol_set a s :=
Z (lf_symbol_container a s) (is_lf_symbol a s).

Lemma inc_lf_symbol_set : forall a s u,
inc u (lf_symbol_set a s) = is_lf_symbol a s u.
Proof.
ir. 
uf lf_symbol_set. 
ap iff_eq; ir. 
Ztac. Ztac. app inc_lf_symbol_container. 
Qed. 

Definition lfc_rqcat a s :=
Category.Notations.create (objects a)
(lf_symbol_set a s) (lf_comp_rep a s) (lf_id_rep a) (structure a).

Lemma is_ob_lfc_rqcat : forall a s x,
has_left_fractions a s -> 
is_ob (lfc_rqcat a s) x = ob a x.
Proof.
ir. uf lfc_rqcat. 
rw is_ob_create. 
ap iff_eq; ir. ap is_ob_ob. lu. am. 
ap ob_is_ob. am. 
Qed.

Lemma is_mor_lfc_rqcat : forall a s u,
has_left_fractions a s -> 
is_mor (lfc_rqcat a s) u = is_lf_symbol a s u.
Proof.
ir. 
uf lfc_rqcat. rw is_mor_create. 
rww inc_lf_symbol_set. 
Qed.

Lemma comp_lfc_rqcat : forall a s u v,
has_left_fractions a s -> 
is_lf_symbol a s u -> 
is_lf_symbol a s v ->
source u = target v -> 
comp (lfc_rqcat a s) u v = lf_comp_rep a s u v.
Proof.
ir. 
uf lfc_rqcat. 
rw comp_create. tv. rww inc_lf_symbol_set. 
rww inc_lf_symbol_set. am. 
Qed.

Lemma id_lfc_rqcat : forall a s x,
has_left_fractions a s -> ob a x ->
id (lfc_rqcat a s) x = lf_id_rep a x.
Proof.
ir. uf lfc_rqcat. 
rw id_create. tv. app ob_is_ob. 
Qed.


Lemma rqcat_lfc_rqcat : forall a s,
has_left_fractions a s -> 
rqcat (lfc_rqcat a s).
Proof.
ir. uhg; ee.
uf lfc_rqcat. 
ap create_like. 
ir. rwi is_mor_lfc_rqcat H0. 
uh H0; ee. 
uh H0; ee. rw H0. 
uf lf_symbol. rww Arrow.create_like. 
am. 

ir. 
rwi is_ob_lfc_rqcat H0. rww is_mor_lfc_rqcat. rww id_lfc_rqcat. 
app is_lf_symbol_lf_id_rep. 
am. 

ir. 
rwi is_ob_lfc_rqcat H0. 
rww id_lfc_rqcat. rww source_lf_id_rep. 
am. 

ir. 
rwi is_ob_lfc_rqcat H0. 
rww id_lfc_rqcat. rww target_lf_id_rep. 
am. 

ir. 
rwi is_mor_lfc_rqcat H0. 
rww is_ob_lfc_rqcat. 
assert (source u = source (lf_forward u)).
rww source_lf_forward. uh H0; ee; am. 
rw H1. rww ob_source. 
ap mor_lf_forward. sh s; am. am. 

ir. 
rwi is_mor_lfc_rqcat H0. 
rww is_ob_lfc_rqcat. 
assert (target u = source (lf_backward u)).
rww source_lf_backward. uh H0; ee; am. 
rw H1. rww ob_source. 
ap mor_lf_backward. sh s; am. am. 

ir. 
rwi is_mor_lfc_rqcat H0. 
rwi is_mor_lfc_rqcat H1. 
rww  is_mor_lfc_rqcat. 
rww comp_lfc_rqcat. 
app is_lf_symbol_lf_comp_rep. am. am. 


ir. 
rwi is_mor_lfc_rqcat H0. 
rwi is_mor_lfc_rqcat H1. 
rww comp_lfc_rqcat. rww source_lf_comp_rep.
am. am. 

ir. 
rwi is_mor_lfc_rqcat H0. 
rwi is_mor_lfc_rqcat H1. 
rww comp_lfc_rqcat. rww target_lf_comp_rep.
am. am. 
Qed. 


Definition lfer a s :=
Z (Cartesian.product (lf_symbol_set a s) (lf_symbol_set a s))
(fun z => lf_equiv a s (pr1 z) (pr2 z)).

Lemma related_lfer : forall a s u v,
has_left_fractions a s -> 
related (lfer a s) u v = lf_equiv a s u v.
Proof.
ir. 
ap iff_eq; ir. 
ufi lfer H0.
uh H0. 
cp (Z_pr H0). 
cbv beta in H1. rwi pr1_pair H1. rwi pr2_pair H1. am. 

uhg. uf lfer. 
ap Z_inc. ap product_pair_inc. 
rw inc_lf_symbol_set. uh H0; ee. 
nin H0. ee. uh H0; ee. am. 
uh H0. nin H0. ee. 
rww inc_lf_symbol_set. uh H1; ee; am. 
rw pr1_pair. rw pr2_pair. am. 
Qed.

Lemma related_lfer_rw : forall a s u v,
has_left_fractions a s ->
related (lfer a s) u v =
(is_lf_symbol a s u & is_lf_symbol a s v &
source u = source v & target u = target v & 
lf_equiv a s u v).
Proof.
ir. ap iff_eq; ir. rwi related_lfer H0.
uh H0. nin H0. ee. 
uh H0; ee; am. uh H1; ee; am. 
uh H0; uh H1; ee. rw H9. sy; am. 
uh H0; uh H1; ee.
rww H5. uhg. sh x; ee; am. am. 
rw related_lfer. ee; am. am. 
Qed. 

Lemma inc_lfer : forall a s x,
has_left_fractions a s -> 
inc x (lfer a s) = 
(is_pair x & (related (lfer a s) (pr1 x) (pr2 x))).
Proof.
ir. ap iff_eq; ir. 
ee. ufi lfer H0. Ztac. 
cp (product_pr H1). ee; am. 
ufi lfer H0. Ztac. 
cp (product_pr H1). ee. 
rw related_lfer. am. am. 
ee. 
uf lfer. ap Z_inc. 
ap product_inc. am. 
rwi related_lfer H1. 
rw inc_lf_symbol_set. uh H1.
nin H1. ee. uh H1; ee; am. am. 
rwi related_lfer H1. 
rw inc_lf_symbol_set. uh H1.
nin H1. ee. uh H2; ee; am. am. 
rwi related_lfer H1. 
am. am. 
Qed. 

Lemma lf_equiv_properties : forall a s u v,
lf_equiv a s u v -> 
(lf_equiv a s u v &
is_lf_symbol a s u & is_lf_symbol a s v &
ob a (source u) & ob a (target u) &
ob a (source v) & ob a (target v) &
source u = source v & target u = target v).
Proof.
ir. dj. 
am. uh H. nin H. ee. uh H; ee; am. 
uh H. nin H. ee. uh H2; ee; am. 
assert (source u = source (lf_forward u)).
rw source_lf_forward. tv. uh H1; ee; am. 
rw H3. rww ob_source. ap mor_lf_forward.
sh s; am. 

assert (target u = source (lf_backward u)).
rw source_lf_backward. tv. uh H1; ee; am. 
rw H4. rww ob_source. ap mor_lf_backward.
sh s; am. 

assert (source v = source (lf_forward v)).
rw source_lf_forward. tv. uh H2; ee; am. 
rw H5. rww ob_source. ap mor_lf_forward.
sh s; am. 

assert (target v = source (lf_backward v)).
rw source_lf_backward. tv. uh H2; ee; am. 
rw H6. rww ob_source. ap mor_lf_backward.
sh s; am. 

uh H. nin H. ee. 
transitivity (source x).

uh H. ee. nin H12. 
ee. wr H14. rww source_lf_extend. 

uh H7. ee. nin H12; ee. 
wr H14. rww source_lf_extend. 

uh H. nin H. ee. 

transitivity (target x).
uh H; ee. nin H13. ee. wr H15. 
rww target_lf_extend. 

uh H8. ee. nin H13. ee. 
wr H15. rww target_lf_extend. 
Qed. 


Lemma lf_ob_target : forall a u,
(exists s, (is_lf_symbol a s u)) -> 
ob a (target u).
Proof.
ir. nin H. 
assert (target u = source (lf_backward u)).
rww source_lf_backward. uh H; ee; am. 
rw H0. rww ob_source. 
ap mor_lf_backward. sh x; am. 
Qed. 

Lemma lf_ob_source : forall a u,
(exists s, (is_lf_symbol a s u)) -> 
ob a (source u).
Proof.
ir. nin H. 
assert (source u = source (lf_forward u)).
rww source_lf_forward. uh H; ee; am. 
rw H0. rww ob_source. 
ap mor_lf_forward. sh x; am. 
Qed. 


Lemma rqcat_equiv_rel_lfer : forall a s,
has_left_fractions a s -> 
rqcat_equiv_rel (lfc_rqcat a s) (lfer a s).
Proof.
ir. 


uhg; ee; ir.

app rqcat_lfc_rqcat. 
ap show_equivalence_relation. 
uhg. ir. 
rwi inc_lfer H0. ee; am. am. 
ir. rwi related_lfer H0. 
rw related_lfer. app lf_equiv_symm. am. am. 

ir. rwi related_lfer H0. rwi related_lfer H1. 
rw related_lfer. 
ap lf_equiv_trans. am. sh y. ee; am. am.
am. am. 

rwi related_lfer_rw H0; try am. ee. 
rw is_mor_lfc_rqcat. am. am. 

rwi related_lfer_rw H0; try am. ee. 
rw is_mor_lfc_rqcat. am. am. 
rwi related_lfer_rw H0; try am. ee.
am. 
rwi related_lfer_rw H0; try am. ee.
am. 

rw related_lfer. ap lf_equiv_refl. am. 
rwi is_mor_lfc_rqcat H0. am. am. 
am. 

rwi related_lfer_rw H0. 
rwi related_lfer_rw H1. ee. 
rw related_lfer. 
rw comp_lfc_rqcat. rw comp_lfc_rqcat. 
ap lf_comp_indep. 
am. am. am. am. am. am. am. wr H8. wrr H5. am. 
am. am. am. am. am. am. 


rwi is_mor_lfc_rqcat H0. 
assert (ob a (target u)). 
ap lf_ob_target. sh s; am. 
rww related_lfer.
rww comp_lfc_rqcat. 
rww id_lfc_rqcat. 
app lf_left_id. 
rww id_lfc_rqcat. 
app is_lf_symbol_lf_id_rep. 
rww id_lfc_rqcat. 
rww source_lf_id_rep. am. 

rwi is_mor_lfc_rqcat H0. 
assert (ob a (source u)).
ap lf_ob_source. sh s; am. 
rww comp_lfc_rqcat. 
rww id_lfc_rqcat. 
rww related_lfer. 
app lf_right_id. 
rww id_lfc_rqcat. 
app is_lf_symbol_lf_id_rep. 
rww id_lfc_rqcat. 
rww target_lf_id_rep. am. 


rwi is_mor_lfc_rqcat H0. 
rwi is_mor_lfc_rqcat H1. 
rwi is_mor_lfc_rqcat H2. 
rww related_lfer. 
rww comp_lfc_rqcat. rww comp_lfc_rqcat. 
rww comp_lfc_rqcat. rww comp_lfc_rqcat. 
app lf_comp_rep_assoc. 
rww comp_lfc_rqcat. 
app is_lf_symbol_lf_comp_rep. 
rww comp_lfc_rqcat. rww target_lf_comp_rep.
rww comp_lfc_rqcat. app is_lf_symbol_lf_comp_rep.
rww comp_lfc_rqcat. rww source_lf_comp_rep. 
am. am. am. 
Qed.

Definition left_frac_cat a s :=
quotient_cat (lfc_rqcat a s) (lfer a s).

Lemma left_frac_cat_axioms : forall a s,
has_left_fractions a s -> 
Category.axioms (left_frac_cat a s). 
Proof.
ir. 
uf left_frac_cat. 
ap rq_quotient_cat_axioms. 
app rqcat_equiv_rel_lfer. 
Qed.


Definition lf_class a s u := arrow_class (lfer a s) u.

Lemma source_lf_class : forall a s u,
source (lf_class a s u) = source u.
Proof.
ir. uf lf_class. rww source_arrow_class.
Qed. 

Lemma target_lf_class : forall a s u,
target (lf_class a s u) = target u.
Proof.
ir. uf lf_class. rww target_arrow_class.
Qed. 

Lemma ob_left_frac_cat : forall a s x,
has_left_fractions a s ->
ob (left_frac_cat a s) x = ob a x.
Proof.
ir. ap iff_eq; ir. 
ufi left_frac_cat H0.
rwi rq_ob_quotient_cat H0. 
rwi is_ob_lfc_rqcat H0. 
am. am. 
app rqcat_equiv_rel_lfer. 

uf left_frac_cat. rw rq_ob_quotient_cat. 
rww is_ob_lfc_rqcat. 
app rqcat_equiv_rel_lfer. 
Qed.

Lemma mor_left_frac_cat : forall a s v,
has_left_fractions a s ->
mor (left_frac_cat a s) v =
(exists u, (is_lf_symbol a s u & v = lf_class a s u)).
Proof.
ir. ap iff_eq; ir. 
ufi left_frac_cat H0.
rwi rq_mor_quotient_cat H0. 
uh H0. 
ee. nin H1; ee. 
sh x. ee. 
rwi is_mor_lfc_rqcat H1. am. am. am. 
app rqcat_equiv_rel_lfer. 
nin H0. 
ee. uf left_frac_cat. 
rw rq_mor_quotient_cat. uhg; ee.
app rqcat_equiv_rel_lfer. 
sh x. ee. rww is_mor_lfc_rqcat. 
am. app rqcat_equiv_rel_lfer. 
Qed.


Lemma comp_left_frac_cat_lf_class : forall a s u v,
has_left_fractions a s ->
is_lf_symbol a s u -> is_lf_symbol a s v ->
source u = target v ->
comp (left_frac_cat a s) (lf_class a s u) (lf_class a s v) =
lf_class a s (lf_comp_rep a s u v).
Proof.
ir. 
uf left_frac_cat. 
rw rq_comp_quotient_cat. 
uf lf_class. 
rw rq_quot_comp_arrow_class. 
rw comp_lfc_rqcat. tv. 
am. am. am. am. 
app rqcat_equiv_rel_lfer. 
rww is_mor_lfc_rqcat. 
rww is_mor_lfc_rqcat. 
am. 
app rqcat_equiv_rel_lfer. 
uhg; ee. 
app rqcat_equiv_rel_lfer. 
sh u. ee. 
rww is_mor_lfc_rqcat. tv. 
uhg; ee. 
app rqcat_equiv_rel_lfer. 
sh v. ee. 
rww is_mor_lfc_rqcat. tv. 
rww source_lf_class. 
rww target_lf_class. 
Qed.

Lemma id_left_frac_cat : forall a s x,
has_left_fractions a s -> ob a x ->
id (left_frac_cat a s) x = lf_class a s (lf_id_rep a x).
Proof.
ir. 
uf left_frac_cat. 
rw rq_id_quotient_cat. 
uf quot_id. rw id_lfc_rqcat. 
reflexivity. am. am. 
app rqcat_equiv_rel_lfer. 
rww is_ob_lfc_rqcat. 
Qed.

Lemma eq_lf_class : forall a s u v,
has_left_fractions a s ->
is_lf_symbol a s u -> is_lf_symbol a s v -> 
(lf_class a s u = lf_class a s v) = (lf_equiv a s u v). 
Proof.
ir. ap iff_eq; ir. 
ufi lf_class H2. 
wr related_lfer. 
rewrite <- rq_arrow_class_eq with (a:= (lfc_rqcat a s)).
am. 
app rqcat_equiv_rel_lfer. 
rww is_mor_lfc_rqcat. am. 

uf lf_class. 
rewrite rq_arrow_class_eq with (a:= (lfc_rqcat a s)).
rww related_lfer. 
app rqcat_equiv_rel_lfer. 
rww is_mor_lfc_rqcat.
Qed.



Definition lf_taut a s u := 
lf_class a s (taut_lf_symbol a u).

Definition lf_inverse a s u := 
lf_class a s (inverse_lf_symbol a u).

Lemma source_lf_taut : forall a s u,
source (lf_taut a s u) = source u.
Proof.
ir. uf lf_taut. 
rw source_lf_class. 
rww source_taut_lf_symbol.  
Qed.

Lemma target_lf_taut : forall a s u,
mor a u -> 
target (lf_taut a s u) = target u.
Proof.
ir. uf lf_taut. 
rw target_lf_class. 
rww target_taut_lf_symbol.  
Qed.

Lemma source_lf_inverse : forall a s u,
mor a u -> 
source (lf_inverse a s u) = target u.
Proof.
ir. uf lf_inverse. 
rw source_lf_class. 
rww source_inverse_lf_symbol.  
Qed.

Lemma target_lf_inverse : forall a s u,
mor a u -> 
target (lf_inverse a s u) = source u.
Proof.
ir. uf lf_inverse. 
rw target_lf_class. 
rww target_inverse_lf_symbol.  
Qed.


Lemma mor_lf_taut : forall a s u,
has_left_fractions a s -> mor a u ->
mor (left_frac_cat a s) (lf_taut a s u).
Proof.
ir. uf left_frac_cat. 
rw rq_mor_quotient_cat. 
uhg; ee. 
app rqcat_equiv_rel_lfer. 
sh (taut_lf_symbol a u). ee. 
rww is_mor_lfc_rqcat. 
app is_lf_symbol_taut_lf_symbol. 
reflexivity. 
app rqcat_equiv_rel_lfer. 
Qed.

Lemma mor_lf_inverse : forall a s u,
has_left_fractions a s -> inc u s -> 
mor (left_frac_cat a s) (lf_inverse a s u).
Proof.
ir. 
assert (mor a u).
ap inc_hlf_mor. sh s; ee; am. 
uf left_frac_cat. 
rw rq_mor_quotient_cat. 
uhg; ee. 
app rqcat_equiv_rel_lfer. 
sh (inverse_lf_symbol a u). ee. 
rww is_mor_lfc_rqcat. 
app is_lf_symbol_inverse_lf_symbol. 
reflexivity. 
app rqcat_equiv_rel_lfer. 
Qed.

Lemma lf_taut_id : forall a s x,
has_left_fractions a s -> ob a x ->  
lf_taut a s (id a x) = id (left_frac_cat a s) x.
Proof.
ir. 
uf left_frac_cat. 
rw rq_id_quotient_cat. 
uf quot_id. 
rw id_lfc_rqcat. 
uf lf_taut. 
rw taut_lf_symbol_id. 
reflexivity. am. am. am. 
app rqcat_equiv_rel_lfer. 
rww is_ob_lfc_rqcat. 
Qed.

Lemma comp_lf_class : forall a s u v,
has_left_fractions a s -> 
is_lf_symbol a s u -> is_lf_symbol a s v ->
source u = target v ->
comp (left_frac_cat a s) (lf_class a s u) (lf_class a s v) =
lf_class a s (lf_comp_rep a s u v).
Proof.
ir. 

assert (related (lfer a s) u (arrow_rep
(lf_class a s u))).
apply rq_related_arrow_rep with (a:= lfc_rqcat a s). 
app rqcat_equiv_rel_lfer. 
rww is_mor_lfc_rqcat. tv. 

assert (related (lfer a s) v (arrow_rep
(lf_class a s v))).
apply rq_related_arrow_rep with (a:= lfc_rqcat a s). 
app rqcat_equiv_rel_lfer. 
rww is_mor_lfc_rqcat. tv. 

rwi related_lfer_rw H3. 
rwi related_lfer_rw H4. 
ee. 



uf left_frac_cat.
rw rq_comp_quotient_cat. 
transitivity (lf_class a s (lf_comp_rep a s 
(arrow_rep (lf_class a s u)) (arrow_rep (lf_class a s v)))).

uf quot_comp. 
rw comp_lfc_rqcat. 
reflexivity. 
am. am. am. wr H10. wr H7. 
am. 

rw eq_lf_class. 
ap lf_comp_indep. 
am. app lf_equiv_symm. 
app lf_equiv_symm. 
wr H10. wrr H7. am. 
ap is_lf_symbol_lf_comp_rep. am. 
am. am. 
wr H10. wrr H7. 
app is_lf_symbol_lf_comp_rep. 
app rqcat_equiv_rel_lfer. 
uf lf_class. 
ap rq_quotient_arrow_arrow_class. 
app rqcat_equiv_rel_lfer. 
rww is_mor_lfc_rqcat. 
uf lf_class. 
ap rq_quotient_arrow_arrow_class. 
app rqcat_equiv_rel_lfer. 
rww is_mor_lfc_rqcat. 
rww source_lf_class. rww target_lf_class. am. am. 
Qed. 

Lemma comp_lf_taut : forall a s u v,
has_left_fractions a s ->
mor a u -> mor a v -> source u = target v ->
comp (left_frac_cat a s) (lf_taut a s u) (lf_taut a s v) =
lf_taut a s (comp a u v).
Proof.
ir. uf lf_taut. 
rw comp_lf_class. 
rww eq_lf_class. 
app comp_taut_lf_symbol. 
ap is_lf_symbol_lf_comp_rep. 
am. 
app is_lf_symbol_taut_lf_symbol. 
app is_lf_symbol_taut_lf_symbol. 
rww source_taut_lf_symbol. 
rww target_taut_lf_symbol. 
app is_lf_symbol_taut_lf_symbol. 
rww mor_comp. am. 
app is_lf_symbol_taut_lf_symbol. 
app is_lf_symbol_taut_lf_symbol. 
rww source_taut_lf_symbol. 
rww target_taut_lf_symbol. 
Qed. 

Lemma are_inverse_lf_taut_lf_inverse : forall a s u,
has_left_fractions a s -> inc u s ->
are_inverse (left_frac_cat a s) (lf_taut a s u) (lf_inverse a s u).
Proof.
ir. 
assert (mor a u).
ap inc_hlf_mor. sh s; ee; am. 

assert (is_lf_symbol a s (taut_lf_symbol a u)).
app is_lf_symbol_taut_lf_symbol. 
assert (is_lf_symbol a s (inverse_lf_symbol a u)).
app is_lf_symbol_inverse_lf_symbol. 
assert (source (taut_lf_symbol a u) = target (inverse_lf_symbol a u)).
rww source_taut_lf_symbol. 
rww target_inverse_lf_symbol. 
assert (source (inverse_lf_symbol a u) = target (taut_lf_symbol a u)).
rw source_inverse_lf_symbol. 
rww target_taut_lf_symbol. am. 



uhg; ee. 
app mor_lf_taut. app mor_lf_inverse. 
rw source_lf_taut. rww target_lf_inverse. 
rw source_lf_inverse. rww target_lf_taut. am. 

transitivity (lf_class a s (lf_comp_rep a s (taut_lf_symbol a u)
(inverse_lf_symbol a u))).
uf lf_taut. uf lf_inverse. 
rw comp_lf_class. reflexivity. 
am. am. am. am. 

rw id_left_frac_cat. 
rw eq_lf_class. 
assert (source (lf_inverse a s u) = target u).
rww source_lf_inverse. rw H6. 
app lf_right_inverse. am. 
ap is_lf_symbol_lf_comp_rep. 
am. am. am. am. 
ap is_lf_symbol_lf_id_rep. 
am. rw source_lf_inverse. rww ob_target. 
am. am. 
rw source_lf_inverse. rww ob_target. am. 

transitivity (lf_class a s (lf_comp_rep a s (inverse_lf_symbol a u)
(taut_lf_symbol a u))).
uf lf_taut. uf lf_inverse. 
rw comp_lf_class. reflexivity. 
am. am. am. am. 

rw id_left_frac_cat. 
rw eq_lf_class. 
assert (source (lf_taut a s u) = source u).
rww source_lf_taut. rw H6. 
app lf_left_inverse. am. 
ap is_lf_symbol_lf_comp_rep. 
am. am. am. am. 
ap is_lf_symbol_lf_id_rep. 
am. rw source_lf_taut. rww ob_source. 
am. 
rw source_lf_taut. rww ob_source. 
Qed.

Lemma is_lf_symbol_arrow_rep : forall a s y,
has_left_fractions a s ->
mor (left_frac_cat a s) y ->
is_lf_symbol a s (arrow_rep y).
Proof.
ir. 
assert (is_mor (lfc_rqcat a s) (arrow_rep y)).
apply rq_mor_arrow_rep with (r := lfer a s). 
ufi left_frac_cat H0. 
rwi rq_mor_quotient_cat H0. am. 
app rqcat_equiv_rel_lfer. 
rwi is_mor_lfc_rqcat H1. am. am. 
Qed.

Lemma lf_class_arrow_rep : forall a s y,
has_left_fractions a s ->
mor (left_frac_cat a s) y ->
lf_class a s (arrow_rep y) = y.
Proof.
ir. 
uf lf_class. 
rewrite rq_arrow_class_arrow_rep with (a:= lfc_rqcat a s). 
tv. 
ufi left_frac_cat H0. 
rwi rq_mor_quotient_cat H0. am. 
app rqcat_equiv_rel_lfer. 
Qed.

Lemma lf_source_arrow_rep : forall y,
(exists a, exists s, (has_left_fractions a s &
mor (left_frac_cat a s) y)) ->
source (arrow_rep y) = source y.
Proof.
ir. 
nin H. nin H. ee. 
cp (lf_class_arrow_rep H H0). 
transitivity (source (lf_class x x0 (arrow_rep y))).
rww source_lf_class. rww H1. 
Qed.

Lemma lf_target_arrow_rep : forall y,
(exists a, exists s, (has_left_fractions a s &
mor (left_frac_cat a s) y)) ->
target (arrow_rep y) = target y.
Proof.
ir. 
nin H. nin H. ee. 
cp (lf_class_arrow_rep H H0). 
transitivity (target (lf_class x x0 (arrow_rep y))).
rww target_lf_class. rww H1. 
Qed.

Lemma comp_etc_arrow_rep : forall a s y,
has_left_fractions a s -> 
mor (left_frac_cat a s) y ->
comp (left_frac_cat a s) 
(lf_inverse a s (lf_backward (arrow_rep y)))
(lf_taut a s (lf_forward (arrow_rep y))) = y.
Proof.
ir. 
transitivity (lf_class a s (arrow_rep y)).
set (k:= arrow_rep y).
assert (is_lf_symbol a s k).
uf k. 
ap is_lf_symbol_arrow_rep. 
am. am. 
assert (mor a (lf_forward k)).
ap mor_lf_forward. sh s; am. 
assert (mor a (lf_backward k)).
ap mor_lf_backward. sh s; am. 
assert (inc (lf_backward k) s).
ap inc_lf_backward. sh a; am. 

uf lf_inverse. uf lf_taut.
rw comp_lf_class. 
rw eq_lf_class.
app lf_equiv_symm.
ap lf_symbol_equiv. am.
am. am. 
ap is_lf_symbol_lf_comp_rep. 
am. ap is_lf_symbol_inverse_lf_symbol.
am. ap inc_lf_backward. sh a; am. 
ap is_lf_symbol_taut_lf_symbol. 
am. ap  mor_lf_forward. sh s; am. 
rw source_inverse_lf_symbol. 
rw target_taut_lf_symbol. 
rww target_lf_forward.
sh a; sh s; am. am. am. am. am. 
ap is_lf_symbol_inverse_lf_symbol.
am. ap inc_lf_backward. sh a; am. 
ap is_lf_symbol_taut_lf_symbol. 
am. ap  mor_lf_forward. sh s; am. 
rw source_inverse_lf_symbol. 
rw target_taut_lf_symbol. 
rww target_lf_forward.
sh a; sh s; am. am. am. 

ap lf_class_arrow_rep. am. am. 
Qed.

Lemma comp_etc_lf_symbol : forall a s k,
has_left_fractions a s -> 
is_lf_symbol a s k ->
comp (left_frac_cat a s) 
(lf_inverse a s (lf_backward k))
(lf_taut a s (lf_forward k)) = lf_class a s k.
Proof.
ir. 

assert (mor a (lf_forward k)).
ap mor_lf_forward. sh s; am. 
assert (mor a (lf_backward k)).
ap mor_lf_backward. sh s; am. 
assert (inc (lf_backward k) s).
ap inc_lf_backward. sh a; am. 

uf lf_inverse. uf lf_taut.
rw comp_lf_class. 
rw eq_lf_class.
app lf_equiv_symm.
ap lf_symbol_equiv. am.
am. am. 
ap is_lf_symbol_lf_comp_rep. 
am. ap is_lf_symbol_inverse_lf_symbol.
am. ap inc_lf_backward. sh a; am. 
ap is_lf_symbol_taut_lf_symbol. 
am. ap  mor_lf_forward. sh s; am. 
rw source_inverse_lf_symbol. 
rw target_taut_lf_symbol. 
rww target_lf_forward.
sh a; sh s; am. am. am. am. am. 
ap is_lf_symbol_inverse_lf_symbol.
am. ap inc_lf_backward. sh a; am. 
ap is_lf_symbol_taut_lf_symbol. 
am. ap  mor_lf_forward. sh s; am. 
rw source_inverse_lf_symbol. 
rw target_taut_lf_symbol. 
rww target_lf_forward.
sh a; sh s; am. am. am. 
Qed.

Lemma lfc_mor_expression : forall a s y,
has_left_fractions a s ->
mor (left_frac_cat a s) y ->
(exists u, exists v, (mor a u & inc v s & target u = target v &
y = comp  (left_frac_cat a s) (lf_inverse a s v) (lf_taut a s u))).
Proof.
ir. 
cp (is_lf_symbol_arrow_rep H H0).


sh (lf_forward (arrow_rep y)).
sh (lf_backward (arrow_rep y)).
ee. 
ap mor_lf_forward. 
sh s; am. 
ap inc_lf_backward. sh a; am. 
rww target_lf_forward. 
sh a; sh s; am. 
sy; ap comp_etc_arrow_rep. am. am. 
Qed.


(** Now we define the projection functor from [a] to
[left_frac_cat a s]. It turns out that it is
easier to do this directly than to use the
stuff about [qfunctor] at the end of the 
[Associating_Quotient] module above. **)

Definition lf_proj a s := 
Functor.create a (left_frac_cat a s) (lf_taut a s).

Lemma source_lf_proj : forall a s,
source (lf_proj a s) = a.
Proof.
ir. uf lf_proj. 
rw Functor.source_create. tv. 
Qed.

Lemma target_lf_proj : forall a s,
target (lf_proj a s) = (left_frac_cat a s).
Proof.
ir. uf lf_proj. 
rw Functor.target_create. tv. 
Qed.

Lemma lf_proj_property : forall a s,
has_left_fractions a s ->
Functor.property a (left_frac_cat a s) (fun (x:E)=> x)
(lf_taut a s).
Proof.
ir. 
uhg; ee; ir.
lu. 
app left_frac_cat_axioms. 
rww ob_left_frac_cat. 
rww lf_taut_id. 
app mor_lf_taut. 
rww source_lf_taut. 
rww target_lf_taut. 
rww comp_lf_taut. 
Qed. 

Lemma lf_proj_axioms : forall a s,
has_left_fractions a s -> 
Functor.axioms (lf_proj a s).
Proof.
ir. uf lf_proj. ap Functor.create_axioms. 
sh (fun (x:E)=> x).
ap lf_proj_property. am. 
Qed. 

Lemma fob_lf_proj : forall a s x,
has_left_fractions a s -> ob a x ->
fob (lf_proj a s) x = x.
Proof.
ir. 
cp (lf_proj_property H).
exact (fob_property_create H1 H0).  
Qed. 

Lemma fmor_lf_proj : forall a s y,
has_left_fractions a s -> mor a y ->
fmor (lf_proj a s) y = lf_taut a s y.
Proof.
ir. 
uf lf_proj. 
rw Functor.fmor_create. tv. am. 
Qed. 

Lemma invertible_fmor_lf_proj : forall a s y,
has_left_fractions a s -> inc y s ->
invertible (left_frac_cat a s) (fmor (lf_proj a s) y).
Proof.
ir. 
uhg. sh (lf_inverse a s y).
rw fmor_lf_proj. 

app are_inverse_lf_taut_lf_inverse.
am. ap inc_hlf_mor. sh s; ee; am. 
Qed.

Lemma inverse_fmor_lf_proj : forall a s y,
has_left_fractions a s -> inc y s ->
inverse (left_frac_cat a s) (fmor (lf_proj a s) y) =
lf_inverse a s y.
Proof.
ir. 
ap inverse_eq. 
rww fmor_lf_proj. app are_inverse_lf_taut_lf_inverse.
ap inc_hlf_mor. sh s; ee; am. 
Qed.

(** Next we define a functor [lf_dotted] whenever
we have a functor [f] with [source f = a] such 
that [fmor f y] is invertible when [inc y s]. This
is to get the universal property of [left_frac_cat]. **)

Definition lf_dotted_situation a s f :=
has_left_fractions a s &
Functor.axioms f &
source f = a &
(forall y, inc y s -> invertible (target f) (fmor f y)).

Definition lf_symb_dot_situation a s f u :=
lf_dotted_situation a s f &
is_lf_symbol a s u.

Definition lf_symb_dot_facts a s f u:=
lf_symb_dot_situation a s f u &
is_lf_symbol a s u &
lf_dotted_situation a s f &
has_left_fractions a s &
Functor.axioms f &
source f = a &
(forall y, inc y s -> invertible (target f) (fmor f y)) &
mor (source f) (lf_forward u) &
mor (source f) (lf_backward u) &
inc (lf_backward u) s &
mor (target f) (fmor f (lf_forward u)) &
mor (target f) (fmor f (lf_backward u)) &
lf_symbol_like u &
source (fmor f (lf_forward u)) = fob f (source u) &
source (fmor f (lf_backward u)) = fob f (target u) &
target (fmor f (lf_forward u)) = fob f (lf_vertex u) &
target (fmor f (lf_backward u)) = fob f (lf_vertex u) &
invertible (target f) (fmor f (lf_backward u)) &
mor (target f) (inverse (target f) (fmor f (lf_backward u))) &
source (inverse (target f) (fmor f (lf_backward u))) = 
fob f (lf_vertex u).

Lemma lf_symb_dot_situation_rw : forall a s f u,
lf_symb_dot_situation a s f u = lf_symb_dot_facts a s f u.
Proof.
ir. 
ap iff_eq; ir. 
uhg; dj.
am. 
uh H0; ee; am. uh H0; ee; am. 
uh H2; ee; am. uh H2; ee; am. 
uh H2; ee; am. uh H2; ee; au. 
ap mor_lf_forward. sh s. rww H5. 
ap mor_lf_backward. sh s. rww H5. 
ap inc_lf_backward. sh a; am. 
app mor_fmor. app mor_fmor.
uh H1; ee; am. 
rww source_fmor. rww source_lf_forward.
rww source_fmor. rww source_lf_backward.
rww target_fmor. 
rw target_lf_forward. tv. sh a; sh s; am.
rw target_fmor. rw target_lf_backward. tv. 
am. am. ap H6. am. 
ap mor_inverse. am. 
rw source_inverse. am. am. 

uh H; ee; am. 
Qed.




Definition lf_symb_dot (a s:E) f u :=
comp (target f) 
(inverse (target f) (fmor f (lf_backward u))) 
(fmor f (lf_forward u)).

Lemma source_lf_symb_dot : forall a s f u,
lf_symb_dot_situation a s f u ->
source (lf_symb_dot a s f u) = fob f (source u).
Proof.
ir. 
rwi lf_symb_dot_situation_rw H. 
uh H; ee.
uf lf_symb_dot.
rww source_comp. 
rww source_inverse. 
rww H14. 
Qed.

Lemma target_lf_symb_dot : forall a s f u,
lf_symb_dot_situation a s f u -> 
target (lf_symb_dot a s f u) = fob f (target u).
Proof.
ir. 
rwi lf_symb_dot_situation_rw H. 
uh H; ee.
uf lf_symb_dot.
rw target_comp. 
rww target_inverse. 
am. am. 
rww source_inverse. 
rww H14. 
Qed.

Lemma mor_lf_symb_dot : forall a s f u,
lf_symb_dot_situation a s f u -> 
mor (target f) (lf_symb_dot a s f u).
Proof.
ir. 
rwi lf_symb_dot_situation_rw H. 
uh H; ee.
uf lf_symb_dot. 
rww mor_comp. 
rww source_inverse. 
rww H14. 
Qed.

Lemma lf_symb_dot_beyond_invariant : forall a s f u v,
lf_symb_dot_situation a s f u ->
lf_beyond a s u v -> 
lf_symb_dot a s f u = lf_symb_dot a s f v.
Proof.
ir. 
rwi lf_symb_dot_situation_rw H. 
uh H; uh H0; ee.
nin H5. 
ee. 

uf lf_symb_dot. 


assert (fmor f (lf_forward v) = 
comp (target f) (fmor f x) (fmor f (lf_forward u))).
transitivity (fmor f (comp (source f) x (lf_forward u))).
ap uneq. wr H26.
rww lf_forward_lf_extend. rww H10. 
rww fmor_comp. rww H10. 
rww target_lf_forward. sh a; sh s; am. 

assert (fmor f (lf_backward v) = 
comp (target f) (fmor f x) (fmor f (lf_backward u))).
transitivity (fmor f (comp (source f) x (lf_backward u))).
ap uneq. wr H26.
rww lf_backward_lf_extend. rww H10. 
rww fmor_comp. rww H10. 

assert (target x = lf_vertex v).
wr H26. rww lf_vertex_lf_extend. 

assert (mor (source f) x).
rww H10. 


assert (fmor f x = comp (target f)
(fmor f (lf_backward v)) 
(inverse (target f) (fmor f (lf_backward u)))).
rw H28. 
rw assoc. rw right_inverse. 
assert (target (fmor f (lf_backward u)) = 
source (fmor f x)).
rw H21. rw source_fmor. rww H25. 
am. am. 
rw H31. rww right_id. rww source_fmor. 
app ob_fob. rw H25. rw H10. ap ob_lf_vertex. 
sh s; am. app mor_fmor. 
am. app mor_fmor. 
am. am. 
rww source_fmor. rw H21. rww H25. 
rww target_inverse. tv. 

rw H27. rw H31.
set (c:= fmor f (lf_forward u)).
set (d:= fmor f (lf_backward u)).
set (e:= fmor f (lf_backward v)).
set (b:= target f).

assert (mor b c).
am. 
 
assert (mor b d).
am. 

assert (mor b e).
uf e; uf b. app mor_fmor. 
rw H10. ap mor_lf_backward. sh s; am. 

assert (invertible b d).
am. 

assert (invertible b e).
uf b; uf e. 
ap H11. ap inc_lf_backward. sh a; am. 

assert (target d = target c).
uf c; uf d. rw H20. am. 

assert (source e = source d).
uf e; uf d. rw source_fmor.
rw source_fmor. ap uneq. 
rw source_lf_backward. rw source_lf_backward. sy; am. 
am. uh H2; ee; am. am. rw H10. 
ap mor_lf_backward. sh s; am. am. 
rw H10. ap mor_lf_backward. sh s; am. 

assert (mor b (inverse b d)).
app mor_inverse. 
assert (mor b (inverse b e)).
app mor_inverse. 

rw assoc. 
wr assoc. 
rw left_inverse. 
rw left_id. reflexivity. 
rww ob_source. 
rww mor_comp. 
rww source_inverse. 
rww target_comp. rww target_inverse. sy; am. 
rww source_inverse. tv. am. am. am. 
rww mor_comp. rww source_inverse. 
rww source_inverse. rww target_comp. rww target_inverse. 
rww source_inverse. tv. am. 
app mor_inverse. am. rww target_inverse. rww source_inverse.
tv. 
Qed.


Lemma lf_symb_dot_equiv_invariant : forall a s f u v,
lf_symb_dot_situation a s f u ->
lf_equiv a s u v -> 
lf_symb_dot a s f u = lf_symb_dot a s f v.
Proof.
ir. uh H0; ee. 
nin H0. ee. 
transitivity (lf_symb_dot a s f x).
ap lf_symb_dot_beyond_invariant. am. am. 
sy. ap lf_symb_dot_beyond_invariant. 
uhg; ee. lu. uh H1. ee; am. am. 
Qed.


Lemma lf_symb_dot_make_comp : forall a s f u v w,
lf_symb_dot_situation a s f u ->
lf_symb_dot_situation a s f v ->
fills_in a s u v w ->
lf_symb_dot a s f (lf_make_comp a s u v w) =
comp (target f) (lf_symb_dot a s f u) (lf_symb_dot a s f v).
Proof.
ir. 

uf lf_symb_dot. 
rw lf_backward_lf_make_comp. rw lf_forward_lf_make_comp.
assert (lem1 : source u = target v).
uh H1; ee. am. 
assert (lf_symb_dot_situation a s f w).
uhg; ee. 
lu. uh H1; ee; am. 


assert (a = source f & mor (source f) (lf_backward w) &
mor (source f) (lf_backward u) & 
source (lf_backward w) = target (lf_backward u) &
mor (source f) (lf_forward w) & mor (source f) (lf_forward v) &
source (lf_forward w) = target (lf_forward v)).
uh H; uh H0; uh H2. dj; ee. 
uh H2; ee. sy; am. wr H3. ap mor_lf_backward. 
sh s. am. wr H3; ap mor_lf_backward. sh s; am. 
rw source_lf_backward. rw target_lf_backward. 
uh H1; ee; am. uh H6; ee; am. 
ap mor_lf_forward. wr H3; sh s; am. 
ap mor_lf_forward. wr H3; sh s; am. 
rw source_lf_forward. rw target_lf_forward.
uh H1; ee; am. sh a; sh s; am. uh H9; ee; am. 

ee. 
rw H3. 
rww fmor_comp. rww fmor_comp. 

set (c:= fmor f (lf_forward v)).
set (d:= fmor f (lf_backward v)).
set (e := fmor f (lf_forward u )).
set (g := fmor f (lf_backward u)).
set (h:= fmor f (lf_forward w)).
set (k:= fmor f (lf_backward w)).
set (b:= target f).

assert (mor b c & mor b d & mor b e & mor b g &
mor b h & mor b k & invertible b d & invertible b g &
invertible b k & 
target d = target c & target e = target g &
source d = source e & source h = target c &
source h = target d & source k = target e &
source k = target g & target h = target k &
comp b h d = comp b k e).




rwi lf_symb_dot_situation_rw H;
rwi lf_symb_dot_situation_rw H0; 
rwi lf_symb_dot_situation_rw H2; 
uh H; uh H0; uh H2; ee; try am. 

uf d; uf c.  rw target_fmor. rw target_fmor. 
ap uneq. rw target_lf_backward. rw target_lf_forward.
tv. sh a; sh s; am. am. am. am. am. 

(** To get the numbers easily in the following it
is best to draw a diagram and write down which rewrite
hypothesis numbers go with each end of each arrow. **)

uf e; uf g. rw H62; rw H63. reflexivity. 
uf d; uf e. rw H42. rw H60. app uneq. 
sy; am. 
uf h; uf c. rw H22. rw H43. ap uneq. uh H1; ee; am. 
uf h; uf d. rw H22. rw H44. ap uneq. uh H1; ee; am. 
uf k; uf e. rw H23. rw H62. ap uneq. uh H1; ee; am.
uf k; uf g. rw H23. rw H63. ap uneq. uh H1; ee; am. 
uf h; uf k. rw H24; rw H25. reflexivity. 
uf b; uf h; uf d; uf k; uf e.
rw comp_fmor. rw comp_fmor.
ap uneq. wr H3. uh H1; ee; am. am. 
am. am. rw source_lf_backward. rw target_lf_forward.
uh H1; ee; am. sh a; sh s; am. 
am. am. 
am. am. 
rw source_lf_forward. rw target_lf_backward. uh H1; ee; am. 
am. 



(** Now we get to our main diagram chase, but
the notation has been simplified by all of the above. **)

ee. 

rw assoc. rw inverse_comp. rw assoc. 
ap uneq. 
wr assoc. wr assoc. 

assert (comp b (inverse b k) h = comp b e (inverse b d)).
transitivity (comp b (comp b (inverse b k) h) (comp b d (inverse b d))).
rw right_inverse. 
rw right_id. tv. rww ob_target. 
rww mor_comp. app mor_inverse. rww source_inverse.
sy; am. 
rww source_comp. app mor_inverse. rww source_inverse. 
sy; am. tv. am. 
assert (e = comp b (inverse b k) (comp b h d)).
rw H27. wr assoc. rw left_inverse. 
rw left_id. tv. rww ob_source. am. sy; am. tv. 
am. app mor_inverse. am. am. rww source_inverse. 
am. tv. 

rw H28. rw assoc. rw assoc. ap uneq. 
sy; ap assoc. am. am. app mor_inverse. 
am. rww target_inverse. tv. 
app mor_inverse. rww mor_comp. app mor_inverse. 
rww source_inverse. rww target_comp. 
sy; am. rww source_comp. rww target_inverse. 
tv. app mor_inverse. am. rww mor_comp. 
app mor_inverse. 
rww target_inverse. rww source_inverse. 
sy; am. rww target_comp. app mor_inverse. 
rww target_inverse. tv. 

rww H28. am. app mor_inverse. am. 
rww target_inverse. sy; am. rww source_inverse. tv. 
app mor_inverse. am. am. rww source_inverse. 
sy; am. am. tv. app mor_inverse. app mor_inverse. 
rww mor_comp. 
rww source_inverse. sy; rww target_inverse. 
rww source_inverse. rww target_comp. 
sy; am. tv. 
uhg; ee. uf b. rww category_axioms_target. 
lu. uhg; ee. app mor_is_mor. 
app mor_is_mor. am. am. am. 
app mor_inverse. am. 
rww mor_comp. app mor_inverse. rww source_inverse.
rww source_inverse. sy; am. 
rww target_comp. rww target_inverse. sy; am. 
app mor_inverse. rww source_inverse. tv. 
lu. lu.    
Qed.

Lemma lf_symb_dot_comp_rep : forall a s f u v,
lf_symb_dot_situation a s f u ->
lf_symb_dot_situation a s f v ->
source u = target v -> 
lf_symb_dot a s f (lf_comp_rep a s u v) =
comp (target f) (lf_symb_dot a s f u) (lf_symb_dot a s f v).
Proof.
ir. 
uf lf_comp_rep. 
ap lf_symb_dot_make_comp. 
am. am. 
app fills_in_lf_filler. uh H; ee. uh H; ee; am.
uh H; ee; am. uh H0; ee; am. 
Qed.

Lemma lf_symb_dot_id_rep : forall a s f x,
lf_dotted_situation a s f ->
ob a x ->
lf_symb_dot a s f (lf_id_rep a x) = id (target f) (fob f x).
Proof.
ir. 
uh H; ee. 
uf lf_symb_dot. 

rw lf_backward_lf_id_rep. 
rw lf_forward_lf_id_rep. 
rw fmor_id. 
rw left_inverse. 
rw source_id. tv. 
app  ob_fob. rww H2. 
uhg. sh (id (target f) (fob f x)).

assert (ob (target f) (fob f x)).
app ob_fob. rww H2. 
uhg; ee. ap mor_id. 
am. 
app mor_id. 
rww source_id. rww target_id. 
rww source_id. rww target_id. 
rww left_id. 
rww source_id. app mor_id. 
rww target_id. 
rww left_id. rww source_id. 
app mor_id. rww target_id. am. am. am. 
Qed.



Definition lf_dotted a s f :=
Functor.create (left_frac_cat a s) (target f) 
(fun u => lf_symb_dot a s f (arrow_rep u)).

Lemma source_lf_dotted : forall a s f,
source (lf_dotted a s f) = left_frac_cat a s.
Proof.
ir. uf lf_dotted. rww Functor.source_create. 
Qed. 

Lemma target_lf_dotted : forall a s f,
target (lf_dotted a s f) = target f.
Proof.
ir. uf lf_dotted. rww Functor.target_create. 
Qed.

Lemma lf_equiv_arrow_rep_lf_class : forall a s u,
has_left_fractions a s -> 
is_lf_symbol a s u -> 
lf_equiv a s u (arrow_rep (lf_class a s u)).
Proof.
ir. 
uf lf_class. 
wr related_lfer. 
apply rq_related_arrow_rep_arrow_class with (lfc_rqcat a s). 
app rqcat_equiv_rel_lfer. 
rww is_mor_lfc_rqcat. am. 
Qed. 

Lemma lf_dotted_property : forall a s f,
lf_dotted_situation a s f -> 
Functor.property (left_frac_cat a s) (target f)
(fob f) (fun u => lf_symb_dot a s f (arrow_rep u)).
Proof.
ir. 
uh H; ee. 
uhg; ee; ir. 
app left_frac_cat_axioms. 
rww category_axioms_target. 
rwi ob_left_frac_cat H3. 
app ob_fob. rww H1. am. 


transitivity (lf_symb_dot a s f (lf_id_rep a x)).
rww lf_symb_dot_id_rep. uhg; ee; am. 
rwi ob_left_frac_cat H3. am. am. 

ap lf_symb_dot_equiv_invariant. 
uhg; ee. uhg; ee; am. 
app is_lf_symbol_lf_id_rep. 
rwi ob_left_frac_cat H3. am. am. 

rw id_left_frac_cat. 
app lf_equiv_arrow_rep_lf_class. 
app is_lf_symbol_lf_id_rep. 
rwi ob_left_frac_cat H3. am. am. am. 
rwi ob_left_frac_cat H3. am. am. 

ap mor_lf_symb_dot. 
uhg; ee. uhg; ee; am. 
ap is_lf_symbol_arrow_rep. am. am. 
rw source_lf_symb_dot. 
rewrite rq_source_arrow_rep with 
(a:=lfc_rqcat a s) (r:=lfer a s). tv.
ufi left_frac_cat H3. 
rwi rq_mor_quotient_cat H3. am. 
app rqcat_equiv_rel_lfer. 

uhg; ee. uhg; ee; am. 
ap is_lf_symbol_arrow_rep. am. am. 

rw target_lf_symb_dot. 
rewrite rq_target_arrow_rep with 
(a:=lfc_rqcat a s) (r:=lfer a s). tv.
ufi left_frac_cat H3. 
rwi rq_mor_quotient_cat H3. am. 
app rqcat_equiv_rel_lfer. 

uhg; ee. uhg; ee; am. 
ap is_lf_symbol_arrow_rep. am. am. 

set (p:= arrow_rep u).
set (q:= arrow_rep v).
assert (lf_symb_dot_situation a s f p).
uhg; ee. uhg; ee; am. 
uf p. app is_lf_symbol_arrow_rep. 
assert (lf_symb_dot_situation a s f q).
uhg; ee. uhg; ee; am. 
uf q. app is_lf_symbol_arrow_rep. 

assert (source p = target q).
uf p; uf q. 
rewrite rq_source_arrow_rep with 
(a:=lfc_rqcat a s) (r:=lfer a s). 
rewrite rq_target_arrow_rep with 
(a:=lfc_rqcat a s) (r:=lfer a s). am. 
ufi left_frac_cat H4. 
rwi rq_mor_quotient_cat H4. am. 
app rqcat_equiv_rel_lfer. 
ufi left_frac_cat H3. 
rwi rq_mor_quotient_cat H3. am. 
app rqcat_equiv_rel_lfer. 

transitivity (lf_symb_dot a s f (lf_comp_rep a s p q)).
sy; app lf_symb_dot_comp_rep . 

assert (u = lf_class a s p).
uf p. rw lf_class_arrow_rep. tv. am. 
am. 
assert (v = lf_class a s q).
uf q. rw lf_class_arrow_rep. tv. am. 
am. 

rw H9; rw H10. 

rw comp_lf_class. 
ap lf_symb_dot_equiv_invariant. 
uhg; ee. uhg; ee; am. 
ap is_lf_symbol_lf_comp_rep. am. uh H6; ee; am. 
uh H7; ee; am. am. 
ap lf_equiv_arrow_rep_lf_class. am. 
app is_lf_symbol_lf_comp_rep. uh H6; ee; am. 
uh H7; ee; am. am. uh H6; ee; am. 
uh H7; ee; am. am. 
Qed.

Lemma lf_dotted_axioms : forall a s f,
lf_dotted_situation a s f ->
Functor.axioms (lf_dotted a s f).
Proof.
ir. 
uf lf_dotted. 
ap Functor.create_axioms. 
sh (fob f). 
ap lf_dotted_property. 
am. 
Qed.


Lemma fob_lf_dotted : forall a s f x,
lf_dotted_situation a s f -> 
ob a x ->
fob (lf_dotted a s f) x = fob f x.
Proof.
ir. 
uf lf_dotted. 
ap fob_property_create. 
app lf_dotted_property. 
rww ob_left_frac_cat. uh H; ee; am. 
Qed. 

Lemma fmor_lf_dotted : forall a s f u,
mor (left_frac_cat a s) u -> 
fmor (lf_dotted a s f) u = lf_symb_dot a s f (arrow_rep u).
Proof.
ir.
uf lf_dotted. 
rww fmor_create. 
Qed.

Lemma fmor_lf_dotted_lf_class : forall a s f u,
lf_dotted_situation a s f ->
is_lf_symbol a s u ->
fmor (lf_dotted a s f) (lf_class a s u) = lf_symb_dot a s f u.
Proof.
ir. 
rw fmor_lf_dotted. 
ap lf_symb_dot_equiv_invariant.
uhg; ee.
am. 
ap is_lf_symbol_arrow_rep. uh H; ee; am.
rw mor_left_frac_cat. sh u. 
ee. am. tv. uh H; ee; am. 
ap lf_equiv_symm. 
ap lf_equiv_arrow_rep_lf_class. uh H; ee; am. am.

rw mor_left_frac_cat. sh u. ee. 
am. tv. uh H; ee; am. 
Qed.

(** For some reason these useful lemmas aren't in
the category theory file; they need to be put there. **)



Lemma fmor_lf_dotted_lf_taut : forall a s f y,
lf_dotted_situation a s f ->
mor a y -> 
fmor (lf_dotted a s f) (lf_taut a s y) = fmor f y.
Proof.
ir. 
uf lf_taut. 
cp H. 
uh H1; ee. 
cp H0. wri H3 H5. 
rw fmor_lf_dotted_lf_class. 

uf lf_symb_dot. 
rw lf_backward_taut_lf_symbol.
rw fmor_id. 
rw lf_forward_taut_lf_symbol. 
rw inverse_id. 
rw left_id. tv. app ob_fob. 
rww ob_target. 
app mor_fmor. 
rww target_fmor. tv. tv. 
app  ob_fob. rww ob_target.
am. am. rww ob_target.
am. 
ap is_lf_symbol_taut_lf_symbol. am. am. 
Qed.


Lemma fmor_lf_dotted_lf_inverse : forall a s f y,
lf_dotted_situation a s f ->
inc y s -> 
fmor (lf_dotted a s f) (lf_inverse a s y) = 
inverse (target f) (fmor f y).
Proof.
ir. 
uf lf_inverse. 
cp H. 
uh H1; ee. 
assert (mor a y).
ap inc_hlf_mor. sh s; ee; am. 
cp H5. wri H3 H5. 
rww fmor_lf_dotted_lf_class. 

assert (invertible (target f) (fmor f y)).
au. 

uf lf_symb_dot.
rw lf_backward_inverse_lf_symbol.
rw lf_forward_inverse_lf_symbol.
rw fmor_id. 
rw right_id. tv. 
app ob_fob. rww ob_target. 
app mor_inverse. rww source_inverse. 
rww target_fmor. tv. am. am. 
rww ob_target. 
app is_lf_symbol_inverse_lf_symbol.
Qed.

(** The following lemma shows that [lf_dotted a s f]
solves the problem of giving a functor which 
when composed with [lf_proj a s] yields [f]. **)

Lemma fcompose_lf_dotted_lf_proj : forall a s f,
lf_dotted_situation a s f ->
fcompose (lf_dotted a s f) (lf_proj a s) = f.
Proof.
ir. cp H. uh H0; ee.

ap Functor.axioms_extensionality.
ap fcompose_axioms. 
app lf_dotted_axioms. app lf_proj_axioms. 
rww source_lf_dotted. rww target_lf_proj.
am. rww source_fcompose. rww source_lf_proj.
sy; am. rww target_fcompose. 
rww target_lf_dotted. 

ir. 
rwi source_fcompose H4. 
rwi source_lf_proj H4. 

rw fmor_fcompose. 
rw fmor_lf_proj. 
rw fmor_lf_dotted_lf_taut. tv. am. am. 
am. am. 
app lf_dotted_axioms. 
app lf_proj_axioms. 
rww source_lf_dotted. rww target_lf_proj. 
rww source_lf_proj. 
Qed.

(** The following lemma shows that the solution to the
universal problem  posed above is unique. **)

Lemma lf_dotted_like_unique : forall a s g h,
has_left_fractions a s ->
Functor.axioms g -> Functor.axioms h ->
source g = left_frac_cat a s ->
source h = left_frac_cat a s ->
(fcompose g (lf_proj a s) = fcompose h (lf_proj a s)) ->
g = h.
Proof.
ir. 
assert (target g = target h).
transitivity (target (fcompose g (lf_proj a s))).
rww target_fcompose. rw H4. 
rww target_fcompose. 

ap Functor.axioms_extensionality.
am. am. rww H3. am. 

assert (forall y, mor a y -> 
fmor g (lf_taut a s y) = fmor h (lf_taut a s y)).
ir. 
wr fmor_lf_proj. 
wr fmor_fcompose. 
rw H4. rw fmor_fcompose. tv. am. 
app lf_proj_axioms. rww target_lf_proj. 
rww source_lf_proj. am. 
app lf_proj_axioms. rww target_lf_proj. 
rww source_lf_proj. am. am. 


assert (forall y, inc y s -> 
fmor g (lf_inverse a s y) = fmor h (lf_inverse a s y)).
ir. 
assert (mor a y).
ap inc_hlf_mor. sh s; ee; am. 

wr inverse_fmor_lf_proj. 
rw fmor_inverse. 
rw fmor_inverse. rww H5. 
ap uneq. rw fmor_lf_proj. 
au. am. am. am. 
rw H3. ap invertible_fmor_lf_proj. am. am. am. am. 
rw H2. ap invertible_fmor_lf_proj. am. am. am. am. 
am. 


ir. rwi H2 H8. 
cp (lfc_mor_expression H H8).
nin H9. nin H9. ee. 
rw H12. 

rw fmor_comp. rw fmor_comp. 
rw H7. 
rw H6. rww H5. 
am. am. am. am. 
ap mor_lf_inverse. 
am. am. ap mor_lf_taut. am. am. 
rww source_lf_inverse. rww target_lf_taut. sy; am. 
ap inc_hlf_mor. 
sh s. ee; am. am. am. 
ap mor_lf_inverse. am. am. 
ap mor_lf_taut. am. am. 
rww source_lf_inverse. rww target_lf_taut. sy; am. 
ap inc_hlf_mor. sh s. 
ee; am. 
Qed.


End Left_Fraction_Category.