module Order.Instances.Props where
Propositions🔗
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 p q = ext (Ω-ua p q)
The poset of propositions a top and bottom element, as well as all meets and joins.
Props-has-top : Top Props Props-has-top .Top.top = ⊤Ω Props-has-top .Top.has-top _ _ = tt Props-has-bot : Bottom Props Props-has-bot .Bottom.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 .is-meet.meet≤l = fst Props-has-meets P Q .is-meet.meet≤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
open is-meet-semilattice open is-join-semilattice Props-is-meet-slat : is-meet-semilattice Props Props-is-meet-slat ._∩_ x y = x ∧Ω y Props-is-meet-slat .∩-meets = Props-has-meets Props-is-meet-slat .has-top = Props-has-top Props-is-join-slat : is-join-semilattice Props Props-is-join-slat ._∪_ x y = x ∨Ω y Props-is-join-slat .∪-joins = Props-has-joins Props-is-join-slat .has-bottom = Props-has-bot