Set Implicit Arguments. Unset Strict Implicit. Require Export fiprod. Module Relation. Export Quotient. Definition is_relation r := forall y, inc y r -> is_pair y. Definition substrate r := union2 (Image.create r pr1) (Image.create r pr2). Lemma inc_pr1_substrate : forall r y, inc y r -> inc (pr1 y) (substrate r). Proof. ir. uf substrate. ap union2_first. rw Image.inc_rw. sh y. ee. am. tv. Qed. Lemma inc_pr2_substrate : forall r y, inc y r -> inc (pr2 y) (substrate r). Proof. ir. uf substrate. ap union2_second. rw Image.inc_rw. sh y. ee. am. tv. Qed. Lemma substrate_smallest : forall r s, (forall y, inc y r -> inc (pr1 y) s) -> (forall y, inc y r -> inc (pr2 y) s) -> sub (substrate r) s. Proof. ir. uhg; ir. ufi substrate H1. cp (union2_or H1). nin H2. rwi Image.inc_rw H2. nin H2. ee. wr H3. ap H. am. rwi Image.inc_rw H2. nin H2. ee. wr H3. ap H0. am. Qed. Lemma inc_substrate : forall r x, is_relation r -> inc x (substrate r) = ((exists y, inc (pair x y) r) \/ (exists y, inc (pair y x) r)). Proof. ir. ap iff_eq; ir. ufi substrate H0. cp (union2_or H0). nin H1. ap or_introl. rwi Image.inc_rw H1. nin H1. ee. sh (pr2 x0). assert (pair x (pr2 x0) = x0). wr H2. uh H; ee. cp (H _ H1). uh H3. nin H3. nin H3. rw H3. rw pr1_pair. rw pr2_pair. tv. rww H3. ap or_intror. rwi Image.inc_rw H1. nin H1. ee. sh (pr1 x0). assert (pair (pr1 x0) x = x0). wr H2. uh H; ee. cp (H _ H1). uh H3. nin H3. nin H3. rw H3. rw pr1_pair. rw pr2_pair. tv. rww H3. nin H0. nin H0. assert (x = pr1 (pair x x0)). rww pr1_pair. rw H1. app inc_pr1_substrate. nin H0. assert (x = pr2 (pair x0 x)). rww pr2_pair. rw H1. app inc_pr2_substrate. Qed. Definition related r x y := inc (pair x y) r. Definition is_reflexive r := is_relation r & (forall y, inc y (substrate r) ->related r y y). Lemma reflexive_inc_substrate : forall r x, is_reflexive r -> inc x (substrate r) = inc (pair x x) r. Proof. ir. ap iff_eq; ir. uh H; ee. cp (H1 _ H0). am. rw inc_substrate. ap or_introl. sh x. am. lu. Qed. Lemma reflexive_ap : forall r x, is_reflexive r -> inc x (substrate r) -> related r x x. Proof. ir. uh H; ee. cp (H1 _ H0). am. Qed. Definition is_transitive r := is_relation r & (forall x y z, related r x y -> related r y z -> related r x z). Lemma transitive_ap : forall r x z, is_transitive r -> (exists y, related r x y & related r y z) -> related r x z. Proof. ir. nin H0. uh H; ee. ap (H2 x x0). am. am. Qed. Definition is_symmetric r := is_relation r & (forall x y, related r x y -> related r y x). Lemma symmetric_ap : forall r x y, is_symmetric r -> related r x y -> related r y x. Proof. ir. uh H; ee; au. Qed. Definition is_equivalence_relation r := is_relation r & is_reflexive r & is_transitive r & is_symmetric r. Lemma relation_intersection : forall z, nonempty z -> (forall r, inc r z -> is_relation r) -> is_relation (intersection z). Proof. ir. uhg; ee. ir. unfold is_relation in H0. nin H. apply H0 with y0. am. apply intersection_forall with z. am. am. Qed. Lemma related_intersection : forall z x y, nonempty z -> related (intersection z) x y = (forall r, inc r z -> related r x y). Proof. ir. ap iff_eq; ir. uh H0. uhg. apply intersection_forall with z. am. am. uhg. app intersection_inc. Qed. Lemma substrate_sub : forall r s, sub r s -> sub (substrate r) (substrate s). Proof. ir. uhg; ir. uf substrate. ufi substrate H0. cp (union2_or H0). nin H1. ap union2_first. rwi Image.inc_rw H1. rw Image.inc_rw. nin H1. sh x0; ee. app H. am. ap union2_second. rwi Image.inc_rw H1. rw Image.inc_rw. nin H1. sh x0; ee. app H. am. Qed. Lemma substrate_intersection_sub : forall r z, inc r z -> sub (substrate (intersection z)) (substrate r). Proof. ir. ap substrate_sub. uhg; ir. apply intersection_forall with z. am. am. Qed. Lemma reflexive_intersection : forall z, nonempty z -> (forall r, inc r z -> is_reflexive r) -> is_reflexive (intersection z). Proof. ir. uhg; ee. app relation_intersection. ir. cp (H0 _ H1). uh H2; ee; am. ir. rw related_intersection. ir. cp (H0 _ H2). uh H3; ee. ap H4. assert (sub (substrate (intersection z)) (substrate r)). app substrate_sub. uhg; ir. apply intersection_forall with z. am. am. ap H5. am. am. Qed. Lemma transitive_intersection : forall z, nonempty z -> (forall r, inc r z -> is_transitive r) -> is_transitive (intersection z). Proof. ir. uhg; ee. app relation_intersection. ir. cp (H0 _ H1). uh H2; ee; am. ir. rww related_intersection. ir. rwi related_intersection H1; rwi related_intersection H2. cp (H0 _ H3). uh H4; ee. apply H5 with y. au. au. am. am. am. Qed. Lemma symmetric_intersection : forall z, nonempty z -> (forall r, inc r z -> is_symmetric r) -> is_symmetric (intersection z). Proof. ir. uhg; ee. app relation_intersection. ir. cp (H0 _ H1). uh H2; ee; am. ir. rww related_intersection. ir. rwi related_intersection H1. cp (H0 _ H2). uh H3; ee. ap H4. au. au. Qed. Lemma symmetric_transitive_reflexive : forall r, is_symmetric r -> is_transitive r -> is_reflexive r. Proof. ir. uhg; ee. uh H; ee; am. ir. rwi inc_substrate H1. nin H1. nin H1. app transitive_ap. sh x. ee. am. app symmetric_ap. nin H1. app transitive_ap. sh x. ee. app symmetric_ap. am. uh H; ee; am. Qed. Lemma show_equivalence_relation : forall r, is_relation r -> (forall x y, related r x y -> related r y x) -> (forall x y z, related r x y -> related r y z -> related r x z) -> is_equivalence_relation r. Proof. ir. assert (is_symmetric r). uhg; ee; am. assert (is_transitive r). uhg; ee; am. uhg; ee; try am. app symmetric_transitive_reflexive. Qed. Lemma symmetric_transitive_equivalence : forall r, is_symmetric r -> is_transitive r -> is_equivalence_relation r. Proof. ir. uhg; ee. uh H; ee; am. app symmetric_transitive_reflexive. am. am. Qed. Lemma equivalence_relation_intersection : forall z, nonempty z -> (forall r, inc r z -> is_equivalence_relation r) -> is_equivalence_relation (intersection z). Proof. ir. ap symmetric_transitive_equivalence. app symmetric_intersection. ir. cp (H0 _ H1). lu. app transitive_intersection. ir. cp (H0 _ H1). lu. Qed. Definition class r x := Image.create (Z r (fun y => pr1 y = x)) pr2. Lemma is_pair_rw : forall x, is_pair x = (x = pair (pr1 x) (pr2 x)). Proof. ir. ap iff_eq. ir. cp (pair_recov H). uh H0. sy; am. ir. rw H. ap pair_is_pair. Qed. Lemma inc_class : forall r x y, is_relation r -> inc y (class r x) = related r x y. Proof. ir. uf class. rw Image.inc_rw. ap iff_eq; ir. nin H0. ee. Ztac. assert (x0 = pair x y). uh H; ee. cp (H _ H2). rwi is_pair_rw H4. rw H4. rw H1; rww H3. uhg. wrr H4. sh (pair x y). ee. app Z_inc. rww pr1_pair. rww pr2_pair. Qed. Lemma nonempty_class_symmetric : forall r x, is_symmetric r -> nonempty (class r x) = inc x (substrate r). Proof. ir. ap iff_eq; ir. rw inc_substrate. nin H0. rwi inc_class H0. ap or_introl. sh y. am. lu. lu. rwi inc_substrate H0. nin H0. nin H0. sh x0. rw inc_class. am. lu. nin H0. sh x0. rw inc_class. app symmetric_ap. lu. lu. Qed. Lemma related_product : forall a b x y, related (product a b) x y = (inc x a & inc y b). Proof. ir. ap iff_eq; ir. uh H. cp (product_pr H). rwi pr1_pair H0; rwi pr2_pair H0; xd. uhg. ee; app product_pair_inc. Qed. Lemma full_equivalence_relation : forall b, is_equivalence_relation (Cartesian.product b b). Proof. ir. ap show_equivalence_relation. uhg. ir. cp (Cartesian.product_pr H). ee; am. ir. rwi related_product H. rw related_product; xd. ir. rwi related_product H; rwi related_product H0. rw related_product; xd. Qed. Lemma related_class_eq : forall r u v, is_equivalence_relation r -> related r u u -> related r u v = (class r u = class r v). Proof. ir. ap iff_eq; ir. ap extensionality; uhg; ir. rwi inc_class H2. rw inc_class. ap transitive_ap. lu. sh u. ee. ap symmetric_ap. lu. am. am. lu. lu. rwi inc_class H2. rw inc_class. ap transitive_ap. lu. sh v. ee; try am. lu. lu. wri inc_class H0. rwi H1 H0. rwi inc_class H0. ap symmetric_ap. lu. am. lu. lu. Qed. End Relation. Module Categorical_Relation. Export Category. Export Relation. (** 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_surj f := Functor.axioms f & (forall x, ob (target f) x -> says f x). Definition ob_iso f := ob_inj f & ob_surj f. 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. rww target_comp. rww target_comp. rww 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. 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. Actually we are cheating a tiny bit because the definition [iso_to_full_subcategory] says that the functor is full, faithful, and injective on objects. This should of course be equivalent to saying that it induces an isomorphism to a full subcategory, but we would have to prove that. This will be done in a future version of this file. **) 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. (*** Carlos Simpson, Saturday, November 13th, 2004 ****)