Set Implicit Arguments. Unset Strict Implicit. Require Export updateA. Module Categorical_Relation. Export UpdateA. Export Category. (** we consider relations which preserve the set of objects (it might sometime be necessary to generalize but that presents different difficulties and would require different notation) ***) Definition cat_rel a r := Category.axioms a & is_relation r & (forall x y, related r x y -> mor a x) & (forall x y, related r x y -> 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). Definition cat_equiv_rel a r := cat_rel a r & is_equivalence_relation r & (forall u, 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)). Lemma cat_rel_related_rw : forall a r x y, cat_rel a r -> related r x y = (related r x y & mor a x & mor a y & source x = source y & target x = target y). Proof. ir. ap iff_eq; ir. ee. am. uh H; ee. app (H2 x y). uh H; ee. app (H3 x y). uh H; ee. app (H4 x y). uh H; ee. app (H5 x y). ee; am. Qed. Lemma cer_reflexive : forall a r u, cat_equiv_rel a r -> mor a u -> related r u u. Proof. ir. uh H; ee. au. Qed. Lemma related_comp : forall a r x y u v, cat_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 cat_rel_intersection : forall a z, nonempty z -> (forall r, inc r z -> cat_rel a r) -> cat_rel a (intersection z). Proof. ir. uhg; dj. nin H. cp (H0 _ H). uh H1; ee. am. ap relation_intersection. am. ir. cp (H0 _ H2). uh H3; ee; am. rwi related_intersection H3. nin H. cp (H3 _ H). cp (H0 _ H). uh H5; ee. apply H7 with y. am. am. rwi related_intersection H4. nin H. cp (H4 _ H). cp (H0 _ H). uh H6; ee. apply H9 with x. am. am. rwi related_intersection H5. nin H. cp (H5 _ H). cp (H0 _ H). uh H7; ee. au. am. rwi related_intersection H6. nin H. cp (H6 _ H). cp (H0 _ H). uh H8; ee. au. am. Qed. Lemma cer_intersection : forall a z, nonempty z -> (forall r, inc r z -> cat_equiv_rel a r) -> cat_equiv_rel a (intersection z). Proof. ir. assert (cat_rel a (intersection z)). ap cat_rel_intersection. am. ir. cp (H0 _ H1). uh H2; ee; am. uhg; ee. am. ap equivalence_relation_intersection. am. ir. cp (H0 _ H2). uh H3; ee; am. ir. rww related_intersection. ir. cp (H0 _ H3). uh H4; ee; au. ir. rwi related_intersection H2; rwi related_intersection H3; try am. rww related_intersection. ir. cp (H0 _ H5). uh H6; ee; au. Qed. Definition coarse a := Z (Cartesian.product (morphisms a) (morphisms a)) (fun u => (source (pr1 u) = source (pr2 u) & target (pr1 u) = target (pr2 u))). Lemma related_coarse : forall a x y, Category.axioms a -> related (coarse a) x y = (mor a x & mor a y & source x = source y & target x = target y). Proof. ir. ap iff_eq; ir. ufi coarse H0. uh H0. Ztac. rwi pr1_pair H2; rwi pr1_pair H3; rwi pr2_pair H2; rwi pr2_pair H3. cp (product_pr H1). ee. rwi pr1_pair H5. rwi pr2_pair H6. ap is_mor_mor. am. am. rwi pr1_pair H2; rwi pr1_pair H3; rwi pr2_pair H2; rwi pr2_pair H3. cp (product_pr H1). ee. rwi pr1_pair H5. rwi pr2_pair H6. app is_mor_mor. rwi pr1_pair H2; rwi pr1_pair H3; rwi pr2_pair H2; rwi pr2_pair H3. am. rwi pr1_pair H2; rwi pr1_pair H3; rwi pr2_pair H2; rwi pr2_pair H3. am. ee. uf coarse. uhg. ap Z_inc. ap product_pair_inc. ap mor_is_mor. am. app mor_is_mor. rw pr1_pair. rw pr2_pair. ee. am. am. Qed. Lemma cat_rel_coarse : forall a, Category.axioms a -> cat_rel a (coarse a). Proof. ir. uhg; ee. am. uhg; ee. ir. ufi coarse H0. Ztac. cp (product_pr H1). ee. am. ir. rwi related_coarse H0; ee. am. am. ir. rwi related_coarse H0; ee. am. am. ir. rwi related_coarse H0; ee. am. am. ir. rwi related_coarse H0; ee. am. am. Qed. Lemma cat_equiv_rel_coarse : forall a, Category.axioms a -> cat_equiv_rel a (coarse a). Proof. ir. uhg; dj. ap cat_rel_coarse. am. ap show_equivalence_relation. uh H0; ee; am. ir. rwi related_coarse H1. ee. rw related_coarse; xd. am. ir. rwi related_coarse H1; rwi related_coarse H2. rw related_coarse; xd. transitivity (source y). am. am. transitivity (target y); am. am. am. am. rw related_coarse; xd. rwi related_coarse H3; rwi related_coarse H4. rw related_coarse; ee. rww mor_comp. rww mor_comp. wr H10. rww H5. rww source_comp. rww source_comp. wr H10. rww H5. rww target_comp. rww target_comp. wr H10. rww H5. am. am. am. am. Qed. Lemma sub_coarse : forall a r, cat_rel a r -> sub r (coarse a). Proof. ir. uhg; ir. uh H; ee. cp H1. uh H6. cp (H6 _ H0). rwi is_pair_rw H7. rw H7. change (related (coarse a) (pr1 x) (pr2 x)). assert (related r (pr1 x) (pr2 x)). uhg. wrr H7. rw related_coarse; xd. apply H2 with (pr2 x). am. apply H3 with (pr1 x). am. Qed. Definition relations_between r s := Z (powerset s) (fun y => sub r y). Lemma inc_relations_between : forall r s y, is_relation s -> inc y (relations_between r s) = (sub r y & sub y s & is_relation y). Proof. ir. ap iff_eq; ir. ufi relations_between H0. Ztac. rwi powerset_inc_rw H1. am. rwi powerset_inc_rw H1. uhg; ir. cp (H1 _ H3). ap H. am. ee. uf relations_between. ap Z_inc. ap powerset_inc. am. am. Qed. Definition cer a r := intersection (Z (relations_between r (coarse a)) (fun y=> cat_equiv_rel a y)). Lemma cat_equiv_rel_cer : forall a r, cat_rel a r -> cat_equiv_rel a (cer a r). Proof. ir. assert (cat_equiv_rel a (coarse a)). ap cat_equiv_rel_coarse. uh H; ee; am. cp H0. uh H1; ee. uf cer. ap cer_intersection. sh (coarse a). ap Z_inc. rw inc_relations_between. ee. ap sub_coarse. am. uhg; ir; am. uh H1; ee; am. uh H1; ee; am. am. ir. Ztac. Qed. Lemma cat_rel_subset : forall a r, (exists s, (cat_rel a s & sub r s)) -> cat_rel a r. Proof. ir. nin H. ee. assert (forall u v, related r u v -> related x u v). ir. uf related. ap H0. am. uh H; ee. uhg; ee. am. uhg; ir. ap H2. app H0. ir. apply H3 with y. au. ir. apply H4 with x0. au. au. au. Qed. Lemma sub_cer : forall a r s, sub r s -> cat_equiv_rel a s -> sub (cer a r) s. Proof. ir. assert (cat_rel a r). ap cat_rel_subset. sh s. ee; lu. uf cer. ap intersection_sub. ap Z_inc. rw inc_relations_between. ee. am. ap sub_coarse. lu. lu. assert (cat_equiv_rel a (coarse a)). app cat_equiv_rel_coarse. lu. lu. am. Qed. Lemma cer_contains : forall a r, cat_rel a r -> sub r (cer a r). Proof. ir. assert (cat_equiv_rel a (coarse a)). ap cat_equiv_rel_coarse. lu. uf cer. uhg; ir. ap intersection_inc. sh (coarse a). ap Z_inc. rw inc_relations_between. ee. ap sub_coarse. am. ap sub_coarse. lu. lu. lu. am. ir. Ztac. rwi inc_relations_between H3. ee. ap H3. am. lu. Qed. Definition ker f := Z (coarse (source f)) (fun z => (fmor f (pr1 z) = fmor f (pr2 z))). Lemma related_ker : forall f x y, Functor.axioms f -> related (ker f) x y = (mor (source f) x & mor (source f) y & source x = source y & target x = target y & fmor f x = fmor f y). Proof. ir. ap iff_eq; ir. uh H0. ufi ker H0. assert (related (coarse (source f)) x y). Ztac. assert (fmor f x = fmor f y). Ztac. rwi pr1_pair H3. rwi pr2_pair H3. am. rwi related_coarse H1. xd. lu. assert (related (coarse (source f)) x y). rw related_coarse. xd. lu. uh H1. uhg. uf ker. Ztac. rw pr1_pair. rw pr2_pair. ee; am. Qed. Lemma is_relation_ker : forall f, Functor.axioms f -> is_relation (ker f). Proof. ir. uhg; ir. ufi ker H0; Ztac. assert (cat_equiv_rel (source f) (coarse (source f))). ap cat_equiv_rel_coarse. lu. uh H3. ee. uh H4; ee. ap H4. am. Qed. Lemma cat_rel_ker : forall a f, Functor.axioms f -> a = source f -> cat_rel a (ker f). Proof. ir. rw H0. clear H0. clear a. uhg; ee. lu. ap is_relation_ker. am. ir. rwi related_ker H0. ee; am. am. ir. rwi related_ker H0. ee; am. am. ir. rwi related_ker H0. ee; am. am. ir. rwi related_ker H0. ee; am. am. Qed. Lemma cat_equiv_rel_ker : forall a f, Functor.axioms f -> a = source f -> cat_equiv_rel a (ker f). Proof. ir. rw H0. clear H0. clear a. uhg; ee. app cat_rel_ker. ap show_equivalence_relation. app is_relation_ker. ir. rww related_ker; rwi related_ker H0; try am. xd. ir. rww related_ker. rwi related_ker H0; try am. rwi related_ker H1; try am. xd. transitivity (source y); au. transitivity (target y); au. transitivity (fmor f y); au. ir. rww related_ker. ee. am. am. tv. tv. tv. ir. rwi related_ker H0; try am. rwi related_ker H1; try am. ee. rww related_ker. ee. rww mor_comp. rww mor_comp. wr H8. wrr H5. rww source_comp. rww source_comp. wr H8. wrr H5. rww target_comp. rww target_comp. wr H8. wrr H5. wr comp_fmor. wr comp_fmor. rw H10. rw H6. tv. am. am. am. wr H8. wrr H5. am. am. am. am. Qed. Definition compatible r f := Functor.axioms f & cat_rel (source f) r & sub r (ker f). Lemma compatible_related_ker : forall r f u v, compatible r f -> related r u v -> related (ker f) u v. Proof. ir. uh H; ee. uhg. ap H2. am. Qed. Lemma related_eq_fmor : forall r f u v, compatible r f -> related r u v -> fmor f u = fmor f v. Proof. ir. cp (compatible_related_ker H H0). rwi related_ker H1; ee; try am. lu. Qed. Lemma is_relation_coarse : forall a, Category.axioms a -> is_relation (coarse a). Proof. ir. assert (cat_rel a (coarse a)). ap cat_rel_coarse. am. lu. Qed. Lemma compatible_cer : forall a r f, compatible r f -> a = source f -> compatible (cer a r) f. Proof. ir. uhg; ee. lu. assert (cat_equiv_rel a (cer a r)). ap cat_equiv_rel_cer. uh H; ee. rww H0. wr H0. lu. uf cer. uhg; ir. cp (intersection_use_inc H1). ap H2. ap Z_inc. rw inc_relations_between. ee. uh H; ee; am. uhg; ir. ufi ker H3. rw H0; Ztac. ap is_relation_ker. lu. ap is_relation_coarse. rw H0; lu. ap cat_equiv_rel_ker. lu. am. Qed. Lemma compatible_rw : forall r f, compatible r f = (Functor.axioms f & cat_rel (source f) r & (forall x y, related r x y -> fmor f x = fmor f y)). Proof. ir. ap iff_eq; ir. ee. lu. lu. ir. uh H0. uh H; ee. cp (H2 _ H0). assert (related (ker f) x y). am. rwi related_ker H4. ee; am. am. uhg; ee; try am. uhg. ir. assert (is_pair x). uh H0; ee. ap H3. am. rwi is_pair_rw H3. rw H3. change (related (ker f) (pr1 x) (pr2 x)). rwi H3 H2. assert (related (coarse (source f)) (pr1 x) (pr2 x)). assert (sub r (coarse (source f))). ap sub_coarse. am. uhg. ap H4. am. rwi related_coarse H4. rw related_ker; xd. lu. Qed. End Categorical_Relation. Module Quotient_Category. Export Categorical_Relation. Definition arrow_class r u := Arrow.create (source u) (target u) (class r u). Lemma source_arrow_class : forall r u, source (arrow_class r u) = source u. Proof. ir. uf arrow_class. rww Arrow.source_create. Qed. Lemma target_arrow_class : forall r u, target (arrow_class r u) = target u. Proof. ir. uf arrow_class. rww Arrow.target_create. Qed. Lemma arrow_arrow_class : forall r u, arrow (arrow_class r u) = class r u. Proof. ir. uf arrow_class. rww Arrow.arrow_create. Qed. Lemma inc_arrow_arrow_class : forall a r u v, cat_equiv_rel a r -> 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. Lemma like_arrow_class : forall r u, Arrow.like (arrow_class r u). Proof. ir. uf arrow_class. rww Arrow.create_like. Qed. Definition is_quotient_arrow a r u := cat_equiv_rel a r & (exists y, mor a y & u = arrow_class r y). Lemma is_quotient_arrow_arrow_class : forall a r u, cat_equiv_rel a r -> mor a u -> is_quotient_arrow a r (arrow_class r u). Proof. ir. uhg; ee. am. sh u. ee; try tv; try am. Qed. Definition quotient_morphisms a r := Image.create (morphisms a) (arrow_class r). Lemma inc_quotient_morphisms : forall a r u, cat_equiv_rel a r -> inc u (quotient_morphisms a r) = is_quotient_arrow a r u. Proof. ir. uf quotient_morphisms. rw Image.inc_rw. ap iff_eq; ir. nin H0. ee. wr H1. ap is_quotient_arrow_arrow_class. am. ap is_mor_mor. lu. am. uh H0; ee. nin H1. ee. sh x. ee. change (is_mor a x). ap mor_is_mor. am. sy; am. Qed. Lemma related_arrow_class_eq : forall a r u v, cat_equiv_rel a r -> 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 inc_arrow_class_refl : forall a r u, cat_equiv_rel a r -> 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 nonempty_arrow : forall a r u, is_quotient_arrow a r u -> nonempty (arrow u). Proof. ir. uh H; ee. nin H0. ee. rw H1. sh x. apply inc_arrow_class_refl with a. am. am. Qed. Lemma inc_arrow_rep_arrow : forall a r u, is_quotient_arrow a r u -> inc (arrow_rep u) (arrow u). Proof. ir. uf arrow_rep. ap nonempty_rep. apply nonempty_arrow with a r. am. Qed. Lemma related_arrow_rep_arrow_class : forall a r u, cat_equiv_rel a r -> 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 inc_arrow_rep_arrow with a r. ap is_quotient_arrow_arrow_class. am. am. lu. Qed. Lemma source_arrow_rep : forall a r u, is_quotient_arrow a r u -> source (arrow_rep u) = source u. Proof. ir. uh H; ee. nin H0. ee. cp (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 target_arrow_rep : forall a r u, is_quotient_arrow a r u -> target (arrow_rep u) = target u. Proof. ir. uh H; ee. nin H0. ee. cp (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 arrow_class_arrow_rep : forall a r u, is_quotient_arrow a r u -> arrow_class r (arrow_rep u) = u. Proof. ir. uh H; ee. nin H0. ee. rw H1. sy. rewrite <- related_arrow_class_eq with (a:=a). apply related_arrow_rep_arrow_class with (a:=a). am. am. am. am. Qed. Lemma inc_arrow_facts : forall a r u y, is_quotient_arrow a r u -> inc y (arrow u) -> (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 H8 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 mor_arrow_rep : forall a r u, is_quotient_arrow a r u -> mor a (arrow_rep u). Proof. ir. uh H; ee. nin H0; ee. rw H1. cp (related_arrow_rep_arrow_class H H0). uh H; ee. uh H; ee. apply H8 with x. am. Qed. Lemma related_arrow_rep : forall a r u v, cat_equiv_rel a r -> mor a v -> u = arrow_class r v -> related r v (arrow_rep u). Proof. ir. rw H1. apply related_arrow_rep_arrow_class with a. am. am. Qed. Lemma related_arrow_rep_rw : forall a r u v, cat_equiv_rel a r -> is_quotient_arrow a r u -> 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 <- related_arrow_class_eq with (a:=a). ap transitive_ap. lu. sh (arrow_rep u). ee. rw H5. apply related_arrow_rep_arrow_class with a. am. am. ap symmetric_ap. lu. am. am. am. rw H2. apply related_arrow_rep_arrow_class with a. am. am. Qed. Definition quot_id a r x := arrow_class r (id a x). Definition quot_comp a r u v := arrow_class r (comp a (arrow_rep u) (arrow_rep v)). Lemma source_quot_id : forall a r x, ob a x -> source (quot_id a r x) = x. Proof. ir. uf quot_id. rw source_arrow_class. rww source_id. Qed. Lemma target_quot_id : forall a r x, ob a x -> target (quot_id a r x) = x. Proof. ir. uf quot_id. rw target_arrow_class. rww target_id. Qed. Lemma source_quot_comp : forall a r u v, cat_equiv_rel a r -> is_quotient_arrow a r u -> is_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 source_comp. rewrite source_arrow_rep with (a:=a)(r:=r). tv. am. apply mor_arrow_rep with r. am. apply mor_arrow_rep with r. am. rewrite source_arrow_rep with (a:=a)(r:=r). rewrite target_arrow_rep with (a:=a)(r:=r). am. am. am. Qed. Lemma target_quot_comp : forall a r u v, cat_equiv_rel a r -> is_quotient_arrow a r u -> is_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 target_comp. rewrite target_arrow_rep with (a:=a)(r:=r). tv. am. apply mor_arrow_rep with r. am. apply mor_arrow_rep with r. am. rewrite source_arrow_rep with (a:=a)(r:=r). rewrite target_arrow_rep with (a:=a)(r:=r). am. am. am. Qed. Lemma is_quotient_arrow_quot_id : forall a r x, cat_equiv_rel a r -> ob a x -> is_quotient_arrow a r (quot_id a r x). Proof. ir. uf quot_id. ap is_quotient_arrow_arrow_class. am. app mor_id. Qed. Lemma is_quotient_arrow_quot_comp : forall a r u v, cat_equiv_rel a r -> is_quotient_arrow a r u -> is_quotient_arrow a r v -> source u = target v -> is_quotient_arrow a r (quot_comp a r u v). Proof. ir. uf quot_comp. ap is_quotient_arrow_arrow_class. am. rww mor_comp. apply mor_arrow_rep with r. am. apply mor_arrow_rep with r. am. rewrite source_arrow_rep with (a:=a)(r:=r). rewrite target_arrow_rep with (a:=a)(r:=r). am. am. am. Qed. Lemma arrow_class_eq : forall a r u v, cat_equiv_rel a r -> mor a u -> (arrow_class r u = arrow_class r v) = (related r u v). Proof. ir. sy. ap (related_arrow_class_eq (a:=a)). am. am. Qed. Lemma arrow_class_id : forall a r x, arrow_class r (id a x) = quot_id a r x. Proof. ir. tv. Qed. Lemma quot_comp_arrow_class : forall a r u v, cat_equiv_rel a r -> mor a u -> 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 arrow_class_eq with (a:=a). ap related_comp. am. ap symmetric_ap. lu. ap (related_arrow_rep_arrow_class (a:=a)). am. am. ap symmetric_ap. lu. ap (related_arrow_rep_arrow_class (a:=a)). am. am. rewrite source_arrow_rep with (a:=a)(r:=r). rewrite target_arrow_rep with (a:=a)(r:=r). rw source_arrow_class. rww target_arrow_class. app is_quotient_arrow_arrow_class. app is_quotient_arrow_arrow_class. am. rw mor_comp. tv. ap (mor_arrow_rep (a:=a)(r:=r)). app is_quotient_arrow_arrow_class. ap (mor_arrow_rep (a:=a)(r:=r)). app is_quotient_arrow_arrow_class. rewrite source_arrow_rep with (a:=a)(r:=r). rewrite target_arrow_rep with (a:=a)(r:=r). rw source_arrow_class. rww target_arrow_class. app is_quotient_arrow_arrow_class. app is_quotient_arrow_arrow_class. tv. Qed. Lemma quot_id_left : forall a r a' r' x u, cat_equiv_rel a r -> is_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 (ob a x). rw H1; rw H6; rww ob_target. rw quot_comp_arrow_class. rw left_id. tv. rw H1. wrr H1. am. wr H6; sy; am. tv. am. app mor_id. am. rww source_id. wrr H6. Qed. Lemma quot_id_right : forall a r a' r' x u, cat_equiv_rel a r -> is_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 (ob a x). rw H1; rw H6; rww ob_source. rw quot_comp_arrow_class. rw right_id. tv. rw H1. wrr H1. am. wr H6; sy; am. tv. am. am. app mor_id. rww target_id. wrr H6. sy; am. Qed. Lemma quot_comp_assoc : forall a r a' r' u v w, cat_equiv_rel a r -> is_quotient_arrow a r u -> is_quotient_arrow a r v -> is_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 quot_comp_arrow_class. rw quot_comp_arrow_class. rw quot_comp_arrow_class. rw quot_comp_arrow_class. rw assoc. reflexivity. am. am. am. am. am. tv. am. am. rww mor_comp. rww target_comp. am. am. am. am. am. rww mor_comp. am. rww source_comp. am. am. am. am. Qed. Definition quotient_cat a r := Category.Notations.create (objects a) (quotient_morphisms a r) (quot_comp a r) (quot_id a r) (structure a). Lemma is_ob_quotient_cat : forall a r x, is_ob (quotient_cat a r) x = is_ob a x. Proof. ir. uf quotient_cat. rw is_ob_create. tv. Qed. Lemma is_mor_quotient_cat : forall a r u, cat_equiv_rel a r -> is_mor (quotient_cat a r) u = is_quotient_arrow a r u. Proof. ir. uf quotient_cat. rw is_mor_create. rww inc_quotient_morphisms. Qed. Lemma comp_quotient_cat : forall a r u v, cat_equiv_rel a r -> is_quotient_arrow a r u -> is_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 inc_quotient_morphisms. rww inc_quotient_morphisms. am. Qed. Lemma id_quotient_cat : forall a r x, cat_equiv_rel a r -> ob a x -> id (quotient_cat a r) x = quot_id a r x. Proof. ir. uf quotient_cat. rw id_create. tv. ap ob_is_ob. am. Qed. Lemma quotient_cat_axioms : forall a r, cat_equiv_rel a r -> Category.axioms (quotient_cat a r). Proof. ir. uhg; dj. ir. ap iff_eq; ir. cp H0. rwi is_ob_quotient_cat H0. assert (ob a x). ap is_ob_ob. uh H; ee. uh H; ee; am. am. uhg; ee. am. rw is_mor_quotient_cat. rw id_quotient_cat. ap is_quotient_arrow_quot_id. am. am. am. am. am. rw id_quotient_cat. rww source_quot_id. am. am. rww id_quotient_cat. rww target_quot_id. ir. rwi is_mor_quotient_cat H3. rw id_quotient_cat. rw comp_quotient_cat. rw quot_id_right. tv. am. am. sy; am. tv. tv. am. am. app is_quotient_arrow_quot_id. rww target_quot_id. am. am. am. ir. rwi is_mor_quotient_cat H3. rw id_quotient_cat. rw comp_quotient_cat. rw quot_id_left. tv. am. am. sy; am. tv. tv. am. app is_quotient_arrow_quot_id. am. rww source_quot_id. sy; am. am. am. am. uh H0; ee; am. ir. ap iff_eq; ir. rwi is_mor_quotient_cat H1. uhg; dj. rw is_mor_quotient_cat. am. am. rw is_ob_quotient_cat. uh H1; ee. nin H3. ee. rw H4. rw source_arrow_class. ap ob_is_ob. rww ob_source. rw is_ob_quotient_cat. uh H1; ee. nin H4. ee. rw H5. rw target_arrow_class. ap ob_is_ob. rww ob_target. rwi H0 H4. uh H4; ee. ap H9. am. tv. rwi H0 H3. uh H3; ee. ap H9. am. tv. uh H1. ee. nin H7. ee. rw H8. uf arrow_class. rww Arrow.create_like. am. uh H1; ee. am. ap iff_eq; ir. uh H2; ee. cp H2; cp H3. rwi is_mor_quotient_cat H2. rwi is_mor_quotient_cat H3. uhg; ee. uhg; ee; am. rw is_mor_quotient_cat. rw comp_quotient_cat. ap is_quotient_arrow_quot_comp. am. am. am. am. am. am. am. am. am. rw comp_quotient_cat. rw source_quot_comp. tv. am. am. am. am. am. am. am. am. rw comp_quotient_cat. rw target_quot_comp. tv. am. am. am. am. am. am. am. am. am. am. uh H2; ee; am. uh H3; uh H4; ee. rwi is_mor_quotient_cat H3. rwi is_mor_quotient_cat H7. rwi is_mor_quotient_cat H5. rw comp_quotient_cat. rw comp_quotient_cat. rw comp_quotient_cat. rw comp_quotient_cat. rw quot_comp_assoc. reflexivity. am. am. am. am. am. am. tv. tv. am. am. am. am. am. am. rw comp_quotient_cat. app is_quotient_arrow_quot_comp. am. am. am. am. rww comp_quotient_cat. rww target_quot_comp. am. am. am. am. am. rw comp_quotient_cat. app is_quotient_arrow_quot_comp. am. am. am. am. am. rww comp_quotient_cat. rww source_quot_comp. am. am. am. uf quotient_cat. ap Category.Notations.create_like. Qed. Lemma ob_quotient_cat : forall a r x, cat_equiv_rel a r -> ob (quotient_cat a r) x = ob a x. Proof. ir. ap iff_eq; ir. uh H0; ee. rwi is_ob_quotient_cat H1. ap is_ob_ob. uh H; ee; uh H; ee; am. am. uhg; ee. ap quotient_cat_axioms. am. rw is_ob_quotient_cat. app ob_is_ob. Qed. Lemma mor_quotient_cat : forall a r u, cat_equiv_rel a r -> mor (quotient_cat a r) u = is_quotient_arrow a r u. Proof. ir. ap iff_eq; ir. uh H0; ee. rwi is_mor_quotient_cat H1. am. am. uhg; ee. ap quotient_cat_axioms. am. rww is_mor_quotient_cat. Qed. Lemma mor_quotient_cat_ex : forall a r u, cat_equiv_rel a r -> mor (quotient_cat a r) u = (exists y, mor a y & u = arrow_class r y). Proof. ir. rww mor_quotient_cat. ap iff_eq; ir. uh H0; ee. am. uhg; ee. am. am. Qed. Lemma mor_quotient_cat_quot_id : forall a r x, cat_equiv_rel a r -> ob a x -> mor (quotient_cat a r) (quot_id a r x). Proof. ir. rw mor_quotient_cat. app is_quotient_arrow_quot_id. am. Qed. Lemma mor_quotient_cat_quot_comp : forall a r u v, cat_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 mor_quotient_cat H0. rwi mor_quotient_cat H1. rw mor_quotient_cat. ap is_quotient_arrow_quot_comp. am. am. am. am. am. am. am. Qed. Lemma mor_quotient_cat_arrow_class : forall a r u, cat_equiv_rel a r -> mor a u -> mor (quotient_cat a r) (arrow_class r u). Proof. ir. rw mor_quotient_cat. ap is_quotient_arrow_arrow_class. am. am. am. Qed. (** next quotient_functor is the projection to the quotient and quotient_dotted is the factorizing functor for the universal property. *********************) End Quotient_Category. Module Quotient_Functor. Export Quotient_Category. (** try something strange here: make it depend on fo even though it doesnt, so we can do rewriting ***) Definition qfunctor a b r (fo fm:E-> E) := Functor.create a (quotient_cat b r) (fun u => arrow_class r (fm u)). Lemma source_qfunctor : forall a b r fo fm, source (qfunctor a b r fo fm) = a. Proof. ir. uf qfunctor. rw Functor.source_create. tv. Qed. Lemma target_qfunctor : forall a b r fo fm, target (qfunctor a b r fo fm) = (quotient_cat b r). Proof. ir. uf qfunctor. rw Functor.target_create. tv. Qed. Lemma fmor_qfunctor : forall a b r fo fm u, mor a u -> fmor (qfunctor a b r fo fm) u = arrow_class r (fm u). Proof. ir. uf qfunctor. rw fmor_create. tv. am. Qed. Definition qfunctor_property a b r fo fm := Category.axioms a & cat_equiv_rel b r & (forall x, ob a x -> ob b (fo x)) & (forall u, mor a u -> 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 fob_qfunctor : forall a b r fo fm x, qfunctor_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 ob_fob_qfunctor : forall a b r fo fm x, qfunctor_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 fob_qfunctor. rw ob_quotient_cat. uh H; ee; au. uh H; ee; am. Qed. Lemma mor_fmor_qfunctor : forall a b r fo fm u, qfunctor_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 mor_quotient_cat. ap is_quotient_arrow_arrow_class. lu. uh H; ee; au. lu. Qed. Lemma source_fmor_qfunctor : forall a b r fo fm u, qfunctor_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 fob_qfunctor. uh H; ee; au. rww ob_source. am. Qed. Lemma target_fmor_qfunctor : forall a b r fo fm u, qfunctor_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 fob_qfunctor. uh H; ee; au. rww ob_target. am. Qed. Lemma fmor_qfunctor_id : forall a b r fo fm x, qfunctor_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 id_quotient_cat. rw fob_qfunctor. uf quot_id. rewrite <- 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 fob_qfunctor. uh H; ee; au. app mor_id. Qed. Lemma fmor_qfunctor_comp : forall a b r fo fm u v, qfunctor_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 (cat_equiv_rel b r). lu. rww fmor_qfunctor. rww fmor_qfunctor. rww fmor_qfunctor. rw comp_quotient_cat. rw quot_comp_arrow_class. rewrite <- 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 is_quotient_arrow_arrow_class. uh H; ee; au. app is_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, qfunctor_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 quotient_cat_axioms. lu. ir. rwi source_qfunctor H0. rw target_qfunctor. app ob_fob_qfunctor. ir. rwi source_qfunctor H0. rw target_qfunctor. rw source_qfunctor. sy; app fmor_qfunctor_id. ir. rwi source_qfunctor H0. rw target_qfunctor. app mor_fmor_qfunctor. ir. rwi source_qfunctor H0. rww source_fmor_qfunctor. ir. rwi source_qfunctor H0. rww target_fmor_qfunctor. ir. rwi source_qfunctor H0. rwi source_qfunctor H1. rw target_qfunctor. rw source_qfunctor. sy; app fmor_qfunctor_comp. Qed. Lemma qfunctor_extensionality : forall a b r fo fm a' b' r' fo' fm', a = a' -> b = b' -> r = r' -> qfunctor_property a b r fo fm -> qfunctor_property a' b' r' fo' fm' -> (forall u, mor a u -> related r (fm u) (fm' u)) -> qfunctor a b r fo fm = qfunctor a' b' r' fo' fm'. Proof. ir. ap Functor.axioms_extensionality. app qfunctor_axioms. app qfunctor_axioms. rw source_qfunctor. rww source_qfunctor. rw target_qfunctor. rw target_qfunctor. rw H0; rww H1. ir. rwi source_qfunctor H5. rw fmor_qfunctor. rw fmor_qfunctor. wr H1. rewrite <- related_arrow_class_eq with (a:=b). au. uh H2; ee; am. uh H2; ee; au. wrr H. am. Qed. Lemma eq_qfunctor : forall a b r f fo fm, Functor.axioms f -> source f = a -> target f = (quotient_cat b r) -> qfunctor_property a b r fo fm -> (forall u, mor a u -> related r (fm u) (arrow_rep (fmor f u))) -> f = qfunctor a b r fo fm. Proof. ir. ap Functor.axioms_extensionality. am. ap qfunctor_axioms. am. rw source_qfunctor. am. rw target_qfunctor. am. ir. rw fmor_qfunctor. assert (is_quotient_arrow b r (fmor f u)). wr mor_quotient_cat. wr H1. app mor_fmor. lu. uh H5; ee. nin H6; ee. rw H7. rewrite <- related_arrow_class_eq with (a:=b). ap transitive_ap. lu. sh (arrow_rep (fmor f u)). ee. rw H7. apply related_arrow_rep_arrow_class with (a:=b). lu. am. ap symmetric_ap. lu. ap H3. wrr H0. lu. am. wrr H0. Qed. Lemma qfunctor_property_fob_fmor : forall b r f, Functor.axioms f -> cat_equiv_rel b r -> target f = (quotient_cat b r) -> qfunctor_property (source f) b r (fob f) (fun u => arrow_rep (fmor f u)). Proof. ir. uhg; ee. uh H; ee. am. am. ir. assert (ob (target f) (fob f x)). app ob_fob. rwi H1 H3. rwi ob_quotient_cat H3. am. am. ir. apply mor_arrow_rep with (r:=r). wr mor_quotient_cat. wr H1. app mor_fmor. am. ir. rewrite source_arrow_rep with (a:=b) (r:=r). rw source_fmor. tv. am. am. wr mor_quotient_cat. wr H1. app mor_fmor. am. ir. rewrite target_arrow_rep with (a:=b) (r:=r). rw target_fmor. tv. am. am. wr mor_quotient_cat. wr H1. app mor_fmor. am. ir. assert (ob b (fob f x)). assert (ob (target f) (fob f x)). app ob_fob. rwi H1 H3. rwi ob_quotient_cat H3. am. am. rw fmor_id. rw H1. rw id_quotient_cat. rewrite related_arrow_class_eq with (a:=b). rewrite arrow_class_arrow_rep with (a:=b). tv. app is_quotient_arrow_quot_id. am. apply mor_arrow_rep with (r:=r). app is_quotient_arrow_quot_id. am. am. am. tv. am. ir. assert (is_quotient_arrow b r (fmor f u)). wr mor_quotient_cat. wr H1. app mor_fmor. am. assert (is_quotient_arrow b r (fmor f v)). wr mor_quotient_cat. wr H1. app mor_fmor. am. rewrite related_arrow_class_eq with (a:=b). rewrite arrow_class_arrow_rep with (a:=b). wr comp_fmor. rw H1. rw comp_quotient_cat. reflexivity. am. am. am. rw source_fmor. rw target_fmor. rww H4. am. am. am. am. am. am. am. am. wr mor_quotient_cat. wr H1. ap mor_fmor. am. rww mor_comp. am. am. apply mor_arrow_rep with (r:=r). wr mor_quotient_cat. wr H1. ap mor_fmor. am. rww mor_comp. am. Qed. Lemma eq_qfunctor2 : forall b r f, Functor.axioms f -> cat_equiv_rel b r -> target f = (quotient_cat b r) -> f = qfunctor (source f) b r (fob f) (fun u => arrow_rep (fmor f u)). Proof. ir. ap eq_qfunctor. am. tv. am. ap qfunctor_property_fob_fmor. am. am. am. ir. uh H0; ee. ap H4. apply mor_arrow_rep with (r:=r). wr mor_quotient_cat. wr H1. ap mor_fmor. am. am. uhg; ee; am. Qed. Definition qprojection a r := qfunctor a a r (fun (x:E) => x) (fun (u:E)=> u). Lemma source_qprojection : forall a r, source (qprojection a r) = a. Proof. ir. uf qprojection. rww source_qfunctor. Qed. Lemma target_qprojection : forall a r, target (qprojection a r) = (quotient_cat a r). Proof. ir. uf qprojection. rww target_qfunctor. Qed. Lemma qprojection_property : forall a r, cat_equiv_rel a r -> qfunctor_property a a r (fun (x:E) => x) (fun (u:E)=> u). Proof. ir. uhg; ee. lu. am. ir; tv. ir; tv. ir; tv. ir; tv. ir. uh H; ee. ap H2. app mor_id. ir. uh H; ee. ap H4. rww mor_comp. Qed. Lemma fob_qprojection : forall a r x, cat_equiv_rel a r -> ob a x -> fob (qprojection a r) x = x. Proof. ir. uf qprojection. rww fob_qfunctor. app qprojection_property. Qed. Lemma fmor_qprojection : forall a r u, mor a u -> fmor (qprojection a r) u = (arrow_class r u). Proof. ir. uf qprojection. rw fmor_qfunctor. tv. am. Qed. Lemma fmor_qprojection_arrow_rep : forall a r u, is_quotient_arrow a r u -> fmor (qprojection a r) (arrow_rep u) = u. Proof. ir. rw fmor_qprojection. rewrite arrow_class_arrow_rep with (a:=a). tv. am. apply mor_arrow_rep with (a:=a)(r:=r). am. Qed. Lemma qprojection_axioms : forall a r, cat_equiv_rel a r -> Functor.axioms (qprojection a r). Proof. ir. uf qprojection. ap qfunctor_axioms. app qprojection_property. Qed. Definition qdotted r f := Functor.create (quotient_cat (source f) r) (target f) (fun u => fmor f (arrow_rep u)). Lemma source_qdotted : forall r f, source (qdotted r f) = quotient_cat (source f) r. Proof. ir. uf qdotted. rww Functor.source_create. Qed. Lemma target_qdotted : forall r f, target (qdotted r f) = target f. Proof. ir. uf qdotted. rww Functor.target_create. Qed. Lemma fmor_qdotted : forall r f u, cat_equiv_rel (source f) r -> is_quotient_arrow (source f) r u -> fmor (qdotted r f) u = fmor f (arrow_rep u). Proof. ir. uf qdotted. rw Functor.fmor_create. tv. rww mor_quotient_cat. Qed. Lemma fmor_qdotted_arrow_class : forall r f u, cat_equiv_rel (source f) r -> compatible r f -> mor (source f) u -> fmor (qdotted r f) (arrow_class r u) = fmor f u. Proof. ir. rw fmor_qdotted. rwi compatible_rw H0. ee. sy; ap H3. apply related_arrow_rep_arrow_class with (a:= source f). am. am. am. app is_quotient_arrow_arrow_class. Qed. Lemma fob_qdotted : forall r f x, cat_equiv_rel (source f) r -> compatible r f -> ob (source f) x -> fob (qdotted r f) x = fob f x. Proof. ir. uf fob. rw source_qdotted. rw id_quotient_cat. uf quot_id. rw fmor_qdotted_arrow_class. tv. am. am. app mor_id. am. am. Qed. Lemma fmor_qdotted_quot_id : forall r f x, cat_equiv_rel (source f) r -> compatible r f -> ob (source f) x -> fmor (qdotted r f) (quot_id (source f) r x) = id (target f) (fob f x). Proof. ir. uf quot_id. rw fmor_qdotted_arrow_class. rw fmor_id. tv. uh H0; ee; am. tv. am. am. am. app mor_id. Qed. Lemma fmor_qdotted_quot_comp : forall r f u v, cat_equiv_rel (source f) r -> compatible r f -> is_quotient_arrow (source f) r u -> is_quotient_arrow (source f) r v -> source u = target v -> fmor (qdotted r f) (quot_comp (source f) r u v) = comp (target f) (fmor (qdotted r f) u) (fmor (qdotted r f) v). Proof. ir. uf quot_comp. rww fmor_qdotted_arrow_class. wr comp_fmor. rww fmor_qdotted. rww fmor_qdotted. uh H0; ee; am. apply mor_arrow_rep with (r:=r). am. apply mor_arrow_rep with (r:=r). am. rewrite source_arrow_rep with (a:=source f) (r:=r). rewrite target_arrow_rep with (a:=source f) (r:=r). am. am. am. rww mor_comp. apply mor_arrow_rep with (r:=r). am. apply mor_arrow_rep with (r:=r). am. rewrite source_arrow_rep with (a:=source f) (r:=r). rewrite target_arrow_rep with (a:=source f) (r:=r). am. am. am. Qed. Lemma qdotted_axioms : forall r f, cat_equiv_rel (source f) r -> compatible r f -> Functor.axioms (qdotted r f). Proof. ir. assert (Functor.axioms f). lu. uhg; ee. uf qdotted. uf Functor.create. ap Umorphism.create_like. rw source_qdotted. app quotient_cat_axioms. rw target_qdotted. rww category_axioms_target. ir. rwi source_qdotted H2. rwi ob_quotient_cat H2. rw target_qdotted. rw fob_qdotted. app ob_fob. am. am. am. am. ir. rwi source_qdotted H2. rwi ob_quotient_cat H2. rw target_qdotted. rw fob_qdotted. rw source_qdotted. rw id_quotient_cat. rw fmor_qdotted_quot_id. tv. am. am. am. am. am. am. am. am. am. ir. rwi source_qdotted H2. rwi mor_quotient_cat H2. rw target_qdotted. rw fmor_qdotted. ap mor_fmor. am. apply mor_arrow_rep with (r:=r). am. am. am. am. (** the following section of the proof might provide an example of why we need an untyped environment: we are proving a statement about compatibility with target; in the usual type-theory version of category theory this could well be part of the typing information, so the proof paragraph which is somewhat complicated would be what you would have to do to show (maybe later) that something is well-typed. **************************) ir. rwi source_qdotted H2. rwi mor_quotient_cat H2. rw fob_qdotted. rw fmor_qdotted. rw source_fmor. rewrite source_arrow_rep with (a:=source f) (r:=r). tv. am. am. apply mor_arrow_rep with (r:=r). am. am. am. am. am. uh H2; ee. nin H3; ee. rw H4. rw source_arrow_class. rww ob_source. am. ir. rwi source_qdotted H2. rwi mor_quotient_cat H2. rw fob_qdotted. rw fmor_qdotted. rw target_fmor. rewrite target_arrow_rep with (a:=source f) (r:=r). tv. am. am. apply mor_arrow_rep with (r:=r). am. am. am. am. am. uh H2; ee. nin H3; ee. rw H4. rw target_arrow_class. rww ob_target. am. ir. rwi source_qdotted H2. rwi mor_quotient_cat H2. rwi source_qdotted H3. rwi mor_quotient_cat H3. rw target_qdotted. sy. rw source_qdotted. rw comp_quotient_cat. rw fmor_qdotted_quot_comp. tv. am. am. am. am. am. am. am. am. am. am. am. Qed. Lemma eq_fcompose_qdotted_qprojection : forall r f, cat_equiv_rel (source f) r -> compatible r f -> f = fcompose (qdotted r f) (qprojection (source f) r). Proof. ir. apply Functor.axioms_extensionality. lu. ap fcompose_axioms. ap qdotted_axioms. am. am. ap qprojection_axioms. am. rw source_qdotted. rw target_qprojection. tv. rw source_fcompose. rw source_qprojection. tv. rw target_fcompose. rw target_qdotted. tv. ir. rw fmor_fcompose. assert (fmor (qprojection (source f) r) u = arrow_class r u). rww fmor_qprojection. rw H2. rw fmor_qdotted_arrow_class. tv. am. am. am. app qdotted_axioms. app qprojection_axioms. rw source_qdotted. rw target_qprojection. tv. rw source_qprojection. am. Qed. Lemma compatible_fcompose_qprojection : forall a r f, Functor.axioms f -> cat_equiv_rel a r -> source f = quotient_cat a r -> compatible r (fcompose f (qprojection a r)). Proof. ir. rw compatible_rw; ee. ap fcompose_axioms. am. app qprojection_axioms. rww target_qprojection. rw source_fcompose. rw source_qprojection. lu. ir. assert (mor a x). uh H0; ee. uh H0; ee. apply H7 with y; am. assert (mor a y). uh H0; ee. uh H0; ee. apply H9 with x; am. rw fmor_fcompose. sy; rw fmor_fcompose. rw fmor_qprojection. rw fmor_qprojection. rewrite related_arrow_class_eq with (a:=a) in H2. rw H2. tv. am. am. am. am. am. app qprojection_axioms. rww target_qprojection. rww source_qprojection. am. app qprojection_axioms. rww target_qprojection. rww source_qprojection. Qed. (** the following gives unicity for qdotted **) Lemma eq_qdotted : forall a r f, Functor.axioms f -> cat_equiv_rel a r -> source f = quotient_cat a r -> f = qdotted r (fcompose f (qprojection a r)). Proof. ir. ap Functor.axioms_extensionality. am. ap qdotted_axioms. rw source_fcompose. rww source_qprojection. app compatible_fcompose_qprojection. rw source_qdotted. rw source_fcompose. rw source_qprojection. am. rw target_qdotted. rw target_fcompose. tv. ir. rw fmor_qdotted. rw fmor_fcompose. rw fmor_qprojection_arrow_rep. tv. rwi H1 H2. rwi mor_quotient_cat H2. am. am. am. app qprojection_axioms. rww target_qprojection. rw source_qprojection. apply mor_arrow_rep with (a:=a)(r:=r). rwi H1 H2. rwi mor_quotient_cat H2. am. am. rw source_fcompose. rww source_qprojection. rw source_fcompose. rww source_qprojection. rwi H1 H2. rwi mor_quotient_cat H2. am. am. Qed. End Quotient_Functor. Module Ob_Iso_Functor. Export Functor_Cat. Export Quotient_Functor. (** We study the situation of a functor f which is an isomorphism on objects; in particular we look at the morphism it induces on functor categories. This will allow us, for now, to skip talking about natural transformations to and from quotient categories. Eventually of course it would be desireable to have that theory too. **) Definition pull_morphism a f := Functor.create (functor_cat (target f) a) (functor_cat (source f) a) (fun u => htrans_right u f). Lemma source_pull_morphism : forall f a, source (pull_morphism a f) = (functor_cat (target f) a). Proof. ir. uf pull_morphism. rw Functor.source_create. tv. Qed. Lemma target_pull_morphism : forall f a, target (pull_morphism a f) = (functor_cat (source f) a). Proof. ir. uf pull_morphism. rw Functor.target_create. tv. Qed. Lemma fmor_pull_morphism : forall f a u, mor (functor_cat (target f) a) u -> fmor (pull_morphism a f) u = htrans_right u f. Proof. ir. uf pull_morphism. rw fmor_create. tv. am. Qed. Lemma fob_pull_morphism : forall f a y, Functor.axioms f -> Category.axioms a -> ob (functor_cat (target f) a) y -> fob (pull_morphism a f) y = fcompose y f. Proof. ir. assert (Category.axioms (target f)). uh H; ee; am. uf fob. rw fmor_pull_morphism. rw source_htrans_right. rw source_pull_morphism. rw id_functor_cat. rw source_vident. tv. am. am. am. rw source_pull_morphism. app mor_id. Qed. Lemma pull_morphism_axioms : forall f a, Functor.axioms f -> Category.axioms a -> Functor.axioms (pull_morphism a f). Proof. ir. assert (Category.axioms (source f)). uh H; ee; am. assert (Category.axioms (target f)). uh H; ee; am. uhg; ee. uf pull_morphism; uf Functor.create; ap Umorphism.create_like. rw source_pull_morphism. app functor_cat_axioms. rw target_pull_morphism. app functor_cat_axioms. ir. rwi source_pull_morphism H3. cp H3. rwi ob_functor_cat H4. uh H4; ee. rw target_pull_morphism. rw fob_pull_morphism. rww ob_functor_cat. uhg; ee. app fcompose_axioms. rww source_fcompose. rww target_fcompose. am. am. am. am. am. ir. rwi source_pull_morphism H3. cp H3. rwi ob_functor_cat H4. uh H4; ee. rw target_pull_morphism. rw fob_pull_morphism. rw source_pull_morphism. rw fmor_pull_morphism. rw id_functor_cat. rw id_functor_cat. sy. rw htrans_right_vident. reflexivity. am. am. am. am. am. am. am. am. rw ob_functor_cat. uhg; ee. app fcompose_axioms. rww source_fcompose. rww target_fcompose. am. am. rw id_functor_cat. rw mor_functor_cat. uhg; ee. rww vident_axioms. rww osource_vident. rww otarget_vident. am. am. am. am. am. am. am. am. am. am. ir. rwi source_pull_morphism H3. cp H3. rwi mor_functor_cat H4. uh H4; ee. rw target_pull_morphism. rw fmor_pull_morphism. rw mor_functor_cat. uhg; ee. app htrans_right_axioms. rww osource_htrans_right. rww otarget_htrans_right. am. am. am. am. am. ir. rwi source_pull_morphism H3. cp H3. rwi mor_functor_cat H4. uh H4; ee. rw fmor_pull_morphism. rw fob_pull_morphism. rw source_htrans_right. tv. am. am. rww ob_source. am. am. am. ir. rwi source_pull_morphism H3. cp H3. rwi mor_functor_cat H4. uh H4; ee. rw fmor_pull_morphism. rw fob_pull_morphism. rw target_htrans_right. tv. am. am. rww ob_target. am. am. am. ir. rwi source_pull_morphism H3. rwi source_pull_morphism H4. cp H3; cp H4. rwi mor_functor_cat H6. uh H6; ee. rwi mor_functor_cat H7. uh H7; ee. rw target_pull_morphism. sy; rw source_pull_morphism. rw comp_functor_cat. rw comp_functor_cat. rw fmor_pull_morphism. sy. rw fmor_pull_morphism. rw fmor_pull_morphism. rw vcompose_htrans_right_htrans_right. tv. am. am. am. tv. am. sy; am. am. am. rw mor_functor_cat. uhg; ee. rww vcompose_axioms. rww osource_vcompose. rww otarget_vcompose. am. am. am. am. rw mor_functor_cat. rw fmor_pull_morphism. uhg; ee. app htrans_right_axioms. rww osource_htrans_right. rww otarget_htrans_right. am. am. am. rw mor_functor_cat. rw fmor_pull_morphism. uhg; ee. app htrans_right_axioms. rww osource_htrans_right. rww otarget_htrans_right. am. am. am. rw fmor_pull_morphism. rw fmor_pull_morphism. rww source_htrans_right. rw target_htrans_right. rww H5. am. am. am. am. am. am. am. am. am. am. am. Qed. Definition faithful f := Functor.axioms f & (forall u v, related (ker f) u v -> u = v). Definition says f x := Functor.axioms f & (exists y, (ob (source f) y & fob f y = x)). Definition msays f u := Functor.axioms f & (exists y, (mor (source f) y & fmor f y = u)). Definition full f := Functor.axioms f & (forall u, mor (target f) u -> says f (source u) -> says f (target u) -> msays f u). Definition ob_inj f := Functor.axioms f & (forall x y, ob (source f) x -> ob (source f) y -> fob f x = fob f y -> x = y). Definition iso_to_full_subcategory f := faithful f & full f & ob_inj f. Definition ob_image f := Z (objects (target f)) (fun x => (exists y, (ob (source f) y & fob f y = x))). Definition ob_surj f := Functor.axioms f & (forall x, ob (target f) x -> says f x). Definition ob_iso f := ob_inj f & ob_surj f. Lemma has_finverse_rw : forall f, has_finverse f = (faithful f & full f & ob_iso f). Proof. ir. ap iff_eq; ir. uh H. nin H. uh H; ee. uhg; ee. am. ir. rwi related_ker H5. ee. transitivity (fmor x (fmor f u)). wr fmor_fcompose. rw H4. rw fmor_fidentity. tv. am. am. am. am. am. rw H9. wrr fmor_fcompose. rw H4. rww fmor_fidentity. am. uhg; ee. am. ir. uhg; ee. am. sh (fmor x u). ee. rw H1. app mor_fmor. rww H2. wrr fmor_fcompose. rw H3. rww fmor_fidentity. rww H2. rww H2. uhg. ee. uhg; ee. am. ir. transitivity (fob x (fob f x0)). wrr fob_fcompose. rw H4. rww fob_fidentity. rw H7. wrr fob_fcompose. rw H4. rww fob_fidentity. uhg; ee; try am. ir. uhg; ee. am. sh (fob x x0). ee. rw H1. app ob_fob. rww H2. wrr fob_fcompose. rw H3. rww fob_fidentity. rww H2. rww H2. ee. uh H; uh H0; uh H1; ee. uh H1; uh H2; ee. clear H0 H1 H2. set (gmprop := fun x => fun y => (mor (source f) y & fmor f y = x)). set (gm := fun x => choose (gmprop x)). assert (lem1 : forall x, mor (target f) x -> ex (gmprop x)). ir. assert (msays f x). ap H3. am. ap H5. rww ob_source. ap H5. rww ob_target. uh H1; ee. am. assert (lem2 : forall x, mor (target f) x -> (mor (source f) (gm x) & fmor f (gm x) = x)). ir. change (gmprop x (gm x)). uf gm. ap choose_pr. app lem1. set (gobprop := fun x => fun y => (ob (source f) y & fob f y = x)). set (gob := fun x => choose (gobprop x)). assert (lem3 : forall x, ob (target f) x -> ex (gobprop x)). ir. assert (says f x). ap H5. am. uh H1; ee. am. assert (lem4 : forall x, ob (target f) x -> (ob (source f) (gob x) & fob f (gob x) = x)). ir. change (gobprop x (gob x)). uf gob. ap choose_pr. app lem3. assert (source_gm : forall u, mor (target f) u -> source (gm u) = gob (source u)). ir. cp (lem2 _ H0); ee. assert (ob (target f) (source u)). rww ob_source. cp (lem4 _ H7). ee. ap H6. rww ob_source. am. rw H9. wr source_fmor. rw H2. tv. am. am. assert (target_gm : forall u, mor (target f) u -> target (gm u) = gob (target u)). ir. cp (lem2 _ H0); ee. assert (ob (target f) (target u)). rww ob_target. cp (lem4 _ H7). ee. ap H6. rww ob_target. am. rw H9. wr target_fmor. rw H2. tv. am. am. assert (id_gob : forall x, ob (target f) x -> id (source f) (gob x) = gm (id (target f) x)). ir. ap H4. cp (lem4 _ H0); ee. rw related_ker. ee. app mor_id. assert (mor (target f) (id (target f) x)). app mor_id. cp (lem2 _ H7). ee; am. rw source_gm. rww source_id. rww source_id. app mor_id. rww target_id. rww target_gm. rww target_id. app mor_id. rw fmor_id. rw H2. assert (mor (target f) (id (target f) x)). app mor_id. cp (lem2 _ H7). ee. sy; am. am. tv. am. am. assert (comp_gm : forall u v, mor (target f) u -> mor (target f) v -> source u = target v -> comp (source f) (gm u) (gm v) = gm (comp (target f) u v)). ir. cp (lem2 _ H0); cp (lem2 _ H1); ee. assert (mor (target f) (comp (target f) u v)). rww mor_comp. cp (lem2 _ H11). ee. ap H4. rw related_ker. ee. rww mor_comp. rww source_gm; rww target_gm. rww H2. am. rww source_comp. rww source_gm. rww source_gm. rww source_comp. rww source_gm. rww target_gm. rww H2. rww target_comp. rww target_gm. rww target_gm. rww target_comp. rww source_gm. rww target_gm. rww H2. wrr comp_fmor. rw H13. rw H10; rw H9. tv. rw source_gm. rw target_gm. rww H2. am. am. am. uhg. sh (Functor.create (target f) (source f) gm). uhg; dj. am. ap Functor.create_axioms. sh gob. uhg; ee. rww category_axioms_target. rww category_axioms_source. ir. cp (lem4 _ H1); ee; am. ir. app id_gob. ir. cp (lem2 _ H1); ee; am. ir. rww source_gm. ir. rww target_gm. ir. rww comp_gm. rww Functor.target_create. rww Functor.source_create. (** composition in one direction **) ap Functor.axioms_extensionality. ap fcompose_axioms. am. am. am. rw fidentity_axioms. tv. rw Functor.source_create. rww category_axioms_target. rw source_fcompose. rw Functor.source_create. rw source_fidentity. tv. rw target_fcompose. rw target_fidentity. rww Functor.source_create. ir. rwi Functor.source_create H7. rwi source_fcompose H8. rwi Functor.source_create H8. cp (lem2 _ H8); ee. rw fmor_fcompose. rw fmor_create. rw fmor_fidentity. am. rw Functor.source_create. am. am. am. am. rww Functor.target_create. rww Functor.source_create. (** composition in the other direction **) ap Functor.axioms_extensionality. ap fcompose_axioms. am. am. am. rw fidentity_axioms. tv. rww category_axioms_source. rw source_fcompose. rw source_fidentity. tv. rw target_fcompose. rw target_fidentity. rww Functor.target_create. ir. rwi Functor.source_create H7. rwi source_fcompose H9. rwi Functor.source_create H8. rw fmor_fcompose. rw fmor_create. rw fmor_fidentity. ap H4. assert (mor (target f) (fmor f u)). app mor_fmor. cp (lem2 _ H10); ee. rw related_ker. ee. am. am. rww source_gm. rww source_fmor. assert (ob (target f) (fob f (source u))). app ob_fob. rww ob_source. cp (lem4 _ H13); ee. app H6. rww ob_source. rww target_gm. rww target_fmor. assert (ob (target f) (fob f (target u))). app ob_fob. rww ob_target. cp (lem4 _ H13); ee. app H6. rww ob_target. am. am. am. app mor_fmor. am. am. rww Functor.source_create. am. Qed. Definition is_full_subcategory a b := is_subcategory a b & (forall u, mor b u -> ob a (source u) -> ob a (target u) -> mor a u). Definition full_subcategory (a:E) (obp : E -> Prop) := subcategory a obp (fun u => (obp (source u) & obp (target u))). Lemma full_subcategory_property : forall a obp, Category.axioms a -> subcategory_property a obp (fun u => (obp (source u) & obp (target u))). Proof. ir. uhg; ee. am. ir. ee. rww source_comp. rww target_comp. ir. ee. rww source_id. rww target_id. ir. ee; am. ir. ee; am. Qed. Lemma full_subcategory_axioms : forall a obp, Category.axioms a -> Category.axioms (full_subcategory a obp). Proof. ir. uf full_subcategory. ap subcategory_axioms. ap full_subcategory_property. am. Qed. Lemma is_subcategory_full_subcategory : forall a obp, Category.axioms a -> is_subcategory (full_subcategory a obp) a. Proof. ir. uf full_subcategory. ap subcategory_is_subcategory. ap full_subcategory_property. am. Qed. Lemma ob_full_subcategory : forall a obp x, axioms a -> ob (full_subcategory a obp) x = (ob a x & obp x). Proof. ir. uf full_subcategory. rw ob_subcategory. tv. app full_subcategory_property. Qed. Lemma mor_full_subcategory : forall a obp u, axioms a -> mor (full_subcategory a obp) u = (mor a u & obp (source u) & obp (target u)). Proof. ir. uf full_subcategory. rw mor_subcategory. tv. app full_subcategory_property. Qed. Lemma id_full_subcategory : forall a obp x, axioms a -> ob (full_subcategory a obp) x -> id (full_subcategory a obp) x = id a x. Proof. ir. uf full_subcategory. rww id_subcategory. app full_subcategory_property. rwi ob_full_subcategory H0; ee; am. rwi ob_full_subcategory H0; ee; am. Qed. Lemma comp_full_subcategory : forall a obp u v, axioms a -> mor (full_subcategory a obp) u -> mor (full_subcategory a obp) v -> source u = target v -> comp (full_subcategory a obp) u v = comp a u v. Proof. ir. uf full_subcategory. rwi mor_full_subcategory H0. rwi mor_full_subcategory H1. ee. rww comp_subcategory. app full_subcategory_property. ee; am. ee; am. am. am. Qed. Lemma is_full_subcategory_full_subcategory : forall a obp, Category.axioms a -> is_full_subcategory (full_subcategory a obp) a. Proof. ir. uhg; ee. app is_subcategory_full_subcategory. ir. rwi ob_full_subcategory H1. rwi ob_full_subcategory H2; ee. rww mor_full_subcategory; ee; am. am. am. Qed. Definition subcategory_inclusion a b := Functor.create a b (fun u => u). Lemma source_subcategory_inclusion : forall a b, source (subcategory_inclusion a b) = a. Proof. ir. uf subcategory_inclusion. rww Functor.source_create. Qed. Lemma target_subcategory_inclusion : forall a b, target (subcategory_inclusion a b) = b. Proof. ir. uf subcategory_inclusion. rww Functor.target_create. Qed. Lemma fmor_subcategory_inclusion : forall a b u, is_subcategory a b -> mor a u -> fmor (subcategory_inclusion a b) u = u. Proof. ir. uf subcategory_inclusion. rww fmor_create. Qed. Lemma fob_subcategory_inclusion : forall a b x, is_subcategory a b -> ob a x -> fob (subcategory_inclusion a b) x = x. Proof. ir. uf subcategory_inclusion. rw fob_create. rww source_id. am. Qed. Lemma subcategory_inclusion_axioms : forall a b, is_subcategory a b -> Functor.axioms (subcategory_inclusion a b). Proof. ir. uf subcategory_inclusion. uh H; ee. ap Functor.create_axioms. sh (fun x:E => x). uhg; ee. am. am. am. ir; sy; au. am. ir; tv. ir; tv. ir. rww H4. Qed. Lemma faithful_subcategory_inclusion : forall a b, is_subcategory a b -> faithful (subcategory_inclusion a b). Proof. ir. uhg; ee. app subcategory_inclusion_axioms. uh H; ee. ir. rwi related_ker H6; ee. rwi source_subcategory_inclusion H6. rwi source_subcategory_inclusion H7. rwi fmor_subcategory_inclusion H10. rwi fmor_subcategory_inclusion H10. am. uhg; ee; am. am. uhg; ee; am. am. ap subcategory_inclusion_axioms. uhg; ee; am. Qed. Lemma ob_inj_subcategory_inclusion : forall a b, is_subcategory a b -> ob_inj (subcategory_inclusion a b). Proof. ir. uhg. ee. app subcategory_inclusion_axioms. ir. rwi source_subcategory_inclusion H0; rwi source_subcategory_inclusion H1; ee. rwi fob_subcategory_inclusion H2. rwi fob_subcategory_inclusion H2. am. am. am. am. am. Qed. Lemma full_subcategory_inclusion : forall a b, is_full_subcategory a b -> full (subcategory_inclusion a b). Proof. ir. uh H; ee. uhg; ee. app subcategory_inclusion_axioms. ir. rwi target_subcategory_inclusion H1. uhg; ee. app subcategory_inclusion_axioms. sh u. ee. rw source_subcategory_inclusion. app H0. uh H2; ee. nin H4. ee. rwi source_subcategory_inclusion H4. rwi fob_subcategory_inclusion H5. wrr H5. am. am. uh H3; ee. nin H4. ee. rwi source_subcategory_inclusion H4. rwi fob_subcategory_inclusion H5. wrr H5. am. am. rww fmor_subcategory_inclusion. app H0. uh H2; ee. nin H4. ee. rwi source_subcategory_inclusion H4. rwi fob_subcategory_inclusion H5. wrr H5. am. am. uh H3; ee. nin H4. ee. rwi source_subcategory_inclusion H4. rwi fob_subcategory_inclusion H5. wrr H5. am. am. Qed. Lemma is_full_subcategory_rw : forall a b, is_full_subcategory a b = (is_subcategory a b & full (subcategory_inclusion a b)). Proof. ir. ap iff_eq; ir. ee. uh H; ee; am. app full_subcategory_inclusion. ee. uhg; ee; try am. ir. uh H0; ee. assert (msays (subcategory_inclusion a b) u). ap H4. rww target_subcategory_inclusion. uhg; ee. app subcategory_inclusion_axioms. sh (source u). ee. rww source_subcategory_inclusion. rww fob_subcategory_inclusion. uhg; ee. app subcategory_inclusion_axioms. sh (target u). ee. rww source_subcategory_inclusion. rww fob_subcategory_inclusion. uh H5; ee. nin H6; ee. rwi source_subcategory_inclusion H6. rwi fmor_subcategory_inclusion H7. wrr H7. am. am. Qed. Definition ob_image_fs f := full_subcategory (target f) (fun x => inc x (ob_image f)). Lemma is_subcategory_ob_image_fs : forall f, Functor.axioms f -> is_subcategory (ob_image_fs f) (target f). Proof. ir. uf ob_image_fs. app is_subcategory_full_subcategory. rww category_axioms_target. Qed. Lemma is_full_subcategory_ob_image_fs : forall f, Functor.axioms f -> is_full_subcategory (ob_image_fs f) (target f). Proof. ir. uf ob_image_fs. app is_full_subcategory_full_subcategory. rww category_axioms_target. Qed. Lemma inc_ob_image : forall f x, Functor.axioms f -> inc x (ob_image f) = (exists y, (ob (source f) y & fob f y = x)). Proof. ir. ap iff_eq; ir. ufi ob_image H0. Ztac. uf ob_image. Ztac. ap ob_is_ob. nin H0. ee. wr H1. app ob_fob. Qed. Lemma ob_ob_image_fs : forall f x, Functor.axioms f -> ob (ob_image_fs f) x = inc x (ob_image f). Proof. ir. ap iff_eq; ir. ufi ob_image_fs H0. rwi ob_full_subcategory H0. ee. am. rwi ob_full_subcategory H0. rww category_axioms_target. rww category_axioms_target. uf ob_image_fs. rw ob_full_subcategory. ee. rwi inc_ob_image H0. nin H0; ee. wr H1. app ob_fob. am. am. rww category_axioms_target. Qed. Lemma mor_ob_image_fs : forall f u, Functor.axioms f -> mor (ob_image_fs f) u = (mor (target f) u & inc (source u) (ob_image f) & inc (target u) (ob_image f)). Proof. ir. ap iff_eq; ir. ufi ob_image_fs H0. rwi mor_full_subcategory H0. xd. rww category_axioms_target. uf ob_image_fs. rw mor_full_subcategory; xd. rww category_axioms_target. Qed. Definition ob_image_factor f := Functor.create (source f) (ob_image_fs f) (fmor f). Lemma source_ob_image_factor : forall f, source (ob_image_factor f) = source f. Proof. ir. uf ob_image_factor. rww Functor.source_create. Qed. Lemma target_ob_image_factor : forall f, target (ob_image_factor f) = ob_image_fs f. Proof. ir. uf ob_image_factor. rww Functor.target_create. Qed. Lemma fmor_ob_image_factor : forall f u, Functor.axioms f -> mor (source f) u -> fmor (ob_image_factor f) u = fmor f u. Proof. ir. uf ob_image_factor. rww fmor_create. Qed. Lemma fob_ob_image_factor : forall f x, Functor.axioms f -> ob (source f) x -> fob (ob_image_factor f) x = fob f x. Proof. ir. uf ob_image_factor. rww fob_create. Qed. Lemma ob_image_factor_axioms : forall f, Functor.axioms f -> Functor.axioms (ob_image_factor f). Proof. ir. uf ob_image_factor. assert (is_full_subcategory (ob_image_fs f) (target f)). app is_full_subcategory_ob_image_fs. uh H0; ee. uh H0; ee. ap Functor.create_axioms. sh (fob f). uhg; ee. rww category_axioms_source. am. ir. uf ob_image_fs. rw ob_full_subcategory. ee. app ob_fob. uf ob_image. Ztac. ap ob_is_ob. app ob_fob. sh x; ee. am. tv. rww category_axioms_target. ir. rw H7. rww fmor_id. rw ob_ob_image_fs. rw inc_ob_image. sh x; ee. am. tv. am. am. ir. rw mor_ob_image_fs. ee. app mor_fmor. rw inc_ob_image. sh (source u). ee. rww ob_source. rww source_fmor. am. rw inc_ob_image. sh (target u). ee. rww ob_target. rww target_fmor. am. am. ir. rww source_fmor. ir. rww target_fmor. ir. uf ob_image_fs. rww comp_full_subcategory. rww comp_fmor. rw mor_full_subcategory. ee. app mor_fmor. rw inc_ob_image. sh (source u). ee. rww ob_source. rww source_fmor. am. rw inc_ob_image. sh (target u). ee. rww ob_target. rww target_fmor. am. am. rw mor_full_subcategory. ee. app mor_fmor. rw inc_ob_image. sh (source v). ee. rww ob_source. rww source_fmor. am. rw inc_ob_image. sh (target v). ee. rww ob_target. rww target_fmor. am. am. rww source_fmor. rww target_fmor. rww H10. Qed. Lemma ob_image_factorization : forall f, Functor.axioms f -> f = fcompose (subcategory_inclusion (ob_image_fs f) (target f)) (ob_image_factor f). Proof. ir. cp (ob_image_factor_axioms H). cp (is_full_subcategory_ob_image_fs H). cp H1. uh H2. ee. cp H2. uh H4; ee. ap Functor.axioms_extensionality. am. ap fcompose_axioms. app subcategory_inclusion_axioms. app ob_image_factor_axioms. rww source_subcategory_inclusion. rww target_ob_image_factor. rww source_fcompose. rww source_ob_image_factor. rww target_fcompose. rww target_subcategory_inclusion. ir. rw fmor_fcompose. rw fmor_subcategory_inclusion. rw fmor_ob_image_factor. tv. am. am. am. assert (ob_image_fs f = target (ob_image_factor f)). rww target_ob_image_factor. rw H12. ap mor_fmor. am. rww source_ob_image_factor. app subcategory_inclusion_axioms. am. rww source_subcategory_inclusion. rww target_ob_image_factor. rww source_ob_image_factor. Qed. Lemma ob_surj_ob_image_factor : forall f, Functor.axioms f -> ob_surj (ob_image_factor f). Proof. ir. uhg; ee. app ob_image_factor_axioms. ir. rwi target_ob_image_factor H0. rwi ob_ob_image_fs H0. rwi inc_ob_image H0; nin H0; ee. uhg; ee. app ob_image_factor_axioms. sh x0. ee. rww source_ob_image_factor. rww fob_ob_image_factor. am. am. Qed. Lemma ob_inj_ob_image_factor : forall f, Functor.axioms f -> ob_inj (ob_image_factor f) = ob_inj f. Proof. ir. ap iff_eq; ir. uh H0; ee. uhg; ee; try am. ir. ap H1. rww source_ob_image_factor. rww source_ob_image_factor. rww fob_ob_image_factor. rww fob_ob_image_factor. uh H0; ee. uhg; ee. app ob_image_factor_axioms. ir. ap H1. wrr source_ob_image_factor. wrr source_ob_image_factor. wrr fob_ob_image_factor. sy. wrr fob_ob_image_factor. sy; am. wrr source_ob_image_factor. wrr source_ob_image_factor. Qed. Lemma ob_iso_ob_image_factor : forall f, Functor.axioms f -> ob_iso (ob_image_factor f) = ob_inj f. Proof. ir. ap iff_eq; ir. uh H0; ee. rwi ob_inj_ob_image_factor H0. am. am. uhg; ee. rww ob_inj_ob_image_factor. app ob_surj_ob_image_factor. Qed. Lemma full_ob_image_factor : forall f, Functor.axioms f -> full (ob_image_factor f) = full f. Proof. ir. ap iff_eq; ir. uh H0; ee. uhg; ee. am. ir. assert (inc (source u) (ob_image f)). uh H3; ee. rw inc_ob_image. am. am. assert (inc (target u) (ob_image f)). uh H4; ee. rw inc_ob_image. am. am. assert (msays (ob_image_factor f) u). ap H1. rww target_ob_image_factor. rw mor_ob_image_fs. ee. am. am. am. am. uhg; ee. am. uh H3; ee. nin H7. sh x; ee. rww source_ob_image_factor. rww fob_ob_image_factor. uhg; ee. am. uh H4; ee. nin H7. sh x; ee. rww source_ob_image_factor. rww fob_ob_image_factor. uh H7; ee. nin H8; ee. uhg; ee. am. sh x. ee. wrr source_ob_image_factor. wrr fmor_ob_image_factor. wrr source_ob_image_factor. uh H0; ee. uhg; ee. app ob_image_factor_axioms. ir. uhg; ee. app ob_image_factor_axioms. rwi target_ob_image_factor H2. rwi mor_ob_image_fs H2. ee. rwi inc_ob_image H5. rwi inc_ob_image H6. nin H5; nin H6; ee. assert (msays f u). app H1. uhg; ee. am. sh x; ee; am. uhg; ee. am. sh x0; ee; am. uh H9; ee. nin H10; ee. sh x1. ee. rww source_ob_image_factor. rww fmor_ob_image_factor. am. am. am. Qed. Lemma faithful_ob_image_factor : forall f, Functor.axioms f -> faithful (ob_image_factor f) = faithful f. Proof. ir. ap iff_eq; ir. uh H0; uhg; ee. am. ir. rwi related_ker H2. ee. ap H1. rw related_ker. ee. rww source_ob_image_factor. rww source_ob_image_factor. am. am. rww fmor_ob_image_factor. rww fmor_ob_image_factor. app ob_image_factor_axioms. am. uh H0; uhg; ee. app ob_image_factor_axioms. ir. rwi related_ker H2. ee. ap H1. rw related_ker. ee. rwi source_ob_image_factor H2. am. rwi source_ob_image_factor H3. am. am. am. rwi fmor_ob_image_factor H6. rwi fmor_ob_image_factor H6. am. am. rwi source_ob_image_factor H3. am. am. rwi source_ob_image_factor H2. am. am. app ob_image_factor_axioms. Qed. Lemma iso_to_full_subcategory_rw : forall f, iso_to_full_subcategory f = (Functor.axioms f & has_finverse (ob_image_factor f)). Proof. ir. ap iff_eq; ir. dj. uh H; ee. uh H; ee; am. rw has_finverse_rw. uh H; ee. rww faithful_ob_image_factor. rww full_ob_image_factor. rww ob_iso_ob_image_factor. ee. rwi has_finverse_rw H0. ee. rwi faithful_ob_image_factor H0. rwi full_ob_image_factor H1. rwi ob_iso_ob_image_factor H2. uhg; ee; try am. am. am. am. Qed. Lemma subcategory_extensionality : forall a b c, is_subcategory a c -> is_subcategory b c -> (forall u, mor a u -> mor b u) -> (forall u, mor b u -> mor a u) -> a = b. Proof. ir. assert (forall x, ob a x -> ob b x). ir. assert (x = source (id a x)). rww source_id. assert (mor b (id a x)). app H1. app mor_id. rw H4. rww ob_source. assert (forall x, ob b x -> ob a x). ir. assert (x = source (id b x)). rww source_id. assert (mor a (id b x)). app H2. app mor_id. rw H5. rww ob_source. assert (mor a = mor b). ap arrow_extensionality. ir. ap iff_eq; ir; au. assert (ob a = ob b). ap arrow_extensionality. ir. ap iff_eq; ir; au. cp (is_subcategory_eq H). cp (is_subcategory_eq H0). wr H7; wr H8. rw H5; rww H6. Qed. Lemma full_subcategory_extensionality : forall a b c, is_full_subcategory a c -> is_full_subcategory b c -> (forall x, ob a x -> ob b x) -> (forall x, ob b x -> ob a x) -> a = b. Proof. ir. apply subcategory_extensionality with c. uh H; ee; am. uh H0; ee; am. ir. uh H; uh H0; ee. ap H4. uh H; ee. app H9. ap H1. rww ob_source. ap H1. rww ob_target. ir. uh H; uh H0; ee. ap H5. uh H0; ee. app H9. ap H2. rww ob_source. ap H2. rww ob_target. Qed. Lemma iso_to_full_subcategory_interp :forall f, iso_to_full_subcategory f = (exists g, (is_full_subcategory (target g) (target f) & has_finverse g & f = fcompose (subcategory_inclusion (target g) (target f)) g)). Proof. ir. ap iff_eq; ir. sh (ob_image_factor f). ee. rw target_ob_image_factor. ap is_full_subcategory_ob_image_fs. uh H; ee. uh H; ee; am. rwi iso_to_full_subcategory_rw H. ee; am. rw target_ob_image_factor. ap ob_image_factorization. uh H; ee; uh H; ee; am. nin H; ee. assert (Functor.axioms x). uh H0; ee. nin H0. uh H0; ee. am. assert (Functor.axioms f). rw H1. app fcompose_axioms. app subcategory_inclusion_axioms. uh H; ee; am. rww source_subcategory_inclusion. assert (source f = source x). rw H1. rww source_fcompose. assert (x = ob_image_factor f). ap Functor.axioms_extensionality. am. app ob_image_factor_axioms. rww source_ob_image_factor. sy; am. rw target_ob_image_factor. apply full_subcategory_extensionality with (target f). am. ap is_full_subcategory_ob_image_fs. am. ir. rww ob_ob_image_fs. rw inc_ob_image. rwi has_finverse_rw H0. ee. uh H7; ee. uh H8; ee. cp (H9 _ H5). uh H10; ee. nin H11. ee. sh x1. ee. rww H4. rw H1. rww fob_fcompose. rww fob_subcategory_inclusion. uh H; ee; am. rww H12. app subcategory_inclusion_axioms. uh H; ee; am. rww source_subcategory_inclusion. am. ir. rwi ob_ob_image_fs H5. rwi inc_ob_image H5. nin H5; ee. rwi H1 H6. rwi fob_fcompose H6. rwi fob_subcategory_inclusion H6. wr H6. app ob_fob. wrr H4. uh H; ee; am. app ob_fob. wrr H4. ap subcategory_inclusion_axioms. uh H; ee; am. am. rww source_subcategory_inclusion. wrr H4. am. am. ir. rw fmor_ob_image_factor. rw H1. rww fmor_fcompose. rww fmor_subcategory_inclusion. uh H; ee; am. app mor_fmor. ap subcategory_inclusion_axioms. uh H; ee; am. rww source_subcategory_inclusion. am. rww H4. rw iso_to_full_subcategory_rw. ee. am. wrr H5. Qed. Definition mor_image f := Z (morphisms (target f)) (msays f). Lemma sub_mor_image : forall f, sub (mor_image f) (morphisms (target f)). Proof. ir. uhg; ir. ufi mor_image H. Ztac. Qed. Lemma inc_mor_image : forall f u, Functor.axioms f -> inc u (mor_image f) = (exists v, (mor (source f) v & fmor f v = u)). Proof. ir. ap iff_eq; ir. ufi mor_image H0. Ztac. uh H2. ee. nin H3. ee. sh x; ee; am. uf mor_image. nin H0. ee. ap Z_inc. ap mor_is_mor. wr H1. app mor_fmor. uhg. ee; try am. sh x; ee; am. Qed. Definition add_inverses a s := Z (morphisms a) (fun y => inc y s \/ (invertible a y & inc (inverse a y) s)). Lemma sub_add_inverses_refl : forall a s, sub s (morphisms a) -> sub s (add_inverses a s). Proof. ir. uhg; ir. uf add_inverses. ap Z_inc. app H. app or_introl. Qed. Lemma sub_add_inverses_morphisms : forall a s, sub (add_inverses a s) (morphisms a). Proof. ir. uhg; ir. ufi add_inverses H. Ztac. Qed. Lemma inc_add_inverses : forall a s y, Category.axioms a -> sub s (morphisms a) -> inc y (add_inverses a s) = (mor a y & (inc y s \/ (invertible a y & inc (inverse a y) s))). Proof. ir. ap iff_eq; ir. ufi add_inverses H1; Ztac. ap is_mor_mor. am. am. ee. uf add_inverses. Ztac. ap mor_is_mor. am. Qed. Definition inverse_closed a b := is_subcategory a b & (forall u, mor a u -> invertible b u -> mor a (inverse b u)). Lemma sub_add_inverses : forall a b s, inverse_closed a b -> sub s (morphisms a) -> sub (add_inverses b s) (morphisms a). Proof. ir. uhg; ir. rwi inc_add_inverses H1. ee. nin H2. ap H0. am. uh H; ee. assert (x = inverse b (inverse b x)). rww inverse_inverse. rw H5. ap mor_is_mor. ap H4. ap is_mor_mor. uh H; ee; am. change (inc (inverse b x) (morphisms a)). ap H0. am. uhg; ee. sh x. ap are_inverse_symm. ap invertible_inverse. am. uh H; ee. uh H; ee; am. uh H; ee. uh H; ee. uhg; ir. ap mor_is_mor. ap H6. ap is_mor_mor. am. uhg. ap H0. am. Qed. Definition generates a s := Category.axioms a & sub s (morphisms a) & (forall b, is_subcategory b a -> sub s (morphisms b) -> b = a). Lemma faithful_pull_morphism_criterion : forall f a, Category.axioms a -> ob_surj f -> faithful (pull_morphism a f). Proof. ir. uh H0; ee. uhg; ee. app pull_morphism_axioms. ir. rwi related_ker H2. ee. rwi source_pull_morphism H2. rwi source_pull_morphism H3. cp H2; cp H3. rwi mor_functor_cat H7. rwi mor_functor_cat H8. uh H7; uh H8; ee. rwi fmor_pull_morphism H6. rwi fmor_pull_morphism H6. ap Nat_Trans.axioms_extensionality. am. am. am. am. ir. rwi H11 H13. cp (H1 _ H13). uh H14. ee. nin H15. ee. wr H16. wr ntrans_htrans_right. wr ntrans_htrans_right. rww H6. am. am. am. am. uh H0; ee; am. am. uh H0; ee; am. am. app pull_morphism_axioms. Qed. Definition globular t := (Nat_Trans.like t) & (Category.axioms (osource t)) & (Category.axioms (otarget t)) & (Functor.axioms (source t)) & (Functor.axioms (target t)) & (source (target t)) = (osource t) & (target (source t)) = (otarget t). Definition natural_ob t x := ob (osource t) x & mor (otarget t) (ntrans t x) & source (ntrans t x) = fob (source t) x & target (ntrans t x) = fob (target t) x. Definition natural_mor t u := mor (osource t) u & natural_ob t (source u) & natural_ob t (target u) & comp (otarget t) (ntrans t (target u)) (fmor (source t) u) = comp (otarget t) (fmor (target t) u) (ntrans t (source u)). Lemma nat_trans_axioms_rw : forall t, Nat_Trans.axioms t = (globular t & (forall x, ob (osource t) x -> natural_ob t x) & (forall u, mor (osource t) u -> natural_mor t u)). Proof. ir. ap iff_eq; ir. ee. cp H; uh H; uhg; ee. am. am. am. am. am. am. am. ir. uh H; uhg; ee; au. ir. uh H; uhg; ee; au. assert (ob (osource t) (source u)). rww ob_source. uhg; ee; au. assert (ob (osource t) (target u)). rww ob_target. uhg; ee; au. ee. uh H; ee. uhg; ee; try am. ir. cp (H0 _ H8). uh H9; ee. am. ir. cp (H0 _ H8). uh H9; ee; am. ir. cp (H0 _ H8). uh H9; ee; am. ir. cp (H1 _ H8). uh H9; ee; am. Qed. Lemma natural_mor_comp :forall t u v, globular t -> natural_mor t u -> natural_mor t v -> source u = target v -> natural_mor t (comp (osource t) u v). Proof. ir. uh H0; uh H1; ee. uhg; ee. rw mor_comp. tv. am. am. am. tv. rww source_comp. rw target_comp. am. am. am. am. rw target_comp. rw source_comp. uh H; ee. assert (fmor (source t) (comp (osource t) u v) = comp (otarget t) (fmor (source t) u) (fmor (source t) v)). wr source_source. wr comp_fmor. rw H14. reflexivity. am. am. am. am. assert (fmor (target t) (comp (osource t) u v) = comp (otarget t) (fmor (target t) u) (fmor (target t) v)). wr H13. wr comp_fmor. reflexivity. am. rww H13. rww H13. am. rw H15. rw H16. wr assoc. rw H8. rw assoc. sy. rw assoc. wr H5. wr H2. reflexivity. uf otarget. ap mor_fmor. am. rww H13. uf otarget. ap mor_fmor. am. rww H13. uh H3. ee. am. rw source_fmor. rw target_fmor. rww H2. am. rww H13. am. rww H13. rw source_fmor. uh H3; ee. sy; am. am. rww H13. tv. uf otarget. ap mor_fmor. am. rww H13. uh H6; ee. am. wr H14. ap mor_fmor. am. am. rw source_fmor. uh H6; ee; sy; am. am. rww H13. rw target_fmor. uh H6; ee. rw H18. rww H2. am. am. tv. uh H7; ee. am. wr H14. ap mor_fmor. am. am. wr H14. ap mor_fmor. am. am. rw target_fmor. uh H7; ee; am. am. am. rw source_fmor. rw target_fmor. rw H2. reflexivity. am. am. am. am. tv. am. am. am. am. am. am. Qed. Lemma natural_mor_id : forall t x, globular t -> natural_ob t x -> natural_mor t (id (osource t) x). Proof. ir. uh H0; ee. uh H; ee. uhg; ee. ap mor_id. am. uhg; ee. rw source_id. am. am. rw source_id. am. am. rww source_id. rww source_id. rww target_id. uhg; ee; am. rw target_id. rw source_id. uf osource. rw fmor_id. rw H9. rw right_id. rw source_source. wr H8. rw fmor_id. rw left_id. tv. uf otarget. ap ob_fob. am. rww H8. am. am. tv. am. tv. rww H8. wr H9. app ob_fob. am. am. tv. am. tv. am. am. am. Qed. Lemma natural_ob_source :forall t u, globular t -> natural_mor t u -> natural_ob t (source u). Proof. ir. uh H0; ee; am. Qed. Lemma natural_ob_target : forall t u, globular t -> natural_mor t u -> natural_ob t (target u). Proof. ir. uh H0; ee; am. Qed. Definition naturality_subcategory t := subcategory (osource t) (natural_ob t) (natural_mor t). Lemma is_subcategory_naturality_subcategory : forall t, globular t -> is_subcategory (naturality_subcategory t) (osource t). Proof. ir. uf naturality_subcategory. ap subcategory_is_subcategory. uhg; ee. uh H; ee; am. ir. app natural_mor_comp. ir. app natural_mor_id. ir. app natural_ob_source. ir. app natural_ob_target. Qed. Lemma ob_naturality_subcategory : forall t x, globular t -> ob (naturality_subcategory t) x = natural_ob t x. Proof. ir. uf naturality_subcategory. rw ob_subcategory. ap iff_eq; ir. ee; am. ee. uh H0; ee; am. am. uhg; ee. uh H; ee; am. ir. app natural_mor_comp. ir. app natural_mor_id. ir. app natural_ob_source. ir. app natural_ob_target. Qed. Lemma mor_naturality_subcategory : forall t u, globular t -> mor (naturality_subcategory t) u = natural_mor t u. Proof. ir. uf naturality_subcategory. rw mor_subcategory. ap iff_eq; ir. ee; am. ee. uh H0; ee; am. am. uhg; ee. uh H; ee; am. ir. app natural_mor_comp. ir. app natural_mor_id. ir. app natural_ob_source. ir. app natural_ob_target. Qed. Lemma invertible_left_multiply : forall a u v w, invertible a u -> mor a v -> mor a w -> source u = target v -> source u = target w -> comp a u v = comp a u w -> v = w. Proof. ir. assert (mor a u). uh H; ee. nin H. uh H; ee; am. transitivity (comp a (comp a (inverse a u) u) v). rw left_inverse. rw left_id. tv. rww ob_source. am. sy; am. tv. am. rww assoc. rw H4. 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. app mor_inverse. rww source_inverse. Qed. Lemma natural_mor_inverse : forall t u, globular t -> invertible (osource t) u -> natural_mor t u -> natural_mor t (inverse (osource t) u). Proof. ir. cp H; uh H; cp H1; uh H1; ee. uhg; ee. ap mor_inverse. am. rww source_inverse. rww target_inverse. rw target_inverse. rw source_inverse. rw fmor_inverse. rw fmor_inverse. apply invertible_left_multiply with (a:=otarget t) (u:=fmor (target t) u). uf otarget. ap invertible_fmor. am. rww H11. tv. rw mor_comp. tv. uh H4; ee; am. rw H12. ap mor_inverse. wr H12. ap invertible_fmor. am. am. tv. rw target_inverse. rw source_fmor. uh H4; ee; am. am. am. ap invertible_fmor. am. am. tv. tv. rw mor_comp. tv. ap mor_inverse. ap invertible_fmor. am. rww H11. tv. uh H5; ee. am. rw source_inverse. rw target_fmor. sy. uh H5; ee; am. am. rww H11. ap invertible_fmor. am. rww H11. tv. tv. rw source_fmor. rw target_comp. sy. uh H4; ee; am. uh H4; ee; am. rw H12. ap mor_inverse. ap invertible_fmor. am. am. am. rw target_inverse. rw source_fmor. uh H4; ee; am. am. am. ap invertible_fmor. am. am. tv. am. rww H11. rw source_fmor. sy. rw target_comp. rw target_inverse. rw source_fmor. tv. am. rww H11. app invertible_fmor. rww H11. app mor_inverse. app invertible_fmor. rww H11. uh H5; ee; am. rw source_inverse. rw target_fmor. sy. uh H5; ee; am. am. rww H11. app invertible_fmor. rww H11. am. rww H11. (** Before doing this main goal we do some lemmas to help with the subgoals. **) assert (lem1: mor (otarget t) (ntrans t (target u))). uh H5; ee; am. assert (lem2: mor (otarget t) (fmor (target t) u)). uf otarget. ap mor_fmor. am. rww H11. assert (lem3: invertible (target (target t)) (fmor (target t) u)). ap invertible_fmor. am. rww H11. tv. assert (lem4: invertible (target (target t)) (fmor (source t) u)). ap invertible_fmor. am. am. am. assert (lem5: mor (otarget t) (fmor (source t) u)). uf otarget. rw target_target. wr H12. ap mor_fmor. am. am. assert (lem6: mor (otarget t) (ntrans t (source u))). uh H4; ee; am. (** Here is the main part of the proof. **) wr assoc. wr H6. rw assoc. rw H12. rw right_inverse. rw right_id. sy. wr assoc. rw right_inverse. rw left_id. tv. (** That was the proof, now we have 36 subgoals **) uf otarget. rw ob_target. tv. am. am. rw target_fmor. uh H5; ee; am. am. rww H11. tv. am. am. app mor_inverse. am. rww target_inverse. rww source_inverse. rw target_fmor. sy. uh H5; ee; am. am. rww H11. tv. rww ob_target. am. rw target_fmor. uh H5; ee; am. am. am. tv. am. am. am. rw H12. ap mor_inverse. am. rw target_fmor. uh H5; ee; am. am. am. rw source_fmor. sy. rw target_inverse. rw source_fmor. tv. am. am. rww H12. am. am. tv. am. am. rw H12. ap mor_inverse. am. rw source_fmor. sy. uh H4; ee; am. am. rww H11. rw target_inverse. rw source_fmor. uh H4; ee; am. am. am. rww H12. tv. am. rww H11. am. am. am. tv. am. am. Qed. Lemma inverse_closed_naturality_subcategory : forall t, globular t -> inverse_closed (naturality_subcategory t) (osource t). Proof. ir. uhg; ee. ap is_subcategory_naturality_subcategory. am. ir. rw mor_naturality_subcategory. ap natural_mor_inverse. am. am. wrr mor_naturality_subcategory. am. Qed. Lemma sub_add_inverses_naturality_subcategory : forall s t, globular t -> sub s (morphisms (naturality_subcategory t)) -> sub (add_inverses (osource t) s) (morphisms (naturality_subcategory t)). Proof. ir. ap sub_add_inverses. app inverse_closed_naturality_subcategory. am. Qed. Definition equalizer_subcategory f g := subcategory (source f) (fun x => (fob f x = fob g x)) (fun u => (fmor f u = fmor g u)). Lemma equalizer_subcategory_property : forall f g, Functor.axioms f -> Functor.axioms g -> source f = source g -> target f = target g -> subcategory_property (source f) (fun x => (fob f x = fob g x)) (fun u => (fmor f u = fmor g u)). Proof. ir. uhg; ee. uh H; ee; am. ir. wr comp_fmor. rw H1. wr comp_fmor. rw H6. rw H7. rw H2. reflexivity. am. wrr H1. wrr H1. am. am. am. am. am. ir. rw fmor_id. rw H1. rw fmor_id. rw H4. rww H2. am. tv. wrr H1. am. tv. am. ir. transitivity (source (fmor f u)). rww source_fmor. rw H4. rww source_fmor. wrr H1. ir. transitivity (target (fmor f u)). rww target_fmor. rw H4. rww target_fmor. wrr H1. Qed. Lemma is_subcategory_equalizer_subcategory : forall f g, Functor.axioms f -> Functor.axioms g -> source f = source g -> target f = target g -> is_subcategory (equalizer_subcategory f g) (source f). Proof. ir. uf equalizer_subcategory. ap subcategory_is_subcategory. app equalizer_subcategory_property. Qed. Lemma ob_equalizer_subcategory : forall f g x, Functor.axioms f -> Functor.axioms g -> source f = source g -> target f = target g -> ob (equalizer_subcategory f g) x = (ob (source f) x & fob f x = fob g x). Proof. ir. ap iff_eq; ir. ufi equalizer_subcategory H3. rwi ob_subcategory H3. ee. am. am. app equalizer_subcategory_property. ee. uf equalizer_subcategory. rw ob_subcategory. ee; am. app equalizer_subcategory_property. Qed. Lemma mor_equalizer_subcategory : forall f g u, Functor.axioms f -> Functor.axioms g -> source f = source g -> target f = target g -> mor (equalizer_subcategory f g) u = (mor (source f) u & fmor f u = fmor g u). Proof. ir. ap iff_eq; ir. ufi equalizer_subcategory H3. rwi mor_subcategory H3. ee. am. am. app equalizer_subcategory_property. ee. uf equalizer_subcategory. rw mor_subcategory. ee; am. app equalizer_subcategory_property. Qed. Lemma mor_equ_subcat_inverse : forall f g u, Functor.axioms f -> Functor.axioms g -> source f = source g -> target f = target g -> invertible (source f) u -> mor (equalizer_subcategory f g) u -> mor (equalizer_subcategory f g) (inverse (source f) u). Proof. ir. rw mor_equalizer_subcategory. ee. ap mor_inverse. am. rw fmor_inverse. rw H1. rw fmor_inverse. rwi mor_equalizer_subcategory H4. ee. rw H5; rww H2. am. am. am. am. am. wrr H1. tv. am. am. tv. am. am. am. am. Qed. Lemma inverse_closed_equalizer_subcatgory : forall f g, Functor.axioms f -> Functor.axioms g -> source f = source g -> target f = target g -> inverse_closed (equalizer_subcategory f g) (source f). Proof. ir. uhg; ee. app is_subcategory_equalizer_subcategory. ir. app mor_equ_subcat_inverse. Qed. Lemma mor_equ_subcat_fmor : forall f g h u, Functor.axioms f -> Functor.axioms g -> Functor.axioms h -> source g = target f -> source h = target f -> fcompose g f = fcompose h f -> mor (source f) u -> mor (equalizer_subcategory g h) (fmor f u). Proof. ir. rww mor_equalizer_subcategory. ee. rw H2. app mor_fmor. transitivity (fmor (fcompose g f) u). rww fmor_fcompose. rw H4. rww fmor_fcompose. rww H3. transitivity (target (fcompose g f)). rww target_fcompose. rw H4. rww target_fcompose. Qed. Lemma sub_mor_image_equalizer_subcategory : forall f g h, Functor.axioms f -> Functor.axioms g -> Functor.axioms h -> source g = target f -> source h = target f -> fcompose g f = fcompose h f -> sub (mor_image f) (morphisms (equalizer_subcategory g h)). Proof. ir. uhg; ir. rwi inc_mor_image H5. nin H5. ee. ap mor_is_mor. wr H6. app mor_equ_subcat_fmor. am. Qed. Lemma sub_add_inverses_equalizer_subcategory : forall f g h, Functor.axioms f -> Functor.axioms g -> Functor.axioms h -> source g = target f -> source h = target f -> fcompose g f = fcompose h f -> sub (add_inverses (target f) (mor_image f)) (morphisms (equalizer_subcategory g h)). Proof. ir. ap sub_add_inverses. wr H2. app inverse_closed_equalizer_subcatgory. rww H3. transitivity (target (fcompose g f)). rww target_fcompose. rw H4. rww target_fcompose. app sub_mor_image_equalizer_subcategory. Qed. Lemma equalizer_subcategory_extensionality_criterion : forall f g, Functor.axioms f -> Functor.axioms g -> source f = source g -> target f = target g -> equalizer_subcategory f g = source f -> f = g. Proof. ir. ap Functor.axioms_extensionality. am. am. am. am. ir. wri H3 H4. rwi mor_equalizer_subcategory H4. ee; am. am. am. am. am. Qed. Lemma fcompose_eq_shows_eq : forall f g h, Functor.axioms f -> Functor.axioms g -> Functor.axioms h -> source g = target f -> source h = target f -> fcompose g f = fcompose h f -> generates (target f) (add_inverses (target f) (mor_image f)) -> g = h. Proof. ir. assert (target g = target h). transitivity (target (fcompose g f)). rww target_fcompose. rw H4. rww target_fcompose. assert (equalizer_subcategory g h = target f). uh H5; ee. ap H8. wr H2. app is_subcategory_equalizer_subcategory. rww H3. app sub_add_inverses_equalizer_subcategory. app equalizer_subcategory_extensionality_criterion. rww H3. rww H2. Qed. Lemma ob_inj_pull_morphism_criterion : forall f a, Category.axioms a -> ob_iso f -> generates (target f) (add_inverses (target f) (mor_image f)) -> ob_inj (pull_morphism a f). Proof. ir. assert (Functor.axioms f). lu. uhg; ee. ap pull_morphism_axioms. am. am. ir. rwi source_pull_morphism H3. cp H3. rwi ob_functor_cat H3. rwi source_pull_morphism H4. cp H4. rwi ob_functor_cat H4. uh H3; uh H4; ee. rwi fob_pull_morphism H5; try am. rwi fob_pull_morphism H5; try am. apply fcompose_eq_shows_eq with (f:= f). am. am. am. am. am. am. am. uh H2; ee; am. am. uh H2; ee; am. am. Qed. (** Now we get back to the proof of the criterion for fullness of pull_morphism, which is what we introduced the naturality_subcategory for. This is basically a horn-filler problem, and the ``horn'' condition is given by the first definition we make. We then proceed to construct the filler called (ntdotted f g h u), and use the notion of naturality_subcategory to prove that it is a natural transformation. ******) Definition full_pull_situation f g h u := Functor.axioms f & Functor.axioms g & Functor.axioms h & Nat_Trans.axioms u & source g = target f & source h = target f & fcompose g f = source u & fcompose h f = target u & ob_iso f & generates (target f) (add_inverses (target f) (mor_image f)). Lemma full_pull_additional_facts : forall f g h u, full_pull_situation f g h u -> (target g = otarget u & target h = otarget u & source f = osource u & source g = source h & target g = target h & osource u = source f). Proof. ir. uh H; dj; ee. wr target_source. wr H5. rww target_fcompose. am. uf otarget. wr H7. rww target_fcompose. uf osource. wr H7. rww source_fcompose. rww H7. rww H1. uf osource. wr H10. rww source_fcompose. Qed. Definition ob_inverse_pr f x y:= ob (source f) y & fob f y = x. Definition ob_inverse f x := choose (ob_inverse_pr f x). Lemma exists_ob_inverse_pr : forall f x, ob_iso f -> ob (target f) x -> exists y, ob_inverse_pr f x y. Proof. ir. uh H; ee. uh H1; ee. cp (H2 _ H0). uh H3. ee. nin H4. ee. sh x0. uhg; ee. am. am. Qed. Lemma fob_ob_inverse : forall f x, ob_iso f -> ob (target f) x -> fob f (ob_inverse f x) = x. Proof. ir. cp (exists_ob_inverse_pr H H0). cp (choose_pr H1). cbv beta in H2. uh H2. ee. am. Qed. Lemma ob_ob_inverse : forall f x, ob_iso f -> ob (target f) x -> ob (source f) (ob_inverse f x). Proof. ir. cp (exists_ob_inverse_pr H H0). cp (choose_pr H1). cbv beta in H2. uh H2. ee. am. Qed. Lemma ob_inverse_fob : forall f x, ob_iso f -> ob (source f) x -> ob_inverse f (fob f x) = x. Proof. ir. cp H. uh H; ee. uh H; ee. ap H3. app ob_ob_inverse. app ob_fob. am. rww fob_ob_inverse. app ob_fob. Qed. Definition ntdotted f g h u := Nat_Trans.create g h (fun x => ntrans u (ob_inverse f x)). Lemma source_ntdotted : forall f g h u, source (ntdotted f g h u) = g. Proof. ir. uf ntdotted. rw Nat_Trans.source_create. tv. Qed. Lemma target_ntdotted : forall f g h u, target (ntdotted f g h u) = h. Proof. ir. uf ntdotted. rw Nat_Trans.target_create. tv. Qed. Lemma osource_ntdotted : forall f g h u, osource (ntdotted f g h u) = source g. Proof. ir. uf osource. rww source_ntdotted. Qed. Lemma otarget_ntdotted : forall f g h u, otarget (ntdotted f g h u) = target h. Proof. ir. uf otarget. rww target_ntdotted. Qed. Lemma globular_ntdotted : forall f g h u, full_pull_situation f g h u -> globular (ntdotted f g h u). Proof. ir. cp (full_pull_additional_facts H). uh H; uhg; ee. uf ntdotted. ap Nat_Trans.create_like. rww osource_ntdotted. uh H6; ee; am. rw otarget_ntdotted. uh H7; ee; am. rww source_ntdotted. rww target_ntdotted. rw target_ntdotted. rww osource_ntdotted. sy; am. rw source_ntdotted. rww otarget_ntdotted. Qed. Lemma ntrans_ntdotted : forall f g h u x, full_pull_situation f g h u -> ob (target f) x -> ntrans (ntdotted f g h u) x = ntrans u (ob_inverse f x). Proof. ir. uf ntdotted. rw ntrans_create. tv. ap ob_is_ob. uh H; ee. rww H4. Qed. Lemma ntrans_ntdotted_fob : forall f g h u x, full_pull_situation f g h u -> ob (source f) x -> ntrans (ntdotted f g h u) (fob f x) = ntrans u x. Proof. ir. rw ntrans_ntdotted. rw ob_inverse_fob. tv. uh H; ee; am. am. am. ap ob_fob. uh H; ee; am. am. Qed. Lemma natural_ob_ntdotted : forall f g h u x, full_pull_situation f g h u -> ob (target f) x -> natural_ob (ntdotted f g h u) x. Proof. ir. assert (lem1 : full_pull_situation f g h u). am. cp (full_pull_additional_facts H). uh H; ee. uhg; ee. rw osource_ntdotted. rww H10. rw otarget_ntdotted. rw ntrans_ntdotted. rw H2. ap mor_ntrans. am. rw H6. ap ob_ob_inverse. am. am. tv. am. am. rw ntrans_ntdotted. rw source_ntdotted. rw source_ntrans. wr H12. rw fob_fcompose. rw fob_ob_inverse. tv. am. am. am. am. am. app ob_ob_inverse. am. rw H6. app ob_ob_inverse. am. am. rw ntrans_ntdotted. rw target_ntdotted. rw target_ntrans. wr H13. rww fob_fcompose. rww fob_ob_inverse. app ob_ob_inverse. am. rw H6. app ob_ob_inverse. am. am. Qed. Lemma natural_mor_ntdotted_fmor : forall f g h u y, full_pull_situation f g h u -> mor (source f) y -> natural_mor (ntdotted f g h u) (fmor f y). Proof. ir. cp H. cp (full_pull_additional_facts H). uh H; ee. uhg; ee. rw osource_ntdotted. rw H11. app mor_fmor. ap natural_ob_ntdotted. am. rw source_fmor. app ob_fob. rww ob_source. am. am. ap natural_ob_ntdotted. am. rw target_fmor. app ob_fob. rww ob_target. am. am. rw otarget_ntdotted. rw target_ntdotted. rw source_ntdotted. rw target_fmor. rw source_fmor. rw ntrans_ntdotted_fob. rw ntrans_ntdotted_fob. rw H3. assert (fmor g (fmor f y) = fmor (source u) y). wr H13. rww fmor_fcompose. assert (fmor h (fmor f y) = fmor (target u) y). wr H14. rww fmor_fcompose. rw H17; rw H18. app carre. rww H7. am. rww ob_source. am. rww ob_target. am. am. am. am. Qed. Lemma sub_mor_image_naturality_subcategory : forall f g h u, full_pull_situation f g h u -> sub (mor_image f) (morphisms (naturality_subcategory (ntdotted f g h u))). Proof. ir. uhg; ir. ap mor_is_mor. rw mor_naturality_subcategory. rwi inc_mor_image H0. nin H0. ee. wr H1. ap natural_mor_ntdotted_fmor. am. am. uh H; ee; am. app globular_ntdotted. Qed. Lemma sub_add_inverses_naturality_subcategory_ntdotted : forall f g h u, full_pull_situation f g h u -> sub (add_inverses (target f) (mor_image f)) (morphisms (naturality_subcategory (ntdotted f g h u))). Proof. ir. assert (target f = osource (ntdotted f g h u)). rww osource_ntdotted. uh H; ee; sy; am. rw H0. ap sub_add_inverses_naturality_subcategory. app globular_ntdotted. ap sub_mor_image_naturality_subcategory. am. Qed. Lemma naturality_subcategory_ntdotted_all : forall f g h u, full_pull_situation f g h u -> naturality_subcategory (ntdotted f g h u) = target f. Proof. ir. cp (sub_add_inverses_naturality_subcategory_ntdotted H). cp H. uh H; ee. uh H10; ee. ap H12. assert (target f = osource (ntdotted f g h u)). rww osource_ntdotted. sy; am. rw H13. ap is_subcategory_naturality_subcategory. app globular_ntdotted. app sub_add_inverses_naturality_subcategory_ntdotted. Qed. Lemma ntdotted_axioms : forall f g h u, full_pull_situation f g h u -> Nat_Trans.axioms (ntdotted f g h u). Proof. ir. cp (naturality_subcategory_ntdotted_all H). rw nat_trans_axioms_rw. ee. app globular_ntdotted. ir. rwi osource_ntdotted H1. wr ob_naturality_subcategory. rw H0. uh H; ee. wrr H5. app globular_ntdotted. ir. rwi osource_ntdotted H1. wr mor_naturality_subcategory. rw H0. uh H; ee. wrr H5. app globular_ntdotted. Qed. Lemma htrans_right_ntdotted : forall f g h u, full_pull_situation f g h u -> htrans_right (ntdotted f g h u) f = u. Proof. ir. ap Nat_Trans.axioms_extensionality. ap htrans_right_axioms. uh H; ee; am. app ntdotted_axioms. rw osource_ntdotted. uh H; ee. am. uh H; ee; am. rw source_htrans_right. rw source_ntdotted. uh H; ee; am. rw target_htrans_right. rw target_ntdotted. uh H; ee; am. ir. rwi osource_htrans_right H0. rw ntrans_htrans_right. rw ntrans_ntdotted_fob. tv. am. am. am. Qed. Lemma full_pull_morphism_criterion : forall f a, Category.axioms a -> ob_iso f -> generates (target f) (add_inverses (target f) (mor_image f)) -> full (pull_morphism a f). Proof. ir. assert (Functor.axioms f). lu. assert (lem1: axioms (target f)). uh H2; ee; am. uhg; ee. app pull_morphism_axioms. ir. uhg; ee. app pull_morphism_axioms. rwi target_pull_morphism H3. cp H3. rwi mor_functor_cat H6. uh H6; ee. uh H4. uh H5. ee. clear H4. clear H5. nin H9; nin H10; ee. rwi source_pull_morphism H5. cp H5. rwi source_pull_morphism H4. cp H4. rwi fob_pull_morphism H10. rwi fob_pull_morphism H9. rwi ob_functor_cat H11; rwi ob_functor_cat H12. uh H11; uh H12; ee. assert (full_pull_situation f x0 x u). uhg; ee; try am. sh (ntdotted f x0 x u). ee. rw source_pull_morphism. rw mor_functor_cat. uhg; ee. app ntdotted_axioms. rw osource_ntdotted. am. rw otarget_ntdotted. am. am. am. rw fmor_pull_morphism. rw htrans_right_ntdotted. tv. am. rw mor_functor_cat. uhg; ee. app ntdotted_axioms. rw osource_ntdotted. am. rw otarget_ntdotted. am. am. am. am. am. am. am. am. am. am. am. am. am. am. am. am. am. uh H2; ee; am. am. Qed. (** putting the above criteria together we get the main theorem of this module. Recall that the definition [iso_to_full_subcategory] says that the functor is full, faithful, and injective on objects. This is equivalent to saying that it induces an isomorphism to a full subcategory, see Lemma [iso_to_full_subcategory_interp] above. **) Lemma iso_to_full_subcategory_pull_morphism_criterion : forall f a, Category.axioms a -> ob_iso f -> generates (target f) (add_inverses (target f) (mor_image f)) -> iso_to_full_subcategory (pull_morphism a f). Proof. ir. uhg; ee. ap faithful_pull_morphism_criterion. am. uh H0; ee; am. ap full_pull_morphism_criterion. am. am. am. ap ob_inj_pull_morphism_criterion. am. am. am. Qed. End Ob_Iso_Functor. Module Associating_Quotient. Export Quotient_Category. Export Quotient_Functor. (** 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. 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]. *) 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.