useronym · October 16, 2018 14:59
diff --git a/Path.agda b/Path.agda
 data Path {A : Set} (R : A → A → Set) : A → A → Set where
  ∅    : ∀ {a} → Path R a a
  _>>_ : ∀ {a b c} → R a b → Path R b c → Path R a c
 infixr 5 _>>_

 _>|_ : ∀ {R a b c} → R a b → R b c → Path R a c
 a >| b = a >> b >> ∅
	data Path {A : Set} (R : A → A → Set) : A → A → Set where
	∅ : ∀ {a} → Path R a a
	_>>_ : ∀ {a b c} → R a b → Path R b c → Path R a c
	infixr 5 _>>_

	_>\|_ : ∀ {R a b c} → R a b → R b c → Path R a c
	a >\| b = a >> b >> ∅