Agda-2.3.2.2: examples/AIM6/Path/Elem.agda

module Elem where

open import Prelude
open import Star

Elem : {X : Set}(R : Rel X) -> Rel X
Elem R x y = Star (LeqBool [×] R) (false , x) (true , y)