open import Cat.Prelude

open import Order.Base

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