From 95ee86134967ca944ef9180a3fa6e59eb3d6da97 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 11 Jul 2024 00:49:14 -0500 Subject: [PATCH] retract --- src/HottBook/Chapter3.lagda.md | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index d244cbc..5bc997b 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/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 ```