\import Data.Or

\func Rel (A : \Type) : \Type => A -> A -> \Type

\record StraightJoin {A : \Type} (a b : A) (rel : Rel A)
  | common-reduct : A
  | a~>cr : rel a common-reduct
  | b~>cr : rel b common-reduct

\data Closure {A : \Type} (R : A -> A -> \Type) (a b : A)
  | c-trivial (a = b)
  | c-basic (a `R` b)
  | c-connect (c : A) (a `R` c) (Closure R c b)
  \where {
    \func compose {A : \Type} {R : Rel A} {a b c : A} (a~>b : Closure R a b) (b~>c : Closure R b c) : Closure R a c \elim a~>b, b~>c
      | c-basic r, rx => c-connect b r rx
      | c-connect c1 r a~>b, rx => c-connect c1 r (compose a~>b rx)
      | c-trivial idp, b~>c => b~>c

    \func lift {A B : \Type} {rel : Rel A} {rel' : Rel B} (map : A -> B)
               (rel-map : \Pi {a b : A} (rel a b) -> rel' (map a) (map b))
               (x y : A)
               (closure : Closure rel x y) : Closure rel' (map x) (map y) \elim closure
      | c-basic r => c-basic (rel-map r)
      | c-connect c r closure => c-connect (map c) (rel-map r) (lift map rel-map c y closure)
      | c-trivial idp => c-trivial idp

    \func flatten {A : \Type} {rel : Rel A}
                  {x y : A}
                  (closure : Closure (Closure rel) x y) : Closure rel x y \elim closure
      | c-basic r => r
      | c-connect c r closure => compose r (flatten closure)
      | c-trivial idp => c-trivial idp

    \func extract
      {A : \Type} {rel : Rel A}
      {x y : A}
      (closure : Closure rel x y)
      : Or (x = y) (\Sigma (z : A) (rel x z)) \elim closure
      | c-trivial p => inl p
      | c-basic r => inr (y, r)
      | c-connect c r closure => inr (c, r)
  }