Ord.lol

Ordering_Polytype : *p
 = (Data:*) -> (Lt:Data) -> (Eq:Data) -> (Gt:Data) -> Data
Ordering : *m = Monotype Ordering_Polytype

Ord_Lt : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Lt)
Ord_Eq : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Eq)
Ord_Gt : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Gt)

:load Eq.lol

Ord_Compare (X:*) = X -> X -> Ordering

Ord_Class
 (X:*) (Data:*)
 =  (eq:Eq X)
 -> (compare:Ord_Compare X)
 -> Data
Ord_Polytype
 (X:*) : *p
 = (Data:*) -> Ord_Class X Data -> Data
Ord
 (X:*) : *m
 = Monotype (Ord_Polytype X)

ord
 (X:*)
 (eq:Eq X)
 (compare:Ord_Compare X)
 : Ord X
 = monotype (Ord_Polytype X)
    (λ(Data:*) (ord_class:Ord_Class X Data) ->
      ord_class eq compare)
unOrd
 (X:*) (Data:*)
 (ord_class:Ord_Class X Data)
 (ord:Ord X)
 : Data
 = polytype (Ord_Polytype X) ord Data ord_class

Ord_eq
 (X:*) (ord:Ord X)
 : Eq X
 = unOrd X (Eq X)
    (λ(eq:Eq X) (compare:Ord_Compare X) -> eq)
    ord
Ord_compare
 (X:*) (ord:Ord X)
 : Ord_Compare X
 = unOrd X (Ord_Compare X)
    (λ(eq:Eq X) (compare:Ord_Compare X) -> compare)
    ord