RelationList.agda

RelationList.agda

module RelationList (A : Set)  where

-- Converse of relation
converse : (A → A → Set) → (A → A → Set)
converse R a a' = R a' a

-- A list of things (a1, a2, ... an) with relations
-- u -R-> a1 -R-> a2 -R-> ... -R-> an -R-> v
data Rist' (R : A → A → Set) (v : A) : (u : A) → Set where
  rnil : {u : A} → (r : R u v) → Rist' R v u
  rcons : {u : A} → (x : A) (r : R u x) → Rist' R v x → Rist' R v u

-- An order of arguments that seems nicer.
Rist : (u : A) (R : A → A → Set) (v : A) → Set
Rist u R v = Rist' R v u

rsnoc : (R : A → A → Set) (u v : A) → Rist u R v → (x : A) (r : R v x) → Rist u R x
rsnoc R u v (rnil r') x r = rcons v r' (rnil r)
rsnoc R u v (rcons x' r' ℓ) x r = rcons x' r' (rsnoc R x' v ℓ x r)

rrev : (R : A → A → Set) (u v : A) → Rist u R v → Rist v (converse R) u
rrev R u v (rnil r) = rnil r
rrev R u v (rcons x r ℓ) = rsnoc (converse R) v x (rrev R x v ℓ) u r