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 $\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