1 (*********************************************************************************************************************************)
2 (* NaturalDeductionCategory: *)
4 (* Natural Deduction proofs form a category *)
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_builtfrom_structural f); auto.
52 intros; apply (ndr_builtfrom_structural f); auto.
53 intros; apply ndr_comp_associativity.
56 (* Judgments form a binoidal category *)
57 Instance jud_first (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => x,,a) :=
58 { fmor := fun b c (f:b /⋯⋯/ c) => f ** (nd_id a) }.
59 intros; unfold eqv; simpl; apply ndr_prod_respects; auto.
60 intros; unfold eqv in *; simpl in *; reflexivity.
61 intros; unfold eqv in *; simpl in *; apply (ndr_builtfrom_structural (nd_id a)); auto.
62 intros; unfold eqv in *; simpl in *.
63 setoid_rewrite <- ndr_prod_preserves_comp.
64 apply (ndr_builtfrom_structural (f;;g)); auto.
66 Instance jud_second (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => a,,x) :=
67 { fmor := fun b c (f:b /⋯⋯/ c) => (nd_id a) ** f }.
68 intros; unfold eqv; simpl; apply ndr_prod_respects; auto.
69 intros; unfold eqv in *; simpl in *; reflexivity.
70 intros; unfold eqv in *; simpl in *; apply (ndr_builtfrom_structural (nd_id a)); auto.
71 intros; unfold eqv in *; simpl in *.
72 setoid_rewrite <- ndr_prod_preserves_comp.
73 apply (ndr_builtfrom_structural (f;;g)); auto.
75 Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (@T_Branch (??Judgment)) :=
76 { bin_first := jud_first
77 ; bin_second := jud_second }.
79 (* and that category is commutative (all morphisms central) *)
80 Instance Judgments_Category_Commutative : CommutativeCat Judgments_Category_binoidal.
81 apply Build_CommutativeCat.
82 intros; apply Build_CentralMorphism; intros; unfold eqv; simpl in *.
83 setoid_rewrite <- (ndr_prod_preserves_comp (nd_id a) g f (nd_id d)).
84 setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g).
85 setoid_rewrite ndr_comp_left_identity.
86 setoid_rewrite ndr_comp_right_identity.
88 setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)).
89 setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f).
90 setoid_rewrite ndr_comp_left_identity.
91 setoid_rewrite ndr_comp_right_identity.
95 (* Judgments form a premonoidal category *)
96 Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)).
97 refine {| iso_forward := nd_assoc ; iso_backward := nd_cossa |}.
98 unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto.
99 unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto.
101 Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
102 refine {| iso_forward := nd_cancelr ; iso_backward := nd_rlecnac |};
103 unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto.
105 Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
106 refine {| iso_forward := nd_cancell ; iso_backward := nd_llecnac |};
107 unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto.
109 Instance jud_mon_cancelr : jud_first [] <~~~> functor_id Judgments_Category :=
110 { ni_iso := jud_cancelr_iso }.
111 intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
113 Instance jud_mon_cancell : jud_second [] <~~~> functor_id Judgments_Category :=
114 { ni_iso := jud_cancell_iso }.
115 intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
117 Instance jud_mon_assoc : forall a b, a ⋊- >>>> - ⋉b <~~~> - ⋉b >>>> a ⋊- :=
118 { ni_iso := fun c => jud_assoc_iso a c b }.
119 intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
121 Instance jud_mon_assoc_rr : forall a b, - ⋉(a ⊗ b) <~~~> - ⋉a >>>> - ⋉b.
124 refine {| ni_iso := fun c => (jud_assoc_iso _ _ _) |}.
125 intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
127 Instance jud_mon_assoc_ll : forall a b, (a ⊗ b) ⋊- <~~~> b ⋊- >>>> a ⋊- :=
128 { ni_iso := fun c => jud_assoc_iso _ _ _ }.
129 intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
131 Instance Judgments_Category_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] :=
132 { pmon_cancelr := jud_mon_cancelr
133 ; pmon_cancell := jud_mon_cancell
134 ; pmon_assoc := jud_mon_assoc
135 ; pmon_assoc_rr := jud_mon_assoc_rr
136 ; pmon_assoc_ll := jud_mon_assoc_ll
138 unfold functor_fobj; unfold fmor; simpl;
139 apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10.
140 unfold functor_fobj; unfold fmor; simpl;
141 apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10.
142 intros; unfold eqv; simpl; auto; reflexivity.
143 intros; unfold eqv; simpl; auto; reflexivity.
144 intros; unfold eqv; simpl; apply Judgments_Category_Commutative.
145 intros; unfold eqv; simpl; apply Judgments_Category_Commutative.
146 intros; unfold eqv; simpl; apply Judgments_Category_Commutative.
149 (* commutative premonoidal categories are monoidal *)
150 Instance Judgments_Category_monoidal : MonoidalCat Judgments_Category_premonoidal :=
151 { mon_commutative := Judgments_Category_Commutative }.
153 (* Judgments also happens to have a terminal object - the empty list of judgments *)
154 Instance Judgments_Category_Terminal : TerminalObject Judgments_Category [].
155 refine {| drop := nd_weak ; drop_unique := _ |}.
156 abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant).
159 (* Judgments is also a diagonal category via nd_copy *)
160 Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
162 refine {| copy := nd_copy |}; intros; simpl.
163 setoid_rewrite ndr_comp_associativity.
164 setoid_rewrite <- (ndr_prod_preserves_copy f).
165 apply ndr_comp_respects; try reflexivity.
168 apply ndr_prod_preserves_comp.
169 setoid_rewrite ndr_comp_left_identity.
170 setoid_rewrite ndr_comp_right_identity.
172 setoid_rewrite ndr_comp_associativity.
173 setoid_rewrite <- (ndr_prod_preserves_copy f).
174 apply ndr_comp_respects; try reflexivity.
177 apply ndr_prod_preserves_comp.
178 setoid_rewrite ndr_comp_left_identity.
179 setoid_rewrite ndr_comp_right_identity.
183 (* Judgments is a cartesian category: it has a terminal object, diagonal morphisms, and the right naturalities *)
184 Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal :=
185 { car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal }.
186 intros; unfold eqv; simpl; symmetry; apply ndr_copy_then_weak_left.
187 intros; unfold eqv; simpl; symmetry; apply ndr_copy_then_weak_right.
190 End Judgments_Category.
192 Close Scope pf_scope.
193 Close Scope nd_scope.