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! Props .Poset.β€-refl x = x Props .Poset.β€-trans g f x = f (g x) Props .Poset.β€-antisym = Ξ©-ua