Library cont_adj


Require Import Setoid.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import plotkin.
Require Import embed.
Require Import joinable.
Require Import approx_rels.
Require Import profinite.
Require Import profinite_adj.
Require Import cont_functors.

Continuous adjoint functors

Here we lift the lifting and forgetful adjoint functors into the category of embeddings and prove that they are continuous.

Definition forgetEMBED_map (A B:ob PLT) (f:A B) : forgetPLT_ob A forgetPLT_ob B :=
  Embedding true (forgetPLT_ob A) (forgetPLT_ob B)
    (@embed_map false A B f)
    (@embed_mono false A B f)
    (@embed_reflects false A B f)
    (fun _ => I)
    (@embed_directed2 false A B f).

Program Definition forgetEMBED : functor (EMBED false) (EMBED true) :=
  Functor (EMBED false) (EMBED true) forgetPLT_ob forgetEMBED_map _ _ _.
Solve Obligations of forgetEMBED using auto.

Program Definition liftEMBED_map (A B:ob PLT) (f:A B) : liftPPLT_ob A liftPPLT_ob B :=
  Embedding false (liftPPLT_ob A) (liftPPLT_ob B)
    (fun x => match x with None => None | Some a => Some (f a) end)
    _ _ _ _.

Program Definition liftEMBED : functor (EMBED true) (EMBED false) :=
  Functor (EMBED true) (EMBED false) liftPPLT_ob liftEMBED_map _ _ _.

Require Import bilimit.

Lemma forgetEMBED_continuous : continuous_functor forgetEMBED.

Lemma liftEMBED_continuous : continuous_functor liftEMBED.