src/Enrichment_ch2_8.v

   1 Generalizable All Variables.
   2 Require Import Notations.
   3 Require Import Categories_ch1_3.
   4 Require Import Functors_ch1_4.
   5 Require Import Isomorphisms_ch1_5.
   6 Require Import ProductCategories_ch1_6_1.
   7 Require Import InitialTerminal_ch2_2.
   8 Require Import Subcategories_ch7_1.
   9 Require Import NaturalTransformations_ch7_4.
  10 Require Import NaturalIsomorphisms_ch7_5.
  11 Require Import Coherence_ch7_8.
  12 Require Import BinoidalCategories.
  13 Require Import PreMonoidalCategories.
  14 Require Import MonoidalCategories_ch7_8.
  15
  16 (******************************************************************************)
  17 (* Chapter 2.8: Hom Sets and Enriched Categories                              *)
  18 (******************************************************************************)
  19
  20 Class ECategory `(mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI))(Eob:Type)(Ehom:Eob->Eob->V) :=
  21 { ehom               :=  Ehom where "a ~~> b" := (ehom a b)
  22 ; eob_eob            :=  Eob
  23 ; e_v                :=  mn
  24 ; eid                :   forall a,          EI~>(a~~>a)
  25 ; eid_central        :   forall a,          CentralMorphism (eid a)
  26 ; ecomp              :   forall {a b c},    (a~~>b)⊗(b~~>c) ~> (a~~>c)
  27 ; ecomp_central      :>  forall {a b c},    CentralMorphism (@ecomp a b c)
  28 ; eleft_identity     :   forall {a b  },    eid a ⋉ (a~~>b) >>> ecomp ~~ #(pmon_cancell _)
  29 ; eright_identity    :   forall {a b  },    (a~~>b) ⋊ eid b >>> ecomp ~~ #(pmon_cancelr _)
  30 ; eassociativity     :   forall {a b c d},  #(pmon_assoc _ _ (_~~>_))⁻¹ >>> ecomp ⋉ (c~~>d) >>> ecomp ~~ (a~~>b) ⋊ ecomp >>> ecomp
  31 }.
  32 Notation "a ~~> b" := (@ehom _ _ _ _ _ _ _ _ _ _ a b) : category_scope.
  33 Coercion eob_eob : ECategory >-> Sortclass.
  34
  35 Lemma ecomp_is_functorial `{ec:ECategory}{a b c}{x}(f:EI~~{V}~~>(a~~>b))(g:EI~~{V}~~>(b~~>c)) :
  36    ((x ~~> a) ⋊-) \ (iso_backward (pmon_cancelr EI) >>> ((- ⋉EI) \ f >>> (((a ~~> b) ⋊-) \ g >>> ecomp))) >>> ecomp ~~
  37    ((x ~~> a) ⋊-) \ f >>> (ecomp >>> (#(pmon_cancelr (x ~~> b)) ⁻¹ >>> (((x ~~> b) ⋊-) \ g >>> ecomp))).
  38
  39    set (@fmor_preserves_comp) as fmor_preserves_comp'.
  40
  41    (* knock off the leading (x ~~> a) ⋊ f *)
  42    repeat setoid_rewrite <- associativity.
  43    set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) f) as qq.
  44    apply iso_shift_right' in qq.
  45    setoid_rewrite <- associativity in qq.
  46    apply symmetry in qq.
  47    apply iso_shift_left' in qq.
  48    apply symmetry in qq.
  49    simpl in qq.
  50    setoid_rewrite <- qq.
  51    clear qq.
  52    repeat setoid_rewrite associativity.
  53    repeat setoid_rewrite <- fmor_preserves_comp'.
  54    repeat setoid_rewrite associativity.
  55    apply comp_respects; try reflexivity.
  56
  57    (* rewrite using the lemma *)
  58    assert (forall {a b c x}(g:EI~~{V}~~>(b ~~> c)),
  59     ((bin_second(BinoidalCat:=bc) (x ~~> a)) \ ((bin_second(BinoidalCat:=bc) (a ~~> b)) \ g))
  60     ~~
  61     (#(pmon_assoc (x ~~> a) _ _)⁻¹ >>>
  62      (bin_second(BinoidalCat:=bc) ((x ~~> a) ⊗ (a ~~> b))) \ g >>> #(pmon_assoc (x ~~> a) _ _))).
  63     symmetry.
  64
  65     setoid_rewrite associativity.
  66     symmetry.
  67     apply iso_shift_right'.
  68     setoid_rewrite <- pmon_coherent_l.
  69     set (ni_commutes (pmon_assoc_ll (x0~~>a0) (a0~~>b0))) as qq.
  70     simpl in *.
  71     apply (qq _ _ g0).
  72    setoid_rewrite H.
  73    clear H.
  74
  75    (* rewrite using eassociativity *)
  76    repeat setoid_rewrite associativity.
  77    set (@eassociativity _ _ _ _ _ _ _ _ _ ec x a) as qq.
  78    setoid_rewrite <- qq.
  79    clear qq.
  80    unfold e_v.
  81
  82    (* knock off the trailing ecomp *)
  83    repeat setoid_rewrite <- associativity.
  84    apply comp_respects; try reflexivity.
  85
  86    (* cancel out the adjacent assoc/cossa pair *)
  87    repeat setoid_rewrite associativity.
  88    setoid_rewrite juggle2.
  89    etransitivity.
  90    apply comp_respects; [ idtac |
  91    repeat setoid_rewrite <- associativity;
  92    etransitivity; [ idtac | apply left_identity ];
  93    apply comp_respects; [ idtac | reflexivity ];
  94    apply iso_comp1 ].
  95    apply reflexivity.
  96
  97    (* now swap the order of ecomp⋉(b ~~> c) and ((x ~~> a) ⊗ (a ~~> b))⋊g *)
  98    repeat setoid_rewrite associativity.
  99    set (@centralmor_first) as se.
 100    setoid_rewrite <- se.
 101    clear se.
 102
 103    (* and knock the trailing (x ~~> b)⋊ g off *)
 104    repeat setoid_rewrite <- associativity.
 105    apply comp_respects; try reflexivity.
 106
 107    (* push the ecomp forward past the rlecnac *)
 108    set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (@ecomp _ _ _ _ _ _ _ _ _ ec x a b)) as qq.
 109    symmetry in qq.
 110    apply iso_shift_left' in qq.
 111    setoid_rewrite associativity in qq.
 112    symmetry in qq.
 113    apply iso_shift_right' in qq.
 114    simpl in qq.
 115    setoid_rewrite qq.
 116    clear qq.
 117
 118    (* and knock off the trailing ecomp *)
 119    apply comp_respects; try reflexivity.
 120
 121    setoid_replace (iso_backward ((pmon_cancelr) ((x ~~> a) ⊗ (a ~~> b)))) with
 122      (iso_backward ((pmon_cancelr) ((x ~~> a) ⊗ (a ~~> b))) >>> id _).
 123    simpl.
 124    set (@iso_shift_right') as ibs.
 125    simpl in ibs.
 126    apply ibs.
 127    clear ibs.
 128
 129    set (MacLane_ex_VII_1_1 (a~~>b) (x~~>a)) as q.
 130    simpl in q.
 131    setoid_rewrite <- q.
 132    clear q.
 133    setoid_rewrite juggle3.
 134    set (fmor_preserves_comp ((x ~~> a) ⋊-)) as q.
 135    simpl in q.
 136    setoid_rewrite q.
 137    clear q.
 138    setoid_rewrite iso_comp1.
 139    setoid_rewrite fmor_preserves_id.
 140    setoid_rewrite right_identity.
 141    apply iso_comp1.
 142
 143    (* leftovers *)
 144    symmetry.
 145    apply right_identity.
 146    apply ecomp_central.
 147    Qed.
 148
 149 Lemma underlying_associativity `{ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)} :
 150    forall {a b : Eob} (f : EI ~~{ V }~~> a ~~> b) {c : Eob}
 151    (g : EI ~~{ V }~~> b ~~> c) {d : Eob} (h : EI ~~{ V }~~> c ~~> d),
 152    ((((#(pmon_cancelr EI) ⁻¹ >>> (f ⋉ EI >>> (a ~~> b) ⋊ g)) >>> ecomp) ⋉ EI >>> (a ~~> c) ⋊ h)) >>> ecomp ~~
 153    ((f ⋉ EI >>> (a ~~> b) ⋊ ((#(pmon_cancelr EI) ⁻¹ >>> (g ⋉ EI >>> (b ~~> c) ⋊ h)) >>> ecomp))) >>> ecomp.
 154
 155   intros; symmetry; etransitivity;
 156      [ setoid_rewrite associativity; apply comp_respects;
 157         [ apply reflexivity | repeat setoid_rewrite associativity; apply (ecomp_is_functorial(x:=a) g h) ] | idtac ].
 158
 159   repeat setoid_rewrite <- fmor_preserves_comp.
 160     repeat setoid_rewrite <- associativity.
 161     apply comp_respects; try reflexivity.
 162     apply comp_respects; try reflexivity.
 163
 164   set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) f) as qq.
 165     apply iso_shift_right' in qq.
 166     symmetry in qq.
 167     setoid_rewrite <- associativity in qq.
 168     apply iso_shift_left' in qq.
 169     apply (fmor_respects (bin_first EI)) in qq.
 170     setoid_rewrite <- fmor_preserves_comp in qq.
 171     setoid_rewrite qq.
 172     clear qq.
 173
 174   repeat setoid_rewrite <- fmor_preserves_comp.
 175     repeat setoid_rewrite associativity.
 176     apply comp_respects; try reflexivity.
 177
 178   repeat setoid_rewrite associativity.
 179   set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (@ecomp _ _ _ _ _ _ _ _ _ ec a b c)) as qq.
 180     apply iso_shift_right' in qq.
 181     symmetry in qq.
 182     setoid_rewrite <- associativity in qq.
 183     apply iso_shift_left' in qq.
 184     symmetry in qq.
 185     simpl in qq.
 186     setoid_rewrite qq.
 187     clear qq.
 188
 189   repeat setoid_rewrite <- associativity.
 190     apply comp_respects; try reflexivity.
 191
 192   idtac.
 193     set (iso_shift_left'
 194          (iso_backward (pmon_cancelr (a ~~> b)) ⋉ EI >>> ((a ~~> b) ⋊ g) ⋉ EI) ((a ~~> b) ⋊ g)
 195          ((pmon_cancelr ((a ~~> b) ⊗ (b ~~> c))))) as xx.
 196     symmetry.
 197     etransitivity; [ apply xx | apply comp_respects; try reflexivity ].
 198     clear xx.
 199
 200   setoid_rewrite (fmor_preserves_comp (bin_first EI)).
 201     set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) ((iso_backward (pmon_cancelr (a ~~> b)) >>> (a ~~> b) ⋊ g))) as qq.
 202     simpl in qq.
 203     setoid_rewrite <- qq.
 204     clear qq.
 205
 206   setoid_rewrite <- associativity.
 207     setoid_rewrite iso_comp1.
 208     apply left_identity.
 209
 210   Qed.
 211
 212 Instance Underlying `(ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)) : Category Eob (fun a b => EI~>(a~~>b)) :=
 213 { id    := fun a                                  => eid a
 214 ; comp  := fun a b c g f                          => #(pmon_cancelr _)⁻¹ >>> (g ⋉ _ >>> _ ⋊ f) >>> ecomp
 215 ; eqv   := fun a b (f:EI~>(a~~>b))(g:EI~>(a~~>b)) => f ~~ g
 216 }.
 217   abstract (intros; apply Build_Equivalence;
 218     [ unfold Reflexive
 219     | unfold Symmetric
 220     | unfold Transitive]; intros; simpl; auto).
 221   abstract (intros; unfold Proper; unfold respectful; intros; simpl;
 222   repeat apply comp_respects; try apply reflexivity;
 223     [ apply (fmor_respects (bin_first EI)) | idtac ]; auto;
 224     apply (fmor_respects (bin_second (a~~>b))); auto).
 225   abstract (intros;
 226     set (fun c d => centralmor_first(c:=c)(d:=d)(CentralMorphism:=(eid_central a))) as q;
 227     setoid_rewrite q;
 228     repeat setoid_rewrite associativity;
 229     setoid_rewrite eleft_identity;
 230     setoid_rewrite <- (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn));
 231     setoid_rewrite <- associativity;
 232     set (coincide pmon_triangle) as qq;
 233     setoid_rewrite qq;
 234     simpl;
 235     setoid_rewrite iso_comp2;
 236     apply left_identity).
 237   abstract (intros;
 238     repeat setoid_rewrite associativity;
 239     setoid_rewrite eright_identity;
 240     setoid_rewrite <- (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn));
 241     setoid_rewrite <- associativity;
 242     simpl;
 243     setoid_rewrite iso_comp2;
 244     apply left_identity).
 245   abstract (intros;
 246     repeat setoid_rewrite associativity;
 247     apply comp_respects; try reflexivity;
 248     repeat setoid_rewrite <- associativity;
 249     apply underlying_associativity).
 250   Defined.
 251 Coercion Underlying : ECategory >-> Category.
 252
 253 Class EFunctor
 254   `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
 255    {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
 256    {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
 257    (EFobj : Eob1 -> Eob2)
 258 :=
 259 { efunc_fobj           := EFobj
 260 ; efunc                :  forall a b:Eob1, (a ~~> b) ~~{V}~~> ( (EFobj a) ~~> (EFobj b) )
 261 ; efunc_central        :  forall a b,      CentralMorphism (efunc a b)
 262 ; efunc_preserves_id   :  forall a,        eid a >>> efunc a a ~~ eid (EFobj a)
 263 ; efunc_preserves_comp :  forall a b c,    (efunc a b) ⋉ _ >>>  _ ⋊ (efunc b c) >>> ecomp ~~ ecomp >>> efunc a c
 264 }.
 265 Coercion efunc_fobj : EFunctor >-> Funclass.
 266 Implicit Arguments efunc [ Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 EFobj ].
 267
 268 Definition efunctor_id
 269   `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
 270    {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
 271    : EFunctor ec1 ec1 (fun x => x).
 272   refine {| efunc := fun a b => id (a ~~> b) |}.
 273   abstract (intros; apply Build_CentralMorphism; intros;
 274     setoid_rewrite fmor_preserves_id;
 275     setoid_rewrite right_identity;
 276     setoid_rewrite left_identity;
 277     reflexivity).
 278   abstract (intros; apply right_identity).
 279   abstract (intros;
 280     setoid_rewrite fmor_preserves_id;
 281     setoid_rewrite right_identity;
 282     setoid_rewrite left_identity;
 283     reflexivity).
 284   Defined.
 285
 286 Definition efunctor_comp
 287   `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
 288    {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
 289    {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
 290    {Eob3}{EHom3}(ec3:ECategory mn Eob3 EHom3)
 291    {Fobj}(F:EFunctor ec1 ec2 Fobj)
 292    {Gobj}(G:EFunctor ec2 ec3 Gobj)
 293    : EFunctor ec1 ec3 (Gobj ○ Fobj).
 294   refine {| efunc := fun a b => (efunc F a b) >>> (efunc G _ _) |}; intros; simpl.
 295   abstract (apply Build_CentralMorphism; intros;
 296     [ set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc1
 297     ; set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc1
 298     ; setoid_rewrite <- (fmor_preserves_comp (-⋉d))
 299     ; setoid_rewrite <- (fmor_preserves_comp (-⋉c))
 300     ; setoid_rewrite <- associativity
 301     ; setoid_rewrite <- fc1
 302     ; setoid_rewrite    associativity
 303     ; setoid_rewrite <- gc1
 304     ; reflexivity
 305     | set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc2
 306     ; set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc2
 307     ; setoid_rewrite <- (fmor_preserves_comp (d⋊-))
 308     ; setoid_rewrite <- (fmor_preserves_comp (c⋊-))
 309     ; setoid_rewrite <- associativity
 310     ; setoid_rewrite    fc2
 311     ; setoid_rewrite    associativity
 312     ; setoid_rewrite    gc2
 313     ; reflexivity ]).
 314   abstract (setoid_rewrite <- associativity;
 315     setoid_rewrite efunc_preserves_id;
 316     setoid_rewrite efunc_preserves_id;
 317     reflexivity).
 318   abstract (repeat setoid_rewrite associativity;
 319     set (fmor_preserves_comp (-⋉(b~~>c))) as q; setoid_rewrite <- q; clear q;
 320     repeat setoid_rewrite associativity;
 321     set (fmor_preserves_comp (((Gobj (Fobj a) ~~> Gobj (Fobj b))⋊-))) as q; setoid_rewrite <- q; clear q;
 322     set (fun d e => centralmor_second(c:=d)(d:=e)(CentralMorphism:=(efunc_central(EFunctor:=F) b c))) as qq;
 323     setoid_rewrite juggle2;
 324     setoid_rewrite juggle2;
 325     setoid_rewrite qq;
 326     clear qq;
 327     repeat setoid_rewrite associativity;
 328     set ((efunc_preserves_comp(EFunctor:=G)) (Fobj a) (Fobj b) (Fobj c)) as q;
 329     repeat setoid_rewrite associativity;
 330     repeat setoid_rewrite associativity in q;
 331     setoid_rewrite q;
 332     clear q;
 333     repeat setoid_rewrite <- associativity;
 334     apply comp_respects; try reflexivity;
 335     set ((efunc_preserves_comp(EFunctor:=F)) a b c) as q;
 336     apply q).
 337   Defined.
 338
 339 Instance UnderlyingFunctor `(EF:@EFunctor Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 Eobj)
 340   : Functor (Underlying ec1) (Underlying ec2) Eobj :=
 341   { fmor := fun a b (f:EI~~{V}~~>(a~~>b)) => f >>> (efunc _ a b) }.
 342   abstract (intros; simpl; apply comp_respects; try reflexivity; auto).
 343   abstract (intros; simpl; apply efunc_preserves_id).
 344   abstract (intros;
 345             simpl;
 346             repeat setoid_rewrite associativity;
 347             setoid_rewrite <- efunc_preserves_comp;
 348             repeat setoid_rewrite associativity;
 349               apply comp_respects; try reflexivity;
 350             set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_first EI)) as qq;
 351               setoid_rewrite <- qq;
 352               clear qq;
 353             repeat setoid_rewrite associativity;
 354               apply comp_respects; try reflexivity;
 355             repeat setoid_rewrite <- associativity;
 356               apply comp_respects; try reflexivity;
 357             set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_second (Eobj a ~~> Eobj b))) as qq;
 358               setoid_rewrite <- qq;
 359               repeat setoid_rewrite <- associativity;
 360               apply comp_respects; try reflexivity;
 361               clear qq;
 362             apply (centralmor_first(CentralMorphism:=(efunc_central a b)))).
 363   Defined.
 364   Coercion UnderlyingFunctor : EFunctor >-> Functor.
 365
 366 Class EBinoidalCat `(ec:ECategory)(bobj   :  ec -> ec -> ec) :=
 367 { ebc_first  :  forall a:ec, EFunctor ec ec (fun x => bobj x a)
 368 ; ebc_second :  forall a:ec, EFunctor ec ec (fun x => bobj a x)
 369 ; ebc_ec     := ec  (* this isn't a coercion - avoids duplicate paths *)
 370 ; ebc_bobj   := bobj
 371 }.
 372
 373 Instance EBinoidalCat_is_binoidal `(ebc:EBinoidalCat(ec:=ec)) : BinoidalCat (Underlying ec) ebc_bobj.
 374   apply Build_BinoidalCat.
 375   apply (fun a => UnderlyingFunctor (ebc_first a)).
 376   apply (fun a => UnderlyingFunctor (ebc_second a)).
 377   Defined.
 378
 379 Coercion EBinoidalCat_is_binoidal : EBinoidalCat >-> BinoidalCat.
 380
 381 (* Enriched Fibrations *)
 382 Section EFibration.
 383
 384   Context `{E:ECategory}.
 385   Context  {Eob2}{Ehom2}{B:@ECategory Ob Hom V bin_obj' mn EI mn Eob2 Ehom2}.
 386   Context  {efobj}(F:EFunctor E B efobj).
 387
 388   (*
 389    * A morphism is prone if its image factors through the image of
 390    * another morphism with the same codomain just in case the factor
 391    * is the image of a unique morphism.  One might say that it
 392    * "uniquely reflects factoring through morphisms with the same
 393    * codomain".
 394    *)
 395   Definition Prone {e e'}(φ:EI~~{V}~~>(e'~~>e)) :=
 396   forall e'' (ψ:EI~~{V}~~>(e''~~>e)) (g:(efobj e'')~~{B}~~>(efobj e')),
 397        (comp(Category:=B) _ _ _ g (φ >>> (efunc F _ _))) ~~
 398        ψ >>> (efunc F _ _)
 399    ->  { χ:e''~~{E}~~>e' & ψ ~~ χ >>> φ & g ~~ comp(Category:=V) _ _ _ χ (efunc F e'' e') }.
 400        (* FIXME: χ must also be unique *)
 401
 402   (* a functor is a Street Fibration if morphisms with codomain in its image are, up to iso, the images of prone morphisms *)
 403
 404   (* Street was the first to define non-evil fibrations using isomorphisms (for cleavage_pf below) rather than equality *)
 405   Structure StreetCleavage (e:E)(b:B)(f:b~~{B}~~>(efobj e)) :=
 406   { cleavage_e'   : E
 407   ; cleavage_pf   : (efobj cleavage_e') ≅ b
 408   ; cleavage_phi  : cleavage_e' ~~{E}~~> e
 409   ; cleavage_cart : Prone cleavage_phi
 410   ; cleavage_eqv  : #cleavage_pf >>> f  ~~ comp(Category:=V) _ _ _ cleavage_phi (efunc F _ _)
 411   }.
 412
 413   (* if V, the category enriching E and B is V-enriched, we get a functor Bop->Vint *)
 414
 415   (* Every equivalence of categories is a Street fibration *)
 416
 417   (* this is actually a "Street Fibration", the non-evil version of a Grothendieck Fibration *)
 418   Definition EFibration := forall e b f, exists cl:StreetCleavage e b f, True.
 419
 420   Definition ClovenEFibration := forall e b f, StreetCleavage e b f.
 421
 422   (*
 423    * Now, a language has polymorphic types iff its category of
 424    * judgments contains a second enriched category, the category of
 425    * Kinds, and the category of types is fibered over the category of
 426    * Kinds, and the weakening functor-of-fibers has a right adjoint.
 427    *
 428    * http://ncatlab.org/nlab/show/Grothendieck+fibration
 429    *
 430    * I suppose we'll need to also ask that the R-functors takes
 431    * Prone morphisms to Prone morphisms.
 432    *)
 433 End EFibration.
 434