1 (*********************************************************************************************************************************)
2 (* NaturalDeductionCategory: *)
4 (* Natural Deduction proofs form a category (under mild assumptions, see below) *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
13 Require Import Algebras_ch4.
14 Require Import Categories_ch1_3.
15 Require Import Functors_ch1_4.
16 Require Import Isomorphisms_ch1_5.
17 Require Import OppositeCategories_ch1_6_2.
18 Require Import Enrichment_ch2_8.
19 Require Import Subcategories_ch7_1.
20 Require Import NaturalTransformations_ch7_4.
21 Require Import NaturalIsomorphisms_ch7_5.
22 Require Import Coherence_ch7_8.
23 Require Import InitialTerminal_ch2_2.
24 Require Import BinoidalCategories.
25 Require Import PreMonoidalCategories.
26 Require Import MonoidalCategories_ch7_8.
31 (* proofs form a category, with judgment-trees as the objects *)
32 Section Judgments_Category.
34 Context {Judgment : Type}.
35 Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
36 Context (nd_eqv : @ND_Relation Judgment Rule).
38 Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2).
40 (* there is a category whose objects are judgments and whose morphisms are proofs *)
41 Instance Judgments_Category : Category (Tree ??Judgment) (fun h c => h /⋯⋯/ c) :=
42 { id := fun h => nd_id _
43 ; comp := fun a b c f g => f ;; g
44 ; eqv := fun a b f g => f === g
46 intros; apply Build_Equivalence;
47 [ unfold Reflexive; intros; reflexivity
48 | unfold Symmetric; intros; symmetry; auto
49 | unfold Transitive; intros; transitivity y; auto ].
50 unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto.
51 intros; apply ndr_comp_left_identity.
52 intros; apply ndr_comp_right_identity.
53 intros; apply ndr_comp_associativity.
56 Hint Extern 1 => apply nd_structural_id0.
57 Hint Extern 1 => apply nd_structural_id1.
58 Hint Extern 1 => apply nd_structural_weak.
59 Hint Extern 1 => apply nd_structural_copy.
60 Hint Extern 1 => apply nd_structural_prod.
61 Hint Extern 1 => apply nd_structural_comp.
62 Hint Extern 1 => apply nd_structural_cancell.
63 Hint Extern 1 => apply nd_structural_cancelr.
64 Hint Extern 1 => apply nd_structural_llecnac.
65 Hint Extern 1 => apply nd_structural_rlecnac.
66 Hint Extern 1 => apply nd_structural_assoc.
67 Hint Extern 1 => apply nd_structural_cossa.
68 Hint Extern 1 => apply weak'_structural.
70 Instance jud_first (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => x,,a) :=
71 { fmor := fun b c (f:b /⋯⋯/ c) => f ** (nd_id a) }.
72 intros; unfold eqv; simpl.
73 apply ndr_prod_respects; auto.
74 intros; unfold eqv in *; simpl in *.
76 intros; unfold eqv in *; simpl in *.
77 setoid_rewrite <- ndr_prod_preserves_comp.
78 setoid_rewrite ndr_comp_left_identity.
81 Instance jud_second (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => a,,x) :=
82 { fmor := fun b c (f:b /⋯⋯/ c) => (nd_id a) ** f }.
83 intros; unfold eqv; simpl.
84 apply ndr_prod_respects; auto.
85 intros; unfold eqv in *; simpl in *.
87 intros; unfold eqv in *; simpl in *.
88 setoid_rewrite <- ndr_prod_preserves_comp.
89 setoid_rewrite ndr_comp_left_identity.
92 Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (fun x y => x,,y) :=
93 { bin_first := jud_first
94 ; bin_second := jud_second }.
95 Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)).
97 {| iso_forward := nd_assoc
98 ; iso_backward := nd_cossa |};
99 abstract (simpl; auto).
101 Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
103 {| iso_forward := nd_cancelr
104 ; iso_backward := nd_rlecnac |};
105 abstract (simpl; auto).
107 Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
109 {| iso_forward := nd_cancell
110 ; iso_backward := nd_llecnac |};
111 abstract (simpl; auto).
113 Instance jud_mon_cancelr : jud_first [] <~~~> functor_id Judgments_Category :=
114 { ni_iso := jud_cancelr_iso }.
115 intros; unfold eqv in *; simpl in *.
116 apply ndr_comp_preserves_cancelr.
118 Instance jud_mon_cancell : jud_second [] <~~~> functor_id Judgments_Category :=
119 { ni_iso := jud_cancell_iso }.
120 intros; unfold eqv in *; simpl in *.
121 apply ndr_comp_preserves_cancell.
123 Instance jud_mon_assoc : forall a b, a ⋊- >>>> - ⋉b <~~~> - ⋉b >>>> a ⋊- :=
124 { ni_iso := fun c => jud_assoc_iso a c b }.
125 intros; unfold eqv in *; simpl in *.
126 apply ndr_comp_preserves_assoc.
128 Instance jud_mon_assoc_rr : forall a b, - ⋉(a ⊗ b) <~~~> - ⋉a >>>> - ⋉b.
131 refine {| ni_iso := fun c => (jud_assoc_iso _ _ _) |}.
132 intros; unfold eqv in *; simpl in *.
133 apply ndr_comp_preserves_assoc.
135 Instance jud_mon_assoc_ll : forall a b, (a ⊗ b) ⋊- <~~~> b ⋊- >>>> a ⋊- :=
136 { ni_iso := fun c => jud_assoc_iso _ _ _ }.
137 intros; unfold eqv in *; simpl in *.
138 apply ndr_comp_preserves_assoc.
141 Instance Judgments_Category_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] :=
142 { pmon_cancelr := jud_mon_cancelr
143 ; pmon_cancell := jud_mon_cancell
144 ; pmon_assoc := jud_mon_assoc
145 ; pmon_assoc_rr := jud_mon_assoc_rr
146 ; pmon_assoc_ll := jud_mon_assoc_ll
148 unfold functor_fobj; unfold fmor; simpl;
149 apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto.
151 unfold functor_fobj; unfold fmor; simpl;
152 apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto.
154 intros; unfold eqv; simpl; auto.
156 intros; unfold eqv; simpl; auto.
158 intros; unfold eqv; simpl.
159 apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
161 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
163 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
164 setoid_rewrite ndr_comp_left_identity.
165 setoid_rewrite ndr_comp_right_identity.
166 apply ndr_prod_respects; try reflexivity.
167 apply ndr_structural_indistinguishable; auto.
169 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
171 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
172 setoid_rewrite ndr_comp_left_identity.
173 setoid_rewrite ndr_comp_right_identity.
174 apply ndr_prod_respects; try reflexivity.
175 apply ndr_structural_indistinguishable; auto.
177 intros; unfold eqv; simpl.
178 apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
180 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
182 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
183 setoid_rewrite ndr_comp_left_identity.
184 setoid_rewrite ndr_comp_right_identity.
185 apply ndr_prod_respects; try reflexivity.
186 apply ndr_structural_indistinguishable; auto.
188 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
190 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
191 setoid_rewrite ndr_comp_left_identity.
192 setoid_rewrite ndr_comp_right_identity.
193 apply ndr_prod_respects; try reflexivity.
194 apply ndr_structural_indistinguishable; auto.
196 intros; unfold eqv; simpl.
197 apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
199 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
201 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
202 setoid_rewrite ndr_comp_left_identity.
203 setoid_rewrite ndr_comp_right_identity.
204 apply ndr_prod_respects; try reflexivity.
205 apply ndr_structural_indistinguishable; auto.
207 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
209 etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
210 setoid_rewrite ndr_comp_left_identity.
211 setoid_rewrite ndr_comp_right_identity.
212 apply ndr_prod_respects; try reflexivity.
213 apply ndr_structural_indistinguishable; auto.
217 Instance Judgments_Category_monoidal : MonoidalCat Judgments_Category_premonoidal.
218 apply Build_MonoidalCat.
219 apply Build_CommutativeCat.
220 intros; apply Build_CentralMorphism; intros; unfold eqv; simpl in *.
222 setoid_rewrite <- (ndr_prod_preserves_comp (nd_id a) g f (nd_id d)).
223 setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g).
224 setoid_rewrite ndr_comp_left_identity.
225 setoid_rewrite ndr_comp_right_identity.
228 setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)).
229 setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f).
230 setoid_rewrite ndr_comp_left_identity.
231 setoid_rewrite ndr_comp_right_identity.
235 Instance Judgments_Category_Terminal : TerminalObject Judgments_Category [].
236 refine {| drop := nd_weak' ; drop_unique := _ |}.
237 abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant).
240 Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
242 refine {| copy := nd_copy |}; intros; simpl.
243 setoid_rewrite ndr_comp_associativity.
244 setoid_rewrite <- (ndr_prod_preserves_copy f).
245 apply ndr_comp_respects; try reflexivity.
248 apply ndr_prod_preserves_comp.
249 setoid_rewrite ndr_comp_left_identity.
250 setoid_rewrite ndr_comp_right_identity.
252 setoid_rewrite ndr_comp_associativity.
253 setoid_rewrite <- (ndr_prod_preserves_copy f).
254 apply ndr_comp_respects; try reflexivity.
257 apply ndr_prod_preserves_comp.
258 setoid_rewrite ndr_comp_left_identity.
259 setoid_rewrite ndr_comp_right_identity.
263 Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal :=
264 { car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal }.
266 intros; unfold hom; simpl; unfold functor_fobj; unfold fmor; simpl.
267 apply ndr_structural_indistinguishable; auto.
268 intros; unfold hom; simpl; unfold functor_fobj; unfold fmor; simpl.
269 apply ndr_structural_indistinguishable; auto.
272 End Judgments_Category.
274 Close Scope pf_scope.
275 Close Scope nd_scope.