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≀b≀c a \le b \le c

to mean something like β€œa≀ca \le c through the intermediate step bb”. In the syntax, we intersperse the justification for why a≀ba \le b and b≀cb \le c. We also allow equality steps, so chains like a≀b=b′≀ca \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

infixr 2 _=⟨_⟩_ _=˘⟨_⟩_ _β‰€βŸ¨_⟩_
infix  3 _β‰€βˆŽ

instance
  H-Level-≀ : βˆ€ {x y} {n} β†’ H-Level (x ≀ y) (suc n)
  H-Level-≀ = prop-instance ≀-thin