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 ≀\le relations take values in propositions, much like the category of sets is where the Hom\mathbf{Hom} 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!
Props .Poset.≀-refl x = x
Props .Poset.≀-trans g f x = f (g x)
Props .Poset.≀-antisym = Ξ©-ua