From 0cb341072ce0602f9ff30889d7aede37f02c4425 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 02:07:10 +0000
Subject: [PATCH] auto gitdoc commit

---
 src/HottBook/Chapter2.lagda.md | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 312df30..52c6a2f 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -56,12 +56,12 @@ transport {l₁} {l₂} {A} {x} {y} P p = J (λ x y p → P x → P y) (λ x →
 TODO
 
 ```
-lift : {A : Set} (P : A → Set) {x y : A}
-  → (u : P x)
-  → (p : x ≡ y)
-  → (x , u) ≡ (y , transport P p u)
-lift {A} P {x} {y} u p =
-  J (λ a b p → (a , {!  !}) ≡ (b , {!   !})) (λ x → {!   !}) x y p
+-- lift : {A : Set} (P : A → Set) {x y : A}
+--   → (u : P x)
+--   → (p : x ≡ y)
+--   → (x , u) ≡ (y , transport P p u)
+-- lift {A} P {x} {y} u p =
+--   J (λ a b p → (x , {!  !}) ≡ (y , {!   !})) (λ x → {!   !}) x y p
 ```
 
 Verifying its property: