open import Cat.Displayed.Univalence.Thin
open import Cat.Prelude

open import Order.Base

module Order.Reasoning {β ββ²} (P : Poset β ββ²) where


# Partial order syntaxπ

This module defines a syntax for reasoning with transitivity in a partial order. Simply speaking, it lets us write chains like

$a \le b \le c$

to mean something like β$a \le c$ through the intermediate step $b$β. In the syntax, we intersperse the justification for why $a \le b$ and $b \le c$. We also allow equality steps, so chains like $a \le b = b' \le c$ are supported, too.

open Poset-on (P .snd) public

Ob : Type β
Ob = β P β

private variable
a b c d : β P β

_β€β¨_β©_ : (a : β P β) β a β€ b β b β€ c β a β€ c
_=β¨_β©_ : (a : β P β) β a β‘ b β b β€ c β a β€ c
_=Λβ¨_β©_ : (a : β P β) β b β‘ a β b β€ c β a β€ c
_β€β    : (a : β P β) β a β€ a

f β€β¨ p β©β€ q = β€-trans p q
f =β¨ p β©= q = subst (_β€ _) (sym p) q
f =Λβ¨ p β©=Λ q = subst (_β€ _) p q
f β€β = β€-refl