Set Implicit Arguments. Unset Strict Implicit. Require Export gzdef1. Module Associating_Quotient. Export Quotient_Category. (** We need a notion of taking the quotient of an object which is like a category but isn't associative or left and right unitary. This is to apply to the left and right fraction constructions of localizations. The first task is therefore to divide up category axioms into two parts; the first part called rqcat is for ``pre-quotient cat''. *) Definition rqcat a := Category.Notations.like a & (forall u, is_mor a u -> Arrow.like u) & (forall x, is_ob a x -> is_mor a (id a x)) & (forall x, is_ob a x -> source (id a x) = x) & (forall x, is_ob a x -> target (id a x) = x) & (forall u, is_mor a u -> is_ob a (source u)) & (forall u, is_mor a u -> is_ob a (target u)) & (forall u v, is_mor a u -> is_mor a v -> source u = target v -> is_mor a (comp a u v)) & (forall u v, is_mor a u -> is_mor a v -> source u = target v -> source (comp a u v) = source v) & (forall u v, is_mor a u -> is_mor a v -> source u = target v -> target (comp a u v) = target u). Lemma rq_is_ob_source : forall a u, rqcat a -> is_mor a u -> is_ob a (source u). Proof. ir. uh H; ee. au. Qed. Lemma rq_is_ob_target : forall a u, rqcat a -> is_mor a u -> is_ob a (target u). Proof. ir. uh H; ee. au. Qed. Lemma rq_is_mor_id : forall a x, rqcat a -> is_ob a x -> is_mor a (id a x). Proof. ir. uh H; ee. au. Qed. Lemma rq_source_id : forall a x, rqcat a -> is_ob a x -> source (id a x) = x. Proof. ir. uh H; ee. au. Qed. Lemma rq_target_id : forall a x, rqcat a -> is_ob a x -> target (id a x) = x. Proof. ir. uh H; ee. au. Qed. Lemma rq_is_mor_comp : forall a u v, rqcat a -> is_mor a u -> is_mor a v -> source u = target v -> is_mor a (comp a u v). Proof. ir. uh H; ee. au. Qed. Lemma rq_source_comp : forall a u v, rqcat a -> is_mor a u -> is_mor a v -> source u = target v -> source (comp a u v) = source v. Proof. ir. uh H; ee. au. Qed. Lemma rq_target_comp : forall a u v, rqcat a -> is_mor a u -> is_mor a v -> source u = target v -> target (comp a u v) = target u. Proof. ir. uh H; ee. au. Qed. Definition left_id_ok a := (forall u, is_mor a u -> comp a (id a (target u)) u = u). Definition right_id_ok a := (forall u, is_mor a u -> comp a u (id a (source u)) = u). Definition assoc_ok a := (forall u v w, is_mor a u -> is_mor a v -> is_mor a w -> source u = target v -> source v = target w -> comp a (comp a u v) w = comp a u (comp a v w)). Lemma cat_axioms_rw_rq : forall a, Category.axioms a = (rqcat a & left_id_ok a & right_id_ok a & assoc_ok a). Proof. ir. ap iff_eq; ir. ee. uhg; ee; ir. uh H; ee; am. apply mor_arrow_like with a. app is_mor_mor. ap mor_is_mor. ap mor_id. app is_ob_ob. rww source_id. app is_ob_ob. rww target_id. app is_ob_ob. ap ob_is_ob. rww ob_source. app is_mor_mor. ap ob_is_ob. rww ob_target. app is_mor_mor. ap mor_is_mor. rww mor_comp. app is_mor_mor. app is_mor_mor. rww source_comp. app is_mor_mor. app is_mor_mor. rww target_comp. app is_mor_mor. app is_mor_mor. uhg. ir. rww left_id. rww ob_target. app is_mor_mor. app is_mor_mor. uhg. ir. rww right_id. rww ob_source. app is_mor_mor. app is_mor_mor. uhg. ir. rww assoc. app is_mor_mor. app is_mor_mor. app is_mor_mor. ee. uh H0. uh H1. uh H2. uhg; ee; ir; try (ap iff_eq; ir; uhg; ee). am. app rq_is_mor_id. rww rq_source_id. rww rq_target_id. ir. wr H5. ap H1. am. ir. wr H5. ap H0. am. uh H3; ee; am. am. app rq_is_ob_source. app rq_is_ob_target. ap H0. am. app H1. uh H; ee. au. uh H3; ee; am. am. uh H3; ee. app rq_is_mor_comp. uh H3; ee. rww rq_source_comp. uh H3; ee. rww rq_target_comp. uh H3; ee. uh H3; ee; am. uh H3; ee. uh H3; ee; am. uh H3; ee. uh H3; ee; am. uh H3; uh H4; ee. app H2. uh H; ee; am. Qed. Definition rqcat_equiv_rel a r := rqcat a & is_equivalence_relation r & (forall x y, related r x y -> is_mor a x) & (forall x y, related r x y -> is_mor a y) & (forall x y, related r x y -> source x = source y) & (forall x y, related r x y -> target x = target y) & (forall u, is_mor a u -> related r u u) & (forall x y u v, related r x y -> related r u v -> source x = target u -> related r (comp a x u) (comp a y v)) & (forall u, is_mor a u -> related r (comp a (id a (target u)) u) u) & (forall u, is_mor a u -> related r (comp a u (id a (source u))) u) & (forall u v w, is_mor a u -> is_mor a v -> is_mor a w -> source u = target v -> source v = target w -> related r (comp a (comp a u v) w) (comp a u (comp a v w))). Lemma rq_inc_arrow_arrow_class : forall a r u v, rqcat_equiv_rel a r -> is_mor a v -> inc v (arrow (arrow_class r u)) = related r u v. Proof. ir. rw arrow_arrow_class. rww inc_class. lu. Qed. Definition rq_quotient_arrow a r u := rqcat_equiv_rel a r & (exists y, is_mor a y & u = arrow_class r y). Lemma rq_quotient_arrow_arrow_class : forall a r u, rqcat_equiv_rel a r -> is_mor a u -> rq_quotient_arrow a r (arrow_class r u). Proof. ir. uhg; ee. am. sh u. ee; try tv; try am. Qed. Lemma rq_inc_quotient_morphisms : forall a r u, rqcat_equiv_rel a r -> inc u (quotient_morphisms a r) = rq_quotient_arrow a r u. Proof. ir. uf quotient_morphisms. rw Image.inc_rw. ap iff_eq; ir. nin H0. ee. wr H1. ap rq_quotient_arrow_arrow_class. am. am. uh H0; ee. nin H1. ee. sh x. ee. change (is_mor a x). am. sy; am. Qed. Lemma rq_related_arrow_class_eq : forall a r u v, rqcat_equiv_rel a r -> is_mor a u -> related r u v = (arrow_class r u = arrow_class r v). Proof. ir. ap iff_eq. ir. cp H0. assert (source u = source v). uh H; ee. uh H; ee. au. assert (target u = target v). uh H; ee. uh H; ee. au. rwi related_class_eq H1. uf arrow_class. rw H3; rw H4; rww H1. lu. ap transitive_ap. lu. sh v. ee; try am. ap symmetric_ap. lu. am. ir. rw related_class_eq. wr arrow_arrow_class. rw H1. rw arrow_arrow_class. tv. lu. uh H; ee. au. Qed. Definition arrow_rep v := rep (arrow v). Lemma rq_inc_arrow_class_refl : forall a r u, rqcat_equiv_rel a r -> is_mor a u -> inc u (arrow (arrow_class r u)). Proof. ir. rw arrow_arrow_class. rw inc_class. uh H; ee. au. lu. Qed. Lemma rq_nonempty_arrow : forall a r u, rq_quotient_arrow a r u -> nonempty (arrow u). Proof. ir. uh H; ee. nin H0. ee. rw H1. sh x. apply rq_inc_arrow_class_refl with a. am. am. Qed. Lemma rq_inc_arrow_rep_arrow : forall a r u, rq_quotient_arrow a r u -> inc (arrow_rep u) (arrow u). Proof. ir. uf arrow_rep. ap nonempty_rep. apply rq_nonempty_arrow with a r. am. Qed. Lemma rq_related_arrow_rep_arrow_class : forall a r u, rqcat_equiv_rel a r -> is_mor a u -> related r u (arrow_rep (arrow_class r u)). Proof. ir. wr inc_class. assert (class r u = arrow (arrow_class r u)). rw arrow_arrow_class. tv. rw H1. apply rq_inc_arrow_rep_arrow with a r. ap rq_quotient_arrow_arrow_class. am. am. lu. Qed. Lemma rq_source_arrow_rep : forall a r u, rq_quotient_arrow a r u -> source (arrow_rep u) = source u. Proof. ir. uh H; ee. nin H0. ee. cp (rq_related_arrow_rep_arrow_class H H0). wri H1 H2. transitivity (source x). uh H; ee. uh H; ee. sy; au. rw H1. rw source_arrow_class. tv. Qed. Lemma rq_target_arrow_rep : forall a r u, rq_quotient_arrow a r u -> target (arrow_rep u) = target u. Proof. ir. uh H; ee. nin H0. ee. cp (rq_related_arrow_rep_arrow_class H H0). wri H1 H2. transitivity (target x). uh H; ee. uh H; ee. sy; au. rw H1. rw target_arrow_class. tv. Qed. Lemma rq_arrow_class_arrow_rep : forall a r u, rq_quotient_arrow a r u -> arrow_class r (arrow_rep u) = u. Proof. ir. uh H; ee. nin H0. ee. rw H1. sy. rewrite <- rq_related_arrow_class_eq with (a:=a). apply rq_related_arrow_rep_arrow_class with (a:=a). am. am. am. am. Qed. Lemma rq_inc_arrow_facts : forall a r u y, rq_quotient_arrow a r u -> inc y (arrow u) -> (is_mor a y & source y = source u & target y = target u). Proof. ir. uh H; ee. nin H1. ee. rwi H2 H0. rwi arrow_arrow_class H0. rwi inc_class H0. uh H; ee. uh H; ee. apply H5 with x. am. lu. nin H1. ee. rwi H2 H0. rwi arrow_arrow_class H0. rwi inc_class H0. transitivity (source x). uh H; ee. uh H; ee. sy; au. rw H2. rww source_arrow_class. lu. nin H1. ee. rwi H2 H0. rwi arrow_arrow_class H0. rwi inc_class H0. transitivity (target x). uh H; ee. uh H; ee. sy; au. rw H2. rww target_arrow_class. lu. Qed. Lemma rq_mor_arrow_rep : forall a r u, rq_quotient_arrow a r u -> is_mor a (arrow_rep u). Proof. ir. uh H; ee. nin H0; ee. rw H1. cp (rq_related_arrow_rep_arrow_class H H0). uh H; ee. uh H; ee. apply H5 with x. am. Qed. Lemma rq_related_arrow_rep : forall a r u v, rqcat_equiv_rel a r -> is_mor a v -> u = arrow_class r v -> related r v (arrow_rep u). Proof. ir. rw H1. apply rq_related_arrow_rep_arrow_class with a. am. am. Qed. Lemma rq_related_arrow_rep_rw : forall a r u v, rqcat_equiv_rel a r -> rq_quotient_arrow a r u -> is_mor a v -> related r v (arrow_rep u) = (u = arrow_class r v). Proof. ir. ap iff_eq; ir. cp H0. uh H3; ee. nin H4. ee. rw H5. rewrite <- rq_related_arrow_class_eq with (a:=a). ap transitive_ap. lu. sh (arrow_rep u). ee. rw H5. apply rq_related_arrow_rep_arrow_class with a. am. am. ap symmetric_ap. lu. am. am. am. rw H2. apply rq_related_arrow_rep_arrow_class with a. am. am. Qed. Lemma rq_source_quot_comp : forall a r u v, rqcat_equiv_rel a r -> rq_quotient_arrow a r u -> rq_quotient_arrow a r v -> source u = target v -> source (quot_comp a r u v) = source v. Proof. ir. uf quot_comp. rw source_arrow_class. rw rq_source_comp. rewrite rq_source_arrow_rep with (a:=a)(r:=r). tv. am. lu. apply rq_mor_arrow_rep with r. am. apply rq_mor_arrow_rep with r. am. rewrite rq_source_arrow_rep with (a:=a)(r:=r). rewrite rq_target_arrow_rep with (a:=a)(r:=r). am. am. am. Qed. Lemma rq_target_quot_comp : forall a r u v, rqcat_equiv_rel a r -> rq_quotient_arrow a r u -> rq_quotient_arrow a r v -> source u = target v -> target (quot_comp a r u v) = target u. Proof. ir. uf quot_comp. rw target_arrow_class. rw rq_target_comp. rewrite rq_target_arrow_rep with (a:=a)(r:=r). tv. am. lu. apply rq_mor_arrow_rep with r. am. apply rq_mor_arrow_rep with r. am. rewrite rq_source_arrow_rep with (a:=a)(r:=r). rewrite rq_target_arrow_rep with (a:=a)(r:=r). am. am. am. Qed. Lemma rq_quotient_arrow_quot_id : forall a r x, rqcat_equiv_rel a r -> is_ob a x -> rq_quotient_arrow a r (quot_id a r x). Proof. ir. uf quot_id. ap rq_quotient_arrow_arrow_class. am. app rq_is_mor_id. lu. Qed. Lemma rq_quotient_arrow_quot_comp : forall a r u v, rqcat_equiv_rel a r -> rq_quotient_arrow a r u -> rq_quotient_arrow a r v -> source u = target v -> rq_quotient_arrow a r (quot_comp a r u v). Proof. ir. uf quot_comp. ap rq_quotient_arrow_arrow_class. am. app rq_is_mor_comp. lu. apply rq_mor_arrow_rep with r. am. apply rq_mor_arrow_rep with r. am. rewrite rq_source_arrow_rep with (a:=a)(r:=r). rewrite rq_target_arrow_rep with (a:=a)(r:=r). am. am. am. Qed. Lemma rq_arrow_class_eq : forall a r u v, rqcat_equiv_rel a r -> is_mor a u -> (arrow_class r u = arrow_class r v) = (related r u v). Proof. ir. sy. ap (rq_related_arrow_class_eq (a:=a)). am. am. Qed. Lemma rq_related_comp : forall a r x y u v, rqcat_equiv_rel a r -> related r x y -> related r u v -> source x = target u -> related r (comp a x u) (comp a y v). Proof. ir. uh H; ee. au. Qed. Lemma rq_quot_comp_arrow_class : forall a r u v, rqcat_equiv_rel a r -> is_mor a u -> is_mor a v -> source u = target v -> quot_comp a r (arrow_class r u) (arrow_class r v) = arrow_class r (comp a u v). Proof. ir. uf quot_comp. rewrite rq_arrow_class_eq with (a:=a). ap rq_related_comp. am. ap symmetric_ap. lu. ap (rq_related_arrow_rep_arrow_class (a:=a)). am. am. ap symmetric_ap. lu. ap (rq_related_arrow_rep_arrow_class (a:=a)). am. am. rewrite rq_source_arrow_rep with (a:=a)(r:=r). rewrite rq_target_arrow_rep with (a:=a)(r:=r). rw source_arrow_class. rww target_arrow_class. app rq_quotient_arrow_arrow_class. app rq_quotient_arrow_arrow_class. am. ap rq_is_mor_comp. lu. ap (rq_mor_arrow_rep (a:=a)(r:=r)). app rq_quotient_arrow_arrow_class. ap (rq_mor_arrow_rep (a:=a)(r:=r)). app rq_quotient_arrow_arrow_class. rewrite rq_source_arrow_rep with (a:=a)(r:=r). rewrite rq_target_arrow_rep with (a:=a)(r:=r). rw source_arrow_class. rww target_arrow_class. app rq_quotient_arrow_arrow_class. app rq_quotient_arrow_arrow_class. Qed. Lemma rq_left_id_related : forall a r u, rqcat_equiv_rel a r -> is_mor a u -> related r (comp a (id a (target u )) u) u. Proof. ir. uh H; ee. au. Qed. Lemma rq_right_id_related : forall a r u, rqcat_equiv_rel a r -> is_mor a u -> related r (comp a u (id a (source u ))) u. Proof. ir. uh H; ee. au. Qed. Lemma rq_assoc_related : forall a r u v w, rqcat_equiv_rel a r -> is_mor a u -> is_mor a v -> is_mor a w -> source u = target v -> source v = target w -> related r (comp a (comp a u v) w) (comp a u (comp a v w)). Proof. ir. uh H; ee. au. Qed. Lemma rq_quot_id_left : forall a r a' r' x u, rqcat_equiv_rel a r -> rq_quotient_arrow a r u -> x = target u -> a' = a -> r' = r -> quot_comp a r (quot_id a' r' x) u = u. Proof. ir. rw H2; rw H3. uh H0; ee. nin H4; ee. rw H5. uf quot_id. assert (target u = target x0). rw H5. rewrite target_arrow_class. tv. assert (is_ob a x). rw H1; rw H6. app rq_is_ob_target. lu. rw rq_quot_comp_arrow_class. rewrite <- rq_related_arrow_class_eq with (a:=a). rw H1. rw H6. app rq_left_id_related. am. ap rq_is_mor_comp. lu. ap rq_is_mor_id. lu. am. am. rww rq_source_id. rw H1. am. lu. am. ap rq_is_mor_id. lu. am. am. rww rq_source_id. rw H1. am. lu. Qed. Lemma rq_quot_id_right : forall a r a' r' x u, rqcat_equiv_rel a r -> rq_quotient_arrow a r u -> x = source u -> a' = a -> r' = r -> quot_comp a r u (quot_id a' r' x) = u. Proof. ir. rw H2; rw H3. uh H0; ee. nin H4; ee. rw H5. uf quot_id. assert (source u = source x0). rw H5. rewrite source_arrow_class. tv. assert (is_ob a x). rw H1; rw H6. app rq_is_ob_source. lu. rw rq_quot_comp_arrow_class. rewrite <- rq_related_arrow_class_eq with (a:=a). rw H1. rw H6. app rq_right_id_related. am. ap rq_is_mor_comp. lu. am. ap rq_is_mor_id. lu. am. rww rq_target_id. rw H1. sy; am. lu. am. am. ap rq_is_mor_id. lu. am. rww rq_target_id. rw H1. sy; am. lu. Qed. Lemma rq_quot_comp_assoc : forall a r a' r' u v w, rqcat_equiv_rel a r -> rq_quotient_arrow a r u -> rq_quotient_arrow a r v -> rq_quotient_arrow a r w -> source u = target v -> source v = target w -> a' = a -> r' = r -> quot_comp a r (quot_comp a' r' u v) w = quot_comp a r u (quot_comp a' r' v w). Proof. ir. rw H5; rw H6. clear H5 H6. uh H0; uh H1; uh H2; ee. nin H7; nin H6; nin H5; ee. clear H0 H1 H2. assert (source x = target x0). transitivity (source u). rw H10. rww source_arrow_class. rw H3. rw H9. rww target_arrow_class. assert (source x0 = target x1). transitivity (source v). rw H9. rww source_arrow_class. rw H4. rw H8. rww target_arrow_class. rw H10; rw H9; rw H8. rw rq_quot_comp_arrow_class. rw rq_quot_comp_arrow_class. rw rq_quot_comp_arrow_class. rw rq_quot_comp_arrow_class. rewrite <- rq_related_arrow_class_eq with (a:=a). ap rq_assoc_related. am. am. am. am. am. am. am. app rq_is_mor_comp. lu. app rq_is_mor_comp. lu. rw rq_source_comp. am. lu. am. am. am. am. am. app rq_is_mor_comp. lu. rww rq_target_comp. lu. am. am. am. am. am. app rq_is_mor_comp. lu. am. rww rq_source_comp. lu. am. am. am. am. Qed. Lemma rq_is_mor_quotient_cat : forall a r u, rqcat_equiv_rel a r -> is_mor (quotient_cat a r) u = rq_quotient_arrow a r u. Proof. ir. uf quotient_cat. rw is_mor_create. rww rq_inc_quotient_morphisms. Qed. Lemma rq_comp_quotient_cat : forall a r u v, rqcat_equiv_rel a r -> rq_quotient_arrow a r u -> rq_quotient_arrow a r v -> source u = target v -> comp (quotient_cat a r) u v = quot_comp a r u v. Proof. ir. uf quotient_cat. rw comp_create. tv. rww rq_inc_quotient_morphisms. rww rq_inc_quotient_morphisms. am. Qed. Lemma rq_id_quotient_cat : forall a r x, rqcat_equiv_rel a r -> is_ob a x -> id (quotient_cat a r) x = quot_id a r x. Proof. ir. uf quotient_cat. rw id_create. tv. am. Qed. Lemma rq_source_quot_id : forall a r x, rqcat_equiv_rel a r -> is_ob a x -> source (quot_id a r x) = x. Proof. ir. uf quot_id. rw source_arrow_class. uh H; ee. uh H; ee. ap H13. am. Qed. Lemma rq_target_quot_id : forall a r x, rqcat_equiv_rel a r -> is_ob a x -> target (quot_id a r x) = x. Proof. ir. uf quot_id. rw target_arrow_class. uh H; ee. uh H; ee. ap H14. am. Qed. Lemma rqcat_quotient_cat : forall a r, rqcat_equiv_rel a r -> rqcat (quotient_cat a r). Proof. ir. uhg; ee; ir. uf quotient_cat. ap Category.Notations.create_like. rwi rq_is_mor_quotient_cat H0. uh H0; ee. nin H1. ee. rw H2. uf arrow_class. rww Arrow.create_like. am. rwi is_ob_quotient_cat H0. rww rq_id_quotient_cat. rww rq_is_mor_quotient_cat. app rq_quotient_arrow_quot_id. rwi is_ob_quotient_cat H0. rww rq_id_quotient_cat. rww rq_source_quot_id. rwi is_ob_quotient_cat H0. rww rq_id_quotient_cat. rww rq_target_quot_id. rw is_ob_quotient_cat. rwi rq_is_mor_quotient_cat H0. uh H0; ee. nin H1. ee. rw H2. rw source_arrow_class. ap rq_is_ob_source. lu. am. am. rw is_ob_quotient_cat. rwi rq_is_mor_quotient_cat H0. uh H0; ee. nin H1. ee. rw H2. rw target_arrow_class. ap rq_is_ob_target. lu. am. am. rwi rq_is_mor_quotient_cat H0. rwi rq_is_mor_quotient_cat H1. rww rq_is_mor_quotient_cat. rww rq_comp_quotient_cat. app rq_quotient_arrow_quot_comp. am. am. rwi rq_is_mor_quotient_cat H0. rwi rq_is_mor_quotient_cat H1. rww rq_comp_quotient_cat. rww rq_source_quot_comp. am. am. rwi rq_is_mor_quotient_cat H0. rwi rq_is_mor_quotient_cat H1. rww rq_comp_quotient_cat. rww rq_target_quot_comp. am. am. Qed. Lemma rq_quotient_cat_axioms : forall a r, rqcat_equiv_rel a r -> Category.axioms (quotient_cat a r). Proof. ir. rw cat_axioms_rw_rq. ee. ap rqcat_quotient_cat. am. uhg. ir. rwi rq_is_mor_quotient_cat H0. assert (is_ob a (target u)). uh H0; ee. nin H1. ee. rw H2. rw target_arrow_class. app rq_is_ob_target. lu. rww rq_comp_quotient_cat. rww rq_id_quotient_cat. rww rq_quot_id_left. rww rq_id_quotient_cat. app rq_quotient_arrow_quot_id. rww rq_id_quotient_cat. rww rq_source_quot_id. am. uhg. ir. rwi rq_is_mor_quotient_cat H0. assert (is_ob a (source u)). uh H0; ee. nin H1. ee. rw H2. rw source_arrow_class. app rq_is_ob_source. lu. rww rq_comp_quotient_cat. rww rq_id_quotient_cat. rww rq_quot_id_right. rww rq_id_quotient_cat. app rq_quotient_arrow_quot_id. rww rq_id_quotient_cat. rww rq_target_quot_id. am. uhg; ir. rwi rq_is_mor_quotient_cat H0; try am. rwi rq_is_mor_quotient_cat H1; try am. rwi rq_is_mor_quotient_cat H2; try am. rww rq_comp_quotient_cat. rww rq_comp_quotient_cat. rww rq_quot_comp_assoc. sy. rw rq_comp_quotient_cat. rw rq_comp_quotient_cat. tv. am. am. am. am. am. am. rww rq_comp_quotient_cat. app rq_quotient_arrow_quot_comp. rww rq_comp_quotient_cat. rww rq_target_quot_comp. rww rq_comp_quotient_cat. app rq_quotient_arrow_quot_comp. rww rq_comp_quotient_cat. rww rq_source_quot_comp. Qed. Lemma rq_ob_quotient_cat : forall a r x, rqcat_equiv_rel a r -> ob (quotient_cat a r) x = is_ob a x. Proof. ir. ap iff_eq; ir. uh H0; ee. rwi is_ob_quotient_cat H1. am. uhg. ee. ap rq_quotient_cat_axioms. am. rw is_ob_quotient_cat. am. Qed. Lemma rq_mor_quotient_cat : forall a r u, rqcat_equiv_rel a r -> mor (quotient_cat a r) u = rq_quotient_arrow a r u. Proof. ir. ap iff_eq; ir. uh H0; ee. rwi rq_is_mor_quotient_cat H1. am. am. uhg; ee. ap rq_quotient_cat_axioms. am. rww rq_is_mor_quotient_cat. Qed. Lemma rq_mor_quotient_cat_ex : forall a r u, rqcat_equiv_rel a r -> mor (quotient_cat a r) u = (exists y, is_mor a y & u = arrow_class r y). Proof. ir. rww rq_mor_quotient_cat. ap iff_eq; ir. uh H0; ee. am. uhg; ee. am. am. Qed. Lemma rq_mor_quotient_cat_quot_id : forall a r x, rqcat_equiv_rel a r -> is_ob a x -> mor (quotient_cat a r) (quot_id a r x). Proof. ir. rw rq_mor_quotient_cat. app rq_quotient_arrow_quot_id. am. Qed. Lemma rq_mor_quotient_cat_quot_comp : forall a r u v, rqcat_equiv_rel a r -> mor (quotient_cat a r) u -> mor (quotient_cat a r) v -> source u = target v -> mor (quotient_cat a r) (quot_comp a r u v). Proof. ir. rwi rq_mor_quotient_cat H0. rwi rq_mor_quotient_cat H1. rw rq_mor_quotient_cat. ap rq_quotient_arrow_quot_comp. am. am. am. am. am. am. am. Qed. Lemma rq_mor_quotient_cat_arrow_class : forall a r u, rqcat_equiv_rel a r -> is_mor a u -> mor (quotient_cat a r) (arrow_class r u). Proof. ir. rw rq_mor_quotient_cat. ap rq_quotient_arrow_arrow_class. am. am. am. Qed. (** Now we look at how to define a functor into a quotient in the above sense; the basic notation is the same as [qfunctor] in [qcat.v]. *) Export Quotient_Functor. Definition rqfunctor_property a b r fo fm := Category.axioms a & rqcat_equiv_rel b r & (forall x, ob a x -> is_ob b (fo x)) & (forall u, mor a u -> is_mor b (fm u)) & (forall u, mor a u -> source (fm u) = fo (source u)) & (forall u, mor a u -> target (fm u) = fo (target u)) & (forall x, ob a x -> related r (fm (id a x)) (id b (fo x))) & (forall u v, mor a u -> mor a v -> source u = target v -> related r (fm (comp a u v)) (comp b (fm u) (fm v))). Lemma rq_fob_qfunctor : forall a b r fo fm x, rqfunctor_property a b r fo fm -> ob a x -> fob (qfunctor a b r fo fm) x = fo x. Proof. ir. uf fob. rw fmor_qfunctor. rw source_arrow_class. rw source_qfunctor. uh H; ee. rw H4. rww source_id. app mor_id. rw source_qfunctor. app mor_id. Qed. Lemma rq_ob_fob_qfunctor : forall a b r fo fm x, rqfunctor_property a b r fo fm -> ob a x -> ob (quotient_cat b r) (fob (qfunctor a b r fo fm) x). Proof. ir. rww rq_fob_qfunctor. rw rq_ob_quotient_cat. uh H; ee; au. uh H; ee; am. Qed. Lemma rq_mor_fmor_qfunctor : forall a b r fo fm u, rqfunctor_property a b r fo fm -> mor a u -> mor (quotient_cat b r) (fmor (qfunctor a b r fo fm) u). Proof. ir. rww fmor_qfunctor. rww rq_mor_quotient_cat. ap rq_quotient_arrow_arrow_class. lu. uh H; ee; au. lu. Qed. Lemma rq_source_fmor_qfunctor : forall a b r fo fm u, rqfunctor_property a b r fo fm -> mor a u -> source (fmor (qfunctor a b r fo fm) u) = fob (qfunctor a b r fo fm) (source u). Proof. ir. rw fmor_qfunctor. rw source_arrow_class. rww rq_fob_qfunctor. uh H; ee; au. rww ob_source. am. Qed. Lemma rq_target_fmor_qfunctor : forall a b r fo fm u, rqfunctor_property a b r fo fm -> mor a u -> target (fmor (qfunctor a b r fo fm) u) = fob (qfunctor a b r fo fm) (target u). Proof. ir. rw fmor_qfunctor. rw target_arrow_class. rww rq_fob_qfunctor. uh H; ee; au. rww ob_target. am. Qed. Lemma rq_fmor_qfunctor_id : forall a b r fo fm x, rqfunctor_property a b r fo fm -> ob a x -> fmor (qfunctor a b r fo fm) (id a x) = id (quotient_cat b r) (fob (qfunctor a b r fo fm) x). Proof. ir. rw fmor_qfunctor. rw rq_id_quotient_cat. rw rq_fob_qfunctor. uf quot_id. rewrite <- rq_related_arrow_class_eq with (a:=b). uh H; ee; au. lu. assert (mor a (id a x)). app mor_id. uh H; ee; au. am. am. lu. rww rq_fob_qfunctor. uh H; ee; au. app mor_id. Qed. Lemma rq_fmor_qfunctor_comp : forall a b r fo fm u v, rqfunctor_property a b r fo fm -> mor a u -> mor a v -> source u = target v -> fmor (qfunctor a b r fo fm) (comp a u v) = comp (quotient_cat b r) (fmor (qfunctor a b r fo fm) u) (fmor (qfunctor a b r fo fm) v). Proof. ir. assert (rqcat_equiv_rel b r). lu. rww fmor_qfunctor. rww fmor_qfunctor. rww fmor_qfunctor. rw rq_comp_quotient_cat. rw rq_quot_comp_arrow_class. rewrite <- rq_related_arrow_class_eq with (a:=b). uh H; ee; au. am. assert (mor a (comp a u v)). rww mor_comp. uh H; ee; au. am. uh H; ee; au. uh H; ee; au. uh H; ee. rww H7; rww H8. rww H2. am. app rq_quotient_arrow_arrow_class. uh H; ee; au. app rq_quotient_arrow_arrow_class. uh H; ee; au. rw source_arrow_class. rw target_arrow_class. uh H; ee. rww H7; rww H8. rww H2. rww mor_comp. Qed. Lemma qfunctor_axioms : forall a b r fo fm, rqfunctor_property a b r fo fm -> Functor.axioms (qfunctor a b r fo fm). Proof. ir. uhg; ee. uf qfunctor. uf Functor.create. ap Umorphism.create_like. rw source_qfunctor. lu. rw target_qfunctor. ap rq_quotient_cat_axioms. lu. ir. rwi source_qfunctor H0. rw target_qfunctor. app rq_ob_fob_qfunctor. ir. rwi source_qfunctor H0. rw target_qfunctor. rw source_qfunctor. sy; app rq_fmor_qfunctor_id. ir. rwi source_qfunctor H0. rw target_qfunctor. app rq_mor_fmor_qfunctor. ir. rwi source_qfunctor H0. rww rq_source_fmor_qfunctor. ir. rwi source_qfunctor H0. rww rq_target_fmor_qfunctor. ir. rwi source_qfunctor H0. rwi source_qfunctor H1. rw target_qfunctor. rw source_qfunctor. sy; app rq_fmor_qfunctor_comp. Qed. End Associating_Quotient. 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 := multiplicative_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 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, (multiplicative_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 (multiplicative_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. 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; 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; 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; 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 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 invertible_id : forall a b x, a = b -> ob a x -> invertible a (id b x). Proof. ir. wr H. uhg; ee. sh (id a x). uhg; dj. app mor_id. app mor_id. rww source_id. rww target_id. rww source_id. rww target_id. rww source_id. rww left_id. rww target_id. rww source_id. rww left_id. rww target_id. Qed. Lemma inverse_id : forall a b x, a = b -> ob a x -> inverse a (id b x) = id a x. Proof. ir. wr H. assert (invertible a (id a x)). app invertible_id. transitivity (comp a (inverse a (id a x)) (id a x)). rww right_id. app mor_inverse. rww source_inverse. rww target_id. rww left_inverse. rww source_id. Qed. 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.