retract

src/HottBook/Chapter3.lagda.md

@@ -423,6 +423,40 @@ lemma3∙11∙6 {A} {P} allContr =
   in center , λ x → Pa-isProp center x
 ```
 
+### Retraction
+
+```
+record retraction {A B : Set l} (r : A → B) : Set l where
+  field
+    s : B → A
+    ε : (y : B) → (r (s y) ≡ y)
+
+_isRetractOf_ : (A B : Set l) → Set l
+B isRetractOf A = Σ (A → B) retraction
+```
+
+### Lemma 3.11.7
+
+```
+-- lemma3∙11∙7 : {A B : Set l} → B isRetractOf A → isContr A → isContr B
+-- lemma3∙11∙7 {A = A} {B = B} BretractA Acontr =
+--   let
+--     open Σ
+--     open retraction
+
+--     r = BretractA .fst
+--     s = BretractA .snd .s
+--     a₀ = Σ.fst Acontr
+--     b₀ = r a₀
+
+--     ε : (y : B) → r (s y) ≡ y
+--     ε = BretractA .snd .ε
+
+--     sContr : (b : B) → s b ≡ a₀
+--     sContr b = {! Acontr .snd (s b)  !}
+--   in b₀ , λ b → {!   !} ∙ (ε b)
+```
+
 ### Lemma 3.11.8
 
 ```