From d490aac37c55dcdaaf3fca152846f13acbb447c6 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 20 Mar 2011 18:53:23 -0700 Subject: [PATCH] add formalization of Arrows and Freyd Categories --- src/Arrows.v | 965 +++++++++++++++++++++++++++++++++++++++++++++++++ src/FreydCategories.v | 44 +++ 2 files changed, 1009 insertions(+) create mode 100644 src/Arrows.v create mode 100644 src/FreydCategories.v diff --git a/src/Arrows.v b/src/Arrows.v new file mode 100644 index 0000000..50ba604 --- /dev/null +++ b/src/Arrows.v @@ -0,0 +1,965 @@ +(*******************************************************************************) +(* 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. + diff --git a/src/FreydCategories.v b/src/FreydCategories.v new file mode 100644 index 0000000..de6e4ee --- /dev/null +++ b/src/FreydCategories.v @@ -0,0 +1,44 @@ +(*******************************************************************************) +(* Freyd Categories *) +(*******************************************************************************) + +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 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. + +Class FreydCategory +{ Ob : Type } +{ freyd_bobj : Ob -> Ob -> Ob } +{ HomC : Ob -> Ob -> Type } +{ freyd_C : Category Ob HomC } +{ freyd_C_terminal : Terminal freyd_C } +{ freyd_C_binoidal : BinoidalCat freyd_C freyd_bobj } +( freyd_C_monoidal : PreMonoidalCat freyd_C_binoidal 1 ) := +{ freyd_K_hom : Ob -> Ob -> Type +; freyd_K :> Category Ob freyd_K_hom +; freyd_C_cartesian : CartesianCat freyd_C_monoidal +; freyd_K_binoidal :> BinoidalCat freyd_K freyd_bobj +; freyd_K_monoidal :> PreMonoidalCat freyd_K_binoidal (one(Terminal:=freyd_C_terminal)) +; freyd_K_braided : BraidedCat freyd_K_monoidal +; freyd_K_symmetric : SymmetricCat freyd_K_braided +; freyd_F :> PreMonoidalFunctor freyd_C_monoidal freyd_K_monoidal (fun x => x) +; freyd_F_central : forall `(f:a~~{freyd_C}~~>b), CentralMorphism(C:=freyd_K) (freyd_F \ f) +; freyd_F_strict_first : forall a b, #(mf_preserves_first(PreMonoidalFunctor:=freyd_F) a b) ~~ id (bin_first a b) +; freyd_F_strict_second : forall a b, #(mf_preserves_second(PreMonoidalFunctor:=freyd_F) a b) ~~ id (bin_second a b) +; freyd_F_strict_a : forall a b c, freyd_F \ #(pmon_assoc freyd_C_monoidal a b c) ~~ #(pmon_assoc freyd_K_monoidal _ _ _) +; freyd_F_strict_cl : forall a, freyd_F \ #(pmon_cancell freyd_C_monoidal a) ~~ #(pmon_cancell freyd_K_monoidal _) +; freyd_F_strict_cr : forall a, freyd_F \ #(pmon_cancelr freyd_C_monoidal a) ~~ #(pmon_cancelr freyd_K_monoidal _) +}. +Coercion freyd_K_monoidal : FreydCategory >-> PreMonoidalCat. +Coercion freyd_F : FreydCategory >-> PreMonoidalFunctor. +Coercion freyd_K : FreydCategory >-> Category. -- 1.7.10.4