--- /dev/null
+Require Import Preamble.
+Require Import General.
+
+Require Import HaskKinds.
+Require Import HaskLiteralsAndTyCons.
+
+Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
+Require Import HaskCore.
+
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
+Require Import HaskWeak.
+
+Require Import HaskCoreToWeak.
+
+Require Import HaskStrongTypes.
+Require Import HaskStrong.
+
+Require Import NaturalDeduction.
+Require Import NaturalDeductionToLatex.
+
+Require Import HaskProof.
+
+Require Import HaskProofToStrong.
+Require Import HaskStrongToWeak.
+Require Import HaskWeakToCore.
+(*Require Import HaskWeakToStrong.*)
+Require Import HaskStrongToProof.
+(*Require Import HaskProofToLatex.*)
+
+(*Require Import HaskStrongCategory.*)
+(*Require Import Extraction.*)
+
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+Require Import SliceCategories_ch1_6_4.
+
+Require Import EpicMonic_ch2_1.
+Require Import InitialTerminal_ch2_2.
+Require Import SectionRetract_ch2_4.
+
+Require Import Equalizers_ch3_3.
+Require Import CoEqualizers_ch3_4.
+
+Require Import Algebras_ch4.
+
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import FunctorCategories_ch7_7.
+
+Require Import Subcategories_ch7_1.
+
+Require Import Coherence_ch7_8.
+Require Import MonoidalCategories_ch7_8.
+
+Require Import Enrichment_ch2_8.
+Require Import RepresentableStructure_ch7_2.
+
+Require Import Yoneda_ch8.
+(*Require Import Exponentials_ch6.*)
+
+(*Require Import CategoryOfCategories_ch7_1.*)
+(*Require Import Adjoints_ch9.*)
+
+Require Import NaturalDeductionCategory.
+
+Require Import Reification.
+Require Import GeneralizedArrow.
+Require Import GeneralizedArrowFromReification.
+Require Import ReificationFromGeneralizedArrow.
+Require Import ReificationCategory.
+Require Import GeneralizedArrowCategory.
+Require Import ReificationsEquivalentToGeneralizedArrows.
+
+Require Import HaskProofCategory.
+Require Import ProgrammingLanguage.
+
+(* very slow! *)
+Require Import FreydCategories.
+Require Import Arrows.
+
+
--- /dev/null
+(***********************************************************************************************************************************
+ *
+ * This is the Coq development accompanying
+ *
+ * __Multi-Level Programs are Generalized Arrows__
+ *
+ * Best viewed on a 132-character-wide display (use the first line of this file to size your window)
+ *
+ * This file makes extensive use of Unicode (UTF-8); please make sure your text editor supports it.
+ *
+ * Here is the version of Coq I used:
+ *
+ * megacz@skolem:~$ coqc -v
+ * The Coq Proof Assistant, version 8.3pl1 (March 2011)
+ * compiled on Mar 17 2011 21:07:25 with OCaml 3.11.2
+ *
+ * Warning: this script may take a half-hour or more to typecheck, even on a very fast machine.
+ * It also needs about 1.5GB of ram; if you have less than that it will run unbearably slowly.
+ *
+ * I recommend checking it using the following command:
+ *
+ * coqc -noglob -dont-load-proofs GArrows.v
+ *
+ **********************************************************************************************************************************)
+
+Require Import Coq.Unicode.Utf8.
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Setoids.Setoid.
+Require Setoid.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import Omega.