exercise 3.5, closes #44

src/CubicalHott/Exercise3-5.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Exercise3-5 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+
+exercise : {A : Type} → isProp A ≃ (A → isContr A)
+exercise {A} = isoToEquiv (iso f g fg gf) where
+  f : isProp A → A → isContr A
+  f isPropA a = a , (λ y → isPropA a y)
+
+  g : (A → isContr A) → isProp A
+  g p x y =
+    let z = snd (p x) in
+    sym (z x) ∙ z y
+
+  fg : section f g
+  fg ff = funExt λ x → isPropIsContr (f (g ff) x) (ff x)
+
+  gf : retract f g
+  gf prop = funExt (λ x → funExt (λ y → isProp→isSet prop x y (g (f prop) x y) (prop x y)))