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 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.
24 Require Import Reification.
25 Require Import NaturalDeduction.
26 Require Import NaturalDeductionCategory.
27 Require Import ProgrammingLanguage.
28 Require Import ProgrammingReification.
32 Context (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME).
33 Context (GuestHost:TwoLevelLanguage).
35 Definition FlatObject (x:TypesL _ _ Host) :=
36 forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
38 Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject.
40 Context (F:Retraction (TypesL _ _ Host) FlatSubCategory).
42 Definition FlatteningOfReification :=
43 garrow_from_reification Guest Host GuestHost >>>> F.
45 Lemma FlatteningIsNotDestructive :
46 FlatteningOfReification >>>> retraction_retraction F >>>> HomFunctor _ (me_i Host) ≃ GuestHost.
48 set (@roundtrip_reification_to_reification _ Guest _ _ Host GuestHost) as q.
49 unfold mf_f in *; simpl in *.
54 refine (if_respects _ (if_id _)).
55 unfold FlatteningOfReification.
60 apply (if_associativity (garrow_functor Guest Host GuestHost) F (retraction_retraction F)).
63 apply if_right_identity.
64 refine (if_respects (if_id _) _).
66 apply retraction_composes.