module Order.Diagram.Lub.Subset where

# Joins of subsetsπ

Imagine you have a poset $A$ whose carrier has size $ΞΊ,$ which furthermore has least upper bounds for $ΞΊ-small$ families of elements. But imagine that you have a second universe $Ξ»,$ and you have a $Ξ»-small$ predicate $P:P_{Ξ»}(A).$ Normally, youβd be out of luck: there is no reason for $A$ to admit $(ΞΊβΞ»)-sized$ joins.

But since weβve assumed propositional
resizing, we can resize (pointwise)
$P$
to be valued in the universe
$ΞΊ;$
That way we can turn the total space
$β«P$
into a
$ΞΊ-small$
type! By projecting the first component, we have a
$ΞΊ-small$
family of elements, which has a join. This is a good definition for the
**join of the subset
$P$**.

module Join-subsets {o β} (F : Poset o β) {β : {I : Type o} (f : I β β F β) β β F β} (β-lubs : β {I} f β is-lub F f (β {I} f)) where open Order.Reasoning F private module P = Lubs.Lubs F β-lubs

opaque βΛ’ : β (P : β F β β Ξ©) β β F β βΛ’ P = β {I = Ξ£[ t β F ] β‘ (t β P)} fst βΛ’-inj : β {P : β F β β Ξ©} {x} β x β P β x β€ βΛ’ P βΛ’-inj x = P.β-inj (_ , (inc x)) βΛ’-universal : β {P : β F β β Ξ©} {x} β (β i β i β P β i β€ x) β βΛ’ P β€ x βΛ’-universal f = P.β-universal _ Ξ» (i , w) β f i (β‘-out! w)