src/ProgrammingLanguageFlattening.v

   1 (*********************************************************************************************************************************)
   2 (* ProgrammingLanguageFlattening                                                                                                 *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Categories_ch1_3.
   9 Require Import InitialTerminal_ch2_2.
  10 Require Import Functors_ch1_4.
  11 Require Import Isomorphisms_ch1_5.
  12 Require Import ProductCategories_ch1_6_1.
  13 Require Import OppositeCategories_ch1_6_2.
  14 Require Import Enrichment_ch2_8.
  15 Require Import Subcategories_ch7_1.
  16 Require Import NaturalTransformations_ch7_4.
  17 Require Import NaturalIsomorphisms_ch7_5.
  18 Require Import BinoidalCategories.
  19 Require Import PreMonoidalCategories.
  20 Require Import MonoidalCategories_ch7_8.
  21 Require Import Coherence_ch7_8.
  22 Require Import Enrichment_ch2_8.
  23 Require Import RepresentableStructure_ch7_2.
  24 Require Import FunctorCategories_ch7_7.
  25
  26 Require Import Reification.
  27 Require Import NaturalDeduction.
  28 Require Import NaturalDeductionCategory.
  29 Require Import GeneralizedArrow.
  30 Require Import ProgrammingLanguage.
  31 Require Import ProgrammingLanguageReification.
  32 Require Import SectionRetract_ch2_4.
  33 Require Import GeneralizedArrowFromReification.
  34 Require Import Enrichments.
  35 Require Import ReificationsAndGeneralizedArrows.
  36
  37 Section Flattening.
  38
  39   Context `(Guest:ProgrammingLanguage) `(Host :ProgrammingLanguage).
  40   Context (GuestHost:TwoLevelLanguage Guest Host).
  41
  42   Definition FlatObject (x:TypesL Host) :=
  43     forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
  44
  45   Instance FlatSubCategory : FullSubcategory (TypesL Host) FlatObject.
  46
  47     Context  (F:RetractionOfCategories (TypesL Host) (FullSubCategoriesAreCategories FlatSubCategory)).
  48
  49     Definition FlatteningOfReification HostMonic HostMonoidal :=
  50       (ga_functor
  51         (@garrow_from_reification
  52           (TypesEnrichedInJudgments Guest)
  53           (TypesEnrichedInJudgments Host)
  54           HostMonic HostMonoidal GuestHost))
  55         >>>> F.
  56
  57     Lemma FlatteningIsNotDestructive HostMonic HostMonoidal :
  58       FlatteningOfReification HostMonic HostMonoidal >>>> retraction_retraction F >>>> HomFunctor _ []
  59       ≃ (reification_rstar GuestHost).
  60       apply if_inv.
  61       set (@roundtrip_reification_to_reification (TypesEnrichedInJudgments Guest) (TypesEnrichedInJudgments Host)
  62         HostMonic HostMonoidal GuestHost) as q.
  63       unfold mf_F in *; simpl in *.
  64       eapply if_comp.
  65       apply q.
  66       clear q.
  67       unfold mf_F; simpl.
  68       unfold pmon_I.
  69       apply (if_respects
  70         (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
  71         (FlatteningOfReification HostMonic HostMonoidal >>>> retraction_retraction F)
  72         (HomFunctor (TypesL Host) [])
  73         (HomFunctor (TypesL Host) [])); [ idtac | apply (if_id _) ].
  74       unfold FlatteningOfReification.
  75       unfold mf_F; simpl.
  76       apply if_inv.
  77       eapply if_comp.
  78       apply (if_associativity (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost) F
  79                (retraction_retraction F)).
  80       eapply if_comp; [ idtac | apply if_right_identity ].
  81       apply (if_respects
  82         (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
  83         (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
  84         (F >>>> retraction_retraction F)
  85         (functor_id _)).
  86       apply (if_id _).
  87       apply retraction_composes.
  88       Qed.
  89
  90 End Flattening.
  91
  92