Require Import coqrel.LogicalRelations.
Require Import structures.Lattice.
Require Import structures.Completion.
Require Import lattices.Downset.
Require Import lattices.Upset.

Module CDL <: LatticeCategory.
  Section DEF.
    Context {L M : cdlattice} (f : L → M).

    Class Morphism := mor : Sup.Morphism f ∧ Inf.Morphism f.
    Global Instance cmor_sup : Morphism → Sup.Morphism f := @proj1 _ _.
    Global Instance cmor_inf : Morphism → Inf.Morphism f := @proj2 _ _.

    Instance mor_ref :
      Morphism → PosetMorphism f.
  End DEF.

  Lemma id_mor (L : cdlattice) :
    Morphism (fun x:L ⇒ x).

  Lemma compose_mor {A B C : cdlattice} (g : B → C) (f : A → B) :
    Morphism f →
    Morphism g →
    Morphism (fun a ⇒ g (f a)).

  Existing Instance mor_ref.

End CDL.

Module Type JoinMeetDense (LC : LatticeCompletion CDL).

  Axiom join_meet_dense :
    ∀ {C : poset} (x : LC.F C),
      ∃ I J (c : ∀ i:I, J i → C), x = sup i, inf j, LC.emb (c i j).

  Axiom meet_join_dense :
    ∀ {C : poset} (x : LC.F C),
      ∃ I J (c : ∀ i:I, J i → C), x = inf i, sup j, LC.emb (c i j).

End JoinMeetDense.

Module Type FCDSpec := LatticeCompletion CDL <+ JoinMeetDense.

Module FCD : FCDSpec.

  Definition F (C : poset) := upset (downset C).

  Section DEF.
    Context {C : poset}.

    Definition emb (c : C) := up (down c).

    Lemma emb_mor c1 c2 :
      emb c1 [= emb c2 ↔ c1 [= c2.

    Context {L : cdlattice}.

    Definition ext (f : C → L) (x : F C) :=
      Upset.ext (Downset.ext f) x.

    Context {f : C → L} `{Hf : !PosetMorphism f}.

    Instance ext_mor :
      CDL.Morphism (ext f).

    Lemma ext_ana :
      (∀ x, ext f (emb x) = f x).

    Lemma ext_unique (g : F C → L) `{!CDL.Morphism g} :
      (∀ x, g (emb x) = f x) → ∀ x, g x = ext f x.

  End DEF.

  Include (LatticeCompletionDefs CDL).

  Lemma meet_join_dense {C : poset} (x : F C) :
    ∃ I J c, x = inf i : I, sup j : J i, emb (c i j).

  Lemma join_meet_dense {C : poset} (x : F C) :
    ∃ I J c, x = sup i : I, inf j : J i, emb (c i j).

End FCD.