Sets/GCHtoAC: simplify further

HoTT · Sep 3, 2023 · d4e3bd5 · d4e3bd5
1 parent 33f9950
commit d4e3bd5
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/theories/Sets/GCHtoAC.v b/theories/Sets/GCHtoAC.v
@@ -68,9 +68,8 @@ Context {EM : ExcludedMiddle}.
 Lemma PE (P P' : HProp) :
   P <-> P' -> P = P'.
 Proof.
-  intros [f g]. apply path_trunctype.
-  apply (equiv_adjointify f g).
-  all: intro x; apply path_ishprop.
+  intros iff. apply path_trunctype.
+  rapply (equiv_iff_hprop_uncurried iff).
 Qed.
 
 Lemma path_bool_prop :