Library cont_functors

Require Import basics.
Require Import categories.
Require Import preord.
Require Import directed.

Directed colimits and continuous functors.

Record directed_system (I:directed_preord) (C:category) :=
  { ds_F : I -> ob C
  ; ds_hom : forall i j:I, i j -> ds_F i ds_F j
  ; ds_ident : forall i (Hii:ii), ds_hom i i Hii id
  ; ds_compose : forall i j k (Hij:ij) (Hjk:jk) (Hik:ik),
                       ds_hom j k Hjk ds_hom i j Hij ds_hom i k Hik

Record cocone (I:directed_preord) C (DS:directed_system I C) :=
  { cocone_point :> ob C
  ; cocone_spoke : forall i, ds_F DS i cocone_point
  ; cocone_commute : forall i j (Hij:ij),
       cocone_spoke i cocone_spoke j ds_hom DS i j Hij

Record directed_colimit (I:directed_preord) C (DS:directed_system I C)
  (XC:cocone DS) :=
  { colim_univ : forall (YC:cocone DS), XC YC
  ; colim_commute : forall (YC:cocone DS) i,
       cocone_spoke YC i colim_univ YC cocone_spoke XC i
  ; colim_uniq : forall (YC:cocone DS) (f:XC YC),
       (forall i, cocone_spoke YC i f cocone_spoke XC i) ->
       f colim_univ YC

Program Definition dir_sys_app I C D
  (DS:directed_system I C) (F:functor C D)
  : directed_system I D:=

  DirSys I D
    (fun i => F (ds_F DS i))
    (fun i j Hij => F·(ds_hom DS i j Hij))
    _ _.

Program Definition cocone_app I C D (DS:directed_system I C)
  (CC:cocone DS) (F:functor C D)
  : cocone (dir_sys_app DS F) :=

  Cocone (dir_sys_app DS F) (F CC) (fun i => F·cocone_spoke CC i) _.

Definition continuous_functor (C D:category) (F:functor C D) :=
  forall I (DS:directed_system I C) (CC:cocone DS),
    directed_colimit DS CC ->
    directed_colimit (dir_sys_app DS F) (cocone_app CC F).

Fixpoints of continuous functors.

We can construct fixpoints of continuous endofunctors in any category that has an initial object and colimits of directed systems.
This is essentially the categorical analogue of Kleene's fixpoint theorem for posets.

Require Import Arith.
Section fixpoint.
  Variable C:initialized.
  Variable F:functor C C.

  Variable colimit_cocone :
    forall (I:directed_preord) (DS:directed_system I C), cocone DS.

  Variable has_colimits :
    forall (I:directed_preord) (DS:directed_system I C),
            directed_colimit DS (colimit_cocone I DS).

Iterated application of the functor F; the initial object provides the base case of the recursion.
  Fixpoint iterF (x:nat) : ob C :=
    match x with
    | O => ¡
    | S x' => F (iterF x')

  Lemma HSle0 j (Hij: S j <= O) : False.

Iterated action of the functor F on homs. The base case is provided by the universal hom associated to ¡.
  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 => initiate
    | 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.

The Kleene chain is a directed system.
  Program Definition kleene_chain : directed_system nat_dirord C :=
    DirSys nat_dirord C iterF iter_hom _ _.

The fixpoint we desire is the point of the colimiting cocone corresponding to the Kleene chain.
It is mildly interesting to note that we can construct the fixpoint object without the continuity assumption.
However, if we suppose F is a continuous functor, we can demonstrate that fixpoint forms an initial algebra and thus actually is the least fixpoint of F.
  Hypothesis Fcontinuous : continuous_functor F.

Because F is continuous, the additional application of F to the fixpoint colimiting cocone is a colimiting cocone for the n+1 Kleene chain.
  Let BL := Fcontinuous
               nat_dirord kleene_chain
               (colimit_cocone nat_dirord kleene_chain)
               (has_colimits nat_dirord kleene_chain).

  Program Definition cocone_plus1 : cocone (dir_sys_app kleene_chain F)
    := Cocone (dir_sys_app kleene_chain F) fixpoint
      (fun i => cocone_spoke (colimit_cocone nat_dirord kleene_chain) (S i)) _.

The algebra associated with the fixpoint.
  Definition fixpoint_alg : alg C F
    := @Alg C F fixpoint (colim_univ BL cocone_plus1).

Next we define the catamorphism by iterating the action of a given algebra.
  Section cata.
    Variable AG : alg C F.

    Fixpoint cata_hom' (i:nat) : iterF i AG :=
      match i as i' return iterF i' AG with
      | O => initiate
      | S i' => Alg.iota AG F·(cata_hom' i')

    Lemma cata_hom_iter_hom : forall (i j:nat_ord) (Hij:ij),
      cata_hom' i cata_hom' j (iter_hom i j Hij).

    Program Definition AG_cocone : cocone kleene_chain :=
      Cocone _ _ cata_hom' cata_hom_iter_hom.

    Program Definition AG_cocone' :
      cocone (dir_sys_app kleene_chain F) :=
        Cocone _ _ (fun i => cata_hom' (S i)) _.

    Definition cata_hom : fixpoint AG :=
      colim_univ (has_colimits nat_dirord kleene_chain) AG_cocone.

    Program Definition cata_alg_hom : Alg.alg_hom fixpoint_alg AG :=
      Alg.Alg_hom cata_hom _.
  End cata.

Now we show that the catamorphims is universal and construct the initial algebra.
With the initial algebra in hand, we immediately get an isomorphism via standard facts about initial algebras.
  Definition fixpoint_iso :
    F fixpoint fixpoint :=

    Isomorphism C (F fixpoint) fixpoint
      (colim_univ BL cocone_plus1)
      (Alg.out _ F fixpoint_initial)
      (Alg.out_in _ F fixpoint_initial)
      (Alg.in_out _ F fixpoint_initial).

End fixpoint.

Standard continuous functors.

The identity and constant functors are continuous, as is the composition of two continuous functors.
Pairing and projection functors are also continuous.

Lemma identF_continuous (C:category) : continuous_functor id(C).

Lemma fconst_continuous (C D:category) (X:ob D) : continuous_functor (fconst C D X).

Lemma composeF_continuous (C D E:category)
  (F:functor D E) (G:functor C D) :
  continuous_functor F ->
  continuous_functor G ->
  continuous_functor (F G).

Section pairF_continuous.
  Variables C D E:category.
  Variable F:functor C D.
  Variable G:functor C E.

  Section cocones.
    Variable I:directed_preord.
    Variable DS:directed_system I C.

    Program Definition cocone_fstF (YC:cocone (dir_sys_app DS (pairF F G)))
      : cocone (dir_sys_app DS F)
      := Cocone (dir_sys_app DS F)
                (obl (cocone_point YC))
                (fun i => homl (cocone_spoke YC i))

    Program Definition cocone_sndF (YC:cocone (dir_sys_app DS (pairF F G)))
      : cocone (dir_sys_app DS G)
      := Cocone (dir_sys_app DS G)
                (obr (cocone_point YC))
                (fun i => homr (cocone_spoke YC i))
  End cocones.

  Hypothesis HcontF : continuous_functor F.
  Hypothesis HcontG : continuous_functor G.

  Lemma pairF_continuous : continuous_functor (pairF F G).
End pairF_continuous.

Section fstF_continuous.
  Variables C D:category.
  Variable I:directed_preord.
  Variable DS:directed_system I (PROD C D).
  Variable CC:cocone DS.
  Variable Hcolim : directed_colimit DS CC.

  Program Definition fstF_cocone
    (CC1 : cocone (dir_sys_app DS (fstF C D))) : cocone DS
    := Cocone DS (PROD.Ob C D (cocone_point CC1)
                                          (obr (cocone_point CC)))
                 (fun i => PROD.Hom C D _ _
                            (cocone_spoke CC1 i)
                            (homr (cocone_spoke CC i) :
                                 obr (ds_F DS i) obr (cocone_point CC)))


  Definition fstF_univ (YC : cocone (dir_sys_app DS (fstF C D))) :
    cocone_app CC (fstF C D) YC :=
    homl (colim_univ Hcolim (fstF_cocone YC)).

  Lemma fstF_continuous' :
    directed_colimit (dir_sys_app DS (fstF C D)) (cocone_app CC (fstF C D)).
End fstF_continuous.

Lemma fstF_continuous C D :
  continuous_functor (fstF C D).

Section sndF_continuous.
  Variables C D:category.
  Variable I:directed_preord.
  Variable DS:directed_system I (PROD C D).
  Variable CC:cocone DS.
  Variable Hcolim : directed_colimit DS CC.

  Program Definition sndF_cocone
    (CC1 : cocone (dir_sys_app DS (sndF C D))) : cocone DS
    := Cocone DS (PROD.Ob C D (obl (cocone_point CC))
                              (cocone_point CC1))
                 (fun i => PROD.Hom C D _ _
                            (homl (cocone_spoke CC i) :
                                 obl (ds_F DS i) obl (cocone_point CC))
                            (cocone_spoke CC1 i))

  Definition sndF_univ (YC : cocone (dir_sys_app DS (sndF C D))) :
    cocone_app CC (sndF C D) YC :=
    homr (colim_univ Hcolim (sndF_cocone YC)).

  Lemma sndF_continuous' :
    directed_colimit (dir_sys_app DS (sndF C D)) (cocone_app CC (sndF C D)).
End sndF_continuous.

Lemma sndF_continuous C D : continuous_functor (sndF C D).