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.

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