Library sumprod_functor


Require Import List.
Require Import NArith.

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.

Sum and product functors

Here we define the functors for sum and produce in the category of embeddings and show that they are continuous.

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

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

  Program Definition prod_fmap : PLT.prod A C PLT.prod B D
    := Embedding hf (PLT.prod A C) (PLT.prod B D) (fun x => (f (fst x), g (snd x)))
         _ _ _ _.

End prod_functor.

Program Definition prodF hf
  : functor (PROD (EMBED hf) (EMBED hf)) (EMBED hf) :=

  Functor (PROD (EMBED hf) (EMBED hf)) (EMBED hf)
     (fun (AB:ob (PROD (EMBED hf) (EMBED hf))) =>
         PLT.prod (@obl (EMBED hf) (EMBED hf) AB)
                  (@obr (EMBED hf) (EMBED hf) AB))
     (fun (AB CD:ob (PROD (EMBED hf) (EMBED hf))) (f:AB CD) =>
       prod_fmap hf _ _ _ _
         (@homl (EMBED hf) (EMBED hf) AB CD f)
         (@homr (EMBED hf) (EMBED hf) AB CD f))
     _ _ _.

Lemma prodF_continuous hf : continuous_functor (prodF hf).

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

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

  Definition sum_fmap_func (x:A+C) : B+D :=
    match x with
    | inl a => inl (f a)
    | inr b => inr (g b)
    end.

  Program Definition sum_fmap : PLT.sum A C PLT.sum B D
    := Embedding hf (PLT.sum A C) (PLT.sum B D) sum_fmap_func _ _ _ _.
End sum_functor.

Program Definition sumF hf
  : functor (PROD (EMBED hf) (EMBED hf)) (EMBED hf) :=

  Functor (PROD (EMBED hf) (EMBED hf)) (EMBED hf)
     (fun (AB:ob (PROD (EMBED hf) (EMBED hf))) =>
         PLT.sum (@obl (EMBED hf) (EMBED hf) AB)
                 (@obr (EMBED hf) (EMBED hf) AB))
     (fun (AB CD:ob (PROD (EMBED hf) (EMBED hf))) (f:AB CD) =>
       sum_fmap hf _ _ _ _
         (@homl (EMBED hf) (EMBED hf) AB CD f)
         (@homr (EMBED hf) (EMBED hf) AB CD f))
     _ _ _.

Lemma sumF_continuous hf : continuous_functor (sumF hf).