Require Import NaturalIsomorphisms_ch7_5.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
+Require Import InitialTerminal_ch2_2.
Open Scope nd_scope.
Open Scope pf_scope.
Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
Context (nd_eqv : @ND_Relation Judgment Rule).
- (* actually you can use any type as the objects, so long as you give a mapping from that type to judgments *)
- Context {Ob : Type}.
- Context (ob2judgment : Ob -> Judgment).
- Coercion ob2judgment : Ob >-> Judgment.
-
Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2).
- Instance Judgments_Category
- : Category (Tree ??Ob) (fun h c => (mapOptionTree ob2judgment h) /⋯⋯/ (mapOptionTree ob2judgment c)) :=
+ Instance Judgments_Category : Category (Tree ??Judgment) (fun h c => h /⋯⋯/ c) :=
{ id := fun h => nd_id _
; comp := fun a b c f g => f ;; g
; eqv := fun a b f g => f === g
Defined.
Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category :=
- (fun xy =>
- match xy with
- | pair_obj x y => T_Branch x y
- end).
+ fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy).
Definition Judgments_Category_monoidal_endofunctor_fmor :
forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) ->
((Judgments_Category_monoidal_endofunctor_fobj a)
destruct a.
destruct b.
destruct X.
+ simpl in *.
exact (h**h0).
Defined.
Definition Judgments_Category_monoidal_endofunctor
Defined.
Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)).
- apply (@Build_Isomorphic _ _ Judgments_Category _ _
- (@nd_assoc _ Rule (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c)
- : (a,, b),, c ~~{Judgments_Category}~~> a,, (b,, c))
- (@nd_cossa _ Rule (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c)
- : a,, (b,, c) ~~{Judgments_Category}~~> (a,, b),, c)); simpl; auto.
+ refine
+ {| iso_forward := nd_assoc
+ ; iso_backward := nd_cossa |};
+ abstract (simpl; auto).
Defined.
Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
- apply (@Build_Isomorphic _ _ Judgments_Category _ _
- (@nd_cancelr _ Rule (mapOptionTree ob2judgment a) : a,,[] ~~{Judgments_Category}~~> a)
- (@nd_rlecnac _ Rule (mapOptionTree ob2judgment a) : a ~~{Judgments_Category}~~> a,,[])); simpl; auto.
+ refine
+ {| iso_forward := nd_cancelr
+ ; iso_backward := nd_rlecnac |};
+ abstract (simpl; auto).
Defined.
Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
- apply (@Build_Isomorphic _ _ Judgments_Category _ _
- (@nd_cancell _ Rule (mapOptionTree ob2judgment a) : [],,a ~~{Judgments_Category}~~> a)
- (@nd_llecnac _ Rule (mapOptionTree ob2judgment a) : a ~~{Judgments_Category}~~> [],,a)); simpl; auto.
+ refine
+ {| iso_forward := nd_cancell
+ ; iso_backward := nd_llecnac |};
+ abstract (simpl; auto).
Defined.
Definition jud_mon_cancelr : (func_rlecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
refine {| ni_iso := fun x => jud_cancelr_iso x |}; intros; simpl.
- setoid_rewrite (ndr_prod_right_identity f).
- repeat setoid_rewrite ndr_comp_associativity.
- apply ndr_comp_respects; try reflexivity.
- symmetry.
- eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
- apply ndr_comp_respects; try reflexivity; simpl; auto.
+ abstract (setoid_rewrite (ndr_prod_right_identity f);
+ repeat setoid_rewrite ndr_comp_associativity;
+ apply ndr_comp_respects; try reflexivity;
+ symmetry;
+ eapply transitivity; [ idtac | apply ndr_comp_right_identity ];
+ apply ndr_comp_respects; try reflexivity; simpl; auto).
Defined.
Definition jud_mon_cancell : (func_llecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
eapply Build_NaturalIsomorphism.
instantiate (1:=fun x => jud_cancell_iso x).
- intros; simpl.
- setoid_rewrite (ndr_prod_left_identity f).
- repeat setoid_rewrite ndr_comp_associativity.
- apply ndr_comp_respects; try reflexivity.
- symmetry.
- eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
- apply ndr_comp_respects; try reflexivity; simpl; auto.
+ abstract (intros; simpl;
+ setoid_rewrite (ndr_prod_left_identity f);
+ repeat setoid_rewrite ndr_comp_associativity;
+ apply ndr_comp_respects; try reflexivity;
+ symmetry;
+ eapply transitivity; [ idtac | apply ndr_comp_right_identity ];
+ apply ndr_comp_respects; try reflexivity; simpl; auto).
Defined.
- Definition jud_mon_assoc_iso :
- forall X,
- (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor) X) ≅
- (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor))) X.
+ Definition jud_mon_assoc_iso : forall X,
+ (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>>
+ Judgments_Category_monoidal_endofunctor) X) ≅
+ (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>>
+ Judgments_Category_monoidal_endofunctor))) X.
intros.
destruct X as [a c].
destruct a as [a b].
- apply (jud_assoc_iso a b c).
+ exact (jud_assoc_iso a b c).
Defined.
Definition jud_mon_assoc :
((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor)
func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)).
refine {| ni_iso := jud_mon_assoc_iso |}.
intros.
- destruct A as [a1 a3]. destruct a1 as [a1 a2].
- destruct B as [b1 b3]. destruct b1 as [b1 b2].
- destruct f as [f1 f3]. destruct f1 as [f1 f2].
- simpl.
+ unfold hom in *.
+ destruct A as [a1 a3]. destruct a1 as [a1 a2]. simpl in *.
+ destruct B as [b1 b3]. destruct b1 as [b1 b2]. simpl in *.
+ destruct f as [f1 f3]. destruct f1 as [f1 f2]. simpl in *.
+ unfold hom in *.
+ unfold ob in *.
+ unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
setoid_rewrite ndr_prod_associativity.
setoid_rewrite ndr_comp_associativity.
setoid_rewrite ndr_comp_associativity.
apply ndr_comp_respects; try reflexivity.
+ etransitivity.
symmetry.
- eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
- apply ndr_comp_respects; try reflexivity; simpl; auto.
+ apply ndr_comp_right_identity.
+ apply ndr_comp_respects; try reflexivity.
+ apply ndr_structural_indistinguishable; auto.
Defined.
Instance Judgments_Category_monoidal : MonoidalCat _ _ Judgments_Category_monoidal_endofunctor [ ] :=
{ mon_cancelr := jud_mon_cancelr
; mon_cancell := jud_mon_cancell
; mon_assoc := jud_mon_assoc }.
- apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto.
- apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto.
+ abstract
+ (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
+ apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto).
+ abstract
+ (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
+ apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto).
Defined.
- Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal.
- admit.
+ Instance Judgments_Category_Terminal : Terminal Judgments_Category.
+ refine {| one := [] ; drop := nd_weak' ; drop_unique := _ |}.
+ abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant).
Defined.
- (* Given some mapping "rep" that turns a (Tree ??T) intoto Judgment,
- * this asserts that we have sensible structural rules with respect
- * to that mapping. Doing all of this "with respect to a mapping"
- * lets us avoid duplicating code for both the antecedent and
- * succedent of sequent deductions. *)
- Class TreeStructuralRules {T:Type}(rep:Tree ??T -> Judgment) :=
- { tsr_eqv : @ND_Relation Judgment Rule where "pf1 === pf2" := (@ndr_eqv _ _ tsr_eqv _ _ pf1 pf2)
- ; tsr_ant_assoc : forall {a b c}, Rule [rep ((a,,b),,c)] [rep ((a,,(b,,c)))]
- ; tsr_ant_cossa : forall {a b c}, Rule [rep (a,,(b,,c))] [rep (((a,,b),,c))]
- ; tsr_ant_cancell : forall {a }, Rule [rep ( [],,a )] [rep ( a )]
- ; tsr_ant_cancelr : forall {a }, Rule [rep (a,,[] )] [rep ( a )]
- ; tsr_ant_llecnac : forall {a }, Rule [rep ( a )] [rep ( [],,a )]
- ; tsr_ant_rlecnac : forall {a }, Rule [rep ( a )] [rep ( a,,[] )]
- }.
+ Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
+ refine {| copy_nt := _ |}.
+ intros.
+ refine {| nt_component := nd_copy |}.
+ intros.
+ unfold hom in *; unfold ob in *; unfold eqv.
+ simpl.
+ rewrite ndr_prod_preserves_copy; auto.
+ reflexivity.
+ Defined.
+
+ Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal.
+ refine {| car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal
+ ; car_one := iso_id [] |}
+ ; intros; unfold hom; simpl
+ ; unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
+
+ apply ndr_structural_indistinguishable; auto.
+ apply nd_structural_comp; auto.
+ apply nd_structural_comp; auto.
+ unfold copy; simpl; apply nd_structural_copy; auto.
+ apply nd_structural_prod; auto.
+ apply nd_structural_comp; auto.
+ apply weak'_structural.
+ apply nd_structural_id0; auto.
+ apply nd_structural_cancell; auto.
+
+ apply ndr_structural_indistinguishable; auto.
+ apply nd_structural_comp; auto.
+ apply nd_structural_comp; auto.
+ unfold copy; simpl; apply nd_structural_copy; auto.
+ apply nd_structural_prod; auto.
+ apply nd_structural_comp; auto.
+ apply weak'_structural.
+ apply nd_structural_id0; auto.
+ apply nd_structural_cancelr; auto.
+ Defined.
(* Structure ExpressionAlgebra (sig:Signature) := *)
projects / coq-hetmet.git / blobdiff