{-# OPTIONS --without-K #-}

open import lib.Base

module lib.Relation where

Rel :  {i} (A : Type i) j  Type (lmax i (lsucc j))
Rel A j = A  A  Type j

Dec :  {i} {A : Type i} {j}  Rel A j  Type (lmax i j)
Dec rel =  a₁ a₂  Coprod (rel a₁ a₂) (¬ (rel a₁ a₂))