src/NaturalDeductionCategory.v

   1 (*********************************************************************************************************************************)
   2 (* NaturalDeductionCategory:                                                                                                     *)
   3 (*                                                                                                                               *)
   4 (*   Natural Deduction proofs form a category                                                                                    *)
   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_builtfrom_structural f); auto.
  52   intros; apply (ndr_builtfrom_structural f); auto.
  53   intros; apply ndr_comp_associativity.
  54   Defined.
  55
  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.
  65     Defined.
  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.
  74     Defined.
  75   Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (@T_Branch (??Judgment)) :=
  76     { bin_first  := jud_first
  77     ; bin_second := jud_second }.
  78
  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.
  87       reflexivity.
  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.
  92       reflexivity.
  93       Defined.
  94
  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.
 100     Defined.
 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.
 104     Defined.
 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.
 108     Defined.
 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.
 112     Defined.
 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.
 116     Defined.
 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.
 120     Defined.
 121   Instance jud_mon_assoc_rr : forall a b, - ⋉(a ⊗ b) <~~~> - ⋉a >>>> - ⋉b.
 122     intros.
 123     apply ni_inv.
 124     refine {| ni_iso := fun c => (jud_assoc_iso _ _ _) |}.
 125     intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto.
 126     Defined.
 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.
 130     Defined.
 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
 137   }.
 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.
 147       Defined.
 148
 149   (* commutative premonoidal categories are monoidal *)
 150   Instance Judgments_Category_monoidal : MonoidalCat Judgments_Category_premonoidal :=
 151     { mon_commutative := Judgments_Category_Commutative }.
 152
 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).
 157     Defined.
 158
 159   (* Judgments is also a diagonal category via nd_copy *)
 160   Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
 161     intros.
 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.
 166       etransitivity.
 167       symmetry.
 168       apply ndr_prod_preserves_comp.
 169       setoid_rewrite ndr_comp_left_identity.
 170       setoid_rewrite ndr_comp_right_identity.
 171       reflexivity.
 172     setoid_rewrite ndr_comp_associativity.
 173       setoid_rewrite <- (ndr_prod_preserves_copy f).
 174       apply ndr_comp_respects; try reflexivity.
 175       etransitivity.
 176       symmetry.
 177       apply ndr_prod_preserves_comp.
 178       setoid_rewrite ndr_comp_left_identity.
 179       setoid_rewrite ndr_comp_right_identity.
 180       reflexivity.
 181       Defined.
 182
 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.
 188     Defined.
 189
 190 End Judgments_Category.
 191
 192 Close Scope pf_scope.
 193 Close Scope nd_scope.