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 ProductCategories_ch1_6_1.
  18 Require Import OppositeCategories_ch1_6_2.
  19 Require Import Enrichment_ch2_8.
  20 Require Import Subcategories_ch7_1.
  21 Require Import NaturalTransformations_ch7_4.
  22 Require Import NaturalIsomorphisms_ch7_5.
  23 Require Import MonoidalCategories_ch7_8.
  24 Require Import Coherence_ch7_8.
  25 Require Import InitialTerminal_ch2_2.
  26
  27 Open Scope nd_scope.
  28 Open Scope pf_scope.
  29
  30 (* proofs form a category, with judgment-trees as the objects *)
  31 Section Judgments_Category.
  32
  33   Context {Judgment : Type}.
  34   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
  35   Context (nd_eqv   : @ND_Relation Judgment Rule).
  36
  37   Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2).
  38
  39   (* there is a category whose objects are judgments and whose morphisms are proofs *)
  40   Instance Judgments_Category : Category (Tree ??Judgment) (fun h c => h /⋯⋯/ c) :=
  41   { id   := fun h          => nd_id _
  42   ; comp := fun a b c f g  => f ;; g
  43   ; eqv  := fun a b f g    => f === g
  44   }.
  45   intros; apply Build_Equivalence;
  46     [ unfold Reflexive; intros; reflexivity
  47     | unfold Symmetric; intros; symmetry; auto
  48     | unfold Transitive; intros; transitivity y; auto ].
  49   unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto.
  50   intros; apply ndr_comp_left_identity.
  51   intros; apply ndr_comp_right_identity.
  52   intros; apply ndr_comp_associativity.
  53   Defined.
  54
  55   (* it is monoidal, with the judgment-tree-formation operator as its tensor *)
  56   Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category :=
  57     fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy).
  58   Definition Judgments_Category_monoidal_endofunctor_fmor :
  59            forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) ->
  60            ((Judgments_Category_monoidal_endofunctor_fobj a)
  61            ~~{Judgments_Category}~~>
  62            (Judgments_Category_monoidal_endofunctor_fobj b)).
  63      intros.
  64      destruct a.
  65      destruct b.
  66      destruct X.
  67      simpl in *.
  68      exact (h**h0).
  69      Defined.
  70   Definition Judgments_Category_monoidal_endofunctor
  71   : Functor (Judgments_Category ×× Judgments_Category) Judgments_Category Judgments_Category_monoidal_endofunctor_fobj.
  72     refine {| fmor := Judgments_Category_monoidal_endofunctor_fmor |}; intros; simpl.
  73     abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; simpl in *; apply ndr_prod_respects; auto).
  74     abstract (destruct a; simpl in *; reflexivity).
  75     abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; simpl in *; apply ndr_prod_preserves_comp).
  76     Defined.
  77
  78   Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)).
  79     refine
  80     {| iso_forward  := nd_assoc
  81      ; iso_backward := nd_cossa |};
  82     abstract (simpl; auto).
  83     Defined.
  84   Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
  85     refine
  86     {| iso_forward  := nd_cancelr
  87      ; iso_backward := nd_rlecnac |};
  88     abstract (simpl; auto).
  89     Defined.
  90   Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
  91     refine
  92     {| iso_forward  := nd_cancell
  93      ; iso_backward := nd_llecnac |};
  94     abstract (simpl; auto).
  95     Defined.
  96
  97   Definition jud_mon_cancelr : (func_rlecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
  98     refine {| ni_iso := fun x => jud_cancelr_iso x |}; intros; simpl.
  99     abstract (setoid_rewrite (ndr_prod_right_identity f);
 100               repeat setoid_rewrite ndr_comp_associativity;
 101               apply ndr_comp_respects; try reflexivity;
 102               symmetry;
 103               eapply transitivity; [ idtac | apply ndr_comp_right_identity ];
 104               apply ndr_comp_respects; try reflexivity; simpl; auto).
 105     Defined.
 106   Definition jud_mon_cancell : (func_llecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
 107     eapply Build_NaturalIsomorphism.
 108     instantiate (1:=fun x => jud_cancell_iso x).
 109     abstract (intros; simpl;
 110               setoid_rewrite (ndr_prod_left_identity f);
 111               repeat setoid_rewrite ndr_comp_associativity;
 112               apply ndr_comp_respects; try reflexivity;
 113               symmetry;
 114               eapply transitivity; [ idtac | apply ndr_comp_right_identity ];
 115               apply ndr_comp_respects; try reflexivity; simpl; auto).
 116     Defined.
 117   Definition jud_mon_assoc_iso : forall X,
 118       (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>>
 119         Judgments_Category_monoidal_endofunctor) X) ≅
 120        (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>>
 121          Judgments_Category_monoidal_endofunctor))) X.
 122     intros.
 123     destruct X as [a c].
 124     destruct a as [a b].
 125     exact (jud_assoc_iso a b c).
 126     Defined.
 127   Definition jud_mon_assoc   :
 128     ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor)
 129     <~~~>
 130     func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)).
 131     refine {| ni_iso := jud_mon_assoc_iso |}.
 132     intros.
 133     unfold hom in *.
 134     destruct A as [a1 a3]. destruct a1 as [a1 a2]. simpl in *.
 135     destruct B as [b1 b3]. destruct b1 as [b1 b2]. simpl in *.
 136     destruct f as [f1 f3]. destruct f1 as [f1 f2]. simpl in *.
 137     unfold hom in *.
 138     unfold ob in *.
 139     unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
 140     setoid_rewrite ndr_prod_associativity.
 141     setoid_rewrite ndr_comp_associativity.
 142     setoid_rewrite ndr_comp_associativity.
 143     apply ndr_comp_respects; try reflexivity.
 144     etransitivity.
 145     symmetry.
 146     apply ndr_comp_right_identity.
 147     apply ndr_comp_respects; try reflexivity.
 148     apply ndr_structural_indistinguishable; auto.
 149     Defined.
 150
 151   Instance Judgments_Category_monoidal : MonoidalCat _ _ Judgments_Category_monoidal_endofunctor [ ] :=
 152   { mon_cancelr := jud_mon_cancelr
 153   ; mon_cancell := jud_mon_cancell
 154   ; mon_assoc   := jud_mon_assoc   }.
 155     abstract
 156       (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
 157         apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto).
 158     abstract
 159       (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
 160         apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto).
 161     Defined.
 162
 163   Instance Judgments_Category_Terminal : Terminal Judgments_Category.
 164     refine {| one := [] ; drop := nd_weak' ; drop_unique := _ |}.
 165       abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant).
 166     Defined.
 167
 168   Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
 169     refine {| copy_nt := _ |}.
 170     intros.
 171     refine {| nt_component := nd_copy |}.
 172     intros.
 173     unfold hom in *; unfold ob in *; unfold eqv.
 174     simpl.
 175     rewrite ndr_prod_preserves_copy; auto.
 176     reflexivity.
 177     Defined.
 178
 179   Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal.
 180     refine {| car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal
 181       ; car_one := iso_id [] |}
 182       ; intros; unfold hom; simpl
 183       ; unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
 184
 185     apply ndr_structural_indistinguishable; auto.
 186     apply nd_structural_comp; auto.
 187     apply nd_structural_comp; auto.
 188     unfold copy; simpl; apply nd_structural_copy; auto.
 189     apply nd_structural_prod; auto.
 190     apply nd_structural_comp; auto.
 191     apply weak'_structural.
 192     apply nd_structural_id0; auto.
 193     apply nd_structural_cancell; auto.
 194
 195     apply ndr_structural_indistinguishable; auto.
 196     apply nd_structural_comp; auto.
 197     apply nd_structural_comp; auto.
 198     unfold copy; simpl; apply nd_structural_copy; auto.
 199     apply nd_structural_prod; auto.
 200     apply nd_structural_comp; auto.
 201     apply weak'_structural.
 202     apply nd_structural_id0; auto.
 203     apply nd_structural_cancelr; auto.
 204     Defined.
 205
 206 End Judgments_Category.
 207
 208 Close Scope pf_scope.
 209 Close Scope nd_scope.