Library bilimit

Require Import Setoid.
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 directed.
Require Import cont_functors.
Require Import cpo.

Bilimits and fixpoints of continuous functors.

Here we construct the colimit of directed systems. The carrier of the bilimit is the disjoint union of the directed system. The order on the bilimit elements holds if there exists some larger poset into which both elements can be embedded where the ordering holds.
Section bilimit.
  Variable hf:bool.
  Variable I:directed_preord.
  Variable DS:directed_system I (EMBED hf).

  Record limset :=
    { idx : I
    ; elem : ds_F DS idx

  Definition limset_order (x y:limset) :=
    exists k (Hxk : idx x k) (Hyk : idx y k),
      ds_hom DS (idx x) k Hxk (elem x)
       ds_hom DS (idx y) k Hyk (elem y).

This lemma shows that if two elements compare in any larger poset, the compare in every larger poset.
  Lemma limset_order_exists_forall x y :
    limset_order x y <->
    forall k (Hxk : idx x k) (Hyk : idx y k),
      ds_hom DS (idx x) k Hxk (elem x)
       ds_hom DS (idx y) k Hyk (elem y).

  Lemma limset_order_refl (x:limset) : limset_order x x.

  Lemma limset_order_trans (x y z:limset) :
    limset_order x y -> limset_order y z -> limset_order x z.

  Definition limord_mixin :=
    Preord.Mixin limset limset_order limset_order_refl limset_order_trans.

  Canonical Structure limord := Preord.Pack limset limord_mixin.

The order is decidable.
  Lemma limset_order_dec (x y:limset) :
    { limset_order x y } + { ~limset_order x y }.

Furthermore, all the elements can be enumerated.
  Definition limset_enum : eset limord :=
    fun n => let (p,q) := pairing.unpairing n in
         match eff_enum _ (dir_effective I) p with
         | Some i =>
              match eff_enum _ (PLT.effective (ds_F DS i)) q with
              | Some x => Some (LimSet i x)
              | None => None
         | None => None

Thus, the bilimit is an effective order.
Moreover, the bilimit has normal sets.
Altogether, this makes the bilimit a plotkin order.
Here we define the spokes of the colimit cocone.
  Program Definition limset_spoke (i:I) : hom (EMBED hf) (ds_F DS i) bilimit
    := Embedding hf (ds_F DS i : ob (EMBED hf)) bilimit
    (fun x => LimSet i x) _ _ _ _.

  Lemma limset_spoke_commute : forall i j (Hij:ij),
     limset_spoke i limset_spoke j ds_hom DS i j Hij.

  Definition bilimit_cocone : cocone DS :=
    Cocone DS bilimit limset_spoke limset_spoke_commute.

  Section bilimit_univ.
    Variable YC:cocone DS.

    Program Definition limord_univ : bilimit YC :=
      Embedding hf bilimit (YC : ob (EMBED hf))
        (fun x => let (i,x') := x in cocone_spoke YC i x')
        _ _ _ _.

    Lemma limord_univ_commute i :
      cocone_spoke YC i limord_univ limset_spoke i.

    Lemma limord_univ_uniq (f:bilimit YC) :
      (forall i, cocone_spoke YC i f limset_spoke i) ->
      f limord_univ.
  End bilimit_univ.

  Definition bilimit_construction : directed_colimit DS bilimit_cocone :=
    DirectedColimit DS bilimit_cocone

  Program Definition ep_set : dir_preord I (PLT.hom_ord hf bilimit bilimit) :=
    Preord.Hom _ _
        (fun i => embed (embed_ep_pair (limset_spoke i))
                  project (embed_ep_pair (limset_spoke i)))

  Program Definition Iset : Preord.carrier (cl_eset (directed_hf_cl hf) I)
    := exist _ (eff_enum I (dir_effective I)) _.

  Lemma bilimit_cpo_colimit : forall x y:bilimit,
    y x ->
    exists i a,
      y limset_spoke i a /\
      limset_spoke i a x.

  Lemma bilimit_cpo_colimit1 :
    id(bilimit) ∐(image ep_set Iset).

  Lemma bilimit_cpo_colimit2 :
    id(bilimit) ∐(image ep_set Iset).

End bilimit.

The following two constructions show that a cocone is a colimit in EMBED iff every element can be factored through a spoke of the cocone.
Passing thorough these constructions is generally the easiest way to demonstrate that an embedding functor is continuous.
Section colimit_decompose.
  Variable hf:bool.
  Variable I:directed_preord.
  Variable DS : directed_system I (EMBED hf).
  Variable CC : cocone DS.
  Variable Hcolimit : directed_colimit DS CC.

  Lemma colimit_decompose : forall x:cocone_point CC,
    { i:I & { a:ds_F DS i | cocone_spoke CC i a x }}.
End colimit_decompose.

Section colimit_decompose2.
  Variable hf:bool.
  Variable I:directed_preord.
  Variable DS : directed_system I (EMBED hf).
  Variable CC : cocone DS.
  Hypothesis decompose : forall x:cocone_point CC,
    { i:I & { a:ds_F DS i | cocone_spoke CC i a x }}.

  Definition decompose_univ_func (YC:cocone DS) (x:cocone_point CC) :=
    cocone_spoke YC
       (projT1 (decompose x))
       (projT1 (projT2 (decompose x))).

  Program Definition decompose_univ (YC:cocone DS) : CC YC :=
    Embedding hf (cocone_point CC: ob (EMBED hf))
                 (cocone_point YC : ob (EMBED hf))
                 (decompose_univ_func YC) _ _ _ _.

  Program Definition decompose_is_colimit : directed_colimit DS CC :=
    DirectedColimit DS CC decompose_univ _ _.
End colimit_decompose2.

With the bilimit in hand, we can construct the least fixpoint of continuous functors in the embeddings over the category of partial plotkin orders by appeal to the general fixpoint construction for continuous functors.
Section fixpoint.
  Variable F:functor (EMBED true) (EMBED true).
  Hypothesis Fcontinuous : continuous_functor F.

  Definition fixpoint : ob (EMBED true) :=
           (bilimit_cocone true).

  Definition fixpoint_initial : Alg.initial_alg (EMBED true) F :=
           (bilimit_cocone true)
           (bilimit_construction true)

  Definition fixpoint_iso : F fixpoint fixpoint :=
           (bilimit_cocone true)
           (bilimit_construction true)
End fixpoint.

Require Import Arith.

We can also build fixpoints in the category of total Plotkin orders by requiring a little more data. This proof is a modification of Theorem 79 from Carl Gunter's PhD thesis (CMU, 1985).
Section total_fixpoint.
  Variable F:functor (EMBED false) (EMBED false).
  Hypothesis Fcontinuous : continuous_functor F.

  Variable A:ob PLT.
  Variable h:A F A.

  Fixpoint iterF (x:nat) : ob PLT :=
    match x with
    | O => A
    | S x' => F (iterF x')

  Fixpoint injectA (j:nat) : A iterF j :=
    match j as j' return A iterF j' with
    | 0 => id
    | S n => F·(injectA n) h

  Fixpoint iter_hom (i:nat) : forall (j:nat) (Hij:i <= j), iterF i iterF j :=
    match i as i' return forall (j:nat) (Hij:i' <= j), iterF i' iterF j with
    | O => fun j Hij => injectA j
    | S i' => fun j =>
        match j as j' return forall (Hij:S i' <= j'), iterF (S i') iterF j' with
        | O => fun Hij => False_rect _ (HSle0 i' Hij)
        | S j' => fun Hij => F·(iter_hom i' j' (gt_S_le i' j' Hij))

  Lemma iter_hom_proof_irr i : forall j H1 H2,
    iter_hom i j H1 iter_hom i j H2.

  Program Definition kleene_chain_alt : directed_system nat_dirord (EMBED false) :=
    DirSys nat_dirord _ iterF iter_hom _ _.

  Definition fixpoint_alt : ob PLT := bilimit false nat_dirord kleene_chain_alt.

  Let BL := Fcontinuous
               nat_dirord kleene_chain_alt
               (bilimit_cocone false nat_dirord kleene_chain_alt)
               (bilimit_construction false nat_dirord kleene_chain_alt).

  Program Definition cocone_plus1 : cocone (dir_sys_app kleene_chain_alt F)
    := Cocone (dir_sys_app kleene_chain_alt F) fixpoint_alt
      (fun i => cocone_spoke (bilimit_cocone false nat_dirord kleene_chain_alt) (S i)) _.

  Program Definition cocone_minus1 : cocone kleene_chain_alt
    := Cocone kleene_chain_alt (F fixpoint_alt)
           (fun i =>
              F·(cocone_spoke (bilimit_cocone false nat_dirord kleene_chain_alt) i)
              iter_hom i (S i) (le_S i i (le_refl i)))

  Definition fixpoint_alt_in : F fixpoint_alt fixpoint_alt :=
    colim_univ BL cocone_plus1.
  Definition fixpoint_alt_out : fixpoint_alt F fixpoint_alt :=
    limord_univ false nat_dirord kleene_chain_alt cocone_minus1.

  Lemma fixpoint_alt_in_out : fixpoint_alt_in fixpoint_alt_out id.

  Lemma fixpoint_alt_out_in : fixpoint_alt_out fixpoint_alt_in id.

  Definition fixpoint_embed : A fixpoint_alt :=
    limset_spoke false nat_dirord kleene_chain_alt 0%nat.

  Definition fixpoint_alt_iso : F fixpoint_alt fixpoint_alt :=
    Isomorphism (EMBED false) (F fixpoint_alt) fixpoint_alt

End total_fixpoint.