Set Implicit Arguments. Unset Strict Implicit. Require Import Arith. Require Export category. Module Functor. Export Category. (**** creation and extraction ****) Record data : Type := create { fsource : Category.data; ftarget : Category.data; fob : E1; fmor : E1 }. Lemma data_extensionality : forall f g, fsource f = fsource g -> ftarget f = ftarget g -> (forall x, fob f x = fob g x) -> (forall u, fmor f u = fmor g u) -> f = g. Proof. ir. nin f; nin g. assert (lem_fsource : fsource0 = fsource1). am. assert (lem_ftarget : ftarget0 = ftarget1). am. assert (lem_fob : fob0 = fob1). ap arrow_extensionality. ir. exact (H1 a). assert (lem_fmor : fmor0 = fmor1). ap arrow_extensionality. ir. exact (H2 a). rw lem_fsource; rw lem_ftarget; rw lem_fob; rw lem_fmor; tv. Qed. Lemma fsource_create : forall a b fo fm, fsource (create a b fo fm) = a. Proof. ir. tv. Qed. Lemma ftarget_create : forall a b fo fm, ftarget (create a b fo fm) = b. Proof. ir. tv. Qed. Lemma fob_create : forall a b fo fm x, fob (create a b fo fm) x = (fo x). Proof. ir. tv. Qed. Lemma fmor_create : forall a b fo fm u, fmor (create a b fo fm) u = (fm u). Proof. ir. tv. Qed. Definition axioms f := let a := fsource f in let b := ftarget f in (Category.axioms a) & (Category.axioms b) & (forall x, ob a x -> ob b (fob f x)) & (forall x, ob a x -> id b (fob f x) = fmor f (id a x)) & (forall u, mor a u -> mor b (fmor f u)) & (forall u, mor a u -> source (fmor f u) = fob f (source u)) & (forall u, mor a u -> target (fmor f u) = fob f (target u)) & (forall u v, composable a u v -> composable b (fmor f u) (fmor f v)) & (forall u v, composable a u v -> comp b (fmor f u) (fmor f v) = fmor f (comp a u v)). Definition property a b fo fm := (Category.axioms a) & (Category.axioms b) & (forall x, ob a x -> ob b (fo x)) & (forall x, ob a x -> id b (fo x) = fm (id a 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 u v, composable a u v -> comp b (fm u) (fm v) = fm (comp a u v)). Lemma create_axioms : forall a b (fo fm:E1), property a b fo fm -> axioms (create a b fo fm). Proof. ir. uhg. do 50 (try (rw fsource_create)). do 50 (try (rw ftarget_create)). do 50 (try (rw fmor_create)). dj; try (rw fmor_create); try (rw fob_create). lu. lu. uh H; ee. ap H4. am. uh H; ee. ap H6. am. uh H; ee. ap H8; am. uh H. ee. ap H10; am. uh H; ee. ap H12; am. rwi composable_facts_rw H7. uh H7; ee. ap show_composable. util (H4 u). am. rwi fmor_create H15; am. ap H4; am. util (H5 u); try am. rwi fmor_create H15. rw H15. rw H6. rw H12; tv. am. rw fmor_create. rw fmor_create. uh H; ee. ap H15. am. Qed. Lemma axioms_property : forall f, axioms f -> property (fsource f) (ftarget f) (fob f) (fmor f). Proof. ir. uh H; ee. uhg; xd. Qed. Definition same_data a b (fo fm:E1) a1 b1 (fo1 fm1:E1) := (Category.same a a1) & (Category.same b b1) & (forall x, ob a x -> fo x = fo1 x) & (forall u, mor a u -> fm u = fm1 u). Lemma show_same_data : forall a b fo fm a1 b1 fo1 fm1, (Category.same a a1) -> (Category.same b b1) -> (property a b fo fm) -> (property a1 b1 fo1 fm1) -> (forall u, mor a u -> fm u = fm1 u) -> same_data a b fo fm a1 b1 fo1 fm1. Proof. ir. uhg; xd. ir. assert (lem1: x = (source (id a x))). rwi ob_facts_rw H4. uh H4; ee. sy; am. assert (lem2: id a x = id a1 x). uh H; ee. uh H6; ee. ap H9. am. assert (lem3 : mor a (id a x)). rwi ob_facts_rw H4. uh H4; ee. am. assert (lem4 : fm (id a x) = fm1 (id a1 x)). wr lem2. ap H3. am. rw lem1. uh H1; ee. wr H9. rw lem2. uh H2; ee. wr H16. rwi lem2 lem4. rw lem4. tv. uh H; ee. uh H20; ee. wr H21. wr lem2. am. am. Qed. Lemma create_recovers : forall a b fo fm, let f := (create a b fo fm) in property a b fo fm -> same_data a b fo fm (fsource f) (ftarget f) (fob f) (fmor f). Proof. ir. ap show_same_data. uf f; rw fsource_create. ap same_refl. lu. uf f; rw ftarget_create. ap same_refl; lu. am. ap axioms_property. uf f; ap create_axioms. am. ir. uf f; rw fmor_create; tv. Qed. Definition same f f1 := axioms f & axioms f1 & same_data (fsource f) (ftarget f) (fob f) (fmor f) (fsource f1) (ftarget f1) (fob f1) (fmor f1). Lemma show_same : forall f g, axioms f -> axioms g -> Category.same (fsource f) (fsource g) -> Category.same (ftarget f) (ftarget g) -> (forall u, mor (fsource f) u -> fmor f u = fmor g u) -> same f g. Proof. ir. uhg; ee; try am. ap show_same_data; try am. ap axioms_property; am. ap axioms_property; am. Qed. Lemma ob_fob : forall f x, axioms f -> ob (fsource f) x -> ob (ftarget f) (fob f x). Proof. ir. uh H; ee. au. Qed. Lemma ob_fobv : forall a f x, axioms f -> ob (fsource f) x -> a = ftarget f -> ob a (fob f x). Proof. ir. rw H1. ap ob_fob; am. Qed. Lemma mor_fmor : forall f u, axioms f -> mor (fsource f) u -> mor (ftarget f) (fmor f u). Proof. ir. uh H; ee. au. Qed. Lemma mor_fmorv : forall a f u, axioms f -> mor (fsource f) u -> a = ftarget f -> mor a (fmor f u). Proof. ir. rw H1. ap mor_fmor; am. Qed. Lemma source_fmor : forall f u, axioms f -> mor (fsource f) u -> source (fmor f u) = fob f (source u). Proof. ir. uh H; ee. au. Qed. Lemma target_fmor : forall f u, axioms f -> mor (fsource f) u -> target (fmor f u) = fob f (target u). Proof. ir. uh H; ee. au. Qed. Lemma source_fmorv : forall a f u, axioms f -> mor (fsource f) u -> a = ftarget f -> source (fmor f u) = fob f (source u). Proof. ir. ap source_fmor; am. Qed. Lemma target_fmorv : forall a f u, axioms f -> mor (fsource f) u -> a = ftarget f -> target (fmor f u) = fob f (target u). Proof. ir. ap target_fmor; am. Qed. Lemma id_fob : forall f x, axioms f -> ob (fsource f) x -> id (ftarget f) (fob f x) = fmor f (id (fsource f) x). Proof. ir. uh H; ee. au. Qed. Lemma composable_fmor : forall f u v, axioms f -> composable (fsource f) u v -> composable (ftarget f) (fmor f u) (fmor f v). Proof. ir. uh H; ee. au. Qed. Lemma comp_fmor : forall f u v, axioms f -> composable (fsource f) u v -> comp (ftarget f) (fmor f u) (fmor f v) = fmor f (comp (fsource f) u v). Proof. ir. uh H; ee. au. Qed. Lemma comp_fmorv : forall a f f1 u v, axioms f -> f = f1 -> composable (fsource f) u v -> a = ftarget f -> comp a (fmor f u) (fmor f1 v) = fmor f (comp (fsource f) u v). Proof. ir. rw H2. wr H0. ap comp_fmor; am. Qed. Lemma fmor_compv : forall a f u v, axioms f -> a = fsource f -> composable a u v -> fmor f (comp a u v) = comp (ftarget f) (fmor f u) (fmor f v). Proof. ir. rw H0. sy. rw comp_fmor. tv. am. wr H0; am. Qed. Definition compose (f g:data) := create (fsource g) (ftarget f) (fun x => fob f (fob g x)) (fun u => fmor f (fmor g u)). Definition fcomposable (f g:data) := axioms f & axioms g & fsource f = ftarget g. Lemma fsource_compose : forall (f g:data), fsource (compose f g) = fsource g. Proof. ir. uf compose. rw fsource_create. tv. Qed. Lemma ftarget_compose : forall (f g:data), ftarget (compose f g) = ftarget f. Proof. ir. uf compose. rw ftarget_create. tv. Qed. Lemma fob_compose : forall (f g:data) (x:E), fob (compose f g) x = fob f (fob g x). Proof. ir. uf compose. rw fob_create. tv. Qed. Lemma fmor_compose : forall (f g:data) (u:E), fmor (compose f g) u = fmor f (fmor g u). Proof. ir. uf compose. rw fmor_create. tv. Qed. Lemma compose_axioms : forall f g, fcomposable f g -> axioms (compose f g). Proof. ir. uf compose. ap create_axioms. uh H; ee. uhg; dj. uh H0; ee; am. uh H; ee; am. ap ob_fob. am. rw H1. ap ob_fob. am. am. rw id_fob. ap uneq. rw H1. ap id_fob. am. am. am. rw H1; ap ob_fob; am. ap mor_fmor. am. rw H1. ap mor_fmor. am. am. rw source_fmor. ap uneq. rw source_fmor. tv. am. am. am. rw H1; ap mor_fmor; am. rw target_fmor. ap uneq. rw target_fmor. tv. am. am. am. rw H1; ap mor_fmor; am. rw comp_fmor. ap uneq. rw H1. ap comp_fmor. am. am. am. rw H1. cp H9; rwi composable_facts_rw H9; uh H9; ee. ap show_composable. ap mor_fmor; am. ap mor_fmor; am. rw source_fmor. rw target_fmor. ap uneq. am. am. am. am. am. Qed. Lemma compose_assoc : forall f g h, fcomposable f g -> fcomposable g h -> compose (compose f g) h = compose f (compose g h). Proof. ir. ap data_extensionality. tv. tv. ir. tv. ir. tv. Qed. Definition inclusion (a b:Category.data) := create a b (fun (x:E) => x) (fun (u:E) => u). Definition identity a := inclusion a a. Lemma left_identity : forall f, compose (identity (ftarget f)) f = f. Proof. ir. ap data_extensionality; try tv; try (ir; tv). Qed. Lemma right_identity : forall f, compose f (identity (fsource f)) = f. Proof. ir. ap data_extensionality; try tv; try (ir; tv). Qed. Lemma subcategory_inclusion_axioms : forall a b, subcategory a b -> axioms (inclusion a b). Proof. ir. uh H; ee. uhg; dj. am. am. exact (H1 _ H7). sy. exact (H4 _ H8). exact (H2 _ H9). tv. tv. assert (composable a u v). am. change (composable b u v). rwi composable_facts_rw H13. uh H13; ee. ap show_composable; au. sy. exact (H3 _ _ H13). Qed. End Functor. Module Constant_Functor. Export Functor. Definition constant_functor a b x := create a b (fun y:E => x) (fun u:E => id b x). Definition constant_value f := fob f emptyset. Lemma fsource_constant_functor : forall a b x, fsource (constant_functor a b x) = a. Proof. ir. tv. Qed. Lemma ftarget_constant_functor : forall a b x, ftarget (constant_functor a b x) = b. Proof. ir. tv. Qed. Lemma fob_constant_functor : forall a b x y, fob (constant_functor a b x) y = x. Proof. ir. tv. Qed. Lemma fmor_constant_functor : forall a b x u, fmor (constant_functor a b x) u = id b x. Proof. ir. tv. Qed. Lemma constant_functor_axioms : forall a b x, Category.axioms a -> Category.axioms b -> ob b x -> axioms (constant_functor a b x). Proof. ir. uf constant_functor. ap create_axioms. uhg; ee; try am. ir; am. ir; tv. ir. ap mor_id. am. ir. rw source_id; tv. ir. rw target_id; tv. ir. rw left_id. tv. am. ap mor_id; am. rw target_id. tv. am. Qed. Definition is_constant f := f = constant_functor (fsource f) (ftarget f) (constant_value f). Lemma fob_constant_value : forall f x, is_constant f -> fob f x = constant_value f. Proof. ir. uh H. set (z:= constant_value f). rw H. rw fob_constant_functor. tv. Qed. Lemma fmor_constant_value : forall f u, is_constant f -> fmor f u = id (ftarget f) (constant_value f). Proof. ir. uh H. set (z:= constant_value f). rw H. rw fmor_constant_functor. tv. Qed. Lemma constant_functor_is_constant : forall a b x, Category.axioms a -> ob b x -> is_constant (constant_functor a b x). Proof. ir. uhg. rw fsource_constant_functor. rw ftarget_constant_functor. uf constant_value. rw fob_constant_functor. tv. Qed. End Constant_Functor.