Library lattices.Upset
Require Import FunctionalExtensionality.
Require Import coqrel.LogicalRelations.
Require Import structures.Lattice.
Require Import structures.Completion.
Require Import lattices.Downset.
Require Import coqrel.LogicalRelations.
Require Import structures.Lattice.
Require Import structures.Completion.
Require Import lattices.Downset.
Interface
Module Inf <: LatticeCategory.
Class Morphism {L M : cdlattice} (f : L → M) :=
mor : ∀ {I} (x : I → L), f (linf x) = inf i, f (x i).
Lemma mor_meet `{Morphism} x y :
f (x && y) = f x && f y.
Local Transparent meet.
Lemma mor_ref {L M : cdlattice} (f : L → M) :
Morphism f →
PosetMorphism f.
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)).
Hint Immediate mor_ref : typeclass_instances.
End Inf.
Opposite order
Program Definition opp_poset (C : poset) : poset :=
{|
poset_carrier := C;
ref x y := y [= x;
|}.
Program Definition opp_cdlat (L : cdlattice) : cdlattice :=
{|
cdl_poset := opp_poset L;
lsup I x := linf x;
linf I x := lsup x;
|}.
(*
Definition opp_map {A B} (f : A -> B) : opp A -> opp B :=
fun '(opp_in a) => opp_in (f a).
Instance opp_map_ref {A B} `{Poset A} `{Poset B} (f : A -> B) :
PosetMorphism f ->
PosetMorphism (opp_map f).
Proof.
intros Hf. split. intros x y Hxy. cbn in *. rauto.
Qed.
*)
Definition F (C : poset) := opp_cdlat (downset (opp_poset C)).
Section DEFS.
Context {C : poset}.
Definition emb (c : C) : F C :=
Downset.emb (c : opp_poset C).
Lemma emb_mor c1 c2 : emb c1 [= emb c2 ↔ c1 [= c2.
Context {L : cdlattice}.
Definition ext (f : C → L) (x : F C) : L :=
Downset.ext (f : opp_poset C → opp_cdlat L) (x : downset (opp_poset C)).
Context {f : C → L} `{Hf : !PosetMorphism f}.
Instance ext_mor :
Inf.Morphism (ext f).
Lemma ext_ana :
(∀ x, ext f (emb x) = f x).
Lemma ext_unique (g : F C → L) `{Hg : !Inf.Morphism g} :
(∀ x, g (emb x) = f x) → ∀ x, g x = ext f x.
End DEFS.
Include (LatticeCompletionDefs Inf).
End Upset.
Notation upset := Upset.F.
Notation up := Upset.emb.