From 1e270130e0af45c0ea1b32350dc9b532eade0199 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 11 Jul 2024 00:31:26 -0500
Subject: [PATCH] lemma 3.11.6

---
 src/HottBook/Chapter3.lagda.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 2a4e8aa..d244cbc 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -417,7 +417,10 @@ lemma3∙11∙6 {A} {P} allContr =
   let
     Pa-isProp : isProp ((x : A) → P x)
     Pa-isProp = example3∙6∙2 λ x → Σ.snd (lemma3∙11∙3.properties.ii (lemma3∙11∙3.i (allContr x)))
-  in {!   !} , {!   !}
+
+    center : (x : A) → P x
+    center x = Σ.fst (allContr x)
+  in center , λ x → Pa-isProp center x
 ```
 
 ### Lemma 3.11.8