From e928451c4c45cdbdd975bbfb229e8cc2616b8194 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 4 Apr 2011 02:06:03 +0000 Subject: [PATCH] major revision: separate Subcategory into {Wide,Full}Subcategory --- README | 11 + src/Enrichment_ch2_8.v | 7 +- src/FreydCategories.v | 18 +- src/General.v- | 602 ----------------------------------- src/InitialTerminal_ch2_2.v | 35 +- src/Isomorphisms_ch1_5.v | 2 +- src/MonoidalCategories_ch7_8.v | 9 +- src/NaturalIsomorphisms_ch7_5.v | 38 +-- src/PreMonoidalCategories.v | 667 +++++++++++++++++++++++++++++++++------ src/PreMonoidalCenter.v | 28 +- src/Preamble.v- | 142 --------- src/Subcategories_ch7_1.v | 161 ++++++---- 12 files changed, 752 insertions(+), 968 deletions(-) delete mode 100644 src/General.v- delete mode 100644 src/Preamble.v- diff --git a/README b/README index bc14203..579d6e1 100644 --- a/README +++ b/README @@ -22,3 +22,14 @@ seems to know what's going on, and several different representations all trigger the bug. Therefore, I have -- unfortunately -- chosen definitions which avoid product categories and bifunctors wherever possible. + +IMPORTANT NOTE ABOUT SUBCATEGORIES: non-wide subcategories (that is, +subcategories which do not include all objects of the parent category) +are awkward to handle in Coq. This is because they unavoidably +involve reasoning about equality of objects, and objects are the +indices of the types of hom-sets. Coq is not very good at dealing +with equality between types which are the indices of other types. For +this reason, I have two kinds of subcategory: WideSubcategory (which +behaves quite nicely) and FullSubcategory (which can cause problems). +Every subcategory of C is a full subcategory of a wide subcategory of +C, and you must formalize it this way. diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v index 275de7b..52a3d2a 100644 --- a/src/Enrichment_ch2_8.v +++ b/src/Enrichment_ch2_8.v @@ -362,9 +362,10 @@ Instance UnderlyingFunctor `(EF:@EFunctor Ob Hom V bin_obj' bc EI mn Eob1 EHom1 Coercion UnderlyingFunctor : EFunctor >-> Functor. Class EBinoidalCat `(ec:ECategory) := -{ ebc_bobj : ec -> ec -> ec -; ebc_first : forall a:ec, EFunctor ec ec (fun x => ebc_bobj x a) -; ebc_second : forall a:ec, EFunctor ec ec (fun x => ebc_bobj a x) +{ ebc_bobj : ec -> ec -> ec +; ebc_first : forall a:ec, EFunctor ec ec (fun x => ebc_bobj x a) +; ebc_second : forall a:ec, EFunctor ec ec (fun x => ebc_bobj a x) +; ebc_ec := ec (* this isn't a coercion - avoids duplicate paths *) }. Instance EBinoidalCat_is_binoidal `(ebc:EBinoidalCat(ec:=ec)) : BinoidalCat (Underlying ec) ebc_bobj. diff --git a/src/FreydCategories.v b/src/FreydCategories.v index 3e26e37..c269e50 100644 --- a/src/FreydCategories.v +++ b/src/FreydCategories.v @@ -22,21 +22,21 @@ Require Import MonoidalCategories_ch7_8. (* A Freyd Category is... *) Class FreydCategory - (* a cartesian category C *) - `(C:CartesianCat(Ob:=Ob)(C:=C1)) + (* a cartesian category C *) + `(C:CartesianCat(Ob:=Ob)(C:=C1)(bin_obj':=bobj)) - (* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *) + (* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *) `(K:PreMonoidalCat(Ob:=Ob)(bin_obj':=bobj)(I:=@one _ _ _ C)) - (* an identity-on-objects functor J:C->Z(K) *) -:= { fc_J : Functor C (Center_is_Monoidal K) (fun x => exist (fun _ => True) x I) + (* an identity-on-objects functor J:C->Z(K) *) +:= { fc_J : Functor C (Center_is_Monoidal K) (fun x => x) - (* which is not only monoidal *) + (* which is a monoidal functor *) ; fc_mf_J : MonoidalFunctor C (Center_is_Monoidal K) fc_J - (* but in fact strict (meaning the functor's coherence maps are identities) *) - (*; fc_strict : forall a b, #(mf_first a b) ~~ id _ - FIXME - I will need to separate Subcategory from FullSubCategory in order to fix this *) + (* and strict (meaning the functor's coherence maps are identities) *) + ; fc_strict_first : forall a b, #(mf_first(PreMonoidalFunctor:=fc_mf_J) a b) ~~ id _ (* mf_consistent gives us mf_second *) +(* ; fc_strict_id : #(mf_i(PreMonoidalFunctor:=fc_mf_J)) ~~ id _*) ; fc_C := C ; fc_K := K diff --git a/src/General.v- b/src/General.v- deleted file mode 100644 index ec5a797..0000000 --- a/src/General.v- +++ /dev/null @@ -1,602 +0,0 @@ -(******************************************************************************) -(* General Data Structures *) -(******************************************************************************) - -Require Import Coq.Unicode.Utf8. -Require Import Coq.Classes.RelationClasses. -Require Import Coq.Classes.Morphisms. -Require Import Coq.Setoids.Setoid. -Require Import Coq.Strings.String. -Require Setoid. -Require Import Coq.Lists.List. -Require Import Preamble. -Generalizable All Variables. -Require Import Omega. - - -Class EqDecidable (T:Type) := -{ eqd_type := T -; eqd_dec : forall v1 v2:T, sumbool (v1=v2) (not (v1=v2)) -; eqd_dec_reflexive : forall v, (eqd_dec v v) = (left _ (refl_equal _)) -}. -Coercion eqd_type : EqDecidable >-> Sortclass. - - -(*******************************************************************************) -(* Trees *) - -Inductive Tree (a:Type) : Type := - | T_Leaf : a -> Tree a - | T_Branch : Tree a -> Tree a -> Tree a. -Implicit Arguments T_Leaf [ a ]. -Implicit Arguments T_Branch [ a ]. - -Notation "a ,, b" := (@T_Branch _ a b) : tree_scope. - -(* tree-of-option-of-X comes up a lot, so we give it special notations *) -Notation "[ q ]" := (@T_Leaf (option _) (Some q)) : tree_scope. -Notation "[ ]" := (@T_Leaf (option _) None) : tree_scope. -Notation "[]" := (@T_Leaf (option _) None) : tree_scope. - -Open Scope tree_scope. - -Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b := - match t with - | T_Leaf x => T_Leaf (f x) - | T_Branch l r => T_Branch (mapTree f l) (mapTree f r) - end. -Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b := - match t with - | T_Leaf None => T_Leaf None - | T_Leaf (Some x) => T_Leaf (Some (f x)) - | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r) - end. -Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b := - match t with - | T_Leaf x => f x - | T_Branch l r => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r) - end. -Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b := - match t with - | T_Leaf None => [] - | T_Leaf (Some x) => f x - | T_Branch l r => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r) - end. -Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) := - match t with - | T_Leaf x => mapLeaf x - | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z) - end. -Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) := - forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }. - -Lemma tree_dec_eq : - forall {Q}(t1 t2:Tree ??Q), - (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) -> - sumbool (t1=t2) (not (t1=t2)). - intro Q. - intro t1. - induction t1; intros. - - destruct a; destruct t2. - destruct o. - set (X q q0) as X'. - inversion X'; subst. - left; auto. - right; unfold not; intro; apply H. inversion H0; subst. auto. - right. unfold not; intro; inversion H. - right. unfold not; intro; inversion H. - destruct o. - right. unfold not; intro; inversion H. - left; auto. - right. unfold not; intro; inversion H. - - destruct t2. - right. unfold not; intro; inversion H. - set (IHt1_1 t2_1 X) as X1. - set (IHt1_2 t2_2 X) as X2. - destruct X1; destruct X2; subst. - left; auto. - - right. - unfold not; intro H. - apply n. - inversion H; auto. - - right. - unfold not; intro H. - apply n. - inversion H; auto. - - right. - unfold not; intro H. - apply n. - inversion H; auto. - Defined. - - - - -(*******************************************************************************) -(* Lists *) - -Notation "a :: b" := (cons a b) : list_scope. -Open Scope list_scope. -Fixpoint leaves {a:Type}(t:Tree (option a)) : list a := - match t with - | (T_Leaf l) => match l with - | None => nil - | Some x => x::nil - end - | (T_Branch l r) => app (leaves l) (leaves r) - end. -(* weak inverse of "leaves" *) -Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) := - match l with - | nil => [] - | (a::b) => [a],,(unleaves b) - end. - -(* a map over a list and the conjunction of the results *) -Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop := - match l with - | nil => True - | (a::al) => f a /\ mapProp f al - end. - -Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l. - induction l. - auto. - simpl. - rewrite IHl. - auto. - Defined. -Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l'). - intros. - induction l; auto. - simpl. - rewrite IHl. - auto. - Defined. -Lemma map_compose : forall A B C (f:A->B)(g:B->C)(l:list A), - (map (g ○ f) l) = (map g (map f l)). - intros. - induction l. - simpl; auto. - simpl. - rewrite IHl. - auto. - Defined. -Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False. - intros. - induction b. - inversion H. - inversion H. apply IHb in H2. - auto. - Defined. -Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False. - induction b. - intros; inversion H. - intros. - inversion H. - apply IHb in H2. - auto. - Defined. - -Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[]. - intros. - destruct h. - destruct o. inversion H. - auto. - inversion H. - Defined. - -Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q. - induction q. - destruct a0; simpl. - reflexivity. - reflexivity. - simpl. - rewrite IHq1. - rewrite IHq2. - reflexivity. - Qed. - -(* handy facts: map preserves the length of a list *) -Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil. - intros. - induction s1. - auto. - assert False. - simpl in H. - inversion H. - inversion H0. - Defined. -Lemma map_on_singleton : forall A B (f:A->B) x (s1:list A), (cons x nil) = map f s1 -> { y : A & s1=(cons y nil) & (f y)=x }. - induction s1. - intros. - simpl in H; assert False. inversion H. inversion H0. - clear IHs1. - intros. - exists a. - simpl in H. - assert (s1=nil). - inversion H. apply map_on_nil in H2. auto. - subst. - auto. - assert (s1=nil). - inversion H. apply map_on_nil in H2. auto. - subst. - simpl in H. - inversion H. auto. - Defined. - -Lemma map_on_doubleton : forall A B (f:A->B) x y (s1:list A), ((x::y::nil) = map f s1) -> - { z : A*A & s1=((fst z)::(snd z)::nil) & (f (fst z))=x /\ (f (snd z))=y }. - intros. - destruct s1. - inversion H. - destruct s1. - inversion H. - destruct s1. - inversion H. - exists (a,a0); auto. - simpl in H. - inversion H. - Defined. - - -Lemma mapTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree A), - (mapTree (g ○ f) l) = (mapTree g (mapTree f l)). - induction l. - reflexivity. - simpl. - rewrite IHl1. - rewrite IHl2. - reflexivity. - Defined. - -Lemma lmap_compose : forall A B C (f:A->B)(g:B->C)(l:list A), - (map (g ○ f) l) = (map g (map f l)). - intros. - induction l. - simpl; auto. - simpl. - rewrite IHl. - auto. - Defined. - -(* sends a::b::c::nil to [[[[],,c],,b],,a] *) -Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) := - match l with - | nil => [] - | (a::b) => (unleaves' b),,[a] - end. - -(* sends a::b::c::nil to [[[[],,c],,b],,a] *) -Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A := - match l with - | nil => [] - | (a::b) => (unleaves'' b),,(T_Leaf a) - end. - -Fixpoint filter {T:Type}(l:list ??T) : list T := - match l with - | nil => nil - | (None::b) => filter b - | ((Some x)::b) => x::(filter b) - end. - -Inductive distinct {T:Type} : list T -> Prop := -| distinct_nil : distinct nil -| distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax). - -Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)). - induction l; auto. - simpl. - omega. - Qed. - -(* decidable quality on a list of elements which have decidable equality *) -Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))), - sumbool (eq l1 l2) (not (eq l1 l2)). - intro T. - intro l1. - induction l1; intros. - destruct l2. - left; reflexivity. - right; intro H; inversion H. - destruct l2 as [| b l2]. - right; intro H; inversion H. - set (IHl1 l2 dec) as eqx. - destruct eqx. - subst. - set (dec a b) as eqy. - destruct eqy. - subst. - left; reflexivity. - right. intro. inversion H. subst. apply n. auto. - right. - intro. - inversion H. - apply n. - auto. - Defined. - - - - -(*******************************************************************************) -(* Length-Indexed Lists *) - -Inductive vec (A:Type) : nat -> Type := -| vec_nil : vec A 0 -| vec_cons : forall n, A -> vec A n -> vec A (S n). - -Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t := - match v with - | vec_nil => nil - | vec_cons n a va => a::(vec2list va) - end. - -Require Import Omega. -Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T. - intro T. - intro len. - intro v. - induction v; intros. - assert False. - inversion pf. - inversion H. - rename n into len. - destruct n0 as [|n]. - exact a. - apply (IHv n). - omega. - Defined. - -Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n. - induction n. - apply vec_nil. - inversion va; subst. - inversion vb; subst. - apply vec_cons; auto. - Defined. - -Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n. - induction n. - apply vec_nil. - inversion v; subst. - apply vec_cons; auto. - Defined. - -Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop := - match l with - | vec_nil => False - | vec_cons _ n m => (n = a) \/ vec_In a m - end. -Implicit Arguments vec_nil [ A ]. -Implicit Arguments vec_cons [ A n ]. - -Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n). - induction n. - apply (vec_cons t vec_nil). - apply vec_cons; auto. - Defined. - -Definition list2vec {T:Type}(l:list T) : vec T (length l). - induction l. - apply vec_nil. - apply vec_cons; auto. - Defined. - -Definition vec_head {n:nat}{T}(v:vec T (S n)) : T. - inversion v; auto. - Defined. -Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n. - inversion v; auto. - Defined. - -Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1). - induction l1. - apply vec_nil. - apply vec_cons. - simpl in *. - inversion v; subst; auto. - apply IHl1. - inversion v; subst; auto. - Defined. - -Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2). - induction l1. - apply v. - simpl in *. - apply IHl1; clear IHl1. - inversion v; subst; auto. - Defined. - -Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20). - - - -(*******************************************************************************) -(* Shaped Trees *) - -(* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *) -Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type := -| st_nil : @ShapedTree T Q [] -| st_leaf : forall {t}, Q -> @ShapedTree T Q [t] -| st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2). - -Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q := -match st with -| st_nil => [] -| st_leaf _ q => [q] -| st_branch _ _ b1 b2 => (unshape b1),,(unshape b2) -end. - -Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx. - induction st. - apply st_nil. - apply st_leaf. apply f. apply q. - apply st_branch; auto. - Defined. - -Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T} - (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx. - induction idx. - destruct a. - apply st_leaf; auto. - inversion st1. - inversion st2. - auto. - apply st_nil. - apply st_branch; auto. - inversion st1; subst; apply IHidx1; auto. - inversion st2; subst; auto. - inversion st2; subst; apply IHidx2; auto. - inversion st1; subst; auto. - Defined. - -Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx. - induction idx. - destruct a. - apply st_leaf; auto. - apply st_nil. - apply st_branch; auto. - Defined. - -Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx), - mapOptionTree f (unshape t) = unshape (mapShapedTree f t). - intros. - induction t; auto. - simpl. - rewrite IHt1. - rewrite IHt2. - reflexivity. - Qed. - - - - -(*******************************************************************************) -(* Type-Indexed Lists *) - -(* an indexed list *) -Inductive IList (I:Type)(F:I->Type) : list I -> Type := -| INil : IList I F nil -| ICons : forall i is, F i -> IList I F is -> IList I F (i::is). -Implicit Arguments INil [ I F ]. -Implicit Arguments ICons [ I F ]. - -(* a tree indexed by a (Tree (option X)) *) -Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type := -| INone : ITree I F [] -| ILeaf : forall i: I, F i -> ITree I F [i] -| IBranch : forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2). -Implicit Arguments INil [ I F ]. -Implicit Arguments ILeaf [ I F ]. -Implicit Arguments IBranch [ I F ]. - - - - -(*******************************************************************************) -(* Extensional equality on functions *) - -Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)). -Hint Transparent extensionality. -Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2). - intros; apply Build_Equivalence; - intros; compute; intros; auto. - rewrite H; rewrite H0; auto. - Defined. - Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f) - with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality. - unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto. - Defined. -Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3), - (extensionality _ _ f f') -> - (extensionality _ _ g g') -> - (extensionality _ _ (g ○ f) (g' ○ f')). - intros. - unfold extensionality. - unfold extensionality in H. - unfold extensionality in H0. - intros. - rewrite H. - rewrite H0. - auto. - Qed. - - - - - - -(* the Error monad *) -Inductive OrError (T:Type) := -| Error : forall error_message:string, OrError T -| OK : T -> OrError T. -Notation "??? T" := (OrError T) (at level 10). -Implicit Arguments Error [T]. -Implicit Arguments OK [T]. - -Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) := - match oe with - | Error s => Error s - | OK t => f t - end. -Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20). - -Fixpoint list2vecOrError {T}(l:list T)(n:nat) : ???(vec T n) := - match n as N return ???(vec _ N) with - | O => match l with - | nil => OK vec_nil - | _ => Error "list2vecOrError: list was too long" - end - | S n' => match l with - | nil => Error "list2vecOrError: list was too short" - | t::l' => list2vecOrError l' n' >>= fun l'' => OK (vec_cons t l'') - end - end. - -Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type := -| Indexed_Error : forall error_message:string, Indexed f (Error error_message) -| Indexed_OK : forall t, f t -> Indexed f (OK t) -. -Ltac xauto := try apply Indexed_Error; try apply Indexed_OK. - - - - - - -(* for a type with decidable equality, we can maintain lists of distinct elements *) -Section DistinctList. - Context `{V:EqDecidable}. - - Fixpoint addToDistinctList (cv:V)(cvl:list V) := - match cvl with - | nil => cv::nil - | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl') - end. - - Fixpoint removeFromDistinctList (cv:V)(cvl:list V) := - match cvl with - | nil => nil - | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl') - end. - - Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) := - match cvrem with - | nil => cvl - | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl) - end. - - Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) := - match cvl1 with - | nil => cvl2 - | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2) - end. -End DistinctList. diff --git a/src/InitialTerminal_ch2_2.v b/src/InitialTerminal_ch2_2.v index af69c6a..c76208e 100644 --- a/src/InitialTerminal_ch2_2.v +++ b/src/InitialTerminal_ch2_2.v @@ -8,27 +8,42 @@ Require Import Isomorphisms_ch1_5. (* Chapter 2.2: Initial and Terminal Objects *) (******************************************************************************) -(* Definition 2.7 *) -Class Initial -`( C : Category ) := -{ zero : C +Class InitialObject +`{ C : Category } + ( initial_obj : C ) := +{ zero := initial_obj ; bottom : forall a, zero ~> a ; bottom_unique : forall `(f:zero~>a), f ~~ (bottom a) }. Notation "? A" := (bottom A) : category_scope. Notation "0" := zero : category_scope. +Coercion zero : InitialObject >-> ob. +Implicit Arguments InitialObject [[Ob][Hom]]. -(* Definition 2.7 *) -Class Terminal -`( C : Category ) := -{ one : C +Class TerminalObject +`{ C : Category } + ( terminal_obj : C ) := +{ one := terminal_obj ; drop : forall a, a ~> one ; drop_unique : forall `(f:a~>one), f ~~ (drop a) }. Notation "! A" := (drop A) : category_scope. Notation "1" := one : category_scope. +Coercion one : TerminalObject >-> ob. +Implicit Arguments TerminalObject [[Ob][Hom]]. -(* Proposition 2.8 *) -(* FIXME: initial and terminal objects are unique up to iso *) +(* initial objects are unique up to iso *) +Lemma initial_unique_up_to_iso `{C:Category}{io1:C}(i1:InitialObject C io1){io2:C}(i2:InitialObject C io2) : io1 ≅ io2. + refine {| iso_backward := bottom(InitialObject:=i2) io1 ; iso_forward := bottom(InitialObject:=i1) io2 |}. + setoid_rewrite (bottom_unique(InitialObject:=i1)); reflexivity. + setoid_rewrite (bottom_unique(InitialObject:=i2)); reflexivity. + Qed. + +(* terminal objects are unique up to iso *) +Lemma terminal_unique_up_to_iso `{C:Category}{to1:C}(t1:TerminalObject C to1){to2:C}(t2:TerminalObject C to2) : to1 ≅ to2. + refine {| iso_backward := drop(TerminalObject:=t1) to2 ; iso_forward := drop(TerminalObject:=t2) to1 |}. + setoid_rewrite (drop_unique(TerminalObject:=t1)); reflexivity. + setoid_rewrite (drop_unique(TerminalObject:=t2)); reflexivity. + Qed. diff --git a/src/Isomorphisms_ch1_5.v b/src/Isomorphisms_ch1_5.v index 40a5f87..65eaf46 100644 --- a/src/Isomorphisms_ch1_5.v +++ b/src/Isomorphisms_ch1_5.v @@ -45,7 +45,7 @@ Definition iso_id `{C:Category}(A:C) : Isomorphic A A. Defined. (* the composition of two isomorphisms is an isomorphism *) -Definition id_comp `{C:Category}{a b c:C}(i1:Isomorphic a b)(i2:Isomorphic b c) : Isomorphic a c. +Definition iso_comp `{C:Category}{a b c:C}(i1:Isomorphic a b)(i2:Isomorphic b c) : Isomorphic a c. intros; apply (@Build_Isomorphic _ _ C a c (#i1 >>> #i2) (#i2⁻¹ >>> #i1⁻¹)); setoid_rewrite juggle3; [ setoid_rewrite (iso_comp1 i2) | setoid_rewrite (iso_comp2 i1) ]; diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v index e9d3799..1ca2009 100644 --- a/src/MonoidalCategories_ch7_8.v +++ b/src/MonoidalCategories_ch7_8.v @@ -148,13 +148,12 @@ Class DiagonalCat `(mc:MonoidalCat) := }. Class CartesianCat `(mc:MonoidalCat) := -{ car_terminal :> Terminal mc -; car_one : one ≅ pmon_I +{ car_terminal :> TerminalObject mc pmon_I ; car_diagonal : DiagonalCat mc -; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell _)) -; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr _)) +; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (drop a ⋉ a) >>> (#(pmon_cancell _)) +; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ drop a) >>> (#(pmon_cancelr _)) ; car_mn := mc }. Coercion car_diagonal : CartesianCat >-> DiagonalCat. -Coercion car_terminal : CartesianCat >-> Terminal. +Coercion car_terminal : CartesianCat >-> TerminalObject. Coercion car_mn : CartesianCat >-> MonoidalCat. diff --git a/src/NaturalIsomorphisms_ch7_5.v b/src/NaturalIsomorphisms_ch7_5.v index 415d13c..f82dba8 100644 --- a/src/NaturalIsomorphisms_ch7_5.v +++ b/src/NaturalIsomorphisms_ch7_5.v @@ -69,7 +69,7 @@ Definition ni_comp `{C:Category}`{D:Category} intros. destruct N1 as [ ni_iso1 ni_commutes1 ]. destruct N2 as [ ni_iso2 ni_commutes2 ]. - exists (fun A => id_comp (ni_iso1 A) (ni_iso2 A)). + exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)). abstract (intros; simpl; setoid_rewrite <- associativity; setoid_rewrite <- ni_commutes1; @@ -79,18 +79,19 @@ Definition ni_comp `{C:Category}`{D:Category} Defined. Definition ni_respects - `{A:Category}`{B:Category}`{C:Category} - {F0obj}{F0:Functor A B F0obj} - {F1obj}{F1:Functor A B F1obj} - {G0obj}{G0:Functor B C G0obj} - {G1obj}{G1:Functor B C G1obj} + `{A:Category}`{B:Category} + {F0obj}(F0:Functor A B F0obj) + {F1obj}(F1:Functor A B F1obj) + `{C:Category} + {G0obj}(G0:Functor B C G0obj) + {G1obj}(G1:Functor B C G1obj) : (F0 <~~~> F1) -> (G0 <~~~> G1) -> ((F0 >>>> G0) <~~~> (F1 >>>> G1)). intro phi. intro psi. destruct psi as [ psi_niso psi_comm ]. destruct phi as [ phi_niso phi_comm ]. refine {| ni_iso := - (fun a => id_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))) |}. + (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))) |}. abstract (intros; simpl; setoid_rewrite <- associativity; setoid_rewrite fmor_preserves_comp; @@ -159,7 +160,7 @@ Definition if_comp `{C:Category}`{D:Category} intros. destruct N1 as [ ni_iso1 ni_commutes1 ]. destruct N2 as [ ni_iso2 ni_commutes2 ]. - exists (fun A => id_comp (ni_iso1 A) (ni_iso2 A)). + exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)). abstract (intros; simpl; setoid_rewrite <- associativity; setoid_rewrite <- ni_commutes1; @@ -201,17 +202,18 @@ Definition if_right_identity `{C1:Category}`{C2:Category} {Fobj1}(F1:Functor C1 Defined. Definition if_respects - `{A:Category}`{B:Category}`{C:Category} - {F0obj}{F0:Functor A B F0obj} - {F1obj}{F1:Functor A B F1obj} - {G0obj}{G0:Functor B C G0obj} - {G1obj}{G1:Functor B C G1obj} + `{A:Category}`{B:Category} + {F0obj}(F0:Functor A B F0obj) + {F1obj}(F1:Functor A B F1obj) + `{C:Category} + {G0obj}(G0:Functor B C G0obj) + {G1obj}(G1:Functor B C G1obj) : (F0 ≃ F1) -> (G0 ≃ G1) -> ((F0 >>>> G0) ≃ (F1 >>>> G1)). intro phi. intro psi. destruct psi as [ psi_niso psi_comm ]. destruct phi as [ phi_niso phi_comm ]. - exists (fun a => id_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))). + exists (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))). abstract (intros; simpl; setoid_rewrite <- associativity; setoid_rewrite fmor_preserves_comp; @@ -227,11 +229,11 @@ Require Import ProductCategories_ch1_6_1. Context `{C1:Category}`{C2:Category} `{D1:Category}`{D2:Category} - {F1Obj}{F1:@Functor _ _ C1 _ _ D1 F1Obj} - {F2Obj}{F2:@Functor _ _ C2 _ _ D2 F2Obj} + {F1Obj}(F1:@Functor _ _ C1 _ _ D1 F1Obj) + {F2Obj}(F2:@Functor _ _ C2 _ _ D2 F2Obj) `{E1:Category}`{E2:Category} - {G1Obj}{G1:@Functor _ _ D1 _ _ E1 G1Obj} - {G2Obj}{G2:@Functor _ _ D2 _ _ E2 G2Obj}. + {G1Obj}(G1:@Functor _ _ D1 _ _ E1 G1Obj) + {G2Obj}(G2:@Functor _ _ D2 _ _ E2 G2Obj). Definition ni_prod_comp_iso A : (((F1 >>>> G1) **** (F2 >>>> G2)) A) ≅ (((F1 **** F2) >>>> (G1 **** G2)) A). unfold functor_fobj. diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v index e09f8ab..4ab56d2 100644 --- a/src/PreMonoidalCategories.v +++ b/src/PreMonoidalCategories.v @@ -67,7 +67,7 @@ Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b Class PreMonoidalFunctor `(PM1:PreMonoidalCat(C:=C1)(I:=I1)) `(PM2:PreMonoidalCat(C:=C2)(I:=I2)) - (fobj : C1 -> C2 ) := + (fobj : C1 -> C2 ) := { mf_F :> Functor C1 C2 fobj ; mf_i : I2 ≅ mf_F I1 ; mf_first : ∀ a, mf_F >>>> bin_first (mf_F a) <~~~> bin_first a >>>> mf_F @@ -81,17 +81,331 @@ Class PreMonoidalFunctor }. Coercion mf_F : PreMonoidalFunctor >-> Functor. -Definition PreMonoidalFunctorsCompose +Section PreMonoidalFunctorsCompose. + Context `{PM1 :PreMonoidalCat(C:=C1)(I:=I1)} `{PM2 :PreMonoidalCat(C:=C2)(I:=I2)} {fobj12:C1 -> C2 } (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12) `{PM3 :PreMonoidalCat(C:=C3)(I:=I3)} {fobj23:C2 -> C3 } - (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23) - : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12). - admit. - Defined. + (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23). + + Definition compose_mf := PMF12 >>>> PMF23. + + Definition compose_mf_i : I3 ≅ PMF23 (PMF12 I1). + eapply iso_comp. + apply (mf_i(PreMonoidalFunctor:=PMF23)). + apply functors_preserve_isos. + apply (mf_i(PreMonoidalFunctor:=PMF12)). + Defined. + + Definition compose_mf_first a : compose_mf >>>> bin_first (compose_mf a) <~~~> bin_first a >>>> compose_mf. + set (mf_first(PreMonoidalFunctor:=PMF12) a) as mf_first12. + set (mf_first(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_first23. + unfold functor_fobj in *; simpl in *. + unfold compose_mf. + eapply ni_comp. + apply (ni_associativity PMF12 PMF23 (- ⋉fobj23 (fobj12 a))). + eapply ni_comp. + apply (ni_respects PMF12 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)). + apply ni_id. + apply mf_first23. + clear mf_first23. + + eapply ni_comp. + eapply ni_inv. + apply (ni_associativity PMF12 (- ⋉fobj12 a) PMF23). + + apply ni_inv. + eapply ni_comp. + eapply ni_inv. + eapply (ni_associativity _ PMF12 PMF23). + + apply ni_respects; [ idtac | apply ni_id ]. + apply ni_inv. + apply mf_first12. + Defined. + + Definition compose_mf_second a : compose_mf >>>> bin_second (compose_mf a) <~~~> bin_second a >>>> compose_mf. + set (mf_second(PreMonoidalFunctor:=PMF12) a) as mf_second12. + set (mf_second(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_second23. + unfold functor_fobj in *; simpl in *. + unfold compose_mf. + eapply ni_comp. + apply (ni_associativity PMF12 PMF23 (fobj23 (fobj12 a) ⋊-)). + eapply ni_comp. + apply (ni_respects PMF12 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)). + apply ni_id. + apply mf_second23. + clear mf_second23. + + eapply ni_comp. + eapply ni_inv. + apply (ni_associativity PMF12 (fobj12 a ⋊ -) PMF23). + + apply ni_inv. + eapply ni_comp. + eapply ni_inv. + eapply (ni_associativity (a ⋊-) PMF12 PMF23). + + apply ni_respects; [ idtac | apply ni_id ]. + apply ni_inv. + apply mf_second12. + Defined. + + Lemma compose_assoc_coherence a b c : + (#((pmon_assoc (compose_mf a) (fobj23 (fobj12 c))) (compose_mf b)) >>> + compose_mf a ⋊ #((compose_mf_second b) c)) >>> + #((compose_mf_second a) (b ⊗ c)) ~~ + (#((compose_mf_second a) b) ⋉ fobj23 (fobj12 c) >>> + #((compose_mf_second (a ⊗ b)) c)) >>> compose_mf \ #((pmon_assoc a c) b). +(* + set (mf_assoc a b c) as x. + set (mf_assoc (fobj12 a) (fobj12 b) (fobj12 c)) as x'. + unfold functor_fobj in *. + simpl in *. + etransitivity. + etransitivity. + etransitivity. + Focus 3. + apply x'. + + apply iso_shift_left' in x'. + + unfold compose_mf_second; simpl. + unfold functor_fobj; simpl. + set (mf_second (fobj12 b)) as m. + assert (mf_second (fobj12 b)=m). reflexivity. + destruct m; simpl. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite fmor_preserves_id. + setoid_rewrite fmor_preserves_id. + setoid_rewrite fmor_preserves_id. + setoid_rewrite right_identity. + setoid_rewrite left_identity. + setoid_rewrite left_identity. + setoid_rewrite left_identity. + + set (mf_second (fobj12 (a ⊗ b))) as m''. + assert (mf_second (fobj12 (a ⊗ b))=m''). reflexivity. + destruct m''; simpl. + unfold functor_fobj; simpl. + setoid_rewrite fmor_preserves_id. + setoid_rewrite fmor_preserves_id. + setoid_rewrite right_identity. + setoid_rewrite left_identity. + setoid_rewrite left_identity. + setoid_rewrite left_identity. + + set (mf_second (fobj12 a)) as m'. + assert (mf_second (fobj12 a)=m'). reflexivity. + destruct m'; simpl. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite left_identity. + setoid_rewrite left_identity. + setoid_rewrite left_identity. + setoid_rewrite right_identity. + assert (fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 (b ⊗ c)) ~~ id _). + (* *) + setoid_rewrite H2. + setoid_rewrite left_identity. + assert ((id (fobj23 (fobj12 a) ⊗ fobj23 (fobj12 b)) ⋉ fobj23 (fobj12 c)) ~~ id _). + (* *) + setoid_rewrite H3. + setoid_rewrite left_identity. + assert (id (fobj23 (fobj12 a ⊗ fobj12 b)) ⋉ fobj23 (fobj12 c) ~~ id _). + (* *) + setoid_rewrite H4. + setoid_rewrite left_identity. + clear H4. + setoid_rewrite left_identity. + assert (id (fobj23 (fobj12 (a ⊗ b))) ⋉ fobj23 (fobj12 c) ~~ id _). + (* *) + setoid_rewrite H4. + setoid_rewrite right_identity. + clear H4. + assert ((fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 b)) ⋉ fobj23 (fobj12 c) ~~ id _). + (* *) + setoid_rewrite H4. + setoid_rewrite left_identity. + clear H4. + unfold functor_comp in ni_commutes0; simpl in ni_commutes0. + unfold functor_comp in ni_commutes; simpl in ni_commutes. + unfold functor_comp in ni_commutes1; simpl in ni_commutes1. + + + unfold functor_fobj in *. + simpl in *. + setoid_rewrite x in x'. + rewrite H1. + set (ni_commutes0 (a ) + setoid_rewrite fmor_preserves_id. + etransitivity. + eapply comp_respects. + reflexivity. + eapply comp_respects. + eapply comp_respects. + apply + Focus 2. + eapply fmor_preserves_id. + setoid_rewrite (fmor_preserves_id PMF23). +*) + admit. + Qed. + + Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12) := + { mf_i := compose_mf_i + ; mf_F := compose_mf + ; mf_first := compose_mf_first + ; mf_second := compose_mf_second }. + intros; unfold compose_mf_first; unfold compose_mf_second. + set (mf_first (PMF12 a)) as x in *. + set (mf_second (PMF12 b)) as y in *. + assert (x=mf_first (PMF12 a)). reflexivity. + assert (y=mf_second (PMF12 b)). reflexivity. + destruct x. + destruct y. + simpl. + repeat setoid_rewrite left_identity. + repeat setoid_rewrite right_identity. + set (mf_consistent (PMF12 a) (PMF12 b)) as later. + apply comp_respects; try reflexivity. + unfold functor_comp. + unfold functor_fobj; simpl. + set (ni_commutes _ _ (id (fobj12 b))) as x. + unfold functor_comp in x. + simpl in x. + unfold functor_fobj in x. + symmetry in x. + etransitivity. + apply x. + clear x. + set (ni_commutes0 _ _ (id (fobj12 a))) as x'. + unfold functor_comp in x'. + simpl in x'. + unfold functor_fobj in x'. + etransitivity; [ idtac | apply x' ]. + clear x'. + setoid_rewrite fmor_preserves_id. + setoid_rewrite fmor_preserves_id. + setoid_rewrite right_identity. + rewrite <- H in later. + rewrite <- H0 in later. + simpl in later. + apply later. + apply fmor_respects. + apply (mf_consistent a b). + + intros. + simpl. + apply mf_center. + apply mf_center. + auto. + + intros. + unfold compose_mf_first; simpl. + set (mf_first (PMF12 b)) as m. + assert (mf_first (PMF12 b)=m). reflexivity. + destruct m. + simpl. + unfold functor_fobj; simpl. + repeat setoid_rewrite <- fmor_preserves_comp. + repeat setoid_rewrite left_identity. + repeat setoid_rewrite right_identity. + + set (mf_cancell b) as y. + set (mf_cancell (fobj12 b)) as y'. + unfold functor_fobj in *. + setoid_rewrite y in y'. + clear y. + setoid_rewrite <- fmor_preserves_comp in y'. + setoid_rewrite <- fmor_preserves_comp in y'. + etransitivity. + apply y'. + clear y'. + + repeat setoid_rewrite <- associativity. + apply comp_respects; try reflexivity. + apply comp_respects; try reflexivity. + repeat setoid_rewrite associativity. + apply comp_respects; try reflexivity. + + set (ni_commutes _ _ (id (fobj12 I1))) as x. + unfold functor_comp in x. + unfold functor_fobj in x. + simpl in x. + setoid_rewrite <- x. + clear x. + setoid_rewrite fmor_preserves_id. + setoid_rewrite fmor_preserves_id. + setoid_rewrite right_identity. + + rewrite H. + simpl. + clear H. + unfold functor_comp in ni_commutes. + simpl in ni_commutes. + apply ni_commutes. + + intros. + unfold compose_mf_second; simpl. + set (mf_second (PMF12 a)) as m. + assert (mf_second (PMF12 a)=m). reflexivity. + destruct m. + simpl. + unfold functor_fobj; simpl. + repeat setoid_rewrite <- fmor_preserves_comp. + repeat setoid_rewrite left_identity. + repeat setoid_rewrite right_identity. + + set (mf_cancelr a) as y. + set (mf_cancelr (fobj12 a)) as y'. + unfold functor_fobj in *. + setoid_rewrite y in y'. + clear y. + setoid_rewrite <- fmor_preserves_comp in y'. + setoid_rewrite <- fmor_preserves_comp in y'. + etransitivity. + apply y'. + clear y'. + + repeat setoid_rewrite <- associativity. + apply comp_respects; try reflexivity. + apply comp_respects; try reflexivity. + repeat setoid_rewrite associativity. + apply comp_respects; try reflexivity. + + set (ni_commutes _ _ (id (fobj12 I1))) as x. + unfold functor_comp in x. + unfold functor_fobj in x. + simpl in x. + setoid_rewrite <- x. + clear x. + setoid_rewrite fmor_preserves_id. + setoid_rewrite fmor_preserves_id. + setoid_rewrite right_identity. + + rewrite H. + simpl. + clear H. + unfold functor_comp in ni_commutes. + simpl in ni_commutes. + apply ni_commutes. + + apply compose_assoc_coherence. + Defined. + +End PreMonoidalFunctorsCompose. + (*******************************************************************************) (* Braided and Symmetric Categories *) @@ -111,144 +425,305 @@ Class SymmetricCat `(bc:BraidedCat) := }. -Section PreMonoidalSubCategory. +(* a wide subcategory inherits the premonoidal structure if it includes all of the coherence maps *) +Section PreMonoidalWideSubcategory. + + Context `(pm:PreMonoidalCat(I:=pmI)). + Context {Pmor}(S:WideSubcategory pm Pmor). + Context (Pmor_first : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (f ⋉ c)). + Context (Pmor_second : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (c ⋊ f)). + Context (Pmor_assoc : forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)). + Context (Pmor_unassoc: forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)⁻¹). + Context (Pmor_cancell: forall {a}, Pmor _ _ #(pmon_cancell a)). + Context (Pmor_uncancell: forall {a}, Pmor _ _ #(pmon_cancell a)⁻¹). + Context (Pmor_cancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)). + Context (Pmor_uncancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)⁻¹). + Implicit Arguments Pmor_first [[a][b][c][f]]. + Implicit Arguments Pmor_second [[a][b][c][f]]. + + Definition PreMonoidalWideSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' x a)~~{S}~~>(bin_obj' y a). + unfold hom; simpl; intros. + destruct f. + simpl in *. + exists (bin_first(BinoidalCat:=pm) a \ x0). + apply Pmor_first; auto. + Defined. + + Definition PreMonoidalWideSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' a x)~~{S}~~>(bin_obj' a y). + unfold hom; simpl; intros. + destruct f. + simpl in *. + exists (bin_second(BinoidalCat:=pm) a \ x0). + apply Pmor_second; auto. + Defined. + + Instance PreMonoidalWideSubcategory_first (a:S) : Functor S S (fun x => bin_obj' x a) := + { fmor := fun x y f => PreMonoidalWideSubcategory_first_fmor a f }. + unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct f'; simpl in *. + apply (fmor_respects (bin_first(BinoidalCat:=pm) a)); auto. + unfold PreMonoidalWideSubcategory_first_fmor; intros; simpl in *. + apply (fmor_preserves_id (bin_first(BinoidalCat:=pm) a)); auto. + unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct g; simpl in *. + apply (fmor_preserves_comp (bin_first(BinoidalCat:=pm) a)); auto. + Defined. + + Instance PreMonoidalWideSubcategory_second (a:S) : Functor S S (fun x => bin_obj' a x) := + { fmor := fun x y f => PreMonoidalWideSubcategory_second_fmor a f }. + unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct f'; simpl in *. + apply (fmor_respects (bin_second(BinoidalCat:=pm) a)); auto. + unfold PreMonoidalWideSubcategory_second_fmor; intros; simpl in *. + apply (fmor_preserves_id (bin_second(BinoidalCat:=pm) a)); auto. + unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct g; simpl in *. + apply (fmor_preserves_comp (bin_second(BinoidalCat:=pm) a)); auto. + Defined. + + Instance PreMonoidalWideSubcategory_is_Binoidal : BinoidalCat S bin_obj' := + { bin_first := PreMonoidalWideSubcategory_first + ; bin_second := PreMonoidalWideSubcategory_second }. + + Definition PreMonoidalWideSubcategory_assoc_iso + : forall a b c, Isomorphic(C:=S) (bin_obj' (bin_obj' a b) c) (bin_obj' a (bin_obj' b c)). + intros. + refine {| iso_forward := existT _ _ (Pmor_assoc a b c) ; iso_backward := existT _ _ (Pmor_unassoc a b c) |}. + simpl; apply iso_comp1. + simpl; apply iso_comp2. + Defined. + + Definition PreMonoidalWideSubcategory_assoc + : forall a b, + (PreMonoidalWideSubcategory_second a >>>> PreMonoidalWideSubcategory_first b) <~~~> + (PreMonoidalWideSubcategory_first b >>>> PreMonoidalWideSubcategory_second a). + intros. + apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (PreMonoidalWideSubcategory_second a >>>> + PreMonoidalWideSubcategory_first b) (PreMonoidalWideSubcategory_first b >>>> + PreMonoidalWideSubcategory_second a) (fun c => PreMonoidalWideSubcategory_assoc_iso a c b)). + intros; simpl. + unfold PreMonoidalWideSubcategory_second_fmor; simpl. + destruct f; simpl. + set (ni_commutes (pmon_assoc(PreMonoidalCat:=pm) a b) x) as q. + apply q. + Defined. + + Definition PreMonoidalWideSubcategory_assoc_ll + : forall a b, + PreMonoidalWideSubcategory_second (a⊗b) <~~~> + PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a. + intros. + apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ + (PreMonoidalWideSubcategory_second (a⊗b)) + (PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a) + (fun c => PreMonoidalWideSubcategory_assoc_iso a b c)). + intros; simpl. + unfold PreMonoidalWideSubcategory_second_fmor; simpl. + destruct f; simpl. + set (ni_commutes (pmon_assoc_ll(PreMonoidalCat:=pm) a b) x) as q. + unfold functor_comp in q; simpl in q. + set (pmon_coherent_l(PreMonoidalCat:=pm)) as q'. + setoid_rewrite q' in q. + apply q. + Defined. + + Definition PreMonoidalWideSubcategory_assoc_rr + : forall a b, + PreMonoidalWideSubcategory_first (a⊗b) <~~~> + PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b. + intros. + apply ni_inv. + apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ + (PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b) + (PreMonoidalWideSubcategory_first (a⊗b)) + (fun c => PreMonoidalWideSubcategory_assoc_iso c a b)). + intros; simpl. + unfold PreMonoidalWideSubcategory_second_fmor; simpl. + destruct f; simpl. + set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=pm) a b) x) as q. + unfold functor_comp in q; simpl in q. + set (pmon_coherent_r(PreMonoidalCat:=pm)) as q'. + setoid_rewrite q' in q. + apply iso_shift_right' in q. + apply iso_shift_left. + symmetry. + setoid_rewrite iso_inv_inv in q. + setoid_rewrite associativity. + apply q. + Defined. + + Definition PreMonoidalWideSubcategory_cancelr_iso : forall a, Isomorphic(C:=S) (bin_obj' a pmI) a. + intros. + refine {| iso_forward := existT _ _ (Pmor_cancelr a) ; iso_backward := existT _ _ (Pmor_uncancelr a) |}. + simpl; apply iso_comp1. + simpl; apply iso_comp2. + Defined. + + Definition PreMonoidalWideSubcategory_cancell_iso : forall a, Isomorphic(C:=S) (bin_obj' pmI a) a. + intros. + refine {| iso_forward := existT _ _ (Pmor_cancell a) ; iso_backward := existT _ _ (Pmor_uncancell a) |}. + simpl; apply iso_comp1. + simpl; apply iso_comp2. + Defined. + + Definition PreMonoidalWideSubcategory_cancelr : PreMonoidalWideSubcategory_first pmI <~~~> functor_id _. + apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ + (PreMonoidalWideSubcategory_first pmI) (functor_id _) PreMonoidalWideSubcategory_cancelr_iso). + intros; simpl. + unfold PreMonoidalWideSubcategory_first_fmor; simpl. + destruct f; simpl. + apply (ni_commutes (pmon_cancelr(PreMonoidalCat:=pm)) x). + Defined. + + Definition PreMonoidalWideSubcategory_cancell : PreMonoidalWideSubcategory_second pmI <~~~> functor_id _. + apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ + (PreMonoidalWideSubcategory_second pmI) (functor_id _) PreMonoidalWideSubcategory_cancell_iso). + intros; simpl. + unfold PreMonoidalWideSubcategory_second_fmor; simpl. + destruct f; simpl. + apply (ni_commutes (pmon_cancell(PreMonoidalCat:=pm)) x). + Defined. + + Instance PreMonoidalWideSubcategory_PreMonoidal : PreMonoidalCat PreMonoidalWideSubcategory_is_Binoidal pmI := + { pmon_assoc := PreMonoidalWideSubcategory_assoc + ; pmon_assoc_rr := PreMonoidalWideSubcategory_assoc_rr + ; pmon_assoc_ll := PreMonoidalWideSubcategory_assoc_ll + ; pmon_cancelr := PreMonoidalWideSubcategory_cancelr + ; pmon_cancell := PreMonoidalWideSubcategory_cancell + }. + apply Build_Pentagon. + intros; unfold PreMonoidalWideSubcategory_assoc; simpl. + set (pmon_pentagon(PreMonoidalCat:=pm) a b c) as q. + simpl in q. + apply q. + apply Build_Triangle. + intros; unfold PreMonoidalWideSubcategory_assoc; + unfold PreMonoidalWideSubcategory_cancelr; unfold PreMonoidalWideSubcategory_cancell; simpl. + set (pmon_triangle(PreMonoidalCat:=pm) a b) as q. + simpl in q. + apply q. + intros. + + set (pmon_triangle(PreMonoidalCat:=pm)) as q. + apply q. + + intros; simpl; reflexivity. + intros; simpl; reflexivity. + + intros; simpl. + apply Build_CentralMorphism; intros; simpl; destruct g; simpl. + apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c). + apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c). + + intros; simpl. + apply Build_CentralMorphism; intros; simpl; destruct g; simpl. + apply (pmon_cancelr_central(PreMonoidalCat:=pm) a). + apply (pmon_cancelr_central(PreMonoidalCat:=pm) a). + + intros; simpl. + apply Build_CentralMorphism; intros; simpl; destruct g; simpl. + apply (pmon_cancell_central(PreMonoidalCat:=pm) a). + apply (pmon_cancell_central(PreMonoidalCat:=pm) a). + Defined. + +End PreMonoidalWideSubcategory. + + +(* a full subcategory inherits the premonoidal structure if it includes the unit object and is closed under object-pairing *) +(* +Section PreMonoidalFullSubcategory. Context `(pm:PreMonoidalCat(I:=pmI)). - Context {Pobj}{Pmor}(S:SubCategory pm Pobj Pmor). + Context {Pobj}(S:FullSubcategory pm Pobj). Context (Pobj_unit:Pobj pmI). Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)). Implicit Arguments Pobj_closed [[a][b]]. - Context (Pmor_first: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f), - Pmor _ _ (Pobj_closed pa pc) (Pobj_closed pb pc) (f ⋉ c)). - Context (Pmor_second: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f), - Pmor _ _ (Pobj_closed pc pa) (Pobj_closed pc pb) (c ⋊ f)). - Context (Pmor_assoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c), - Pmor _ _ - (Pobj_closed (Pobj_closed pa pb) pc) - (Pobj_closed pa (Pobj_closed pb pc)) - #(pmon_assoc a c b)). - Context (Pmor_unassoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c), - Pmor _ _ - (Pobj_closed pa (Pobj_closed pb pc)) - (Pobj_closed (Pobj_closed pa pb) pc) - #(pmon_assoc a c b)⁻¹). - Context (Pmor_cancell: forall {a}(pa:Pobj a), - Pmor _ _ (Pobj_closed Pobj_unit pa) pa - #(pmon_cancell a)). - Context (Pmor_uncancell: forall {a}(pa:Pobj a), - Pmor _ _ pa (Pobj_closed Pobj_unit pa) - #(pmon_cancell a)⁻¹). - Context (Pmor_cancelr: forall {a}(pa:Pobj a), - Pmor _ _ (Pobj_closed pa Pobj_unit) pa - #(pmon_cancelr a)). - Context (Pmor_uncancelr: forall {a}(pa:Pobj a), - Pmor _ _ pa (Pobj_closed pa Pobj_unit) - #(pmon_cancelr a)⁻¹). - Implicit Arguments Pmor_first [[a][b][c][f]]. - Implicit Arguments Pmor_second [[a][b][c][f]]. - Definition PreMonoidalSubCategory_bobj (x y:S) := + Definition PreMonoidalFullSubcategory_bobj (x y:S) := existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)). - Definition PreMonoidalSubCategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), - (PreMonoidalSubCategory_bobj x a)~~{S}~~>(PreMonoidalSubCategory_bobj y a). + Definition PreMonoidalFullSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), + (PreMonoidalFullSubcategory_bobj x a)~~{S}~~>(PreMonoidalFullSubcategory_bobj y a). unfold hom; simpl; intros. - destruct f. destruct a as [a apf]. destruct x as [x xpf]. destruct y as [y ypf]. simpl in *. - exists (x0 ⋉ a). - apply Pmor_first; auto. + apply (f ⋉ a). Defined. - Definition PreMonoidalSubCategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), - (PreMonoidalSubCategory_bobj a x)~~{S}~~>(PreMonoidalSubCategory_bobj a y). + Definition PreMonoidalFullSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), + (PreMonoidalFullSubcategory_bobj a x)~~{S}~~>(PreMonoidalFullSubcategory_bobj a y). unfold hom; simpl; intros. - destruct f. destruct a as [a apf]. destruct x as [x xpf]. destruct y as [y ypf]. simpl in *. - exists (a ⋊ x0). - apply Pmor_second; auto. + apply (a ⋊ f). Defined. - Instance PreMonoidalSubCategory_first (a:S) - : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj x a) := - { fmor := fun x y f => PreMonoidalSubCategory_first_fmor a f }. - unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *. + Instance PreMonoidalFullSubcategory_first (a:S) + : Functor S S (fun x => PreMonoidalFullSubcategory_bobj x a) := + { fmor := fun x y f => PreMonoidalFullSubcategory_first_fmor a f }. + unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; destruct b; simpl in *. apply (fmor_respects (-⋉x)); auto. - unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; simpl in *. + unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; simpl in *. apply (fmor_preserves_id (-⋉x)); auto. - unfold PreMonoidalSubCategory_first_fmor; intros; - destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *. + unfold PreMonoidalFullSubcategory_first_fmor; intros; + destruct a; destruct a0; destruct b; destruct c; simpl in *. apply (fmor_preserves_comp (-⋉x)); auto. Defined. - Instance PreMonoidalSubCategory_second (a:S) - : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj a x) := - { fmor := fun x y f => PreMonoidalSubCategory_second_fmor a f }. - unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *. + Instance PreMonoidalFullSubcategory_second (a:S) + : Functor S S (fun x => PreMonoidalFullSubcategory_bobj a x) := + { fmor := fun x y f => PreMonoidalFullSubcategory_second_fmor a f }. + unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; destruct b; simpl in *. apply (fmor_respects (x⋊-)); auto. - unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; simpl in *. + unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; simpl in *. apply (fmor_preserves_id (x⋊-)); auto. - unfold PreMonoidalSubCategory_second_fmor; intros; - destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *. + unfold PreMonoidalFullSubcategory_second_fmor; intros; + destruct a; destruct a0; destruct b; destruct c; simpl in *. apply (fmor_preserves_comp (x⋊-)); auto. Defined. - Instance PreMonoidalSubCategory_is_Binoidal : BinoidalCat S PreMonoidalSubCategory_bobj := - { bin_first := PreMonoidalSubCategory_first - ; bin_second := PreMonoidalSubCategory_second }. + Instance PreMonoidalFullSubcategory_is_Binoidal : BinoidalCat S PreMonoidalFullSubcategory_bobj := + { bin_first := PreMonoidalFullSubcategory_first + ; bin_second := PreMonoidalFullSubcategory_second }. - Definition PreMonoidalSubCategory_assoc + Definition PreMonoidalFullSubcategory_assoc : forall a b, - (PreMonoidalSubCategory_second a >>>> PreMonoidalSubCategory_first b) <~~~> - (PreMonoidalSubCategory_first b >>>> PreMonoidalSubCategory_second a). - admit. + (PreMonoidalFullSubcategory_second a >>>> PreMonoidalFullSubcategory_first b) <~~~> + (PreMonoidalFullSubcategory_first b >>>> PreMonoidalFullSubcategory_second a). Defined. - Definition PreMonoidalSubCategory_assoc_ll + Definition PreMonoidalFullSubcategory_assoc_ll : forall a b, - PreMonoidalSubCategory_second (a⊗b) <~~~> - PreMonoidalSubCategory_second b >>>> PreMonoidalSubCategory_second a. + PreMonoidalFullSubcategory_second (a⊗b) <~~~> + PreMonoidalFullSubcategory_second b >>>> PreMonoidalFullSubcategory_second a. intros. - admit. Defined. - Definition PreMonoidalSubCategory_assoc_rr + Definition PreMonoidalFullSubcategory_assoc_rr : forall a b, - PreMonoidalSubCategory_first (a⊗b) <~~~> - PreMonoidalSubCategory_first a >>>> PreMonoidalSubCategory_first b. + PreMonoidalFullSubcategory_first (a⊗b) <~~~> + PreMonoidalFullSubcategory_first a >>>> PreMonoidalFullSubcategory_first b. intros. - admit. Defined. - Definition PreMonoidalSubCategory_I := existT _ pmI (Pobj_unit). + Definition PreMonoidalFullSubcategory_I := existT _ pmI Pobj_unit. - Definition PreMonoidalSubCategory_cancelr : PreMonoidalSubCategory_first PreMonoidalSubCategory_I <~~~> functor_id _. - admit. + Definition PreMonoidalFullSubcategory_cancelr + : PreMonoidalFullSubcategory_first PreMonoidalFullSubcategory_I <~~~> functor_id _. Defined. - Definition PreMonoidalSubCategory_cancell : PreMonoidalSubCategory_second PreMonoidalSubCategory_I <~~~> functor_id _. - admit. + Definition PreMonoidalFullSubcategory_cancell + : PreMonoidalFullSubcategory_second PreMonoidalFullSubcategory_I <~~~> functor_id _. Defined. - Instance PreMonoidalSubCategory_PreMonoidal : PreMonoidalCat PreMonoidalSubCategory_is_Binoidal PreMonoidalSubCategory_I := - { pmon_assoc := PreMonoidalSubCategory_assoc - ; pmon_assoc_rr := PreMonoidalSubCategory_assoc_rr - ; pmon_assoc_ll := PreMonoidalSubCategory_assoc_ll - ; pmon_cancelr := PreMonoidalSubCategory_cancelr - ; pmon_cancell := PreMonoidalSubCategory_cancell + Instance PreMonoidalFullSubcategory_PreMonoidal + : PreMonoidalCat PreMonoidalFullSubcategory_is_Binoidal PreMonoidalFullSubcategory_I := + { pmon_assoc := PreMonoidalFullSubcategory_assoc + ; pmon_assoc_rr := PreMonoidalFullSubcategory_assoc_rr + ; pmon_assoc_ll := PreMonoidalFullSubcategory_assoc_ll + ; pmon_cancelr := PreMonoidalFullSubcategory_cancelr + ; pmon_cancell := PreMonoidalFullSubcategory_cancell }. - admit. - admit. - admit. - admit. - admit. - admit. - admit. Defined. - -End PreMonoidalSubCategory. +End PreMonoidalFullSubcategory. +*) \ No newline at end of file diff --git a/src/PreMonoidalCenter.v b/src/PreMonoidalCenter.v index eb7f608..47af620 100644 --- a/src/PreMonoidalCenter.v +++ b/src/PreMonoidalCenter.v @@ -39,7 +39,7 @@ Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c) Qed. (* the central morphisms of a category constitute a subcategory *) -Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f). +Definition Center `(bc:BinoidalCat) : WideSubcategory bc (fun _ _ f => CentralMorphism f). apply Build_SubCategory; intros. apply Build_CentralMorphism; intros. abstract (setoid_rewrite (fmor_preserves_id(bin_first c)); @@ -51,7 +51,6 @@ Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ apply central_morphisms_compose; auto. Qed. - Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c). intro cm. apply Build_CentralMorphism; simpl; intros. @@ -316,21 +315,14 @@ Section Center_is_Monoidal. Context `(pm:PreMonoidalCat(I:=pmI)). - Definition Center_bobj : Center pm -> Center pm -> Center pm. - apply PreMonoidalSubCategory_bobj. - intros; auto. - Defined. - - Definition Center_is_Binoidal : BinoidalCat (Center pm) Center_bobj. - apply PreMonoidalSubCategory_is_Binoidal. - intros. - apply first_preserves_centrality; auto. - intros. - apply second_preserves_centrality; auto. + Definition Center_is_Binoidal : BinoidalCat (Center pm) bin_obj'. + apply PreMonoidalWideSubcategory_is_Binoidal. + intros; apply first_preserves_centrality; auto. + intros; apply second_preserves_centrality; auto. Defined. - Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal (exist _ pmI I). - apply PreMonoidalSubCategory_PreMonoidal. + Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal pmI. + apply PreMonoidalWideSubcategory_PreMonoidal. Defined. Definition Center_is_Monoidal : MonoidalCat Center_is_PreMonoidal. @@ -338,9 +330,9 @@ Section Center_is_Monoidal. apply Build_CommutativeCat. intros. apply Build_CentralMorphism; unfold hom; - intros; destruct f; destruct a; destruct c; destruct d; destruct b; destruct g; simpl in *. - apply centralmor_second. - apply centralmor_second. + intros; destruct f; destruct g; simpl in *. + apply (centralmor_second(CentralMorphism:=c1)). + apply (centralmor_second(CentralMorphism:=c0)). Defined. End Center_is_Monoidal. diff --git a/src/Preamble.v- b/src/Preamble.v- deleted file mode 100644 index e360627..0000000 --- a/src/Preamble.v- +++ /dev/null @@ -1,142 +0,0 @@ -Require Import Coq.Unicode.Utf8. -Require Import Coq.Classes.RelationClasses. -Require Import Coq.Classes.Morphisms. -Require Import Coq.Setoids.Setoid. -Require Setoid. -Require Import Coq.Strings.String. -Export Coq.Unicode.Utf8. -Export Coq.Classes.RelationClasses. -Export Coq.Classes.Morphisms. -Export Coq.Setoids.Setoid. - -Set Printing Width 130. (* Proof General seems to add an extra two columns of overhead *) -Generalizable All Variables. - -(******************************************************************************) -(* Preamble *) -(******************************************************************************) - -Reserved Notation "a -~- b" (at level 10). -Reserved Notation "a ** b" (at level 10). -Reserved Notation "?? x" (at level 1). -Reserved Notation "a ,, b" (at level 50). -Reserved Notation "!! f" (at level 3). -Reserved Notation "!` x" (at level 2). -Reserved Notation "`! x" (at level 2). -Reserved Notation "a ~=> b" (at level 70, right associativity). -Reserved Notation "H ===> C" (at level 100). -Reserved Notation "f >>=>> g" (at level 45). -Reserved Notation "a ~~{ C }~~> b" (at level 100). -Reserved Notation "f <--> g" (at level 20). -Reserved Notation "! f" (at level 2). -Reserved Notation "? f" (at level 2). -Reserved Notation "# f" (at level 2). -Reserved Notation "f '⁻¹'" (at level 1). -Reserved Notation "a ≅ b" (at level 70, right associativity). -Reserved Notation "C 'ᵒᴾ'" (at level 1). -Reserved Notation "F \ a" (at level 20). -Reserved Notation "f >>> g" (at level 45). -Reserved Notation "a ~~ b" (at level 54). -Reserved Notation "a ~> b" (at level 70, right associativity). -Reserved Notation "a ≃ b" (at level 70, right associativity). -Reserved Notation "a ≃≃ b" (at level 70, right associativity). -Reserved Notation "a ~~> b" (at level 70, right associativity). -Reserved Notation "F ~~~> G" (at level 70, right associativity). -Reserved Notation "F <~~~> G" (at level 70, right associativity). -Reserved Notation "a ⊗ b" (at level 40). -Reserved Notation "a ⊗⊗ b" (at level 40). -Reserved Notation "a ⊕ b" (at level 40). -Reserved Notation "a ⊕⊕ b" (at level 40). -Reserved Notation "f ⋉ A" (at level 40). -Reserved Notation "A ⋊ f" (at level 40). -Reserved Notation "- ⋉ A" (at level 40). -Reserved Notation "A ⋊ -" (at level 40). -Reserved Notation "a *** b" (at level 40). -Reserved Notation "a ;; b" (at level 45). -Reserved Notation "[# f #]" (at level 2). -Reserved Notation "a ---> b" (at level 11, right associativity). -Reserved Notation "a <- b" (at level 100, only parsing). -Reserved Notation "G |= S" (at level 75). -Reserved Notation "F -| G" (at level 75). -Reserved Notation "a :: b" (at level 60, right associativity). -Reserved Notation "a ++ b" (at level 60, right associativity). -Reserved Notation "<[ t @]>" (at level 30). -Reserved Notation "<[ t @ n ]>" (at level 30). -Reserved Notation "<[ e ]>" (at level 30). -Reserved Notation "'Λ' x : t :-> e" (at level 9, right associativity, x ident). -Reserved Notation "R ==> R' " (at level 55, right associativity). -Reserved Notation "f ○ g" (at level 100). -Reserved Notation "a ==[ n ]==> b" (at level 20). -Reserved Notation "a ==[ h | c ]==> b" (at level 20). -Reserved Notation "H /⋯⋯/ C" (at level 70). -Reserved Notation "pf1 === pf2" (at level 80). -Reserved Notation "a |== b @@ c" (at level 100). -Reserved Notation "f >>>> g" (at level 45). -Reserved Notation "a >>[ n ]<< b" (at level 100). -Reserved Notation "f **** g" (at level 40). -Reserved Notation "C × D" (at level 40). -Reserved Notation "C ×× D" (at level 45). -Reserved Notation "C ⁽ºᑭ⁾" (at level 1). - -Reserved Notation "'<[' a '|-' t ']>'" (at level 35). - -Reserved Notation "Γ '∌' x" (at level 10). -Reserved Notation "Γ '∌∌' x" (at level 10). -Reserved Notation "Γ '∋∋' x : a ∼ b" (at level 10, x at level 99). -Reserved Notation "Γ '∋' x : c" (at level 10, x at level 99). - -Reserved Notation "a ⇛ b" (at level 40). -Reserved Notation "φ₁ →→ φ₂" (at level 11, right associativity). -Reserved Notation "a '⊢ᴛy' b : c" (at level 20, b at level 99, c at level 80). -Reserved Notation "a '⊢ᴄᴏ' b : c ∼ d" (at level 20, b at level 99). -Reserved Notation "Γ '+' x : c" (at level 50, x at level 99). -Reserved Notation "Γ '++' x : a ∼ b" (at level 50, x at level 99). -Reserved Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" (at level 11, φ₂ at level 99, right associativity). - -Reserved Notation "Γ > past : present '⊢ᴇ' succedent" - (at level 52, past at level 99, present at level 50, succedent at level 50). - -Reserved Notation "'η'". -Reserved Notation "'ε'". -Reserved Notation "'★'". - -Notation "a +++ b" := (append a b) (at level 100). -Close Scope nat_scope. (* so I can redefine '1' *) - -Delimit Scope arrow_scope with arrow. -Delimit Scope biarrow_scope with biarrow. -Delimit Scope garrow_scope with garrow. - -Notation "f ○ g" := (fun x => f(g(x))). -Notation "?? T" := (option T). - -(* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *) -Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100). -Notation "'Λ' '⟨' x ',' y '⟩' e" := (fun xy => match xy with (a,b) => (fun x y => e) a b end) (at level 100). -Notation "'Λ' '⟨' x ',' '⟨' y ',' z '⟩' '⟩' e" := - (fun xyz => match xyz with (a,bc) => match bc with (b,c) => (fun x y z => e) a b c end end) (at level 100). -Notation "'Λ' '⟨' '⟨' x ',' y '⟩' ',' z '⟩' e" := - (fun xyz => match xyz with (ab,c) => match ab with (a,b) => (fun x y z => e) a b c end end) (at level 100). - -Notation "∀ x y z u q , P" := (forall x y z u q , P) - (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity) - : type_scope. -Notation "∀ x y z u q v , P" := (forall x y z u q v , P) - (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity) - : type_scope. -Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P) - (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity) - : type_scope. -Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P) - (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity) - : type_scope. -Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P) - (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity) - : type_scope. -Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P) - (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, right associativity) - : type_scope. -Notation "∀ x y z u q v a b r s t , P" := (forall x y z u q v a b r s t , P) - (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, t ident, - right associativity) - : type_scope. diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v index 78bf98f..2a88a7a 100644 --- a/src/Subcategories_ch7_1.v +++ b/src/Subcategories_ch7_1.v @@ -11,38 +11,64 @@ Require Import OppositeCategories_ch1_6_2. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. -(* Any morphism-predicate which is closed under composition and - * passing to identity morphisms (of either the domain or codomain) - * - * We could recycle the "predicate on morphisms" to determine the - * "predicate on objects", but this causes technical difficulties with - * Coq *) -Class SubCategory `(C:Category Ob Hom)(Pobj:Ob->Type)(Pmor:forall a b:Ob, Pobj a -> Pobj b -> (a~>b) ->Type) : Type := -{ sc_id_included : forall (a:Ob)(pa:Pobj a), Pmor _ _ pa pa (id a) -; sc_comp_included : forall (a b c:Ob)(pa:Pobj a)(pb:Pobj b)(pc:Pobj c) f g, - (Pmor _ _ pa pb f) -> (Pmor _ _ pb pc g) -> (Pmor _ _ pa pc (f>>>g)) +(* + * See the README for an explanation of why there is "WideSubcategory" + * and "FullSubcategory" but no "Subcategory" + *) + +(* a full subcategory requires nothing more than a predicate on objects *) +Class FullSubcategory `(C:Category)(Pobj:C->Type) := { }. + +(* the category construction for full subcategories is simpler: *) +Instance FullSubCategoriesAreCategories `(fsc:@FullSubcategory Ob Hom C Pobj) + : Category (sigT Pobj) (fun dom ran => (projT1 dom)~~{C}~~>(projT1 ran)) := +{ id := fun t => id (projT1 t) +; eqv := fun a b f g => eqv _ _ f g +; comp := fun a b c f g => f >>> g }. + intros; apply Build_Equivalence. unfold Reflexive. + intros; reflexivity. + unfold Symmetric; intros; simpl; symmetry; auto. + unfold Transitive; intros; simpl. transitivity y; auto. + intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto. + intros; simpl. apply left_identity. + intros; simpl. apply right_identity. + intros; simpl. apply associativity. + Defined. +Coercion FullSubCategoriesAreCategories : FullSubcategory >-> Category. (* every category is a subcategory of itself! *) +(* Instance IdentitySubCategory `(C:Category Ob Hom) : SubCategory C (fun _ => True) (fun _ _ _ _ _ => True). intros; apply Build_SubCategory. intros; auto. intros; auto. Defined. - -(* a full subcategory requires nothing more than a predicate on objects *) -Definition FullSubcategory `(C:Category)(Pobj:C->Type) : SubCategory C Pobj (fun _ _ _ _ _ => True). - apply Build_SubCategory; intros; auto. +(* the inclusion operation from a subcategory to its host is a functor *) +Instance InclusionFunctor `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor) + : Functor SP C (fun x => projT1 x) := + { fmor := fun dom ran f => projT1 f }. + intros. unfold eqv in H. simpl in H. auto. + intros. simpl. reflexivity. + intros. simpl. reflexivity. Defined. +*) + + +(* a wide subcategory includes all objects, so it requires nothing more than a predicate on each hom-set *) +Class WideSubcategory `(C:Category Ob Hom)(Pmor:forall a b:Ob, (a~>b) ->Type) : Type := +{ wsc_id_included : forall (a:Ob), Pmor a a (id a) +; wsc_comp_included : forall (a b c:Ob) f g, (Pmor a b f) -> (Pmor b c g) -> (Pmor a c (f>>>g)) +}. -Section SubCategoriesAreCategories. - (* Any such predicate determines a category *) - Instance SubCategoriesAreCategories `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor) - : Category (sigT Pobj) (fun dom ran => sigT (fun f => Pmor (projT1 dom) (projT1 ran) (projT2 dom) (projT2 ran) f)) := - { id := fun t => existT (fun f => Pmor _ _ _ _ f) (id (projT1 t)) (sc_id_included _ (projT2 t)) +(* the category construction for full subcategories is simpler: *) +Instance WideSubCategoriesAreCategories `{C:Category(Ob:=Ob)}{Pmor}(wsc:WideSubcategory C Pmor) + : Category Ob (fun x y => sigT (Pmor x y)) := + { id := fun t => existT _ (id t) (@wsc_id_included _ _ _ _ wsc t) ; eqv := fun a b f g => eqv _ _ (projT1 f) (projT1 g) - ; comp := fun a b c f g => existT (fun f => Pmor _ _ _ _ f) (projT1 f >>> projT1 g) - (sc_comp_included _ _ _ (projT2 a) (projT2 b) (projT2 c) _ _ (projT2 f) (projT2 g)) + ; comp := fun a b c f g => existT (Pmor a c) (projT1 f >>> projT1 g) + (@wsc_comp_included _ _ _ _ wsc _ _ _ _ _ (projT2 f) (projT2 g)) + }. intros; apply Build_Equivalence. unfold Reflexive. intros; reflexivity. @@ -53,47 +79,51 @@ Section SubCategoriesAreCategories. intros; simpl. apply right_identity. intros; simpl. apply associativity. Defined. -End SubCategoriesAreCategories. -Coercion SubCategoriesAreCategories : SubCategory >-> Category. +Coercion WideSubCategoriesAreCategories : WideSubcategory >-> Category. -(* the inclusion operation from a subcategory to its host is a functor *) -Instance InclusionFunctor `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor) - : Functor SP C (fun x => projT1 x) := - { fmor := fun dom ran f => projT1 f }. - intros. unfold eqv in H. simpl in H. auto. - intros. simpl. reflexivity. - intros. simpl. reflexivity. - Defined. +(* the full image of a functor is a full subcategory *) +Section FullImage. -Definition FullImage `(F:Functor(c1:=C)(c2:=D)(fobj:=Fobj)) := FullSubcategory D (fun d => { c:C & (Fobj c)=d }). + Context `(F:Functor(c1:=C)(c2:=D)). -(* any functor may be restricted to its image *) -Section RestrictToImage. - Context `(F:Functor(c1:=C)(c2:=D)(fobj:=Fobj)). - Definition RestrictToImage_fobj : C -> FullImage F. - intros. - exists (F X). - exists X. - reflexivity. - Defined. - Definition RestrictToImage_fmor a b (f:a~>b) : (RestrictToImage_fobj a)~~{FullImage F}~~>(RestrictToImage_fobj b). - exists (F \ f); auto. + Instance FullImage : Category C (fun x y => (F x)~~{D}~~>(F y)) := + { id := fun t => id (F t) + ; eqv := fun x y f g => eqv(Category:=D) _ _ f g + ; comp := fun x y z f g => comp(Category:=D) _ _ _ f g + }. + intros; apply Build_Equivalence. unfold Reflexive. + intros; reflexivity. + unfold Symmetric; intros; simpl; symmetry; auto. + unfold Transitive; intros; simpl. transitivity y; auto. + intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto. + intros; simpl. apply left_identity. + intros; simpl. apply right_identity. + intros; simpl. apply associativity. + Defined. + + Instance FullImage_InclusionFunctor : Functor FullImage D (fun x => F x) := + { fmor := fun x y f => f }. + intros; auto. + intros; simpl; reflexivity. + intros; simpl; reflexivity. Defined. - Instance RestrictToImage : Functor C (FullImage F) RestrictToImage_fobj := - { fmor := fun a b f => RestrictToImage_fmor a b f }. + + Instance RestrictToImage : Functor C FullImage (fun x => x) := + { fmor := fun a b f => F \ f }. intros; simpl; apply fmor_respects; auto. intros; simpl; apply fmor_preserves_id; auto. intros; simpl; apply fmor_preserves_comp; auto. Defined. - Lemma RestrictToImage_splits : F ≃ (RestrictToImage >>>> InclusionFunctor _ _). - exists (fun A => iso_id (F A)). - intros; simpl. - setoid_rewrite left_identity. - setoid_rewrite right_identity. - reflexivity. - Qed. -End RestrictToImage. + Lemma RestrictToImage_splits : F ~~~~ (RestrictToImage >>>> FullImage_InclusionFunctor). + unfold EqualFunctors; simpl; intros; apply heq_morphisms_intro. + apply fmor_respects. + auto. + Defined. + +End FullImage. + +(* Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor) {fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj := { fmor := fun a b f => fmor F f }. @@ -101,7 +131,9 @@ Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj intros. apply (@fmor_preserves_id _ _ _ _ _ _ _ F a). intros. apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f). Defined. +*) +(* (* if a functor's range falls within a subcategory, then it is already a functor into that subcategory *) Section FunctorWithRangeInSubCategory. Context `(Cat1:Category O1 Hom1). @@ -160,6 +192,7 @@ Section FunctorWithRangeInSubCategory. *) End Opposite. End FunctorWithRangeInSubCategory. +*) (* Definition 7.1: faithful functors *) @@ -196,6 +229,7 @@ Definition WeaklyMonic G >>>> F ≃ H >>>> F -> G ≃ H. +(* Section FullFaithfulFunctor_section. Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)). Context (F_full:FullFunctor F). @@ -216,6 +250,9 @@ Section FullFaithfulFunctor_section. Definition ff_functor_section_fmor {a b:FullImage F} (f:a~~{FullImage F}~~>b) : (ff_functor_section_fobj a)~~{C1}~~>(ff_functor_section_fobj b). destruct a as [ a1 [ a2 a3 ] ]. + destruct b as [ b1 [ b2 b3 ] ]. + set (@ff_invert _ _ _ _ _ _ _ _ F_full _ _ f) as f'. + destruct a as [ a1 [ a2 a3 ] ]. subst. unfold ff_functor_section_fobj. simpl. @@ -250,8 +287,8 @@ Section FullFaithfulFunctor_section. Instance ff_functor_section_functor : Functor (FullImage F) C1 ff_functor_section_fobj := { fmor := fun a b f => ff_functor_section_fmor f }. abstract (intros; - destruct a; destruct b; destruct s; destruct s0; destruct f; destruct f'; simpl in *; - subst; simpl; set (F_full x1 x2 x3) as ff1; set (F_full x1 x2 x4) as ff2; destruct ff1; destruct ff2; + destruct a; destruct b; destruct s; destruct s0; simpl in *; + subst; simpl; set (F_full x1 x2 f) as ff1; set (F_full x1 x2 f') as ff2; destruct ff1; destruct ff2; apply F_faithful; etransitivity; [ apply e | idtac ]; symmetry; @@ -269,8 +306,6 @@ Section FullFaithfulFunctor_section. destruct c as [ c1 [ c2 c3 ] ]; subst; simpl in *; - destruct f; - destruct g; simpl in *; apply ff_functor_section_respectful). Defined. @@ -280,10 +315,9 @@ Section FullFaithfulFunctor_section. FullImage F }~~> existT (fun d : C2, {c : C1 & Fobj c = d}) (Fobj b2) (existT (fun c : C1, Fobj c = Fobj b2) b2 (eq_refl _))) - : F \ (let (x1, _) := F_full a2 b2 (let (x1, _) := f in x1) in x1) ~~ projT1 f. - destruct f. + : F \ (let (x1, _) := F_full a2 b2 f in x1) ~~ f. simpl. - set (F_full a2 b2 x) as qq. + set (F_full a2 b2 f) as qq. destruct qq. apply e. Qed. @@ -296,11 +330,10 @@ Section FullFaithfulFunctor_section. destruct b as [ b1 [ b2 b3 ] ]. subst. simpl in *. - inversion f; subst. - inversion f'; subst. simpl in *. apply heq_morphisms_intro. simpl. + unfold RestrictToImage_fmor; simpl. etransitivity; [ idtac | apply H ]. clear H. clear f'. @@ -327,8 +360,7 @@ Section FullFaithfulFunctor_section. destruct A as [ a1 [ a2 a3 ] ]. destruct B as [ b1 [ b2 b3 ] ]. simpl. - destruct f; subst. - simpl. + unfold RestrictToImage_fmor; simpl. setoid_rewrite left_identity. setoid_rewrite right_identity. set (F_full a2 b2 x) as qr. @@ -427,3 +459,4 @@ Section FullFaithfulFunctor_section. Opaque ff_functor_section_splits_niso_helper. End FullFaithfulFunctor_section. +*) \ No newline at end of file -- 1.7.10.4