1 (*********************************************************************************************************************************)
2 (* ProgrammingLanguageFlattening *)
3 (*********************************************************************************************************************************)
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.
26 Require Import Reification.
27 Require Import NaturalDeduction.
28 Require Import NaturalDeductionCategory.
29 Require Import GeneralizedArrow.
30 Require Import ProgrammingLanguageEnrichment.
31 Require Import ProgrammingLanguageReification.
32 Require Import SectionRetract_ch2_4.
33 Require Import GeneralizedArrowFromReification.
34 Require Import Enrichments.
35 Require Import ReificationsAndGeneralizedArrows.
39 Context `(Guest:ProgrammingLanguage) `(Host :ProgrammingLanguage).
40 Context (GuestHost:TwoLevelLanguage Guest Host).
42 Definition FlatObject (x:TypesL Host) :=
43 forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
45 Instance FlatSubCategory : FullSubcategory (TypesL Host) FlatObject.
47 Context (F:RetractionOfCategories (TypesL Host) (FullSubCategoriesAreCategories FlatSubCategory)).
49 Definition FlatteningOfReification HostMonic HostMonoidal :=
51 (@garrow_from_reification
52 (TypesEnrichedInJudgments Guest)
53 (TypesEnrichedInJudgments Host)
54 HostMonic HostMonoidal GuestHost))
57 Lemma FlatteningIsNotDestructive HostMonic HostMonoidal :
58 FlatteningOfReification HostMonic HostMonoidal >>>> retraction_retraction F >>>> HomFunctor _ []
59 ≃ (reification_rstar GuestHost).
61 set (@roundtrip_reification_to_reification (TypesEnrichedInJudgments Guest) (TypesEnrichedInJudgments Host)
62 HostMonic HostMonoidal GuestHost) as q.
63 unfold mf_F in *; simpl in *.
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.
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 ].
82 (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
83 (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost)
84 (F >>>> retraction_retraction F)
87 apply retraction_composes.