From 28788f5751f1e79b25c6ac1968ba584edc8e45d7 Mon Sep 17 00:00:00 2001
From: Meven <meven.bertrand@univ-nantes.fr>
Date: Thu, 15 Apr 2021 11:46:13 +0200
Subject: [PATCH] added a missing exercise

---
 01-introduction-to-hott/solutionsMevenLennonBertrand.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/01-introduction-to-hott/solutionsMevenLennonBertrand.v b/01-introduction-to-hott/solutionsMevenLennonBertrand.v
index 361ad69..e50644b 100644
--- a/01-introduction-to-hott/solutionsMevenLennonBertrand.v
+++ b/01-introduction-to-hott/solutionsMevenLennonBertrand.v
@@ -266,6 +266,13 @@ Section Part_4_Equivalences.
        the fact that q : A → Q is the propositional truncation of A.
     *)
 
+    Definition IsPropTrunc (A Q : Type) (q : A -> Q) :=
+        forall  P : hProp, IsEquiv (fun f : Q -> P => f ∘ q).
+
+    Theorem univ_trunc (A : Type) : (IsPropTrunc A (Trunc (-1) A) tr).
+    Proof.
+    Admitted.
+
   End Exercise_4_2.
 
 End Part_4_Equivalences.