Set Implicit Arguments. Unset Strict Implicit. Require Import Arith. Require Export notation. Module Category. Export Arrow. Record data : Type := create { is_ob : EP; is_mor : EP; comp : E2; id : E1}. Lemma data_extensionality : forall a b, (forall x, is_ob a x = is_ob b x) -> (forall u, is_mor a u = is_mor b u) -> (forall u v, comp a u v = comp b u v) -> (forall x, id a x = id b x) -> a = b. Proof. ir. nin a; nin b. assert (lem_ob: is_ob0 = is_ob1). ap arrow_extensionality. ir. exact (H a). assert (lem_mor: is_mor0 = is_mor1). ap arrow_extensionality. ir. exact (H0 a). assert (lem_comp: comp0 = comp1). ap arrow_extensionality. ir. ap arrow_extensionality. ir. exact (H1 a a0). assert (lem_id : id0 = id1). ap arrow_extensionality. ir. exact (H2 a). rw lem_ob; rw lem_mor; rw lem_comp; rw lem_id; tv. Qed. Lemma is_ob_create : forall o m c i x, is_ob (create o m c i) x = o x. Proof. ir. tv. Qed. Lemma is_mor_create : forall o m c i u, is_mor (create o m c i) u = m u. Proof. ir. tv. Qed. Lemma comp_create : forall o m c i u v, comp (create o m c i) u v = c u v. Proof. ir. tv. Qed. Lemma id_create : forall o m c i x, id (create o m c i) x = i x. Proof. ir. tv. Qed. (**** axioms ****) Definition are_composable a f g := is_mor a f & is_mor a g & source f = target g. Definition is_ob_facts a x := is_ob a x & is_mor a (id a x) & source (id a x) = x & target (id a x) = x & (forall f, is_mor a f-> source f = x -> comp a f (id a x) = f) & (forall f, is_mor a f-> target f = x -> comp a (id a x) f = f). Definition is_mor_facts a f:= is_mor a f & is_ob a (source f) & is_ob a (target f) & comp a (id a (target f)) f = f & comp a f (id a (source f)) = f & Arrow.like f. Definition are_composable_facts a f g:= are_composable a f g & is_mor a (comp a f g) & source (comp a f g) = source g & target (comp a f g) = target f. Definition axioms a := (forall x, is_ob a x = is_ob_facts a x) & (forall u, is_mor a u = is_mor_facts a u) & (forall u v, are_composable a u v = are_composable_facts a u v) & (forall u v w, are_composable a u v -> are_composable a v w -> (comp a (comp a u v) w) = (comp a u (comp a v w))). Definition composable a u v := axioms a & are_composable a u v. Definition mor a u := axioms a & is_mor a u. Definition ob a x := axioms a & is_ob a x. Definition mor_facts c u := mor c u & ob c (source u) & ob c (target u) & comp c (id c (target u)) u = u & comp c u (id c (source u)) = u & Arrow.like u. Lemma mor_facts_rw : forall c u, mor c u = mor_facts c u. Proof. ir. ap iff_eq; ir. cp H; uh H; ee. cp H; uh H; ee. rwi H3 H1. uh H1; ee. uhg; xd. uhg; xd. uhg; xd. uh H; ee; am. Qed. Definition ob_facts c x := ob c x & mor c (id c x) & composable c (id c x) (id c x) & source (id c x) = x & target (id c x) = x & comp c (id c x) (id c x) = (id c x)& (forall u, mor c u -> source u = x -> comp c u (id c x) = u)& (forall u, mor c u -> target u = x -> comp c (id c x) u = u). Lemma ob_facts_rw : forall c x, ob c x = ob_facts c x. Proof. ir. ap iff_eq; ir. cp H; uh H; ee. cp H; uh H; ee. cp H1; uh H1; ee. rwi H H6. uh H6; ee. uhg; xd. uhg; xd. uhg; xd. uhg; xd. rw H8; rw H9; tv. ir. ap H10. lu. am. ir. ap H11; lu. lu. Qed. Definition composable_facts c u v := axioms c & are_composable c u v & mor c u & mor c v & mor c (comp c u v)& source u = target v & source (comp c u v) = source v & target (comp c u v) = target u. Lemma composable_facts_rw : forall c u v, composable c u v = composable_facts c u v. Proof. ir; ap iff_eq; ir. cp H; uh H; ee. cp H; uh H; ee. uhg; dj; try am. uhg; ee. am. lu. uhg; ee; lu. rwi H4 H1. uh H1; ee. uhg; ee; try am. uh H7; ee; am. rwi H4 H7. uh H7. ee. am. rwi H4 H7. uh H7. ee. am. uhg; uh H; xd. Qed. Lemma show_composable : forall c u v, mor c u -> mor c v -> source u = target v -> composable c u v. Proof. ir. cp H; uh H; ee. cp H; uh H; ee. uhg; ee. am. uh H0; ee. uhg; ee; try am. Qed. Lemma show_composable_facts : forall c u v, mor c u -> mor c v -> source u = target v -> composable_facts c u v. Proof. ir. wr composable_facts_rw; ap show_composable; am. Qed. Definition associativity_facts c u v w := composable_facts c u v & composable_facts c v w & composable_facts c u (comp c v w) & composable_facts c (comp c u v) w & comp c u (comp c v w) = comp c (comp c u v) w. Lemma show_associativity_facts : forall c u v w, composable c u v -> composable c v w -> associativity_facts c u v w. Proof. ir. cp H; uh H; ee. cp H; uh H; ee. uhg. do 4 (wr composable_facts_rw). ee; try am. rwi composable_facts_rw H0; rwi composable_facts_rw H1. uh H0; uh H1; ee. ap show_composable. am. am. rw H20. am. ap show_composable. rwi composable_facts_rw H1; uh H1; ee; am. rwi composable_facts_rw H0; uh H0; ee; am. rwi composable_facts_rw H1; uh H1; ee. rw H12. uh H0; ee. uh H14; ee. am. sy; ap H6. am. uh H0; ee; am. Qed. Definition morphism_property (o m:EP) (c:E2) (i:E1) u:= m u & o (source u) & o (target u) & c u (i (source u)) = u & c (i (target u)) u = u & Arrow.like u. Definition object_property (o m:EP) (i:E1) x := o x & m (i x) & source (i x) = x & target (i x) = x. Definition composable_property (m:EP) (c:E2) u v:= m u & m v & source u = target v & m (c u v) & source (c u v) = source v & target (c u v) = target u. Definition property (o m:EP) (c:E2) (i:E1) := (forall x, o x = object_property o m i x) & (forall u, m u = morphism_property o m c i u) & (forall u v, m u -> m v -> source u = target v -> composable_property m c u v) & (forall u v w, m u -> m v -> m w -> source u = target v -> source v = target w -> c (c u v) w = c u (c v w)). Lemma are_composable_create_rw : forall o m c i u v, are_composable (create o m c i) u v = (m u & m v & source u = target v). Proof. ir. ap iff_eq; ir. uh H. rwi is_mor_create H. rwi is_mor_create H. xd. uhg. do 2 (rw is_mor_create). xd. Qed. Lemma create_axioms : forall (o m:EP) (c : E2) (i:E1), property o m c i-> axioms (create o m c i). Proof. ir. set (k:=(create o m c i)). assert (lem1 : forall u v, are_composable k u v = (m u & m v & source u = target v)). ir. ap iff_eq; ir. ufi k H0. rwi are_composable_create_rw H0. xd. uf k. rw are_composable_create_rw. xd. uh H; ee. assert (lem2: forall u, is_mor k u = m u). ir. ap iff_eq; ir. ufi k H3. rwi is_mor_create H3. am. uf k; rw is_mor_create; am. assert (lem3: forall u v, comp k u v = c u v). ir. uf k. rw comp_create; tv. assert (lem5: forall x, id k x = i x). ir. uf k. rw id_create. tv. assert (lem6: forall (x:E), is_ob k x = o x). ir; ap iff_eq; ir. ufi k H3. rwi is_ob_create H3. am. uf k; rw is_ob_create; am. (*** the proof of axioms ***) (*** mor facts ***) uhg; ee; ir. ap iff_eq; ir. cp H3; rwi lem6 H3. rwi H H3. uh H3; ee. uhg; dj. am. rw lem2. rw lem5. am. rw lem5; am. rw lem5; am. rw lem5. rw lem3. rwi lem2 H12. rwi H0 H12. uh H12; ee. wr H13. am. rw lem3. rw lem5. rwi lem2 H13. rwi H0 H13. uh H13; ee. wr H14. am. lu. ap iff_eq; ir. rwi lem2 H3. rwi H0 H3. uh H3; ee. uhg; ee. rw lem2; am. rw lem6; am. rw lem6; am. rw lem3. rw lem5. am. rw lem3. rw lem5. am. lu. lu. ap iff_eq; ir. cp H3; uh H3; ee. rwi lem2 H3. rwi lem2 H5. util (H1 u v). am. am. am. uh H7; ee. uhg; xd. lu. (*** associativity ***) change (c (c u v) w = c u (c v w)). rwi lem1 H3; rwi lem1 H4; ee. ap H2; try am. Qed. Lemma axioms_property : forall c, axioms c -> property (ob c) (mor c) (comp c) (id c). Proof. ir. uhg; ee; ir; try (ap iff_eq; ir); try lu. rwi ob_facts_rw H0. uh H0. ee. uhg; xd. rwi mor_facts_rw H0; uh H0; ee. uhg; xd. cp show_composable_facts. util (H3 c u v); try am. uh H4; ee. uhg; xd. uh H; ee. ap H7. uhg; ee; lu. uhg; ee; lu. Qed. Lemma ob_existence_rw : forall a x, ob a x = (exists f, (mor a f & source f = x)). Proof. ir. ap iff_eq; ir. rwi ob_facts_rw H. uh H; ee. sh (id a x); xd. nin H. ee. rwi mor_facts_rw H. uh H; ee. wr H0; am. Qed. Lemma left_id: forall a x u, ob a x -> mor a u -> target u = x -> comp a (id a x) u = u. Proof. ir. rwi mor_facts_rw H0; uh H0; ee. wr H1; am. Qed. Lemma right_id : forall a x u, ob a x -> mor a u -> source u = x -> comp a u (id a x) = u. Proof. ir. rwi mor_facts_rw H0; uh H0; ee. wr H1; am. Qed. Lemma left_id_unique : forall a e x, axioms a -> mor a e -> source e = x -> (forall f, composable a e f -> comp a e f = f) -> e = id a x. Proof. ir. rwi mor_facts_rw H0. wr H1. uh H0; ee. transitivity (comp a e (id a x)). rw right_id; try tv; try lu. wr H1; am. wr H2. wr H1; tv. ap show_composable. am. rwi ob_facts_rw H3; uh H3; ee; am. rwi ob_facts_rw H3; uh H3; ee; sy; am. Qed. Lemma right_id_unique : forall a e x, axioms a -> mor a e -> target e = x -> (forall f, composable a f e -> comp a f e = f) -> e = id a x. Proof. ir. rwi mor_facts_rw H0. wr H1. uh H0; ee. transitivity (comp a (id a (target e)) e). rw left_id; try tv; try lu. ap H2. ap show_composable. rwi ob_facts_rw H4; uh H4; ee; am. am. rwi ob_facts_rw H4; uh H4; ee; am. Qed. Definition same_data (o m : EP) (c : E2) (i: E1) (o1 m1 : EP) (c1 : E2) (i1: E1):= (forall x, o x = o1 x) & (forall u, m u = m1 u) & (forall u v, m u -> m v -> source u = target v -> c u v = c1 u v) & (forall x, o x -> i x = i1 x). Lemma ob_create : forall o m c i x, property o m c i-> ob (create o m c i) x = o x. Proof. ir. set (k:= create o m c i). assert (lem0 : axioms k). uf k; ap create_axioms; am. assert (lem1 : forall x, ob k x = is_ob k x). ir. ap iff_eq; ir. lu. uhg; ee; am. rw lem1. uf k; rw is_ob_create; tv. Qed. Lemma mor_create : forall o m c i u, property o m c i-> mor (create o m c i) u = m u. Proof. ir. set (k:= create o m c i). assert (lem0 : axioms k). uf k; ap create_axioms; am. assert (lem1 : forall u, mor k u = is_mor k u). ir. ap iff_eq; ir. lu. uhg; ee; am. rw lem1. uf k; rw is_mor_create; tv. Qed. Lemma uncomp : forall a b u v u1 v1, a = b -> u = u1 -> v = v1 -> comp a u v = comp b u1 v1. Proof. ir. rw H; rw H0; rw H1; tv. Qed. Lemma create_recovers : forall o m c i, let k := create o m c i in property o m c i-> same_data o m c i (ob k) (mor k) (comp k) (id k). Proof. ir. assert (lem0 : axioms k). uf k; ap create_axioms; am. assert (lem1 : forall x, ob k x = is_ob k x). ir. ap iff_eq; ir. lu. uhg; ee; am. assert (lem2 : forall u, mor k u = is_mor k u). ir. ap iff_eq; ir. lu. uhg; ee; am. uhg; dj; ir; try (rw lem1); try (rw lem2); uf k; try (rw is_ob_create); try (rw is_mor_create); try (rw comp_create); try (rw id_create); try tv. Qed. Lemma show_same_obs : forall o m c i o1 m1 c1 i1 x, property o m c i -> property o1 m1 c1 i1 -> (forall u, m u = m1 u) -> o x = o1 x. Proof. ir. set (k:= create o m c i). set (k1 := create o1 m1 c1 i1). ap iff_eq; ir. assert (ob k x). uf k; rw ob_create; am. rwi ob_existence_rw H3. nin H3. ee. assert (ob k1 x). rw ob_existence_rw. sh x0; ee; try am. uf k1; rw mor_create. ufi k H3; rwi mor_create H3. wr H1; am. am. am. ufi k1 H5. rwi ob_create H5; am. assert (ob k1 x). uf k1; rw ob_create; am. rwi ob_existence_rw H3. nin H3. ee. assert (ob k x). rw ob_existence_rw. sh x0; ee; try am. uf k; rw mor_create. ufi k1 H3; rwi mor_create H3. rw H1; am. am. am. ufi k H5. rwi ob_create H5; am. Qed. Lemma show_same_id : forall o m c i o1 m1 c1 i1 x, property o m c i -> property o1 m1 c1 i1-> (forall u, m u = m1 u) -> (forall u v, m u -> m v -> source u = target v -> c u v = c1 u v) -> o x -> i x = i1 x. Proof. ir. set (k:= create o m c i). set (k1 := create o1 m1 c1 i1). assert (lem1: axioms k). uf k; ap create_axioms; am. cp H3. cp (show_same_obs x H H0 H1). rwi H5 H4. uh H. ee. rwi H H3. uh H0; ee. rwi H0 H4. uh H3; uh H4; ee. rwi H1 H15. wri H1 H12. rwi H9 H15. rwi H6 H12. uh H15; uh H12; ee. rwi H17 H26. rwi H13 H20. wr H26. wr H2. am. am. rw H1; am. rw H13; sy; am. Qed. Lemma show_same_data : forall o m c i o1 m1 c1 i1, property o m c i-> property o1 m1 c1 i1-> (forall u, m u = m1 u) -> (forall u v, m u -> m v -> source u = target v -> c u v = c1 u v) -> same_data o m c i o1 m1 c1 i1. Proof. ir. uhg; dj; try am. ap (show_same_obs x H H0 H1). ap H2. am. am. am. cp (show_same_id H H0 H1 H2 H6). am. Qed. Definition same a b := axioms a & axioms b & same_data (ob a) (mor a) (comp a) (id a) (ob b) (mor b) (comp b) (id b). Lemma show_same : forall a b, axioms a -> axioms b -> (forall u, mor a u = mor b u) -> (forall u v, composable_facts a u v -> comp a u v = comp b u v) -> same a b. Proof. ir. uf same. ee; try am. ap show_same_data. ap axioms_property; try am. ap axioms_property; am. am. ir. ap H2. wr composable_facts_rw. ap show_composable; am. Qed. Lemma same_refl : forall a, axioms a -> same a a. Proof. ir. ap show_same; try am. ir; tv. ir; tv. Qed. Lemma same_trans : forall a c, (exists b, same a b & same b c) -> same a c. Proof. ir. nin H. ee. uh H; uh H0; ee. uh H4; uh H2; ee. ap show_same; try am. ir. rw H8. ap H5. ir. rw H9. rw H6. tv. wr H8. lu. wr H8; lu. lu. lu. lu. lu. Qed. Lemma same_symm : forall a b, same a b = same b a. Proof. ir. ap iff_eq; ir; uh H; ee; ap show_same; try am. uh H1; ee. ir; sy; ap H2. uh H1; ee; ir. sy. ap H3. rw H2. lu. rw H2; lu. lu. ir. uh H1. ee; au. ir. uh H1; ee. sy; ap H4. rw H3. lu. rw H3; lu. lu. Qed. Definition subcategory (a b : data) := axioms a & axioms b & (forall x, ob a x -> ob b x) & (forall u, mor a u -> mor b u) & (forall u v, composable a u v -> comp a u v = comp b u v) & (forall x, ob a x -> id a x = id b x). Lemma sub_sub_same : forall a b, subcategory a b -> subcategory b a -> same a b. Proof. ir. ap show_same. lu. lu. ir. ap iff_eq; ir. uh H; ee. au. uh H0; ee; au. ir. uh H; ee. ap H5. rw composable_facts_rw; am. Qed. Lemma same_sub : forall a b, same a b -> subcategory a b. Proof. ir. uh H; ee. uh H1; ee. uhg; dj; au. wr H1; am. wr H2; am. rwi composable_facts_rw H9. ap H3; try lu. Qed. Lemma subcategory_trans : forall a c, (exists b, (subcategory a b & subcategory b c))-> subcategory a c. Proof. ir. nin H. ee. uh H; uh H0; uhg; xd. ir. rw H9. rw H4; tv. rwi composable_facts_rw H11. uh H11; ee. ap show_composable. au. au. am. am. ir. wr H5. au. au. Qed. Lemma mor_id : forall a x, ob a x -> mor a (id a x). Proof. ir. rwi ob_facts_rw H; uh H; ee. am. Qed. Lemma source_id : forall a x, ob a x -> source (id a x) = x. Proof. ir. rwi ob_facts_rw H; uh H; ee. am. Qed. Lemma target_id : forall a x, ob a x -> target (id a x) = x. Proof. ir. rwi ob_facts_rw H; uh H; ee. am. Qed. Lemma ob_source : forall a u, mor a u -> ob a (source u). Proof. ir. rwi mor_facts_rw H; uh H; ee. am. Qed. Lemma ob_target : forall a u, mor a u -> ob a (target u). Proof. ir. rwi mor_facts_rw H; uh H; ee. am. Qed. Lemma mor_comp : forall a u v, composable a u v -> mor a (comp a u v). Proof. ir. rwi composable_facts_rw H; uh H; ee. am. Qed. Lemma mor_compv : forall a b u v, composable a u v -> a = b -> mor a (comp b u v). Proof. ir. wr H0. ap mor_comp; am. Qed. Lemma source_comp : forall a u v, composable a u v -> source (comp a u v) = source v. Proof. ir. rwi composable_facts_rw H; uh H; ee. am. Qed. Lemma target_comp : forall a u v, composable a u v -> target (comp a u v) = target u. Proof. ir. rwi composable_facts_rw H; uh H; ee. am. Qed. Lemma assoc : forall a u v w, composable a u v -> composable a v w -> comp a (comp a u v) w = comp a u (comp a v w). Proof. ir. cp (show_associativity_facts H H0). uh H1; ee. sy; am. Qed. Lemma verbose_assoc : forall a1 a2 a3 a4 u v w u1 v1 w1, composable a2 u v -> composable a4 v w -> a1 = a2 -> a2 = a3 -> a3 = a4 -> u= u1 -> v=v1 -> w = w1 -> comp a1 (comp a2 u v) w = comp a3 u1 (comp a4 v1 w1). Proof. ir. rw H1. rw H2. rw H3. rw H4. rw H5. rw H6. ap assoc. wr H3; wr H2; wr H4; wr H5; am. wr H5; wr H6; am. Qed. Lemma assoc_verbose_rw : forall a1 a2 u v w, composable a2 u v -> composable a1 v w -> a1 = a2 -> comp a1 (comp a2 u v) w = comp a2 u (comp a1 v w). Proof. ir. rw H1. rwi H1 H0. ap assoc; am. Qed. Lemma mor_arrow_like : forall a u, mor a u -> Arrow.like u. Proof. ir. rwi mor_facts_rw H. lu. Qed. Definition is_small a := Category.axioms a & Bounded.axioms (ob a) & Bounded.axioms (mor a). Lemma mor_bounded_small : forall a, Category.axioms a -> Bounded.axioms (mor a) -> is_small a. Proof. ir. uhg; ee; try am. set (m:= Bounded.create (mor a)). assert (lem1 : forall y, inc y m = mor a y). ir. uf m. ap Bounded.inc_create. am. apply Bounded.trans_criterion with source m. ir. sh (id a y). ee. rw lem1. ap mor_id. am. rw source_id. tv. am. Qed. Definition objects a := Bounded.create (ob a). Definition morphisms a := Bounded.create (mor a). Lemma inc_objects : forall a x, is_small a -> inc x (objects a) = ob a x. Proof. ir. uf objects. rw Bounded.inc_create. tv. lu. Qed. Lemma inc_morphisms : forall a u, is_small a -> inc u (morphisms a) = mor a u. Proof. ir. uf morphisms. rww Bounded.inc_create. lu. Qed. End Category. Module Opposite. Export Category. Definition opp a := Category.create (is_ob a) (fun u => is_mor a (flip u)) (fun u v => flip (comp a (flip v) (flip u))) (fun x => flip (id a x)). Lemma is_ob_opp : forall a x, is_ob (opp a) x = is_ob a x. Proof. ir. uf opp. rw is_ob_create. tv. Qed. Lemma is_mor_opp : forall a u, is_mor (opp a) u = is_mor a (flip u). Proof. ir. uf opp. rw is_mor_create. tv. Qed. Lemma comp_opp : forall a u v, comp (opp a) u v = flip (comp a (flip v) (flip u)). Proof. ir. uf opp. rw comp_create. tv. Qed. Lemma id_opp : forall a x, id (opp a) x = flip (id a x). Proof. ir. uf opp. rw id_create. tv. Qed. Lemma opp_opp : forall a, opp (opp a) = a. Proof. ir. ap data_extensionality; ir. rw is_ob_opp. rw is_ob_opp. tv. rw is_mor_opp. rw is_mor_opp. rw flip_flip. tv. rw comp_opp. rw comp_opp. rw flip_flip. rw flip_flip. rw flip_flip. tv. rw id_opp. rw id_opp. rw flip_flip. tv. Qed. Lemma opp_axioms : forall a, axioms a -> axioms (opp a). Proof. ir. assert (morli : forall u, is_mor a u -> Arrow.like u). ir. uh H; ee. rwi H1 H0. uh H0; ee. am. assert (obidli : forall x, is_ob a x -> Arrow.like (id a x)). ir. uh H. ee. rwi H H0. uh H0. ee. ap morli. am. assert (flifli : forall u, flip (flip u) = u). ir. rw flip_flip. tv. uf opp. ap create_axioms. assert (ax : axioms a). am. uh H; ee. uhg; dj; try (ap iff_eq; ir). uhg; ee. am. rw flip_flip. rwi H H3. lu. rw source_flip. rwi H H3. lu. au. rw target_flip. rwi H H3; lu. au. lu. uhg; ee. am. wr (flifli u). rw source_flip. rwi H0 H4. lu. au. wr (flifli u). rw target_flip. rwi H0 H4. lu. au. rw flip_flip. assert (source u = target (flip u)). rw target_flip. tv. rw like_flip. au. rw H5. rw left_id. rw flip_flip; tv. rwi H0 H4. uh H4; ee. uhg; ee; am. uhg; ee; am. tv. rw flip_flip. assert (target u = source (flip u)). rw source_flip. tv. rw like_flip. au. rw H5. rw right_id. rw flip_flip. tv. rwi H0 H4. uhg; ee; lu. uhg; ee; am. tv. rw like_flip. au. lu. assert (like u). rw like_flip; au. assert (like v). rw like_flip; au. assert (are_composable a (flip v) (flip u)). uhg; ee; try am. rw source_flip; try am. rw target_flip; try am. sy; am. rwi H1 H10. uh H10; ee. uhg; ee. am. am. am. rw flip_flip. am. rw source_flip. rw H13. rw target_flip. tv. am. rwi H0 H11. uh H11; ee. am. rw target_flip. rw H12. rw source_flip; try am; try tv. rwi H0 H11; lu. assert (like u). rw like_flip; au. assert (like v). rw like_flip; au. assert (like w). rw like_flip; au. assert (are_composable a (flip v) (flip u)). uhg; ee; try am. rw source_flip; try am. rw target_flip; try am. sy; am. rwi H1 H14; uh H14; ee. rw flip_flip. rw flip_flip. ap uneq. sy; ap assoc. ap show_composable. uhg; ee; am. uhg; ee; am. rw source_flip; try am. rw target_flip; try am; try tv. sy; am. ap show_composable; try (uhg; ee; am). rw source_flip; try am. rw target_flip; try am. sy; am. Qed. Lemma opp_axioms_eq : forall a, axioms a = axioms (opp a). Proof. ir. ap iff_eq; ir. ap opp_axioms. am. wr opp_opp. ap opp_axioms; am. Qed. Lemma ob_opp : forall a x, ob (opp a) x = ob a x. Proof. ir. sy. ap iff_eq; ir. uhg; ee. ap opp_axioms. lu. rw is_ob_opp. lu. uhg; ee. rw opp_axioms_eq. lu. wr is_ob_opp. lu. Qed. Lemma mor_opp : forall a u, mor (opp a) u = mor a (flip u). Proof. ir. assert (lem : forall a u, mor (opp a) u -> mor a (flip u)). ir. uhg; ee. rw opp_axioms_eq. lu. wr is_mor_opp. lu. ap iff_eq; ir. au. assert (u = flip (flip u)). rw flip_flip; tv. rw H0. ap lem. rw opp_opp; am. Qed. Lemma composable_opp : forall a u v, composable (opp a) u v = composable a (flip v) (flip u). Proof. ir. ap iff_eq; ir; rwi composable_facts_rw H; ap show_composable; try (wr mor_opp; lu); try (rw mor_opp; lu). rw source_flip. rw target_flip; try (sy; lu). apply mor_arrow_like with (opp a); lu. apply mor_arrow_like with (opp a); lu. wr source_flip. wr target_flip. sy; lu. rw like_flip. apply mor_arrow_like with a; lu. rw like_flip; apply mor_arrow_like with a; lu. Qed. End Opposite. Module Isomorphism. Export Category. Definition are_inverse a u v := composable_facts a u v & composable_facts a v u & comp a u v = id a (source v) & comp a v u = id a (source u). Lemma show_are_inverse : forall a u v, mor a u -> mor a v -> source u = target v -> target u = source v -> comp a u v = id a (source v) -> comp a v u = id a (source u) -> are_inverse a u v. Proof. ir. uhg; ee. ap show_composable_facts; am. ap show_composable_facts; try am. sy; am. am. am. Qed. Lemma are_inverse_symm :forall a u v, are_inverse a u v -> are_inverse a v u. Proof. ir. uh H; ee. uhg; ee; try am. Qed. Definition invertible a u := exists v, are_inverse a u v. Definition inverse a u := choose (are_inverse a u). Lemma invertible_inverse : forall a u, invertible a u -> are_inverse a u (inverse a u). Proof. ir. exact (choose_pr H). Qed. Lemma inverse_unique : forall a u v w, are_inverse a u v -> are_inverse a u w -> v = w. Proof. ir. uh H; uh H0; ee. transitivity (comp a (comp a v u) w). rw assoc. rw H2. rw right_id. tv. uh H0; ee. rwi mor_facts_rw H9. lu. lu. transitivity (target u); try lu; try (sy; lu). rw composable_facts_rw; am. rw composable_facts_rw; am. rw H6. rw left_id. tv. uh H; ee. rwi mor_facts_rw H8; lu. lu. sy; lu. Qed. Lemma inverse_uni : forall v w, (exists a, exists u, (are_inverse a u v & are_inverse a u w)) -> v = w. Proof. ir. nin H. nin H. ee. exact (inverse_unique H H0). Qed. Lemma inverse_eq : forall a u v, are_inverse a u v -> inverse a u = v. Proof. ir. ap inverse_uni. sh a. sh u. ee. ap invertible_inverse. uhg. sh v; am. am. Qed. Lemma inverse_invertible : forall a u, invertible a u -> invertible a (inverse a u). Proof. ir. uhg. sh u. ap are_inverse_symm. ap invertible_inverse. am. Qed. Lemma inverse_inverse : forall a u, invertible a u -> inverse a (inverse a u) = u. Proof. ir. apply inverse_unique with a (inverse a u). ap invertible_inverse. ap inverse_invertible. am. ap are_inverse_symm. ap invertible_inverse. am. Qed. Lemma source_inverse : forall a u, invertible a u -> source (inverse a u) = target u. Proof. ir. cp (invertible_inverse H). uh H0; ee. lu. Qed. Lemma target_inverse : forall a u, invertible a u -> target (inverse a u) = source u. Proof. ir. cp (invertible_inverse H). uh H0; ee. sy; lu. Qed. Lemma left_inverse : forall a u, invertible a u -> comp a (inverse a u) u = id a (source u). Proof. ir. cp (invertible_inverse H). uh H0; ee. am. Qed. Lemma right_inverse : forall a u, invertible a u -> comp a u (inverse a u) = id a (target u). Proof. ir. cp (invertible_inverse H). uh H0; ee. rwi source_inverse H2. am. am. Qed. Lemma mor_inverse : forall a u, invertible a u -> mor a (inverse a u). Proof. ir. cp (invertible_inverse H). uh H0; ee. lu. Qed. Lemma composable_inverse_left : forall a u, invertible a u -> composable a (inverse a u) u. Proof. ir. cp (invertible_inverse H). uh H0; ee. ap show_composable; lu. Qed. Lemma composable_inverse_right : forall a u, invertible a u -> composable a u (inverse a u). Proof. ir. cp (invertible_inverse H). uh H0; ee. ap show_composable; lu. Qed. Lemma composable_inverse : forall a u v, composable a u v -> invertible a u -> invertible a v -> composable a (inverse a v) (inverse a u). Proof. ir. cp (invertible_inverse H0). cp (invertible_inverse H1). cp H. rwi composable_facts_rw H; uh H; ee. ap show_composable. lu. lu. rw source_inverse; try am. rw target_inverse; try am. sy; am. Qed. Lemma invertible_comp_are_inverse : forall a u v, composable a u v -> invertible a u -> invertible a v -> are_inverse a (comp a u v) (comp a (inverse a v) (inverse a u)). Proof. ir. cp (invertible_inverse H0). cp (invertible_inverse H1). cp H. rwi composable_facts_rw H; uh H; ee. ap show_are_inverse. am. ap mor_comp. ap composable_inverse; am. rw source_comp; try am. rw target_comp; try am. rw target_inverse; try am. tv. ap composable_inverse; am. rw target_comp; try am. rw source_comp; try am. rw source_inverse; try am. tv. ap composable_inverse; am. rw assoc. assert (comp a v (comp a (inverse a v) (inverse a u))= inverse a u). wr assoc. rw right_inverse. rw left_id. tv. ap ob_target; am. ap mor_inverse; am. rw target_inverse. am. am. am. ap composable_inverse_right; am. ap composable_inverse; am. rw H12. rw right_inverse; try am. rw source_comp. rw source_inverse. tv. am. ap composable_inverse; am. am. ap show_composable. am. ap mor_comp. ap composable_inverse; am. rw target_comp. rw target_inverse. tv. am. ap composable_inverse; am. rw assoc. assert (comp a (inverse a u) (comp a u v) = v). wr assoc. rw left_inverse; try am. rw left_id. tv. ap ob_source; am. am. sy; am. ap composable_inverse_left; am. am. rw H12. rw left_inverse; try am. rw source_comp; try am. tv. ap composable_inverse; am. ap show_composable. ap mor_inverse; am. ap mor_comp; am. rw source_inverse; try am. rw target_comp; try am. tv. Qed. Lemma invertible_comp : forall a u v, composable a u v -> invertible a u -> invertible a v -> invertible a (comp a u v). Proof. ir. uhg; sh (comp a (inverse a v) (inverse a u)). ap invertible_comp_are_inverse; am. Qed. Lemma inverse_comp : forall a u v, composable a u v -> invertible a u -> invertible a v -> inverse a (comp a u v) = comp a (inverse a v) (inverse a u). Proof. ir. ap inverse_eq. ap invertible_comp_are_inverse; am. Qed. Lemma identity_are_inverse : forall a x, ob a x -> are_inverse a (id a x) (id a x). Proof. ir. rwi ob_facts_rw H. uh H; ee. uhg; ee; try am. wr composable_facts_rw; am. wr composable_facts_rw; am. rw H4. rw H2; tv. rw H4. rw H2; tv. Qed. Lemma inverse_id : forall a x, ob a x -> inverse a (id a x) = id a x. Proof. ir. ap inverse_eq. ap identity_are_inverse; am. Qed. End Isomorphism. Module VerySmall. Export Category. Definition Objects := (o_(b_(j_(e_(c_(DOT 0)))))). Definition Morphisms := (m_(o_(r_(p_(h_(DOT 0)))))). Definition Composition := (c_(o_(m_(p_(DOT 0))))). Definition Identity := (i_(d_(e_(n_(t_(DOT 0)))))). Definition caseObjects a (b : notn) op := match op return (atof op) with (o_(b_(j_(e_(c_(DOT 0)))))) => a | z => (b z) end. Definition caseMorphisms a (b : notn) op := match op return (atof op) with (m_(o_(r_(p_(h_(DOT 0)))))) => a | z => (b z) end. Definition caseComposition a (b : notn) op := match op return (atof op) with (c_(o_(m_(p_(DOT 0))))) => a | z => (b z) end. Definition caseIdentity a (b : notn) op := match op return (atof op) with (i_(d_(e_(n_(t_(DOT 0)))))) => a | z => (b z) end. Definition objects a := extra a Objects. Definition morphisms a := extra a Morphisms. Definition composition a := extra a Composition. Definition identity a := extra a Identity. Definition create_obj (o m:E) (c:E2) (i:E1) (op : nota) := caseObjects o ( caseMorphisms m ( caseComposition (L m (fun u => L m (c u))) ( caseIdentity (L o i) ( da)))) op. Section Construction. Variables o m :E. Variable c : E2. Variable i : E1. Definition create := createN (create_obj o m c i). Lemma objects_create : objects create = o. ir; uf objects; uf create; uf create_obj. notatac1; am. Qed. Lemma morphisms_create : morphisms create = m. ir; uf morphisms; uf create; uf create_obj. notatac1; am. Qed. Lemma composition_create : composition create = L m (fun u => (L m (c u))). Proof. ir. uf create. uf composition. notatac1; am. Qed. Lemma identity_create : identity create = L o i. Proof. ir. uf create. uf identity. notatac1; am. Qed. End Construction. Definition compose a u v := V v (V u (composition a)). Definition ident a x := V x (identity a). Definition like a := a = create (objects a) (morphisms a) (compose a) (ident a). Lemma create_extensionality : forall o m c i o1 m1 c1 i1, o = o1 -> m = m1 -> (forall u v, inc u m -> inc v m -> c u v = c1 u v) -> (forall x, inc x o -> i x = i1 x) -> create o m c i = create o1 m1 c1 i1. Proof. ir. wr H. wr H0. assert (lem1: L m (fun u => L m (c u)) = L m (fun u => L m (c1 u))). ap Function.create_extensionality. tv. ir. ap Function.create_extensionality. tv. au. assert (lem2: L o i = L o i1). ap Function.create_extensionality. tv. au. uf create. uf create_obj. rw lem1. rw lem2. tv. Qed. Lemma create_like : forall o m c i, like (create o m c i). Proof. ir. uf like. ap create_extensionality. rw objects_create; tv. rw morphisms_create; tv. ir. uf compose. rw composition_create. rw create_V_rewrite. rw create_V_rewrite. tv. am. am. ir. uf ident. rw identity_create. rw create_V_rewrite. tv. am. Qed. Definition is_object a x := inc x (objects a). Definition is_morphism a u := inc u (morphisms a). Definition set_data a := Category.create (is_object a) (is_morphism a) (compose a) (ident a). Definition data_set a := create (Bounded.create (is_ob a)) (Bounded.create (is_mor a)) (comp a) (id a). Definition is_very_small a := a = set_data (data_set a). Lemma is_ob_set_data : forall a, is_ob (set_data a) = is_object a. Proof. ir. uf set_data. ap arrow_extensionality. ir. rw is_ob_create. tv. Qed. Lemma is_mor_set_data : forall a, is_mor (set_data a) = is_morphism a. Proof. ir. uf set_data. ap arrow_extensionality. ir. rw is_mor_create. tv. Qed. Lemma comp_set_data : forall a, comp (set_data a) = compose a. Proof. ir. uf set_data. ap arrow_extensionality. ir. ap arrow_extensionality. ir. rw comp_create. tv. Qed. Lemma id_set_data : forall a, id (set_data a) = ident a. Proof. ir. uf set_data. ap arrow_extensionality. ir. rw id_create. tv. Qed. (** for module Bounded in function.v ***) Lemma bounded_create_back : forall x, Bounded.create (fun y => inc y x) = x. Proof. ir. set (p:= fun y=> inc y x). assert (bdd : Bounded.axioms p). uhg. sh x. uhg; ir; ee. ir; am. ir; am. ap extensionality; uhg; ir. change (p x0). ap Bounded.lem1. am. am. ap Bounded.lem2. am. am. Qed. Lemma data_set_set_data : forall a, like a -> data_set (set_data a) = a. Proof. ir. uf data_set. uh H. transitivity (create (objects a) (morphisms a) (compose a) (ident a)). ap create_extensionality. rw is_ob_set_data. uf is_object. rw bounded_create_back. tv. rw is_mor_set_data; uf is_morphism. rw bounded_create_back. tv. ir. rw comp_set_data. tv. ir. rw id_set_data. tv. sy; am. Qed. Lemma is_small_set_data : forall b, like b -> is_very_small (set_data b). Proof. ir. uf is_very_small. rw data_set_set_data. tv. am. Qed. Lemma is_small_set_data_ex : forall a, (exists b, (like b & a = set_data b)) -> is_very_small a. Proof. ir. nin H. ee. rw H0. uhg. rw data_set_set_data. tv. am. Qed. Lemma like_data_set : forall a, like (data_set a). Proof. ir. uf data_set. ap create_like. Qed. Lemma set_data_data_set : forall a, is_very_small a -> set_data (data_set a) = a. Proof. ir. sy; am. Qed. Lemma very_small_small : forall a, axioms a -> is_very_small a -> is_small a. Proof. ir. uhg; ee. am. ap Bounded.criterion. sh (objects (data_set a)). ir. change (is_object (data_set a) y). wr is_ob_set_data. rww set_data_data_set. lu. ap Bounded.criterion. sh (morphisms (data_set a)). ir. change (is_morphism (data_set a) y). wr is_mor_set_data. rww set_data_data_set. lu. Qed. End VerySmall.