open import 1Lab.Prelude

open import Order.Base

module Order.Instances.Lift where


# Lifting posets across universesπ

Suppose you have a poset whose elements are in and relation in but you really need it to have elements or relationships in some larger universe and homs in Fortunately you can uniformly lift the poset to this bigger universe.

Liftα΅ : β {o r} oβ² rβ² β Poset o r β Poset (o β oβ²) (r β rβ²)
Liftα΅ o' r' X .Poset.Ob      = Lift o' β X β
Liftα΅ o' r' X .Poset._β€_ x y = Lift r' $(X .Poset._β€_) (Lift.lower x) (Lift.lower y) Liftα΅ o' r' X .Poset.β€-thin = Lift-is-hlevel 1$ X .Poset.β€-thin
Liftα΅ o' r' X .Poset.β€-refl  = lift $X .Poset.β€-refl Liftα΅ o' r' X .Poset.β€-trans (lift p) (lift q) = lift (X .Poset.β€-trans p q) Liftα΅ o' r' X .Poset.β€-antisym (lift p) (lift q) = ap lift (X .Poset.β€-antisym p q) Lift-monotone-l : β {so sr} bo br {o r} {X : Poset so sr} {Y : Poset o r} β Monotone X Y β Monotone (Liftα΅ bo br X) Y Lift-monotone-l bo br G = F where open Monotone F : Monotone _ _ F .hom (lift x) = G .hom x F .pres-β€ (lift Ξ±) = G .pres-β€ Ξ± Lift-monotone-r : β {so sr} bo br {o r} {X : Poset so sr} {Y : Poset o r} β Monotone X Y β Monotone X (Liftα΅ bo br Y) Lift-monotone-r bo br G = F where open Monotone F : Monotone _ _ F .hom x = lift$ G .hom x
F .pres-β€ Ξ± = lift \$ G .pres-β€ Ξ±