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
to mean something like β through the intermediate step β. In the syntax, we intersperse the justification for why and . We also allow equality steps, so chains like 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