From: Adam Megacz Date: Tue, 5 Apr 2011 06:31:50 +0000 (+0000) Subject: remove Arrows.v X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=37fcc257b54bd8d13ad27f9d80d4a0298429c7ce remove Arrows.v --- diff --git a/src/Arrows.v b/src/Arrows.v deleted file mode 100644 index 50ba604..0000000 --- a/src/Arrows.v +++ /dev/null @@ -1,965 +0,0 @@ -(*******************************************************************************) -(* Hughes Arrows *) -(*******************************************************************************) - -Generalizable All Variables. -Require Import Preamble. -Require Import General. -Require Import Categories_ch1_3. -Require Import Functors_ch1_4. -Require Import Isomorphisms_ch1_5. -Require Import ProductCategories_ch1_6_1. -Require Import EpicMonic_ch2_1. -Require Import InitialTerminal_ch2_2. -Require Import Subcategories_ch7_1. -Require Import NaturalTransformations_ch7_4. -Require Import NaturalIsomorphisms_ch7_5. -Require Import Coherence_ch7_8. -Require Import MonoidalCategories_ch7_8. -Require Import FreydCategories. -Require Import CoqCategory. - -(* these notations are more for printing back than writing input (helps coax Coq into better pretty-printing) *) -Notation "'_swap'" := (fun xy => let (a0, b0) := xy in ⟨b0, a0 ⟩). -Notation "'_assoc'" := (fun xyz => let (ab, c) := xyz in let (a0, b0) := ab in ⟨a0, ⟨b0, c ⟩ ⟩). - -Class Arrow -( arr_hom' : Type->Type->Type ) := -{ arr_hom := arr_hom' (* hack to make Coq notations work *) where "a ~> b" := (arr_hom a b) - -; arr_arr : forall {a b}, (a->b) -> a~>b -; arr_comp : forall {a b c}, a~>b -> b~>c -> a~>c where "f >>> g" := (arr_comp f g) -; arr_first : forall {a b} c, a~>b -> (a*c)~>(b*c) where "f ⋊ d" := (arr_first d f) - -; arr_eqv : forall {a b}, (a~>b) -> (a~>b) -> Prop where "a ~~ b" := (arr_eqv a b) -; arr_eqv_equivalence : forall {a b}, Equivalence (@arr_eqv a b) - -; arr_comp_respects : forall {a b c}, Proper (arr_eqv ==> arr_eqv ==> arr_eqv) (@arr_comp a b c) -; arr_first_respects : forall {a b c}, Proper (arr_eqv ==> arr_eqv) (@arr_first a b c) -; arr_arr_respects : forall {a b}(f g:a->b), Proper (extensionality a b ==> arr_eqv) (@arr_arr a b) - -; arr_left_identity : forall `(f:a~>b), (arr_arr (fun x => x)) >>> f ~~ f -; arr_right_identity : forall `(f:a~>b), f >>> (arr_arr (fun x => x)) ~~ f -; arr_associativity : forall `(f:a~>b)`(g:b~>c)`(h:c~>d), (f >>> g) >>> h ~~ f >>> (g >>> h) -; arr_comp_preserves : forall `(f:a->b)`(g:b->c), arr_arr (g ○ f) ~~ arr_arr f >>> arr_arr g -; arr_extension : forall a b (f:a->b), forall d, (arr_arr f) ⋊ d ~~ arr_arr (Λ⟨x,y⟩ ⟨f x,y⟩) -; arr_first_preserves : forall {d}`(f:a~>b)`(g:b~>c), (f >>> g) ⋊ d ~~ f ⋊ d >>> g ⋊ d -; arr_exchange : forall `(f:a~>b)`(g:c->d), arr_arr (Λ⟨x,y⟩ ⟨x,g y⟩) >>> f ⋊ _ ~~ f ⋊ _ >>> arr_arr (Λ⟨x,y⟩ ⟨x,g y⟩) -; arr_unit : forall {c}`(f:a~>b), f ⋊ c >>> arr_arr (Λ⟨x,y⟩x) ~~ (arr_arr (Λ⟨x,y⟩x)) >>> f -; arr_association : forall {c}{d}`(f:a~>b), (f⋊c)⋊d >>> arr_arr(Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩) ~~ arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩) >>> f⋊_ -}. - -(* - ; loop : forall {a}{b}{c}, (a⊗c~>b⊗c) -> (a~>b) - (* names taken from Figure 7 of Paterson's "A New Notation for Arrows", which match the CCA paper *) - ; left_tightening : forall {a}{b}{c}{f:a⊗b~>c⊗b}{h}, loop (first c a b h >>> f) ~~ h >>> loop f - ; right_tightening : forall {a}{b}{c}{f:a⊗b~>c⊗b}{h}, loop (f >>> first c a b h) ~~ loop f >>> h - ; sliding : forall {a}{b}{c}{f:a⊗c~>b⊗c}{k}, central k -> loop (f >>> second _ _ b k) ~~ loop (second _ _ a k >>> f) - ; vanishing : forall {a}{b}{c}{d}{f:(a⊗c)⊗d~>(b⊗c)⊗d}, loop (loop f) ~~ loop (#assoc⁻¹ >>> f >>> #assoc) - ; superposing : forall {a}{b}{c}{d}{f:a⊗c~>b⊗c}, second _ _ d (loop f) ~~ loop (#assoc >>> second _ _ d f >>> #assoc⁻¹) -*) - -(* register the arrow equivalence relation as a rewritable setoid, with >>> and first as morphisms *) -Add Parametric Relation `(ba:Arrow)(a b:Type) : (arr_hom a b) arr_eqv - reflexivity proved by (@Equivalence_Reflexive _ _ (@arr_eqv_equivalence _ _ a b)) - symmetry proved by (@Equivalence_Symmetric _ _ (@arr_eqv_equivalence _ _ a b)) - transitivity proved by (@Equivalence_Transitive _ _ (@arr_eqv_equivalence _ _ a b)) - as parametric_relation_arr_eqv. - Add Parametric Morphism `(ba:Arrow)(a b c:Type) : (@arr_comp _ _ a b c) - with signature (arr_eqv ==> arr_eqv ==> arr_eqv) as parametric_morphism_arr_comp. - intros; apply arr_comp_respects; auto. - Defined. - Add Parametric Morphism `(ba:Arrow)(a b c:Type) : (@arr_first _ _ a b c) - with signature (arr_eqv ==> arr_eqv) as parametric_morphism_arr_first. - intros; apply arr_first_respects; auto. - Defined. - -Notation "a ~> b" := (arr_hom a b) :arrow_scope. -Notation "f >>> g" := (arr_comp f g) :arrow_scope. -Notation "f ⋊ d" := (arr_first d f) :arrow_scope. -Notation "a ~~ b" := (arr_eqv a b) :arrow_scope. - -Open Scope arrow_scope. - -(* Formalized Definition 2.3 *) -Class BiArrow -( biarr_hom : Type -> Type -> Type ) := -{ biarr_super :> Arrow biarr_hom - -; biarr_biarr : forall {a b}, (a->b) -> (b->a) -> (a~>b) where "f <--> g" := (biarr_biarr g f) -; biarr_inv : forall {a b}, a~>b -> b~>a where "! f" := (biarr_inv f) - -(* BiArrow laws are numbered based on section 5 of Hunen+Jacobs paper *) -; biarr_law3' : forall {a}{b}{c}{f1}{f2:b->c}{g1}{c2:a->b}, f1<-->c2 >>> g1<-->f2 ~~ (f1 ○ g1) <--> (f2 ○ c2) -; biarr_law4' : forall {a}{b}{f:a~>b}, (fun x=>x)<-->(fun x=>x) >>> f ~~ f -; biarr_law4'': forall {a}{b}{f:a~>b}, f >>> (fun x=>x)<-->(fun x=>x) ~~ f -; biarr_law8' : forall {a}{b}{f:a->b}{g}{c}, (f<-->g) ⋊ c ~~ (Λ⟨x,y⟩ ⟨f x,y⟩)<-->(Λ⟨x,y⟩ ⟨g x,y⟩) -; biarr_law22 : forall {a}{b}{f:a~>b}, !(!f) ~~ f -; biarr_law23 : forall {a}{b}{c}{f:b~>c}{g:a~>b}, !(g >>> f) ~~ !f >>> !g -; biarr_law24 : forall {a}{b}{f:a->b}{g}, !(f<-->g) ~~ g<-->f -; biarr_law25 : forall {a}{b}{f:a~>b}{c}, !(f ⋊ _) ~~ (!f) ⋊ c -; biarr_law6' : forall {a}{b}{c}{d}{f:a->b}{g}{h:c~>d}, (h ⋊ _) >>> (Λ⟨x,y⟩ ⟨x,f y⟩)<-->(Λ⟨x,y⟩ ⟨x,g y⟩) ~~ - (Λ⟨x,y⟩ ⟨x,f y⟩)<-->(Λ⟨x,y⟩ ⟨x,g y⟩) >>> (h ⋊ _) - -(* for complete example, we'd also need biarr_biarr_respects and biarr_inv_respects, but this paper isn't about BiArrows *) -}. - -Notation "f <--> g" := (biarr_biarr g f) :biarrow_scope. -Notation "! f" := (biarr_inv f) :biarrow_scope. - -Open Scope biarrow_scope. -Inductive left_invertible `{ba:BiArrow}{a}{b}(f:a~>b) : Prop := LI : ((f >>> !f) ~~ (arr_arr (fun x=>x))) -> left_invertible f. -Inductive right_invertible `{ba:BiArrow}{a}{b}(f:a~>b) : Prop := RI : ((!f >>> f) ~~ (arr_arr (fun x=>x))) -> right_invertible f. -Close Scope biarrow_scope. - -Hint Extern 4 (?A ~~ ?A) => reflexivity. -Hint Extern 6 (?X ~~ ?Y) => apply Equivalence_Symmetric. -Hint Extern 7 (?X ~~ ?Z) => match goal with [H : ?X ~~ ?Y, H' : ?Y ~~ ?Z |- ?X ~~ ?Z] => transitivity Y end. -Hint Extern 10 (?X >>> ?Y ~~ ?Z >>> ?Q) => apply arr_comp_respects; auto. -Hint Constructors Arrow. - -(* Formalized Lemma 3.2 *) -Definition arrows_are_categories : forall `(ba:Arrow), Category Type arr_hom. - intros. - refine - {| id := fun a => arr_arr (fun x => x) - ; comp := fun a b c f g => arr_comp f g - ; eqv := fun a b f g => arr_eqv f g |}; intros; auto. - apply arr_left_identity. - apply arr_right_identity. - apply arr_associativity. - Defined. -Coercion arrows_are_categories : Arrow >-> Category. - -(* a tactic to throw the kitchen sink at Arrow goals; using ATBR (http://coq.inria.fr/contribs/ATBR.html) would be a better idea *) -Ltac magic := - repeat apply arr_comp; - repeat apply arr_first; - repeat apply arr_arr_respects; - repeat setoid_rewrite arr_left_identity; - repeat setoid_rewrite arr_right_identity; - repeat setoid_rewrite <- arr_comp_preserves; - repeat setoid_rewrite arr_extension; - repeat setoid_rewrite arr_first_preserves. - (* need to handle associat, exchange, unit, association *) - -Definition Arrows_are_Binoidal `(ba:Arrow) : BinoidalCat ((arrows_are_categories ba)) prod. - intros; apply Build_BinoidalCat; intros; - [ apply (Build_Functor _ _ (ba) _ _ (ba) (fun X => X*a) - (fun X Y f => (arr_first(Arrow:=ba)) a f)) - | apply (Build_Functor _ _ (ba) _ _ (ba) (fun X => a*X) - (fun X Y f => arr_arr (Λ⟨x,y⟩ ⟨y,x⟩) >>> arr_first(Arrow:=ba) a f >>> arr_arr(Arrow:=ba) (Λ⟨x,y⟩ ⟨y,x⟩))) - ]; intros; simpl; intros; - [ apply arr_first_respects; auto - | setoid_rewrite arr_extension; repeat setoid_rewrite <- arr_comp_preserves; apply arr_arr_respects - | symmetry; apply arr_first_preserves - | repeat apply arr_comp_respects; try reflexivity - | setoid_rewrite arr_extension; repeat setoid_rewrite <- arr_comp_preserves - | setoid_rewrite arr_first_preserves - ]; intros; auto. - idtac. - unfold extensionality; intros; destruct x; auto. - simpl in H; setoid_rewrite H; auto. - apply arr_arr_respects; intros; auto. - unfold extensionality; intros; destruct x; auto. - repeat rewrite arr_associativity; repeat setoid_rewrite <- arr_comp_preserves. - apply arr_comp_respects; try reflexivity. - apply arr_comp_respects; try reflexivity. - setoid_rewrite <- arr_associativity. - repeat setoid_rewrite <- arr_comp_preserves. - setoid_rewrite <- arr_associativity. - apply arr_comp_respects; try reflexivity. - transitivity (arr_comp ((arr_arr(Arrow:=ba)) (fun x=>x)) (arr_first(Arrow:=ba) a g)). - apply arr_comp_respects; try reflexivity. - apply arr_arr_respects; intros; auto; unfold extensionality; intros; auto; try destruct x; auto. - apply arr_left_identity. - Defined. - - Definition arrow_cancelr_iso : forall `(ba:Arrow)(A:ba), (Isomorphic(C:=ba)) (A*Datatypes.unit) A. - intros; apply (Build_Isomorphic _ _ ba (A*Datatypes.unit) A (arr_arr (Λ⟨x,y⟩ x)) (arr_arr (fun x => ⟨x,tt⟩))). - simpl; setoid_rewrite <- arr_comp_preserves; apply arr_arr_respects. - intros; destruct X. auto. auto. - unfold extensionality; intros; simpl. destruct x. destruct u. auto. - simpl; setoid_rewrite <- arr_comp_preserves; reflexivity. - Defined. - Definition arrow_cancelr_ni_iso `(ba:Arrow) - : (((bin_first(BinoidalCat:=Arrows_are_Binoidal ba)) (Datatypes.unit)) <~~~> functor_id (ba)). - intros; eapply Build_NaturalIsomorphism. - instantiate (1:=arrow_cancelr_iso ba). - intros; - transitivity ( - arr_comp(Arrow:=ba) - (fmor (bin_first(BinoidalCat:=Arrows_are_Binoidal ba) Datatypes.unit) f) - (arr_arr(Arrow:=ba) (fun xy : B * unit => let (a, b) := xy in (fun (x : B) (_ : unit) => x) a b)) - ). - symmetry. - apply (arr_unit(Arrow:=ba)(c:=(Datatypes.unit)) f). - apply Equivalence_Reflexive. - Defined. - Definition arrow_cancell_iso `(ba:Arrow) - : forall (A:ba), (Isomorphic(C:=ba)) (Datatypes.unit*A) A. - intros; apply (Build_Isomorphic _ _ ba _ _ (arr_arr (Λ⟨x,y⟩ y)) (arr_arr (fun x => ⟨tt,x⟩))). - simpl; setoid_rewrite <- arr_comp_preserves; apply arr_arr_respects. - intros; destruct X. auto. auto. - unfold extensionality; intros; simpl. destruct x. auto. destruct u. auto. - simpl; setoid_rewrite <- arr_comp_preserves; reflexivity. - Defined. - Definition arrow_cancell_ni_iso `(ba:Arrow) - : (((bin_second(BinoidalCat:=(Arrows_are_Binoidal ba))) (Datatypes.unit)) <~~~> functor_id (ba)). - intros; eapply Build_NaturalIsomorphism. - instantiate (1:=arrow_cancell_iso ba). - intros. simpl. - repeat setoid_rewrite arr_associativity. - setoid_rewrite <- arr_comp_preserves. - simpl; - setoid_replace (arr_arr (fun x : B * unit => let (_, b) := let (a, b) := x in ⟨b, a ⟩ in b)) - with (arr_arr (fun x : B * unit => let (b, _) := x in b)). - setoid_rewrite arr_unit. - setoid_rewrite <- arr_associativity. - magic. - apply arr_comp_respects. - apply arr_arr_respects. - intros; destruct X; auto. - intros; destruct X; auto. - unfold extensionality; intros; simpl. - destruct x; auto. - apply Equivalence_Reflexive. - apply arr_arr_respects. - intros; destruct X; auto. - intros; destruct X; auto. - unfold extensionality; intros; simpl. - destruct x. - auto. - Defined. - - Definition arrow_assoc_iso `(ba:Arrow) : forall A B C, (Isomorphic(C:=ba)) ((A*B)*C) (A*(B*C)). - intros; eapply (Build_Isomorphic _ _ ba _ _ (arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩)) (arr_arr (Λ⟨x,⟨y,z⟩⟩ ⟨⟨x,y⟩,z⟩))); - [ intros; simpl; setoid_rewrite <- arr_comp_preserves - | intros; simpl; simpl; setoid_rewrite <- arr_comp_preserves; apply arr_arr_respects; auto - ]; simpl; try apply arr_arr_respects; intros; try destruct X; try destruct x; try destruct p; auto; - unfold extensionality; intros; intros; destruct x; destruct p; auto. - Defined. - Definition arrow_assoc_ni_iso `(ba:Arrow) : - (∀A : ba, ∀B : ba, - (bin_second(BinoidalCat:=(Arrows_are_Binoidal ba))) A >>>> - (bin_first(BinoidalCat:=(Arrows_are_Binoidal ba))) B <~~~> - (bin_first(BinoidalCat:=(Arrows_are_Binoidal ba))) B >>>> - (bin_second(BinoidalCat:=(Arrows_are_Binoidal ba))) A). - intros. - eapply Build_NaturalIsomorphism. - instantiate (1:=(fun X:ba => (arrow_assoc_iso ba A X B))). - simpl; intros. - setoid_rewrite arr_first_preserves. - setoid_rewrite arr_first_preserves. - setoid_rewrite arr_associativity. - setoid_replace - ( (arr_first(Arrow:=ba) A (arr_first(Arrow:=ba) B f)) >>> @arr_arr arr_hom' ba (B0 * B * A) (A * (B0 * B)) _swap) - with - ((( (arr_first(Arrow:=ba) A (arr_first(Arrow:=ba) B f)) >>> - (arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩))) >>> (arr_arr (Λ⟨x,⟨y,z⟩⟩ ⟨⟨x,y⟩,z⟩))) >>> - @arr_arr arr_hom' ba (B0 * B * A) (A * (B0 * B)) _swap). - setoid_rewrite arr_association. - repeat setoid_rewrite arr_associativity. - setoid_replace - ((arr_first(Arrow:=ba) B (arr_first(Arrow:=ba) A f)) - >>> ((arr_first(Arrow:=ba) B (@arr_arr arr_hom' ba (B0 * A) (A * B0) _swap)) - >>> (@arr_arr arr_hom' ba (A * B0 * B) (A * (B0 * B)) _assoc))) - with - ((((arr_first(Arrow:=ba) B (arr_first(Arrow:=ba) A f)) - >>> (arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩))) - >>> (arr_arr (Λ⟨x,y⟩ ⟨y,x⟩)) - >>> (arr_arr (Λ⟨x,y⟩ ⟨y,x⟩)) - >>> (arr_arr (Λ⟨x,⟨y,z⟩⟩ ⟨⟨x,y⟩,z⟩))) - >>> ((arr_first(Arrow:=ba) B (@arr_arr arr_hom' ba (B0 * A) (A * B0) _swap)) - >>> (@arr_arr arr_hom' ba (A * B0 * B) (A * (B0 * B)) _assoc))). - setoid_rewrite arr_association. - setoid_replace (arr_first(Arrow:=ba) (A*B) f) - with (((arr_first(Arrow:=ba) (A*B) f) - >>> (arr_arr (Λ⟨x,y⟩ ⟨x,(fun q => match q with (a,b) => (b,a) end) y⟩))) - >>> (arr_arr (Λ⟨x,y⟩ ⟨x,(fun q => match q with (a,b) => (b,a) end) y⟩))). - setoid_rewrite <- arr_exchange. - repeat magic. - repeat setoid_rewrite <- arr_associativity. - repeat magic. - repeat setoid_rewrite arr_associativity. - repeat magic. - apply arr_comp_respects. - apply arr_arr_respects. - intros; destruct X; destruct p; auto. - intros; destruct X; destruct p; auto. - unfold extensionality; intros; simpl. - destruct x. destruct p; auto. - apply arr_comp_respects. - reflexivity. - apply arr_arr_respects. - intros; destruct X; destruct p; auto. - intros; destruct X; destruct p; auto. - unfold extensionality; intros; simpl. - destruct x. destruct p; auto. - setoid_rewrite arr_associativity. - magic. - setoid_replace (arr_first(Arrow:=ba) (A*B) f) with (arr_first(Arrow:=ba) (A*B) f >>> arr_arr (fun x => x)). - apply arr_comp_respects. - setoid_rewrite arr_right_identity. - reflexivity. - apply arr_arr_respects. - intros; destruct X; destruct p; auto. - intros; destruct X; destruct p; auto. - unfold extensionality; intros; simpl. - destruct x. destruct p; auto. - setoid_rewrite <- arr_right_identity. - setoid_rewrite arr_associativity. - repeat magic. - reflexivity. - repeat magic. - repeat setoid_rewrite arr_associativity. - repeat magic. - apply arr_comp_respects. - reflexivity. - apply arr_arr_respects. - intros; destruct X; destruct p; auto. - intros; destruct X; destruct p; auto. - unfold extensionality; intros; simpl. - destruct x. destruct p; auto. - repeat setoid_rewrite arr_associativity. - repeat magic. - apply arr_comp_respects. - reflexivity. - apply arr_arr_respects. - intros; destruct X; destruct p; auto. - intros; destruct X; destruct p; auto. - unfold extensionality; intros; simpl. - destruct x. destruct p; auto. - Defined. - - Definition arrow_assoc_rr_iso `(ba:Arrow) := fun a b X:ba => iso_inv _ _ (arrow_assoc_iso ba X a b). - Definition arrow_assoc_rr_ni_iso `(ba:Arrow) : - ∀a b:ba, NaturalIsomorphism - (bin_first(BinoidalCat:=(Arrows_are_Binoidal ba)) ((bin_obj(BinoidalCat:=(Arrows_are_Binoidal ba))) a b)) - ((bin_first(BinoidalCat:=(Arrows_are_Binoidal ba)) a) - >>>> - (bin_first(BinoidalCat:=(Arrows_are_Binoidal ba)) b)). - intros; eapply Build_NaturalIsomorphism. - instantiate(1:=arrow_assoc_rr_iso ba a b). - intros. - simpl. - setoid_replace ((arr_first(Arrow:=ba) (a*b) f)) - with (arr_arr (fun q:A*(a*b) => (Λ⟨x,⟨y,z⟩⟩ ⟨⟨x,y⟩,z⟩) q) - >>> ((arr_arr (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩)) - >>> (arr_first(Arrow:=ba) (a*b) f))). - setoid_rewrite <- arr_association. - repeat setoid_rewrite arr_associativity. - magic. - apply arr_comp_respects. - apply arr_arr_respects. - intros. destruct X. destruct p. auto. - intros. destruct X. destruct p. auto. - unfold extensionality. - intros; auto. - transitivity (arr_first(Arrow:=ba) b (arr_first(Arrow:=ba) a f) >>> arr_arr (fun x=>x)). - setoid_rewrite arr_right_identity. - reflexivity. - apply arr_comp_respects. - reflexivity. - apply arr_arr_respects. - intros. destruct X. destruct p. auto. - intros. destruct X. destruct p. auto. - unfold extensionality. - intros; auto. - destruct x. - destruct p. - auto. - setoid_rewrite <- arr_associativity. - magic. - transitivity (arr_arr (fun x=>x) >>> (arr_first(Arrow:=ba) (a*b) f)). - setoid_rewrite arr_left_identity. - reflexivity. - apply arr_comp_respects. - apply arr_arr_respects. - intros. destruct X. destruct p. auto. - intros. destruct X. destruct p. auto. - unfold extensionality. - intros; auto. - destruct x. - destruct p. - auto. - reflexivity. - Defined. - - Definition arrow_assoc_ll_iso `(ba:Arrow) := fun a b X:ba => arrow_assoc_iso ba a b X. - Definition arrow_assoc_ll_ni_iso `(ba:Arrow) : - forall a b:ba, NaturalIsomorphism - (bin_second(BinoidalCat:=(Arrows_are_Binoidal ba)) ((bin_obj(BinoidalCat:=(Arrows_are_Binoidal ba))) a b)) - ((bin_second(BinoidalCat:=(Arrows_are_Binoidal ba)) b) - >>>> - (bin_second(BinoidalCat:=(Arrows_are_Binoidal ba)) a)). - intros. - eapply Build_NaturalIsomorphism. - simpl; intros. - instantiate(1:=(arrow_assoc_ll_iso ba a b)). - simpl. - magic. - repeat setoid_rewrite arr_associativity. - setoid_replace - ((arr_first a (arr_first(Arrow:=ba) b f)) >>> ((arr_first _ ((@arr_arr arr_hom' ba (B * b) (b * B) _swap))) >>> - @arr_arr arr_hom' ba (b * B * a) (a * (b * B)) _swap)) - with - ((((arr_first a (arr_first(Arrow:=ba) b f) - >>> ((arr_arr(a:=((B*b)*a)) (Λ⟨⟨x,y⟩,z⟩ ⟨x,⟨y,z⟩⟩))))) - >>> (arr_arr(Arrow:=ba) (Λ⟨x,yz⟩ ⟨x,(match yz with (y,z) => (z,y) end)⟩))) - >>> (arr_arr(Arrow:=ba) (Λ⟨x,⟨y,z⟩⟩ ⟨y,⟨z,x⟩⟩))). - setoid_rewrite arr_association. - setoid_replace (arr_arr(a:=((A*b)*a)) _assoc >>> (arr_first(Arrow:=ba) (b*a) f) >>> - arr_arr(Arrow:=ba) - (fun xy : B * (b * a) => - let (a0, b0) := xy in ⟨a0, let (y, z) := b0 in ⟨z, y ⟩ ⟩)) - with - (arr_arr(a:=((A*b)*a)) _assoc >>> ((arr_first(Arrow:=ba) (b*a) f) >>> - arr_arr(Arrow:=ba) - (fun xy : B * (b * a) => - let (a0, b0) := xy in ⟨a0, ((fun xy:b*a => let (a0, b0) := xy in ⟨b0, a0 ⟩)) b0 ⟩))). - setoid_rewrite <- arr_exchange. - repeat magic. - repeat setoid_rewrite <- arr_associativity. - repeat magic. - apply arr_comp_respects. - apply arr_comp_respects. - apply arr_arr_respects. - exact (fun xyz => match xyz with (xy,z) => match xy with (x,y) => (z,(x,y)) end end). - exact (fun xyz => match xyz with (xy,z) => match xy with (x,y) => (z,(x,y)) end end). - unfold extensionality; intros; simpl. - destruct x. - destruct b0. - auto. - reflexivity. - apply arr_arr_respects. - intros. destruct X. destruct b1. auto. - intros. destruct X. destruct b1. auto. - unfold extensionality; intros; simpl. - destruct x. - destruct b1. - auto. - repeat setoid_rewrite <- arr_associativity. - apply arr_comp_respects. - reflexivity. - apply arr_arr_respects. - intros. destruct X. destruct p. auto. - intros. destruct X. destruct p. auto. - unfold extensionality; intros; simpl. - destruct x. - destruct p. - auto. - setoid_rewrite arr_extension. - repeat setoid_rewrite arr_associativity. - magic. - apply arr_comp_respects. - reflexivity. - apply arr_arr_respects. - intros. destruct X. destruct p. auto. - intros. destruct X. destruct p. auto. - unfold extensionality; intros; simpl. - destruct x. - destruct p. - auto. - Defined. - - Instance arrows_monoidal `(ba:Arrow) : PreMonoidalCat (Arrows_are_Binoidal ba) (Datatypes.unit) := - { pmon_assoc := arrow_assoc_ni_iso ba - ; pmon_cancelr := arrow_cancelr_ni_iso ba - ; pmon_cancell := arrow_cancell_ni_iso ba - ; pmon_assoc_ll := arrow_assoc_ll_ni_iso ba - ; pmon_assoc_rr := arrow_assoc_rr_ni_iso ba - }. - apply Build_Pentagon; intros. - intros; simpl. - repeat setoid_rewrite arr_extension. - repeat setoid_rewrite <- arr_comp_preserves. - apply arr_arr_respects; unfold extensionality; intros; simpl; - try destruct x; try destruct X; try destruct b0; try destruct p; auto. - destruct b0. unfold bin_obj. auto. - destruct b0. unfold bin_obj. auto. - destruct b0. unfold bin_obj. auto. - apply Build_Triangle; intros; simpl. - repeat setoid_rewrite arr_extension. - repeat setoid_rewrite <- arr_comp_preserves. - apply arr_arr_respects; unfold extensionality; intros; simpl; - try destruct x; try destruct X; try destruct p; try destruct b0; try destruct p; unfold bin_obj; auto. - simpl. apply arr_arr_respects; - [ exact (fun (xy:unit*unit) => tt) - | exact (fun (xy:unit*unit) => tt) - | idtac - ]; unfold extensionality; intros; simpl; destruct x; destruct u; destruct u0; auto. - intros; reflexivity. - intros; reflexivity. - Defined. - -Definition arrow_inclusion_functor `(ba:Arrow) : Functor coqCategory (ba) (fun x=>x). - intros; apply (Build_Functor _ _ coqCategory _ _ (ba) _ (fun A B => fun f:A->B => arr_arr f)); - intros; unfold eqv; simpl; - [ apply arr_arr_respects; auto - | reflexivity - | symmetry; apply arr_comp_preserves ]. - Defined. - -Instance Arrow_inclusion_is_a_monoidal_functor `(ba:Arrow) -: PreMonoidalFunctor coqPreMonoidalCat (arrows_monoidal ba) (fun x=>x) := -{ mf_F := arrow_inclusion_functor ba -}. - simpl; apply iso_id. - intros; apply (Build_NaturalIsomorphism _ _ coqCategory _ _ (ba) (fun a0 : Type => a0 * a) (fun a0 : Type => a0 * a) _ _ - (fun A:coqCategory => (iso_id(C:=ba)) ((fun a0 : Type => a0 * a) A))). - intros; simpl; setoid_rewrite ((arr_extension(Arrow:=ba)) A B f a); setoid_rewrite <- arr_comp_preserves; reflexivity. - intros; apply (@Build_NaturalIsomorphism _ _ coqCategory _ _ (ba) (fun a0 : Type => a * a0) (fun a0 : Type => a * a0) _ _ - (fun A:coqCategory => (iso_id(C:=ba)) ((fun a0 : Type => a * a0) A))). - intros; simpl; setoid_rewrite arr_extension; repeat setoid_rewrite <- arr_comp_preserves. - apply arr_arr_respects; intros; unfold extensionality; intros; try destruct X; try destruct x; try destruct p; auto. - intros. - intros; apply Build_CentralMorphism; intros. simpl. - - simpl. - setoid_rewrite arr_extension. - setoid_rewrite <- arr_associativity. - setoid_rewrite <- arr_associativity. - repeat setoid_rewrite <- arr_comp_preserves. - transitivity ( - arr_arr (fun x:a*c => let (a0,c0) := x in (c0,a0)) - >>> - arr_arr (fun x:c*a => let (c0,a0) := x in (c0, f a0)) >>> ((arr_first(Arrow:=ba)) b g) >>> - (arr_arr (fun x:d*b => let (d0,b0):=x in (b0,d0)))). - repeat setoid_rewrite <- arr_associativity. - apply arr_comp_respects; try reflexivity. - apply arr_comp_respects; try reflexivity. - repeat setoid_rewrite <- arr_comp_preserves. - apply arr_arr_respects; unfold extensionality; intros; try destruct X; try destruct x; intros; auto. - repeat setoid_rewrite arr_associativity. - apply arr_comp_respects; try reflexivity. - repeat setoid_rewrite <- arr_associativity. - setoid_rewrite <- arr_extension. - setoid_rewrite arr_extension. - repeat setoid_rewrite arr_associativity. - repeat setoid_rewrite <- arr_comp_preserves. - repeat setoid_rewrite <- arr_associativity. - setoid_rewrite arr_exchange. - repeat setoid_rewrite arr_associativity. - apply arr_comp_respects; try reflexivity. - repeat setoid_rewrite <- arr_comp_preserves. - apply arr_arr_respects; unfold extensionality; intros; try destruct X; try destruct x; intros; auto. - - simpl. - setoid_rewrite arr_extension. - setoid_rewrite <- arr_associativity. - setoid_rewrite <- arr_associativity. - repeat setoid_rewrite <- arr_comp_preserves. - transitivity (arr_arr (fun x:c*a => let (c0,a0) := x in (c0, f a0)) >>> ((arr_first(Arrow:=ba)) b g)). - setoid_rewrite arr_exchange. - repeat setoid_rewrite arr_associativity. - apply arr_comp_respects. reflexivity. - repeat setoid_rewrite <- arr_comp_preserves. - apply arr_arr_respects; unfold extensionality; intros; try destruct X; try destruct x; intros; auto. - apply arr_comp_respects; try reflexivity. - apply arr_arr_respects; unfold extensionality; intros; try destruct X; try destruct x; intros; auto. - Defined. - -Definition arrow_swap_iso `(ba:Arrow) : forall A B, (Isomorphic(C:=ba)) (A*B) (B*A). - intros; apply (Build_Isomorphic _ _ ba _ _ (arr_arr (Λ⟨x,y⟩ ⟨y,x⟩)) (arr_arr (Λ⟨x,y⟩ ⟨y,x⟩))); - simpl; setoid_rewrite <- arr_comp_preserves; - apply arr_arr_respects; - intros; auto; intros; auto; - unfold extensionality; intros; simpl. - try destruct X; try destruct x; auto; destruct x; auto. - destruct x. simpl. reflexivity. - Defined. - -Instance arrows_are_braided `(ba:Arrow) : BraidedCat (arrows_monoidal ba). - intros; apply (Build_BraidedCat _ _ (ba) _ _ _ _ (fun A B => arrow_swap_iso ba A B)); - intros; simpl; - repeat setoid_rewrite arr_extension; - repeat setoid_rewrite <- arr_associativity; - repeat setoid_rewrite <- arr_comp_preserves; - apply arr_arr_respects; intros; simpl; try destruct X; auto; unfold extensionality; unfold bin_obj; - intros; auto; try destruct x; try destruct p; try destruct b0; auto. - Defined. - -Instance arrows_are_symmetric `(ba:Arrow) : SymmetricCat (arrows_are_braided ba). - intros; apply Build_SymmetricCat; intros. simpl. reflexivity. - Defined. - -Instance Freyd_from_Arrow `(ba:Arrow) -: FreydCategory coqPreMonoidalCat := -{ freyd_C_cartesian := coqCartesianCat -; freyd_K := ba -; freyd_K_binoidal := Arrows_are_Binoidal ba -; freyd_K_monoidal := arrows_monoidal ba -; freyd_F := Arrow_inclusion_is_a_monoidal_functor ba -; freyd_K_braided := arrows_are_braided ba -; freyd_K_symmetric := arrows_are_symmetric ba -}. - intros; apply Build_CentralMorphism; intros; simpl. - repeat setoid_rewrite arr_extension. - repeat setoid_rewrite <- arr_associativity. - repeat setoid_rewrite <- arr_comp_preserves. - setoid_replace - (arr_arr (fun x : a * c => let (a0, b0) := let (a0, b0) := x in ⟨f a0, b0 ⟩ in ⟨b0, a0 ⟩) >>> (arr_first(Arrow:=ba) b g)) - with - (arr_arr (fun x : a * c => let (a0, b0) := x in ⟨b0,a0 ⟩) >>> (arr_arr (fun x : c * a => let (a0, b0) := x in ⟨a0,f b0 ⟩) - >>> (arr_first(Arrow:=ba) b g))). - setoid_rewrite arr_exchange. - repeat setoid_rewrite arr_associativity. - apply arr_comp_respects; try reflexivity. - apply arr_comp_respects; try reflexivity. - setoid_rewrite <- arr_comp_preserves. - apply arr_arr_respects; intros; simpl; try destruct X; auto; unfold extensionality; unfold bin_obj; - intros; auto; try destruct x; try destruct p; try destruct b0; auto. - - setoid_rewrite <- arr_associativity. - apply arr_comp_respects; try reflexivity. - setoid_rewrite <- arr_comp_preserves. - apply arr_arr_respects; intros; simpl; try destruct X; auto; unfold extensionality; unfold bin_obj; - intros; auto; try destruct x; try destruct p; try destruct b0; auto. - - repeat setoid_rewrite arr_extension. - repeat setoid_rewrite <- arr_comp_preserves. - transitivity ((arr_arr(Arrow:=ba) (fun x:c*a => let (a0,b0):=x in ⟨a0,f b0 ⟩)) >>> (arr_first(Arrow:=ba) b g)); - [ setoid_rewrite arr_exchange | idtac ]; - apply arr_comp_respects; try reflexivity; - apply arr_arr_respects; intros; simpl; try destruct X; auto; unfold extensionality; unfold bin_obj; - intros; auto; try destruct x; try destruct p; try destruct b0; auto. - - intros; simpl; unfold bin_obj; reflexivity. - intros; simpl; unfold bin_obj; reflexivity. - intros; simpl; unfold bin_obj; reflexivity. - intros; simpl; unfold bin_obj; reflexivity. - intros; simpl; unfold bin_obj; reflexivity. - Defined. - -Theorem converter (fc:FreydCategory coqPreMonoidalCat) : forall q:Type, freyd_K(FreydCategory:=fc). - intros. exact q. Defined. - -Notation "` x" := (converter _ x) (at level 1) : temporary_scope1. -Notation "`( x )" := (converter _ x) : temporary_scope1. -Open Scope temporary_scope1. -Notation "a ~~> b" := (freyd_K_hom a b) : category_scope. - -Close Scope arrow_scope. -Open Scope arrow_scope. -Open Scope category_scope. - -Lemma inverse_of_identity_is_identity : forall `{C:Category}{a:C}(i:Isomorphic a a), #i ~~ (id a) -> #i⁻¹ ~~ (id a). - intros. - transitivity (#i >>> #i⁻¹). - setoid_rewrite H. - symmetry; apply left_identity. - apply iso_comp1. - Qed. - -Lemma iso_both_sides' : - forall `{C:Category}{a b c d:C}(f:a~>b)(g:c~>d)(i1:Isomorphic d b)(i2:Isomorphic c a), - f >>> #i1 ⁻¹ ~~ #i2 ⁻¹ >>> g - -> - #i2 >>> f ~~ g >>> #i1. - symmetry. - apply iso_shift_right. - setoid_rewrite <- associativity. - symmetry. - apply iso_shift_left. - auto. - Qed. - -Lemma l1 (fc:FreydCategory coqPreMonoidalCat)`(f:a->b)(d:Type) : - fc \ f ⋉ `d ~~ fc \ (fun xy : a * d => let (a0, b0) := xy in ⟨f a0, b0 ⟩). - intros; set (freyd_K(FreydCategory:=fc)) as kc. - apply (monic #(mf_preserves_first(PreMonoidalFunctor:=fc) d b)). - apply iso_monic. - symmetry. - set (ni_commutes (mf_preserves_first(PreMonoidalFunctor:=fc) d) f) as help. - simpl in help. - symmetry in help. - apply (transitivity(R:=eqv _ _) help). - clear help. - transitivity (id _ >>> fc \ f ⋉ `d). - apply comp_respects; try reflexivity. - set (freyd_F_strict_first d a) as help. - simpl in help. apply help. - symmetry. - transitivity (fc \ f ⋉ `d >>> id _). - apply comp_respects; try reflexivity. - set (freyd_F_strict_first d b) as help. - simpl in help. apply help. - transitivity (fc \ f ⋉ `d). - apply right_identity. - symmetry; apply left_identity. - Qed. - -Lemma l2 (fc : FreydCategory coqPreMonoidalCat) : forall `(f:`a~~>`b)`(g:c->d), - fc \ (fun xy : a * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩) >>> f ⋉ `d ~~ - f ⋉ `c >>> fc \ (fun xy : b * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩). - intros; set (freyd_K(FreydCategory:=fc)) as kc. - symmetry. - apply (monic #((mf_preserves_second(PreMonoidalFunctor:=fc) b d))). - apply iso_monic. - transitivity (f ⋉ `c >>> ((fc \ (fun xy : b * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩)) >>> - #(mf_preserves_second(PreMonoidalFunctor:=fc) `b d))). - apply associativity. - transitivity (f ⋉ `c >>> (#(mf_preserves_second(PreMonoidalFunctor:=fc) `b c) >>> (fc >>>> bin_second (fc b)) \ g)). - apply comp_respects; try reflexivity. - symmetry. - apply (ni_commutes ( (mf_preserves_second(PreMonoidalFunctor:=fc) b)) g). - symmetry. - transitivity (((fc \ (fun xy : a * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩) >>> f ⋉ `d)) >>> id _). - apply comp_respects; try reflexivity. - apply (freyd_F_strict_second(FreydCategory:=fc) b d). - transitivity (((fc \ (fun xy : a * c => let (a0, b0) := xy in ⟨a0, g b0 ⟩) >>> f ⋉ `d))). - apply right_identity. - symmetry. - transitivity (f ⋉ `c >>> (id (`(b*c)) >>> (fc >>>> bin_second (fc b)) \ g)). - apply comp_respects; [ reflexivity | idtac ]. - apply comp_respects; [ - apply (freyd_F_strict_second(FreydCategory:=fc) b c) | - reflexivity ]. - transitivity (f ⋉ `c >>> (fc >>>> bin_second (fc b)) \ g). - apply comp_respects; [ reflexivity | apply left_identity ]. - transitivity (`a ⋊ fc \ g >>> f ⋉ `d). - assert (CentralMorphism (fc \ g)). apply freyd_F_central. - set (centralmor_second(f:=(fc \ g)) f) as help. - apply help. - apply comp_respects; [ idtac | reflexivity ]. - apply (epic #(iso_inv _ _ (mf_preserves_second(PreMonoidalFunctor:=fc) a c))). - set (iso_epic (((mf_preserves_second a) c) ⁻¹)) as q. - apply q. - symmetry. - transitivity (`a ⋊ fc \ g >>> iso_backward (mf_preserves_second(PreMonoidalFunctor:=fc) `a `d)). - apply (ni_commutes (ni_inv (mf_preserves_second(PreMonoidalFunctor:=fc) a)) g). - transitivity (`a ⋊ fc \ g >>> id _). - apply comp_respects; try reflexivity. - apply (inverse_of_identity_is_identity (mf_preserves_second(PreMonoidalFunctor:=fc) `a `d)). - apply (freyd_F_strict_second(FreydCategory:=fc) a d). - transitivity (`a ⋊ fc \ g). - apply right_identity. - symmetry. - transitivity (id _ >>> `a ⋊ fc \ g). - apply comp_respects; try reflexivity. - apply (inverse_of_identity_is_identity (mf_preserves_second(PreMonoidalFunctor:=fc) `a `c)). - apply (freyd_F_strict_second(FreydCategory:=fc) a c). - apply left_identity. - Qed. - -Lemma l3 (fc : FreydCategory coqPreMonoidalCat) : forall `(f:`a~~>`b)(c:Type), - f ⋉ `c >>> fc \ (fun xy : b * c => let (a0, _) := xy in a0) ~~ - fc \ (fun xy : a * c => let (a0, _) := xy in a0) >>> f. - intros; set (freyd_K(FreydCategory:=fc)) as kc. - transitivity (f ⋉ `c >>> (fc \ (comp(Category:=coqCategory) _ _ _ - (fun xy : b * c => let (a0, _) := xy in (a0,tt)) - (fun xy : b * unit => let (a0, _) := xy in a0)))). - apply comp_respects; [ reflexivity | idtac ]. - simpl; apply (fmor_respects(Functor:=fc)). - simpl. intros. destruct x; auto. - symmetry. - transitivity (fc \ (comp(Category:=coqCategory) _ _ _ - (fun xy : a * c => let (a0, _) := xy in (a0,tt)) - (fun xy : a * unit => let (a0, _) := xy in a0)) >>> f). - apply comp_respects; [ idtac | reflexivity ]. - simpl; apply (fmor_respects(Functor:=fc)). - simpl. intros. destruct x; auto. - transitivity ((fc \ (fun xy : a * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>> - fc \ (fun xy : a * unit => let (a0, _) := xy in a0)) >>> f). - apply comp_respects; [ idtac | reflexivity ]. - symmetry; apply (fmor_preserves_comp(Functor:=fc)). - symmetry. - transitivity (f ⋉ `c >>> - (fc \ (fun xy : b * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>> - fc \ (fun xy : b * unit => let (a0, _) := xy in a0))). - apply comp_respects; [ reflexivity | idtac ]. - symmetry; apply (fmor_preserves_comp(Functor:=fc)). - transitivity (f ⋉ `c >>> (fc \ (fun xy : b * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>> #(pmon_cancelr fc b))). - apply comp_respects; [ reflexivity | idtac ]. - apply comp_respects; [ reflexivity | idtac ]. - apply (freyd_F_strict_cr(FreydCategory:=fc) b). - symmetry. - transitivity ((fc \ (fun xy : a * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>> #(pmon_cancelr fc a)) >>> f). - apply comp_respects; [ idtac | reflexivity ]. - apply comp_respects; [ reflexivity | idtac ]. - apply (freyd_F_strict_cr(FreydCategory:=fc) a). - transitivity (((`a ⋊ fc \ (fun _ : c => tt) - >>> iso_backward (mf_preserves_second(PreMonoidalFunctor:=fc) `a unit)) >>> #(pmon_cancelr fc a)) >>> f). - apply comp_respects; [ idtac | reflexivity ]. - apply comp_respects; [ idtac | reflexivity ]. - symmetry. - transitivity (iso_backward (mf_preserves_second(PreMonoidalFunctor:=fc) a c) >>> - fc \ (fun xy : a * c => let (a0, _) := xy in ⟨a0, tt ⟩)). - symmetry. - apply (ni_commutes (ni_inv (mf_preserves_second(PreMonoidalFunctor:=fc) a)) (fun x:c=>tt)). - transitivity (id _ >>> fc \ (fun xy : a * c => let (a0, _) := xy in ⟨a0, tt ⟩)). - apply comp_respects; [ idtac | reflexivity ]. - set (inverse_of_identity_is_identity (mf_preserves_second(PreMonoidalFunctor:=fc) `a `c)) as foo. - simpl in foo. - apply foo. - apply (freyd_F_strict_second(FreydCategory:=fc) a c). - apply left_identity. - symmetry. - transitivity (f ⋉ `c >>> - ((#(mf_preserves_second(PreMonoidalFunctor:=fc) b c) >>> `b ⋊ fc \ (fun _ : c => tt)) >>> - #(pmon_cancelr fc b))). - apply comp_respects; [ reflexivity | idtac ]. - apply comp_respects; [ idtac | reflexivity ]. - transitivity (fc \ (fun xy : b * c => let (a0, _) := xy in ⟨a0, tt ⟩) - >>> #(mf_preserves_second(PreMonoidalFunctor:=fc) b unit)). - symmetry. - transitivity (fc \ (fun xy : b * c => let (a0, _) := xy in ⟨a0, tt ⟩) >>> id _). - apply comp_respects; [ reflexivity | idtac ]. - apply (freyd_F_strict_second(FreydCategory:=fc) b unit). - apply right_identity. - symmetry. - apply (ni_commutes ( (mf_preserves_second(PreMonoidalFunctor:=fc) b)) (fun x:c=>tt)). - transitivity (f ⋉ `c >>> - ((id _ >>> `b ⋊ fc \ (fun _ : c => tt)) >>> - #(pmon_cancelr fc b))). - apply comp_respects; [ reflexivity | idtac ]. - apply comp_respects; [ idtac | reflexivity ]. - apply comp_respects; [ idtac | reflexivity ]. - apply (freyd_F_strict_second(FreydCategory:=fc) b c). - transitivity (f ⋉ `c >>> - ((`b ⋊ fc \ (fun _ : c => tt)) >>> - #(pmon_cancelr fc b))). - apply comp_respects; [ reflexivity | idtac ]. - apply comp_respects; [ idtac | reflexivity ]. - apply left_identity. - symmetry. - transitivity (((`a ⋊ fc \ (fun _ : c => tt) >>> - id _) >>> - #(pmon_cancelr fc a)) >>> f). - apply comp_respects; [ idtac | reflexivity ]. - apply comp_respects; [ idtac | reflexivity ]. - apply comp_respects; [ reflexivity | idtac ]. - set (inverse_of_identity_is_identity (mf_preserves_second(PreMonoidalFunctor:=fc) `a unit)) as foo. - simpl in foo. - apply foo. - apply (freyd_F_strict_second(FreydCategory:=fc) `a unit). - transitivity (((`a ⋊ fc \ (fun _ : c => tt)) >>> #(pmon_cancelr fc a)) >>> f). - apply comp_respects; [ idtac | reflexivity ]. - apply comp_respects; [ idtac | reflexivity ]. - apply right_identity. - symmetry. - transitivity ((f ⋉ `c >>> `b ⋊ fc \ (fun _ : c => tt)) >>> #(pmon_cancelr fc b)). - symmetry; apply associativity. - transitivity ((`a ⋊ fc \ (fun _ : c => tt) >>> f ⋉ `unit) >>> #(pmon_cancelr fc b)). - apply comp_respects; [ idtac | reflexivity ]. - assert (CentralMorphism (fc \ (fun _ : c => tt))). - apply (freyd_F_central(FreydCategory:=fc)). - apply (centralmor_second(CentralMorphism:=H)). - transitivity (`a ⋊ fc \ (fun _ : c => tt) >>> (f ⋉ `unit >>> #(pmon_cancelr fc b))). - apply associativity. - symmetry. - transitivity (`a ⋊ fc \ (fun _ : c => tt) >>> (#(pmon_cancelr fc a) >>> f)). - apply associativity. - apply comp_respects; [ reflexivity | idtac ]. - set (ni_commutes (pmon_cancelr fc)) as help. - simpl in help. apply help. - Qed. - -Lemma l4 (fc : FreydCategory coqPreMonoidalCat) : forall `(f:`a~>b)(c d:Type), - (f ⋉ `c) ⋉ `d >>> fc \ ((fun xyz:(b*c)*d => let (ab, c) := xyz in let (a0, b0) := ab in ⟨a0, ⟨b0, c ⟩ ⟩)) - ~~ fc \ ((fun xyz:(a*c)*d => let (ab, c) := xyz in let (a0, b0) := ab in ⟨a0, ⟨b0, c ⟩ ⟩)) >>> f ⋉ _. - intros; set (freyd_K(FreydCategory:=fc)) as kc. - simpl in f. - symmetry. - transitivity (#(pmon_assoc freyd_K_monoidal _ _ _) >>> f ⋉ (c*d:(freyd_K))). - apply comp_respects; try reflexivity. - apply (freyd_F_strict_a(FreydCategory:=fc) `a d c). - symmetry. - transitivity (((f ⋉ (c: (freyd_K))) ⋉ (d:(freyd_K)) >>> #(pmon_assoc freyd_K_monoidal _ _ _))). - apply comp_respects; try reflexivity. - apply (freyd_F_strict_a(FreydCategory:=fc) `b `d `c). - symmetry. - apply (iso_both_sides' _ _ (pmon_assoc fc `b d c) (pmon_assoc fc `a d c)). - symmetry. - transitivity ( #(ni_iso (pmon_assoc_rr(PreMonoidalCat:=(freyd_K_monoidal(FreydCategory:=fc))) `c `d) a) >>> - (f ⋉ (c:(freyd_K))) ⋉ (d:(freyd_K))). - apply comp_respects; try reflexivity. - symmetry. - apply ((pmon_coherent_r(PreMonoidalCat:=freyd_K_monoidal(FreydCategory:=fc))) a c d). - symmetry. - transitivity (f ⋉ (c*d:(freyd_K)) >>> - #(ni_iso (pmon_assoc_rr(PreMonoidalCat:=(freyd_K_monoidal(FreydCategory:=fc))) _ _ ) _)). - apply comp_respects; try reflexivity. - symmetry. - apply ((pmon_coherent_r(PreMonoidalCat:=freyd_K_monoidal(FreydCategory:=fc))) b c d). - symmetry. - simpl. - apply (@ni_commutes _ _ _ _ _ _ _ _ _ _ (pmon_assoc_rr(PreMonoidalCat:=(freyd_K_monoidal(FreydCategory:=fc))) c d) a `b f). - Qed. - -(* Formalized Theorem 3.17 *) -Definition Arrow_from_Freyd (fc:FreydCategory coqPreMonoidalCat) - : Arrow (fun A B => freyd_K_hom(FreydCategory:=fc) (converter fc A) (converter fc B)). - intros. - set (freyd_K(FreydCategory:=fc)) as kc. - apply (@Build_Arrow - (fun A B => (`A) ~~> (`B)) - (fun A B => fun f:A->B => fc \ f) - (fun (A B C : Type) (X : `A ~~> `B) (X0 : `B ~~> `C) => X >>> X0) - (fun (A B C : coqCategory) (X : `A ~~> `B) => X ⋉ `C) - (fun (A B : Type) (X X0 : `A ~~> `B) => X ~~ X0)); - unfold Proper; unfold Reflexive; unfold Symmetric; unfold Transitive; unfold respectful; - intros ; simpl. - apply Build_Equivalence. - unfold Reflexive; intros. apply Equivalence_Reflexive. - unfold Symmetric; intros. apply Equivalence_Symmetric. auto. - unfold Transitive; intros. transitivity y; auto. - apply comp_respects; auto. - apply (fmor_respects(Functor:=(bin_first(BinoidalCat:=fc) `c))); auto. - apply (fmor_respects(Functor:=fc)); auto. - transitivity ((id _) >>> f). - apply comp_respects; try reflexivity. - apply (fmor_preserves_id(Functor:=fc)). - apply left_identity. - transitivity (f >>> (id _)). - apply comp_respects; try reflexivity. - apply (fmor_preserves_id(Functor:=fc)). - apply right_identity. - apply associativity. - symmetry. apply (fmor_preserves_comp(Functor:=fc) f g). - apply (l1 fc f d). - symmetry; apply (fmor_preserves_comp(Functor:=(bin_first `d)) f g). - apply (l2 fc f g). - apply (l3 fc f c). - apply (l4 fc f c d). - Defined. - -(* one half: every Arrow is isomorphic to its implied Freyd category *) -(* - -(* FIXME: isomorphism of categories must be via a premonoidal functor *) - - -(* FIXME: the isomorphism needs to be a premonoidal functor *) -Theorem arrow_both_defs : forall `(ba:Arrow), IsomorphicCategories (Freyd_from_Arrow ba) (ba). - intros. - apply Build_IsomorphicCategories with (isoc_forward:=ToFunc (functor_id _))(isoc_backward:=ToFunc (functor_id _)). - simpl. unfold EqualFunctors. intros. - simpl; intros; apply (@heq_morphisms_intro (ba) a b _ _); auto. - simpl. unfold EqualFunctors. intros. - simpl; intros; apply (@heq_morphisms_intro (ba) a b _ _); auto. - Defined. - -(* the other half: [the codomain of] every Freyd category is isomorphic to its implied Arrow *) -Theorem arrow_both_defs' : forall (fc:FreydCategory coqPreMonoidalCat), IsomorphicCategories fc ((Arrow_from_Freyd fc)). - Lemma iforward (fc:FreydCategory coqPreMonoidalCat) : Functor fc ((Arrow_from_Freyd fc)) (fun x=> x). - intros; apply (Build_Functor fc ((Arrow_from_Freyd fc)) _ (fun a b f => f)); - intros; auto; simpl; [ idtac | reflexivity ]; - symmetry; apply (fmor_preserves_id(Functor:=fc)). - Defined. - Lemma ibackward (fc:FreydCategory coqPreMonoidalCat) : Functor ((Arrow_from_Freyd fc)) fc (fun x=> x). - intros; apply (Build_Functor ((Arrow_from_Freyd fc)) fc _ (fun a b f => f)); - intros; auto; simpl; [ idtac | reflexivity ]; - apply (fmor_preserves_id(Functor:=fc)). - Defined. - intros; apply (@Build_IsomorphicCategories _ _ (ToFunc (iforward fc)) (ToFunc (ibackward fc))); simpl; intros; auto. - unfold EqualFunctors; simpl; auto. - unfold EqualFunctors; simpl; auto. - Defined. -*) - -Close Scope arrow_scope. -Close Scope temporary_scope1. -Open Scope tree_scope. -