+++ /dev/null
-(*******************************************************************************)
-(* 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.
-
projects / coq-categories.git / commitdiff