diff --git a/src/1Lab/Biimp.lagda.md b/src/1Lab/Biimp.lagda.md
new file mode 100644
index 000000000..3455280b6
--- /dev/null
+++ b/src/1Lab/Biimp.lagda.md
@@ -0,0 +1,143 @@
+---
+description: |
+  Biimplications.
+---
+<!--
+```agda
+open import 1Lab.Reflection.Record
+open import 1Lab.Extensionality
+open import 1Lab.HLevel.Closure
+open import 1Lab.HLevel
+open import 1Lab.Equiv
+open import 1Lab.Type
+
+open import Meta.Invariant
+```
+-->
+```agda
+module 1Lab.Biimp where
+```
+
+# Biimplications
+
+:::{.definition #biimplication}
+A **biimplication** $A \leftrightarrow B$ between a pair of types $A, B$
+is a pair of functions $A \to B, B \to A$.
+:::
+
+```agda
+record _↔_ {ℓ} {ℓ'} (A : Type ℓ) (B : Type ℓ') : Type (ℓ ⊔ ℓ') where
+  no-eta-equality
+  constructor biimp
+  field
+    to : A → B
+    from : B → A
+
+open _↔_
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' : Level
+  A B C : Type ℓ
+```
+-->
+
+<!--
+```agda
+module Biimp (f : A ↔ B) where
+  open _↔_ f public
+```
+-->
+
+If $A$ and $B$ [[n-types]], then the type of biimplications $A \leftrightarrow B$
+is also an n-type.
+
+<!--
+```agda
+private unquoteDecl eqv = declare-record-iso eqv (quote _↔_)
+```
+-->
+
+```agda
+↔-is-hlevel : ∀ n → is-hlevel A n → is-hlevel B n → is-hlevel (A ↔ B) n
+↔-is-hlevel n A-hl B-hl =
+  Iso→is-hlevel n eqv $
+  ×-is-hlevel n
+    (Π-is-hlevel n λ _ → B-hl)
+    (Π-is-hlevel n λ _ → A-hl)
+```
+
+<!--
+```agda
+instance
+  H-Level-↔
+    : ∀ {n}
+    → ⦃ _ : H-Level A n ⦄ ⦃ _ : H-Level B n ⦄
+    → H-Level (A ↔ B) n
+  H-Level-↔ {n = n} .H-Level.has-hlevel =
+    ↔-is-hlevel n (hlevel n) (hlevel n)
+
+instance
+  Extensional-↔
+    : ∀ {ℓr}
+    → ⦃ _ : Extensional ((A → B) × (B → A)) ℓr ⦄
+    → Extensional (A ↔ B) ℓr
+  Extensional-↔ ⦃ e ⦄ = iso→extensional eqv e
+```
+-->
+
+## Working with biimplications
+
+There is an identity biimplication, and biimplications compose.
+
+```agda
+id↔ : A ↔ A
+id↔ .to = id
+id↔ .from = id
+
+_∙↔_ : A ↔ B → B ↔ C → A ↔ C
+(f ∙↔ g) .to = g .to ∘ f .to
+(f ∙↔ g) .from = f .from ∘ g .from
+```
+
+Moreover, every biimplication $A \leftrightarrow B$ induces a biimplication
+$B \leftrightarrow A$.
+
+```agda
+_↔⁻¹ : A ↔ B → B ↔ A
+(f ↔⁻¹) .to = f .from
+(f ↔⁻¹) .from = f .to
+```
+
+## Biimplications and equivalences
+
+Every [[equivalence]] is a biimplication.
+
+```agda
+equiv→biimp : A ≃ B → A ↔ B
+equiv→biimp f .to = Equiv.to f
+equiv→biimp f .from = Equiv.from f
+```
+
+:::{.definition #logical-equivalence}
+
+Every biimplication between [[propositions]] is an [[equivalence]].
+In light of this, biimplications are often referred to as
+**logical equivalences**.
+
+```agda
+biimp→equiv : is-prop A → is-prop B → A ↔ B → A ≃ B
+biimp→equiv A-prop B-prop f =
+  prop-ext A-prop B-prop (f .to) (f .from)
+```
+:::
+
+<!--
+```agda
+infix 21 _↔_
+infixr 30 _∙↔_
+infix 31 _↔⁻¹
+```
+-->
diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md
index 813b24a61..0bbf01a58 100644
--- a/src/1Lab/Equiv.lagda.md
+++ b/src/1Lab/Equiv.lagda.md
@@ -846,7 +846,7 @@ for which constructing equivalences is easy are the [[propositions]]. If
 $P$ and $Q$ are propositions, then any map $P \to P$ (resp. $Q \to Q$)
 must be homotopic to the identity, and consequently any pair of
 functions $P \to Q$ and $Q \to P$ is a pair of inverses. Put another
-way, any *biimplication* between propositions is an equivalence.
+way, any [[biimplication]] between propositions is an equivalence.
 
 ```agda
   biimp-is-equiv : (f : P → Q) → (Q → P) → is-equiv f
diff --git a/src/1Lab/Extensionality.agda b/src/1Lab/Extensionality.agda
index 24311dcfe..0da48a4e1 100644
--- a/src/1Lab/Extensionality.agda
+++ b/src/1Lab/Extensionality.agda
@@ -7,7 +7,6 @@ open import 1Lab.HIT.Truncation
 open import 1Lab.HLevel.Closure
 open import 1Lab.Reflection
 open import 1Lab.Type.Sigma
-open import 1Lab.Resizing
 open import 1Lab.Type.Pi
 open import 1Lab.HLevel
 open import 1Lab.Equiv
@@ -341,11 +340,6 @@ instance
     → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → ∥ B x ∥) ℓr
   Extensional-Σ-trunc ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea
 
-  Extensional-Σ-□
-    : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'}
-    → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → □ (B x)) ℓr
-  Extensional-Σ-□ ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea
-
   Extensional-equiv
     : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
     → ⦃ ea : Extensional (A → B) ℓr ⦄ → Extensional (A ≃ B) ℓr
diff --git a/src/1Lab/Prelude.agda b/src/1Lab/Prelude.agda
index 091268823..02b51b66e 100644
--- a/src/1Lab/Prelude.agda
+++ b/src/1Lab/Prelude.agda
@@ -30,6 +30,8 @@ open import 1Lab.Function.Embedding public
 open import 1Lab.Function.Reasoning public
 open import 1Lab.Equiv.HalfAdjoint public
 
+open import 1Lab.Biimp public
+
 open import 1Lab.Function.Surjection public
 
 open import 1Lab.Univalence public
diff --git a/src/1Lab/Resizing.lagda.md b/src/1Lab/Resizing.lagda.md
index 56bb6f318..6900d7dcf 100644
--- a/src/1Lab/Resizing.lagda.md
+++ b/src/1Lab/Resizing.lagda.md
@@ -4,12 +4,14 @@ open import 1Lab.Function.Surjection
 open import 1Lab.Path.IdentitySystem
 open import 1Lab.Reflection.HLevel
 open import 1Lab.HLevel.Universe
+open import 1Lab.Extensionality
 open import 1Lab.HIT.Truncation
 open import 1Lab.HLevel.Closure
 open import 1Lab.Reflection using (arg ; typeError)
 open import 1Lab.Univalence
 open import 1Lab.Inductive
 open import 1Lab.HLevel
+open import 1Lab.Biimp
 open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type
@@ -91,13 +93,15 @@ instance
 ```
 -->
 
-We can also prove a univalence principle for `Ω`{.Agda}:
+We can also prove a univalence principle for `Ω`{.Agda}: if
+$A, B : \Omega$ are [[logically equivalent|logical-equivalence]],
+then they are equal.
 
 ```agda
-Ω-ua : {A B : Ω} → (∣ A ∣ → ∣ B ∣) → (∣ B ∣ → ∣ A ∣) → A ≡ B
-Ω-ua {A} {B} f g i .∣_∣ = ua (prop-ext! f g) i
-Ω-ua {A} {B} f g i .is-tr =
-  is-prop→pathp (λ i → is-prop-is-prop {A = ua (prop-ext! f g) i})
+Ω-ua : {A B : Ω} → ∣ A ∣ ↔ ∣ B ∣ → A ≡ B
+Ω-ua {A} {B} f i .∣_∣ = ua (prop-ext! (Biimp.to f) (Biimp.from f)) i
+Ω-ua {A} {B} f i .is-tr =
+  is-prop→pathp (λ i → is-prop-is-prop {A = ua (prop-ext! (Biimp.to f) (Biimp.from f)) i})
     (A .is-tr) (B .is-tr) i
 
 instance abstract
@@ -105,10 +109,20 @@ instance abstract
   H-Level-Ω = basic-instance 2 $ retract→is-hlevel 2
     (λ r → el ∣ r ∣ (r .is-tr))
     (λ r → el ∣ r ∣ (r .is-tr))
-    (λ x → Ω-ua (λ x → x) λ x → x)
+    (λ x → Ω-ua id↔)
     (n-Type-is-hlevel {lzero} 1)
 ```
 
+<!--
+```agda
+instance
+  Extensionality-Ω : Extensional Ω lzero
+  Extensionality-Ω .Pathᵉ A B = ∣ A ∣ ↔ ∣ B ∣
+  Extensionality-Ω .reflᵉ A = id↔
+  Extensionality-Ω .idsᵉ = set-identity-system (λ _ _ → hlevel 1) Ω-ua
+```
+-->
+
 The `□`{.Agda} type former is a functor (in the handwavy sense that it
 supports a "map" operation), and can be projected from into propositions
 of any universe. These functions compute on `inc`{.Agda}s, as usual.
@@ -208,7 +222,7 @@ to-is-true
   : ∀ {P Q : Ω} ⦃ _ : H-Level ∣ Q ∣ 0 ⦄
   → ∣ P ∣
   → P ≡ Q
-to-is-true prf = Ω-ua (λ _ → hlevel 0 .centre) (λ _ → prf)
+to-is-true prf = Ω-ua (biimp (λ _ → hlevel 0 .centre) λ _ → prf)
 
 tr-□ : ∀ {ℓ} {A : Type ℓ} → ∥ A ∥ → □ A
 tr-□ (inc x) = inc x
@@ -223,7 +237,7 @@ tr-□ (squash x y i) = squash (tr-□ x) (tr-□ y) i
 ## Connectives
 
 The universe of small propositions contains true, false, conjunctions,
-disjunctions, and implications.
+disjunctions, and (bi)implications.
 
 <!--
 ```agda
@@ -254,6 +268,10 @@ _→Ω_ : Ω → Ω → Ω
 ∣ P →Ω Q ∣ = ∣ P ∣ → ∣ Q ∣
 (P →Ω Q) .is-tr = hlevel 1
 
+_↔Ω_ : Ω → Ω → Ω
+∣ P ↔Ω Q ∣ = ∣ P ∣ ↔ ∣ Q ∣
+(P ↔Ω Q) .is-tr = hlevel 1
+
 ¬Ω_ : Ω → Ω
 ¬Ω P = P →Ω ⊥Ω
 ```
@@ -274,6 +292,16 @@ syntax ∃Ω A (λ x → B) = ∃Ω[ x ∈ A ] B
 syntax ∀Ω A (λ x → B) = ∀Ω[ x ∈ A ] B
 ```
 
+<!--
+```agda
+instance
+  Extensional-Σ-□
+    : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'}
+    → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → □ (B x)) ℓr
+  Extensional-Σ-□ ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea
+```
+-->
+
 These connectives and quantifiers are only provided for completeness;
 if you find yourself building nested propositions, it is generally a good
 idea to construct the large proposition by hand, and then use truncation
diff --git a/src/Cat/Allegory/Base.lagda.md b/src/Cat/Allegory/Base.lagda.md
index 4ad95d088..6c78df6ad 100644
--- a/src/Cat/Allegory/Base.lagda.md
+++ b/src/Cat/Allegory/Base.lagda.md
@@ -219,9 +219,9 @@ to show $R(x, y)$! Fortunately if we we set $\Id(x, a)$, then $R(x,
 y) \simeq R(a, y)$, and we're done.
 
 ```agda
-Rel ℓ .cat .idr {A} {B} R = ext λ x y → Ω-ua
-  (rec! λ a b w → subst (λ e → ∣ R e y ∣) (sym b) w)
-  λ w → inc (x , inc refl , w)
+Rel ℓ .cat .idr {A} {B} R = ext λ x y → biimp
+  (rec! (λ a b w → subst (λ e → ∣ R e y ∣) (sym b) w))
+  (λ w → inc (x , inc refl , w))
 ```
 
 The other interesting bits of the construction are meets, the dual, and
@@ -251,24 +251,24 @@ automatic proof search: that speaks to how contentful it is.</summary>
 
 ```agda
 Rel ℓ .cat .Hom-set x y = hlevel 2
-Rel ℓ .cat .idl R = ext λ x y → Ω-ua
+Rel ℓ .cat .idl R = ext λ x y → biimp
   (rec! λ z x~z z=y → subst (λ e → ∣ R x e ∣) z=y x~z)
-  λ w → inc (y , w , inc refl)
+  (λ w → inc (y , w , inc refl))
 
-Rel ℓ .cat .assoc T S R = ext λ x y → Ω-ua
+Rel ℓ .cat .assoc T S R = ext λ x y → biimp
   (rec! λ a b r s t → inc (b , r , inc (a , s , t)))
   (rec! λ a r b s t → inc (b , inc (a , r , s) , t))
 
 Rel ℓ .≤-thin = hlevel 1
 Rel ℓ .≤-refl x y w = w
 Rel ℓ .≤-trans x y p q z = y p q (x p q z)
-Rel ℓ .≤-antisym p q = ext λ x y → Ω-ua (p x y) (q x y)
+Rel ℓ .≤-antisym p q = ext λ x y → biimp (p x y) (q x y)
 
 Rel ℓ ._◆_ f g a b = □-map (λ { (x , y , w) → x , g a x y , f x b w })
 
 -- This is nice:
 Rel ℓ .dual R = refl
-Rel ℓ .dual-∘ = ext λ x y → Ω-ua
+Rel ℓ .dual-∘ = ext λ x y → biimp
   (□-map λ { (a , b , c) → a , c , b })
   (□-map λ { (a , b , c) → a , c , b })
 Rel ℓ .dual-≤ f≤g x y w = f≤g y x w
diff --git a/src/Cat/CartesianClosed/Lambda.lagda.md b/src/Cat/CartesianClosed/Lambda.lagda.md
index 31eaffebc..19fc2c2c6 100644
--- a/src/Cat/CartesianClosed/Lambda.lagda.md
+++ b/src/Cat/CartesianClosed/Lambda.lagda.md
@@ -23,7 +23,7 @@ module Cat.CartesianClosed.Lambda
         (cc : Cartesian-closed C fp term)
         where
 
-open Binary-products C fp hiding (unique₂)
+open Binary-products C fp
 open Cartesian-closed cc
 open Cat.Reasoning C
 ```
diff --git a/src/Cat/Diagram/Sieve.lagda.md b/src/Cat/Diagram/Sieve.lagda.md
index b4d2906dd..285b37333 100644
--- a/src/Cat/Diagram/Sieve.lagda.md
+++ b/src/Cat/Diagram/Sieve.lagda.md
@@ -163,14 +163,14 @@ contravariant, this means that the assignment $U \mapsto
 ```agda
   abstract
     pullback-id : ∀ {c} {s : Sieve C c} → pullback C.id s ≡ s
-    pullback-id {s = s} = ext λ h → Ω-ua
+    pullback-id {s = s} = ext λ h → biimp
       (subst (_∈ s) (C.idl h))
       (subst (_∈ s) (sym (C.idl h)))
 
     pullback-∘
       : ∀ {u v w} {f : C.Hom w v} {g : C.Hom v u} {R : Sieve C u}
       → pullback (g C.∘ f) R ≡ pullback f (pullback g R)
-    pullback-∘ {f = f} {g} {R = R} = ext λ h → Ω-ua
+    pullback-∘ {f = f} {g} {R = R} = ext λ h → biimp
       (subst (_∈ R) (sym (C.assoc g f h)))
       (subst (_∈ R) (C.assoc g f h))
 ```
diff --git a/src/Cat/Instances/Sheaves/Omega.lagda.md b/src/Cat/Instances/Sheaves/Omega.lagda.md
index 82ac45c98..7827c5b97 100644
--- a/src/Cat/Instances/Sheaves/Omega.lagda.md
+++ b/src/Cat/Instances/Sheaves/Omega.lagda.md
@@ -82,7 +82,7 @@ actually agree on their intersection with $R$:
   sep {U} R {S , cS} {T , cT} α = ext λ {V} h →
     let
       rem₁ : S ∩S ⟦ R ⟧ ≡ T ∩S ⟦ R ⟧
-      rem₁ = ext λ {V} h → Ω-ua
+      rem₁ = ext λ {V} h → biimp
         (λ (h∈S , h∈R) → cT h (subst (J ∋_) (ap fst (α h h∈R)) (max (S .closed h∈S id))) , h∈R)
         (λ (h∈T , h∈R) → cS h (subst (J ∋_) (ap fst (sym (α h h∈R))) (max (T .closed h∈T id))) , h∈R)
 ```
@@ -115,7 +115,7 @@ We omit the symmetric converse for brevity.
 -->
 
 ```agda
-    in Ω-ua (λ h∈S → cT h (rem₂' h∈S)) (λ h∈T → cS h (rem₃ h∈T))
+    in biimp (λ h∈S → cT h (rem₂' h∈S)) (λ h∈T → cS h (rem₃ h∈T))
 ```
 
 Now we have to show that a family $S$ of compatible closed sieves over a
@@ -152,7 +152,7 @@ are painful --- and entirely mechanical --- calculations.
 
 ```agda
     restrict : ∀ {V} (f : Hom V U) (hf : f ∈ R) → pullback f S' ≡ S .part f hf .fst
-    restrict f hf = ext λ {V} h → Ω-ua
+    restrict f hf = ext λ {V} h → biimp
       (rec! λ α →
         let
           step₁ : id ∈ S .part (f ∘ h ∘ id) (⟦ R ⟧ .closed hf (h ∘ id)) .fst
diff --git a/src/Cat/Site/Closure.lagda.md b/src/Cat/Site/Closure.lagda.md
index a6076fd75..4ebe81444 100644
--- a/src/Cat/Site/Closure.lagda.md
+++ b/src/Cat/Site/Closure.lagda.md
@@ -280,7 +280,7 @@ sieve belongs to the saturation in at most one way.
       : ∀ {J : Coverage C ℓs} {U} {R S : Sieve C U}
       → J ∋ R → J ∋ S → J ∋ (R ∩S S)
     ∋-intersect {J = J} {R = R} {S = S} α β = local β
-      (λ {V} f hf → subst (J ∋_) (ext (λ h → Ω-ua (λ fhR → fhR , S .closed hf _) fst)) (pull f α))
+      (λ {V} f hf → subst (J ∋_) (ext (λ h → biimp (λ fhR → fhR , S .closed hf _) fst)) (pull f α))
 ```
 -->
 
diff --git a/src/Cat/Site/Instances/Atomic.lagda.md b/src/Cat/Site/Instances/Atomic.lagda.md
index 7184d298e..3ba0a587b 100644
--- a/src/Cat/Site/Instances/Atomic.lagda.md
+++ b/src/Cat/Site/Instances/Atomic.lagda.md
@@ -360,13 +360,13 @@ proposition $P$ to the sieve which contains any $h$ iff $P$.
 
 <!--
 ```agda
-    m1 .is-natural x y f = ext λ S cl → Ω-ua
+    m1 .is-natural x y f = ext λ S cl → biimp
       (λ hf → cl id (inc (pullback id S , inc (y , f , subst (_∈ S) id-comm hf))))
       (λ hid → subst (_∈ S) id-comm-sym (S .closed hid f))
 
     m2 .η x P .fst .closed hf _ = hf
     m2 .η x P .snd h y = case Atomic.unsaturate C sq y of λ _ _ α → α
-    m2 .is-natural x y f = ext λ P → Σ-prop-path! $ ext λ {V} f → refl
+    m2 .is-natural x y f = ext λ P → Σ-prop-path! trivial!
 ```
 -->
 
@@ -377,8 +377,8 @@ direction is definitional, and the other is not much more complicated.
   ΩJ-is-constant : ΩJ cov Sh.≅ ΩJ'
   ΩJ-is-constant =
     let
-      q = ext λ i X cl → Σ-prop-path! $ ext λ x → Ω-ua
+      q = ext λ i X cl → Σ-prop-path! $ ext λ x → biimp
         (λ p → subst (_∈ X) (idl _) (X .closed p _))
         (λ p → cl id (inc (_ , inc (_ , _ , subst (_∈ X) id-comm (X .closed p id)))))
-    in Sh.make-iso m1 m2 (ext λ _ _ → refl) q
+    in Sh.make-iso m1 m2 trivial! q
 ```
diff --git a/src/Cat/Site/Instances/Frame.lagda.md b/src/Cat/Site/Instances/Frame.lagda.md
index 122862db4..9a5f9d173 100644
--- a/src/Cat/Site/Instances/Frame.lagda.md
+++ b/src/Cat/Site/Instances/Frame.lagda.md
@@ -83,7 +83,7 @@ computed *is* the pullback sieve.
   generate-∩
     : ∀ {U V} (h : V ≤ U) (S : Covering U)
     → generate (∩-covering h S) ≡ pullback h (generate S)
-  generate-∩ V≤U (I , f , p) = ext λ {W} W≤V → Ω-ua
+  generate-∩ V≤U (I , f , p) = ext λ {W} W≤V → biimp
     (rec! λ i W≤fi∩V → inc (i , ≤-trans W≤fi∩V ∩≤l))
     (rec! λ i W≤fi   → inc (i , ∩-universal _ W≤fi W≤V))
 
diff --git a/src/Data/Partial/Base.lagda.md b/src/Data/Partial/Base.lagda.md
index 046edcba0..fb8b69863 100644
--- a/src/Data/Partial/Base.lagda.md
+++ b/src/Data/Partial/Base.lagda.md
@@ -90,7 +90,7 @@ part-ext
   → (∀ xd yd → x .elt xd ≡ y .elt yd)
   → x ≡ y
 part-ext to from p = Part-pathp refl
-  (Ω-ua to from) (funext-dep λ _ → p _ _)
+  (Ω-ua (biimp to from)) (funext-dep λ _ → p _ _)
 ```
 
 To close the initial definitions, if we have a partial element $x : \zap
diff --git a/src/Data/Power.lagda.md b/src/Data/Power.lagda.md
index 0de45bf3b..d513f92cf 100644
--- a/src/Data/Power.lagda.md
+++ b/src/Data/Power.lagda.md
@@ -61,7 +61,7 @@ propositions to each inhabitant of $X$.
 ℙ-ext : {A B : ℙ X}
       → A ⊆ B → B ⊆ A → A ≡ B
 ℙ-ext {A = A} {B = B} A⊆B B⊂A = funext λ x →
-  Ω-ua (A⊆B x) (B⊂A x)
+  Ω-ua (biimp (A⊆B x) (B⊂A x))
 ```
 
 ## Lattice structure
diff --git a/src/Order/Frame.lagda.md b/src/Order/Frame.lagda.md
index 6e39c3e5d..adf6d5673 100644
--- a/src/Order/Frame.lagda.md
+++ b/src/Order/Frame.lagda.md
@@ -303,7 +303,7 @@ Power-frame A .snd .has-top =
 Power-frame A .snd .⋃ k i = ∃Ω _ (λ j → k j i)
 Power-frame A .snd .⋃-lubs k = is-lub-pointwise _ _ λ _ →
   Props-has-lubs λ i → k i _
-Power-frame A .snd .⋃-distribl x f = funext λ i → Ω-ua
+Power-frame A .snd .⋃-distribl x f = ext λ i → biimp
   (rec! λ xi j j~i → inc (j , xi , j~i))
   (rec! λ j xi j~i → xi , inc (j , j~i))
 ```
diff --git a/src/Order/Frame/Free.lagda.md b/src/Order/Frame/Free.lagda.md
index 091e4f50a..3e7155410 100644
--- a/src/Order/Frame/Free.lagda.md
+++ b/src/Order/Frame/Free.lagda.md
@@ -79,7 +79,7 @@ Lower-sets-frame (P , L) = Lower-sets P , L↓-frame where
   L↓-frame .is-frame.has-top = Lower-sets-top P
   L↓-frame .is-frame.⋃ k = Lower-sets-cocomplete P k .Lub.lub
   L↓-frame .is-frame.⋃-lubs k = Lower-sets-cocomplete P k .Lub.has-lub
-  L↓-frame .is-frame.⋃-distribl x f = ext λ arg → Ω-ua
+  L↓-frame .is-frame.⋃-distribl x f = ext λ arg → biimp
     (rec! λ x≤a i fi≤a → inc (i , x≤a , fi≤a))
     (rec! λ i x≤a fi≤a → x≤a , inc (i , fi≤a))
 ```
diff --git a/src/Order/Instances/Props.lagda.md b/src/Order/Instances/Props.lagda.md
index 0e5d64d91..1645fe02c 100644
--- a/src/Order/Instances/Props.lagda.md
+++ b/src/Order/Instances/Props.lagda.md
@@ -44,7 +44,7 @@ Props .Poset._≤_ P Q = ∣ P ∣ → ∣ Q ∣
 Props .Poset.≤-thin = hlevel 1
 Props .Poset.≤-refl x = x
 Props .Poset.≤-trans g f x = f (g x)
-Props .Poset.≤-antisym = Ω-ua
+Props .Poset.≤-antisym p q = ext (biimp p q)
 ```
 
 The poset of propositions a top and bottom element, as well as