From 3f89a07add3bdf11b0ab3f5913539d1ce00fdf90 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 22 Mar 2023 00:32:28 -0500
Subject: [PATCH] details

---
 src/Path2.lagda.md | 3 +++
 1 file changed, 3 insertions(+)

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
 ===
 
+<details>
+<summary>Basics (Path, transport, ap, etc.)</summary>
 ```
 {-# 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)
 ```
+</details>
 
 ```
 -- Path products