From 4c435f3764451fec9e30c2ea4653559ca0e6b125 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 28 Oct 2024 18:56:55 -0500
Subject: [PATCH] exercise 3.5, closes #44

---
 src/CubicalHott/Exercise3-5.agda | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 src/CubicalHott/Exercise3-5.agda

diff --git a/src/CubicalHott/Exercise3-5.agda b/src/CubicalHott/Exercise3-5.agda
new file mode 100644
index 0000000..26124c5
--- /dev/null
+++ b/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)))
\ No newline at end of file