diff --git a/src/Path2.lagda.md b/src/Path2.lagda.md index efdeb81..108d508 100644 --- a/src/Path2.lagda.md +++ b/src/Path2.lagda.md @@ -3,6 +3,7 @@ Path2
Basics (Path, transport, ap, etc.) + ``` {-# OPTIONS --without-K --rewriting #-} @@ -72,8 +73,12 @@ 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 +--- + ``` -- Path products pr₁ : {A B : Type} {a₁ a₂ : A} {b₁ b₂ : B}