(*******************************************************************************) (* 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.