z

src/Path2.lagda.md

@@ -3,6 +3,7 @@ Path2
 
 <details>
 <summary>Basics (Path, transport, ap, etc.)</summary>
+
 ```
 {-# 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)
 ```
+
 </details>
 
+Path products
+---
+
 ```
 -- Path products
 pr₁ : {A B : Type} {a₁ a₂ : A} {b₁ b₂ : B}