module Order where
open import Equality
open import EquationalReasoning
open import Function
open import Level
open import Proposition
open import Sum
open import UIP
record Poset {ℓ : Level}(A : Set ℓ) : Set (lsuc ℓ) where
infix 4 _≤_
field
_≤_ : A → A → Set ℓ
instance {{≤isProp}} : {x y : A} → isProp (x ≤ y)
≤refl : (x : A) → x ≤ x
≤trans : {x y z : A} → x ≤ y → y ≤ z → x ≤ z
≤antisymm : {x y : A} → x ≤ y → y ≤ x → x ≡ y
open Poset{{...}} public
{-# DISPLAY Poset._≤_ _ x y = x ≤ y #-}
record Order {ℓ : Level}(A : Set ℓ) : Set (lsuc ℓ) where
field
instance {{po}} : Poset A
≤tot : (x y : A) → x ≤ y or y ≤ x
open Order{{...}} public
≤ind :
{ℓ ℓ' : Level}
{A : Set ℓ}
{{_ : Order A}}
(B : A → Set ℓ')
(_ : (x : A) → isProp (B x))
(x : A)
(_ : {y : A} → y ≤ x → B y)
(_ : {y : A} → x ≤ y → B y)
→
(y : A) → B y
≤ind {{α}} B β x f g y =
orrec
f
g
(λ _ _ → cong f (≤isProp {{po {{α}}}}))
(λ _ _ → cong g (≤isProp {{po {{α}}}}) )
(λ _ _ → β y)
(≤tot y x)
infix 8 if≤then_else_by_
if≤then_else_by_ :
{ℓ ℓ' : Level}
{A : Set ℓ}
{{_ : Order A}}
{B : Set ℓ'}
(f g : A → A → B)
(e : (x : A) → f x x ≡ g x x)
→
A → A → B
(if≤then f else g by e) x y =
orrec
(λ _ → f x y)
(λ _ → g x y)
(λ _ _ → refl)
(λ _ _ → refl)
(λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x))
(≤tot x y)
if≤then-l :
{ℓ ℓ' : Level}
{A : Set ℓ}
{{_ : Order A}}
{B : Set ℓ'}
(f g : A → A → B)
(e : (x : A) → f x x ≡ g x x)
{x y : A}
→
x ≤ y → (if≤then f else g by e) x y ≡ f x y
if≤then-l f g e {x} {y} u =
let h = orrec
(λ _ → f x y)
(λ _ → g x y)
(λ _ _ → refl)
(λ _ _ → refl)
(λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x))
in
proof:
h (≤tot x y)
≡[ cong h (∥∥isProp) ]
h (inl u mod∇)
≡[ orcompl (λ _ → f x y) (λ _ → g x y) (λ _ _ → refl) (λ _ _ → refl)
(λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x)) u ]
f x y
qed
if≤then-r :
{ℓ ℓ' : Level}
{A : Set ℓ}
{{_ : Order A}}
{B : Set ℓ'}
(f g : A → A → B)
(e : (x : A) → f x x ≡ g x x)
{x y : A}
→
y ≤ x → (if≤then f else g by e) x y ≡ g x y
if≤then-r f g e {x} {y} u =
let h = orrec
(λ _ → f x y)
(λ _ → g x y)
(λ _ _ → refl)
(λ _ _ → refl)
(λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x))
in
proof:
h (≤tot x y)
≡[ cong h (∥∥isProp) ]
h (inr u mod∇)
≡[ orcompr (λ _ → f x y) (λ _ → g x y) (λ _ _ → refl) (λ _ _ → refl)
(λ u v → subst (λ z → f x z ≡ g x z) (≤antisymm u v) (e x)) u ]
g x y
qed
∘if≤then :
{ℓ ℓ' ℓ'' : Level}
{A : Set ℓ}
{{_ : Order A}}
{B : Set ℓ'}
{C : Set ℓ''}
(f g : A → A → B)
(e : (x : A) → f x x ≡ g x x)
(h : B → C)
(x y : A)
→
h ((if≤then f else g by e) x y) ≡
(if≤then h ∘₂ f else h ∘₂ g by λ x → cong h (e x)) x y
∘if≤then {ℓ'' = ℓ''} {A} f g e h x = ≤ind E (λ _ → uip) x f' g'
where
E : A → Set ℓ''
E y =
h ((if≤then f else g by e) x y) ≡
(if≤then h ∘₂ f else h ∘₂ g by λ x → cong h (e x)) x y
f' : {y : A} → y ≤ x → E y
f' {y} u =
proof:
h ((if≤then f else g by e) x y)
≡[ cong h (if≤then-r f g e u) ]
h (g x y)
≡[ symm (if≤then-r (h ∘₂ f ) (h ∘₂ g) (λ x → cong h (e x)) u ) ]
(if≤then h ∘₂ f else h ∘₂ g by λ x → cong h (e x)) x y
qed
g' : {y : A} → x ≤ y → E y
g' {y} v =
proof:
h ((if≤then f else g by e) x y)
≡[ cong h (if≤then-l f g e v) ]
h (f x y)
≡[ symm (if≤then-l (h ∘₂ f ) (h ∘₂ g) (λ x → cong h (e x)) v ) ]
(if≤then h ∘₂ f else h ∘₂ g by λ x → cong h (e x)) x y
qed