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 MonoidalCategories_ch7_8.
  19 Require Import Coherence_ch7_8.
  20 Require Import Enrichment_ch2_8.
  21 Require Import RepresentableStructure_ch7_2.
  22 Require Import FunctorCategories_ch7_7.
  23
  24 Require Import Reification.
  25 Require Import NaturalDeduction.
  26 Require Import NaturalDeductionCategory.
  27 Require Import GeneralizedArrow.
  28 Require Import GeneralizedArrowFromReification.
  29 Require Import ProgrammingLanguage.
  30 Require Import ProgrammingLanguageReification.
  31 Require Import ReificationsAndGeneralizedArrows.
  32
  33 Section Flattening.
  34
  35   Context (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME).
  36   Context (GuestHost:TwoLevelLanguage Guest Host).
  37
  38   Definition FlatObject (x:TypesL _ _ Host) :=
  39     forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
  40
  41   Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject.
  42
  43     Context  (F:Retraction (TypesL _ _ Host) FlatSubCategory).
  44
  45     Definition FlatteningOfReification :=
  46       garrow_from_reification Guest Host GuestHost >>>> F.
  47
  48 (*
  49     Lemma FlatteningIsNotDestructive :
  50       FlatteningOfReification >>>> retraction_retraction F >>>> HomFunctor _ (me_i Host) ≃ GuestHost.
  51       apply if_inv.
  52       set (@roundtrip_reification_to_reification _ Guest _ _ Host GuestHost) as q.
  53       unfold mf_f in *; simpl in *.
  54       apply (if_comp q).
  55       clear q.
  56       unfold me_mf; simpl.
  57       unfold mf_f; simpl.
  58       refine (if_respects _ (if_id _)).
  59       unfold FlatteningOfReification.
  60       unfold mf_f; simpl.
  61       eapply if_comp.
  62       Focus 2.
  63       eapply if_inv.
  64       apply (if_associativity (garrow_functor Guest Host GuestHost) F (retraction_retraction F)).
  65       eapply if_comp.
  66       eapply if_inv.
  67       apply if_right_identity.
  68       refine (if_respects (if_id _) _).
  69       apply if_inv.
  70       apply retraction_composes.
  71       Qed.
  72 *)
  73 End Flattening.
  74
  75