update

src/HottBook/Chapter3.lagda.md

@@ -428,11 +428,21 @@ module section3∙7 where
     ∣_∣ : {A : Set l} → A → ∥ A ∥
     trunc-witness : {A : Set l} → isProp (∥ A ∥)
     
-    rec-trunc : (A : Set) → {B : Set} → isProp B → (f : A → B) → ∥ A ∥ → B
+    rec-trunc : {l l2 : Level} {A : Set l} {B : Set l2} → isProp B → (f : A → B) → ∥ A ∥ → B
 
-    rec-trunc-1 : {A : Set} → {B : Set} → (Bprop : isProp B) → (f : A → B) → (a : A) → rec-trunc A Bprop f (∣ a ∣) ≡ f a
+    rec-trunc-1 : {l l2 : Level} {A : Set l} {B : Set l2}
+      → (Bprop : isProp B)
+      → (f : A → B)
+      → (a : A)
+      → rec-trunc Bprop f (∣ a ∣) ≡ f a
     {-# REWRITE rec-trunc-1 #-}
 
+  ind-trunc : {A : Set} → {B : ∥ A ∥ → Set}
+    → ((x : ∥ A ∥) → isProp (B x))
+    → ((a : A) → B (∣ a ∣))
+    → (x : ∥ A ∥) → B x
+  ind-trunc f g x = rec-trunc (f x) (λ a → {! g x  !}) x
+
 open section3∙7 public
 ```
 
@@ -491,7 +501,7 @@ lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
 lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop witness ∣_∣ rec-func
   where
     rec-func : ∥ P ∥ → P
-    rec-func = rec-trunc P Pprop id
+    rec-func = rec-trunc Pprop id
 
     witness : isProp ∥ P ∥
     witness = trunc-witness

src/HottBook/Chapter4.lagda.md

@@ -110,7 +110,11 @@ lemma4∙1∙2 : {A : Set} {a : A} (q : a ≡ a)
 lemma4∙1∙2 {A} {a} q prop1 g prop3 = (λ x → {!   !}) , {!   !}
   where
     allsets : (x y : A) → isSet (x ≡ y)
-    allsets x y p q r s = {!  trunc-witness ? ? !}
+    allsets x y p q r s =
+      let
+        p1 = g x
+        p2 = g y
+      in {!   !}
 
     ctx = let 
       f = rec-trunc A {!   !} {! g  !}