Skip to content

Instantly share code, notes, and snippets.

@johnchandlerburnham
Created May 28, 2020 22:27
Show Gist options
  • Save johnchandlerburnham/6fcd7305a19030da06b6e5c39eec6bca to your computer and use it in GitHub Desktop.
Save johnchandlerburnham/6fcd7305a19030da06b6e5c39eec6bca to your computer and use it in GitHub Desktop.
Path involution, connection
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;;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment