src/NaturalDeductionCategory.v

   1 (*********************************************************************************************************************************)
   2 (* NaturalDeductionCategory:                                                                                                     *)
   3 (*                                                                                                                               *)
   4 (*   Natural Deduction proofs form a category (under mild assumptions, see below)                                                *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12
  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.
  27
  28 Open Scope nd_scope.
  29 Open Scope pf_scope.
  30
  31 (* proofs form a category, with judgment-trees as the objects *)
  32 Section Judgments_Category.
  33
  34   Context {Judgment : Type}.
  35   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
  36   Context (nd_eqv   : @ND_Relation Judgment Rule).
  37
  38   Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2).
  39
  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
  45   }.
  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.
  54   Defined.
  55
  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.
  69
  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 *.
  75       reflexivity.
  76     intros; unfold eqv in *; simpl in *.
  77       setoid_rewrite <- ndr_prod_preserves_comp.
  78       setoid_rewrite ndr_comp_left_identity.
  79       reflexivity.
  80     Defined.
  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 *.
  86       reflexivity.
  87     intros; unfold eqv in *; simpl in *.
  88       setoid_rewrite <- ndr_prod_preserves_comp.
  89       setoid_rewrite ndr_comp_left_identity.
  90       reflexivity.
  91     Defined.
  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)).
  96     refine
  97     {| iso_forward  := nd_assoc
  98      ; iso_backward := nd_cossa |};
  99     abstract (simpl; auto).
 100     Defined.
 101   Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
 102     refine
 103     {| iso_forward  := nd_cancelr
 104      ; iso_backward := nd_rlecnac |};
 105     abstract (simpl; auto).
 106     Defined.
 107   Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
 108     refine
 109     {| iso_forward  := nd_cancell
 110      ; iso_backward := nd_llecnac |};
 111     abstract (simpl; auto).
 112     Defined.
 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.
 117     Defined.
 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.
 122     Defined.
 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.
 127     Defined.
 128   Instance jud_mon_assoc_rr : forall a b, - ⋉(a ⊗ b) <~~~> - ⋉a >>>> - ⋉b.
 129     intros.
 130     apply ni_inv.
 131     refine {| ni_iso := fun c => (jud_assoc_iso _ _ _) |}.
 132     intros; unfold eqv in *; simpl in *.
 133     apply ndr_comp_preserves_assoc.
 134     Defined.
 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.
 139     Defined.
 140
 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
 147   }.
 148     unfold functor_fobj; unfold fmor; simpl;
 149       apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto.
 150
 151     unfold functor_fobj; unfold fmor; simpl;
 152       apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto.
 153
 154     intros; unfold eqv; simpl; auto.
 155
 156     intros; unfold eqv; simpl; auto.
 157
 158     intros; unfold eqv; simpl.
 159       apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
 160       symmetry.
 161       etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
 162       symmetry.
 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.
 168       symmetry.
 169       etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
 170       symmetry.
 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.
 176
 177     intros; unfold eqv; simpl.
 178       apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
 179       symmetry.
 180       etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
 181       symmetry.
 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.
 187       symmetry.
 188       etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
 189       symmetry.
 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.
 195
 196     intros; unfold eqv; simpl.
 197       apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
 198       symmetry.
 199       etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
 200       symmetry.
 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.
 206       symmetry.
 207       etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
 208       symmetry.
 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.
 214
 215       Defined.
 216
 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 *.
 221
 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.
 226       reflexivity.
 227
 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.
 232       reflexivity.
 233     Defined.
 234
 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).
 238     Defined.
 239
 240   Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
 241     intros.
 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.
 246       etransitivity.
 247       symmetry.
 248       apply ndr_prod_preserves_comp.
 249       setoid_rewrite ndr_comp_left_identity.
 250       setoid_rewrite ndr_comp_right_identity.
 251       reflexivity.
 252     setoid_rewrite ndr_comp_associativity.
 253       setoid_rewrite <- (ndr_prod_preserves_copy f).
 254       apply ndr_comp_respects; try reflexivity.
 255       etransitivity.
 256       symmetry.
 257       apply ndr_prod_preserves_comp.
 258       setoid_rewrite ndr_comp_left_identity.
 259       setoid_rewrite ndr_comp_right_identity.
 260       reflexivity.
 261       Defined.
 262
 263   Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal :=
 264     { car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal }.
 265
 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.
 270     Defined.
 271
 272 End Judgments_Category.
 273
 274 Close Scope pf_scope.
 275 Close Scope nd_scope.