added a missing exercise

HoTT · Apr 16, 2021 · 28788f5 · 28788f5
1 parent 9550fe4
commit 28788f5
Showing 1 changed file with 7 additions and 0 deletions.
diff --git 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.