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.

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