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