Path involution, connection

Path.fm

I: Type
  i<P: (i:I) -> Type> ->
  (I0: P(I.0)) ->
  (I1: P(I.1)) ->
  (IE: Path(P, I0, I1)) ->
  P(i)

I.0: I
  <P> (i0) (i1) (ie) i0

I.1: I
  <P> (i0) (i1) (ie) i1

I.e: Path((i) I, I.0, I.1)
  <P> (abs) abs((i) i)

Path(A: I -> Type, a: A(I.0), b: A(I.1)) : Type
  path<P: (a: A(I.0)) -> (b: A(I.1)) -> Path(A, a, b) -> Type> ->
  (abs: (t: (i:I) -> A(i)) -> P(t(I.0), t(I.1), Path.abs(A, t))) ->
  P(a, b, path)

Path.abs (A: I -> Type) (t: (i:I) -> A(i)): Path(A, t(I.0), t(I.1))
  <P> (abs)
  abs(t)

Path.refl<A: Type>(x: A): Path((i) A, x, x)
  <P> (abs) abs((i) x)

Path.app(A: I -> Type, a: A(I.0), b: A(I.1), e: Path(A, a, b), i: I): A(i)
  i<A>(a, b, e)

Path.ei: Path((i) I, I.1, I.0)
  <P> (abs) abs(Path.neg)

Path.neg(i: I) : I
  i<(i) I>(I.1, I.0, Path.ei)

Path.min(r: I, s: I): I
  r<(i) I>
  | I.0;
  | s;
  | s<(i) Path((x) I, I.0, i)>
    | Path.refl<I>(I.0);
    | I.e;
    | Path.id0_to_ie;;

// This is a 2nd-order Path between the paths `I.0 ~> I.0` and `I.0 ~> I.1`
Path.id0_to_ie : Path((i) Path((x) I, I.0, i), Path.refl<I>(I.0), I.e)
  Path.abs
  | (i) Path((x) I, I.0, i);
  | (i) i<(z) Path((x) I, I.0, z)>
    | Path.refl<I>(I.0);
    | I.e;
    | Path.id0_to_ie;;

Path.max(r: I, s: I): I
 r<(i) I>
 | s;
 | I.1;
 | s<(i) Path((x) I, i, I.1)>
   | I.e;
   | Path.refl<I>(I.1);
   | Path.ie_to_id1;;

// This is a 2nd-order Path between the paths ``I.0 ~> I.1` and `I.1 ~> I.1`
Path.ie_to_id1 : Path((i) Path((x) I, i, I.1), I.e, Path.refl<I>(I.1))
  Path.abs
  | (i) Path((x) I, i, I.1);
  | (i) i<(z) Path((x) I, z, I.1)>
    | I.e;
    | Path.refl<I>(I.1);
    | Path.ie_to_id1;;