Library exp_functor

Require Import List.

Require Import basics.
Require Import categories.
Require Import preord.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import plotkin.
Require Import profinite.
Require Import embed.
Require Import joinable.
Require Import directed.
Require Import cont_functors.
Require Import bilimit.

Embedding functor for exponentials.

Here we define the function space functor in the category of embeddings and prove that is is continuous.

Section map_rel.
  Context {A B C D : preord}.

  Variable f:A -> B.
  Variable g:C -> D.

  Fixpoint map_rel (G:finset (A×C)%cat_ob) : finset (B×D)%cat_ob :=
    match G with
    | nil => nil
    | (a,c)::G' => (f a, g c)::map_rel G'

  Lemma map_rel_inh : forall hf G,
    inh hf G -> inh hf (map_rel G).

  Lemma unmap_rel : forall b d G,
    (b,d) map_rel G ->
    exists a c, (a,c) G /\ f a b /\ g c d.

  Lemma unmap_rel_sub : forall G X,
    G map_rel X ->
    exists G', G' X /\ G map_rel G'.
End map_rel.

Section exp_functor.
  Variable hf:bool.
  Variables A B C D:ob (EMBED hf).

  Variable f:A B.
  Variable g:C D.

  Lemma map_rel_in : forall G a b,
    (a,b) G -> (f a, g b) map_rel f g G.

  Lemma is_joinable_unmap_rel X :
    is_joinable_relation hf (map_rel f g X) ->
    is_joinable_relation hf X.

  Lemma is_joinable_map_rel X :
    is_joinable_relation hf X ->
    is_joinable_relation hf (map_rel f g X).

  Definition exp_fmap_func (X:joinable_relation hf A C) : joinable_relation hf B D :=
    match X with
    | exist G H => exist (is_joinable_relation hf)
                         (map_rel f g G)
                         (is_joinable_map_rel G H)

  Program Definition unimage_jrel (y:finset (B×D)%cat_ob) :=
      (fun ac =>
        exists b d, (b,d) y /\ b f (fst ac) /\ g (snd ac) d)
      (eprod (eff_enum A (PLT.effective A)) (eff_enum C (PLT.effective C))).

  Lemma unimage_jrel_order (y:joinable_relation hf B D) :
    ((forall (x x' : A) (y0 y' : C),
     x x' ->
     y' y0 ->
     (x, y0) unimage_jrel (proj1_sig y) ->
     (x', y') unimage_jrel (proj1_sig y))).

  Lemma unimage_jrel_directed (y:joinable_relation hf B D) :
    (forall a : A,
     directed hf
       (erel_image A C {| orddec := eff_ord_dec A (PLT.effective A) |}
          (unimage_jrel (proj1_sig y)) a)).

  Program Definition exp_fmap : PLT.exp A C PLT.exp B D :=
    Embedding hf (PLT.exp A C) (PLT.exp B D) exp_fmap_func _ _ _ _.
End exp_functor.

Lemma exp_fmap_ident hf (A B:ob (EMBED hf)) (f:AA) (g:BB) :
  f id -> g id ->
  exp_fmap hf A A B B f g id.

Lemma exp_fmap_compose hf (A B C D E F:ob (EMBED hf))
  (f1:B E) (f2:D F)
  (g1:A B) (g2:C D)
  (h1:A E) (h2:C F) :
  f1 g1 h1 ->
  f2 g2 h2 ->
  exp_fmap hf B E D F f1 f2 exp_fmap hf A B C D g1 g2
    exp_fmap hf A E C F h1 h2.

Lemma exp_fmap_respects hf (A B C D:ob (EMBED hf))
   (f f':A B)
   (g g':C D) :
   f f' -> g g' ->
   exp_fmap hf A B C D f g exp_fmap hf A B C D f' g'.

Program Definition expF hf : functor (PROD (EMBED hf) (EMBED hf)) (EMBED hf) :=
    Functor (PROD (EMBED hf) (EMBED hf)) (EMBED hf)
      (fun X => (@PLT.exp hf
                   (@obl (EMBED hf) (EMBED hf) X)
                   (@obr (EMBED hf) (EMBED hf) X)))
      (fun (X Y:ob (PROD (EMBED hf) (EMBED hf))) fg =>
        exp_fmap hf (@obl (EMBED hf) (EMBED hf) X)
                    (@obl (EMBED hf) (EMBED hf) Y)
                    (@obr (EMBED hf) (EMBED hf) X)
                    (@obr (EMBED hf) (EMBED hf) Y)
                    (@homl (EMBED hf) (EMBED hf) X Y fg)
                    (@homr (EMBED hf) (EMBED hf) X Y fg))
      _ _ _.

Section expF_decompose.
  Variable hf:bool.
  Variable I:directed_preord.
  Variables DS1 DS2 : directed_system I (EMBED hf).
  Variable CC1 : cocone DS1.
  Variable CC2 : cocone DS2.

  Hypothesis decompose1 : forall x:cocone_point CC1,
    { i:I & { a:ds_F DS1 i | cocone_spoke CC1 i a x }}.
  Hypothesis decompose2 : forall x:cocone_point CC2,
    { i:I & { a:ds_F DS2 i | cocone_spoke CC2 i a x }}.

  Lemma finrel_decompose
    (X:finset (PLT.ord (cocone_point CC1) × PLT.ord (cocone_point CC2))%cat_ob) :
    forall (Hinh : inh hf X),
    { k:I & { Y:finset (PLT.ord (ds_F DS1 k) × PLT.ord (ds_F DS2 k))%cat_ob |
       X map_rel (cocone_spoke CC1 k) (cocone_spoke CC2 k) Y }}.
End expF_decompose.

Lemma expF_continuous hf : continuous_functor (expF hf).