diff --git a/src/Path2.lagda.md b/src/Path2.lagda.md index 5b295da..efdeb81 100644 --- a/src/Path2.lagda.md +++ b/src/Path2.lagda.md @@ -1,6 +1,8 @@ Path2 === +
+Basics (Path, transport, ap, etc.) ``` {-# OPTIONS --without-K --rewriting #-} @@ -70,6 +72,7 @@ apd {A} {B} f p = path-ind D d p d : (x : A) → D x x (refl x) d x = refl (f x) ``` +
``` -- Path products