module Order.Instances.Props where


In the posetal world, what plays the role of the category of sets is the poset of propositions β€” our relations take values in propositions, much like the category of sets is where the functor takes values.

Unlike β€œthe” category of sets, which is actually a bunch of categories (depending on the universe level of the types we’re considering), there is a single poset of propositions β€” this is the principle of propositional resizing, which we assume throughout.

Props : Poset lzero lzero
Props .Poset.Ob = Ξ©
Props .Poset._≀_ P Q = ∣ P ∣ β†’ ∣ Q ∣
Props .Poset.≀-thin = hlevel 1
Props .Poset.≀-refl x = x
Props .Poset.≀-trans g f x = f (g x)
Props .Poset.≀-antisym = Ξ©-ua

The poset of propositions a top and bottom element, as well as all meets and joins.

Props-has-top : Top Props
Props-has-top = ⊀Ω
Props-has-top .Top.has-top _ _ = tt

Props-has-bot : Bottom Props
Props-has-bot = βŠ₯Ξ©
Props-has-bot .Bottom.has-bottom _ ()

Props-has-joins : βˆ€ P Q β†’ is-join Props P Q (P ∨Ω Q)
Props-has-joins P Q .is-join.l≀join = pure βŠ™ inl
Props-has-joins P Q .is-join.r≀join = pure βŠ™ inr
Props-has-joins P Q .is-join.least R l r = rec! [ l , r ]

Props-has-meets : βˆ€ P Q β†’ is-meet Props P Q (P ∧Ω Q)
Props-has-meets P Q≀l = fst
Props-has-meets P Q≀r = snd
Props-has-meets P Q .is-meet.greatest R l r x = l x , r x

module _ {β„“} {I : Type β„“} (Ps : I β†’ Ξ©) where
  Props-has-glbs : is-glb Props Ps (βˆ€Ξ© I Ps)
  Props-has-glbs .is-glb.glb≀fam i = rec! (_$ i)
  Props-has-glbs .is-glb.greatest R k x = inc (Ξ» i β†’ k i x)

  Props-has-lubs : is-lub Props Ps (βˆƒΞ© I Ps)
  Props-has-lubs .is-lub.fam≀lub i pi = inc (i , pi)
  Props-has-lubs .is-lub.least R k = rec! k