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._≀_) (lower x) (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-≀ Ξ±