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.
open is-partial-order open Poset-on Props : Poset lzero lzero Props = to-poset Ξ© mk-Ξ© where mk-Ξ© : make-poset lzero Ξ© mk-Ξ© .make-poset.rel P Q = β£ P β£ β β£ Q β£ mk-Ξ© .make-poset.id x = x mk-Ξ© .make-poset.thin = hlevel! mk-Ξ© .make-poset.trans g f x = f (g x) mk-Ξ© .make-poset.antisym = Ξ©-ua