diff --git a/Cubical/Data/Empty/Properties.agda b/Cubical/Data/Empty/Properties.agda
index bd3a473cd2..6da0851600 100644
--- a/Cubical/Data/Empty/Properties.agda
+++ b/Cubical/Data/Empty/Properties.agda
@@ -34,3 +34,11 @@ uninhabEquiv ¬a ¬b = isoToEquiv isom
   isom .inv b = rec (¬b b)
   isom .sec b = rec (¬b b)
   isom .ret a = rec (¬a a)
+
+uninhabEquiv⊥ : ∀ {ℓ} {A : Type ℓ}
+  → (A → ⊥) → A ≃ ⊥
+uninhabEquiv⊥ ¬a = uninhabEquiv ¬a (λ ())
+
+uninhabEquiv⊥* : ∀ {ℓ ℓ'} {A : Type ℓ}
+  → (A → ⊥) → A ≃ ⊥* {ℓ'}
+uninhabEquiv⊥* ¬a = uninhabEquiv ¬a (λ ())
diff --git a/Cubical/Data/IterativeSets/OrderedPair.agda b/Cubical/Data/IterativeSets/OrderedPair.agda
index 483a4b9f12..ff609ec064 100644
--- a/Cubical/Data/IterativeSets/OrderedPair.agda
+++ b/Cubical/Data/IterativeSets/OrderedPair.agda
@@ -9,6 +9,7 @@ open import Cubical.Foundations.Prelude
 
 open import Cubical.Functions.Embedding
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
@@ -40,33 +41,60 @@ private
                             (singleton⁰ (singleton⁰ y))
                             unorderedPair⁰≢singleton⁰
 
+orderedPair⁰≡orderedPair⁰ : {x y a b : V⁰ {ℓ}} → ((⟨ x , y ⟩⁰ ≡ ⟨ a , b ⟩⁰) ≃ ((x ≡ a) × (y ≡ b)))
+orderedPair⁰≡orderedPair⁰ {ℓ = ℓ} {x = x} {y = y} {a = a} {b = b} = compEquiv (compEquiv (compEquiv step₁ step₂) step₃) step₄
+  where
+    step₁ : (⟨ x , y ⟩⁰ ≡ ⟨ a , b ⟩⁰)
+            ≃
+            (unorderedPair⁰ (singleton⁰ x) empty⁰ singleton⁰≢empty⁰ ≡ unorderedPair⁰ (singleton⁰ a) empty⁰ singleton⁰≢empty⁰)
+            × (singleton⁰ (singleton⁰ y) ≡ singleton⁰ (singleton⁰ b))
+    step₁ = unorderedPair⁰≡unorderedPair⁰' {x = unorderedPair⁰ (singleton⁰ x) empty⁰ (singleton⁰≢empty⁰ {x = x})}
+                                           {y = singleton⁰ (singleton⁰ y)}
+                                           {a = unorderedPair⁰ (singleton⁰ a) empty⁰ (singleton⁰≢empty⁰ {x = a})}
+                                           {b = singleton⁰ (singleton⁰ b)}
+                                           {x≢y = unorderedPair⁰≢singleton⁰}
+                                           {a≢b = unorderedPair⁰≢singleton⁰}
+                                           unorderedPair⁰≢singleton⁰
+
+    step₂ : (unorderedPair⁰ (singleton⁰ x) empty⁰ singleton⁰≢empty⁰ ≡ unorderedPair⁰ (singleton⁰ a) empty⁰ singleton⁰≢empty⁰)
+            × (singleton⁰ (singleton⁰ y) ≡ singleton⁰ (singleton⁰ b))
+            ≃
+            (((singleton⁰ x ≡ singleton⁰ a) × (empty⁰ {ℓ} ≡ empty⁰))
+              × ((singleton⁰ y ≡ singleton⁰ b)))
+    step₂ = ≃-× (unorderedPair⁰≡unorderedPair⁰' {x = singleton⁰ x}
+                                                         {y = empty⁰}
+                                                         {a = singleton⁰ a}
+                                                         {b = empty⁰}
+                                                         {x≢y = singleton⁰≢empty⁰ {x = x}}
+                                                         {a≢b = singleton⁰≢empty⁰ {x = a}}
+                                                         (singleton⁰≢empty⁰ {x = x}))
+                (invEquiv (singleton⁰≡singleton⁰ {x = singleton⁰ y} {y = singleton⁰ b}))
+
+    step₃ : (((singleton⁰ x ≡ singleton⁰ a) × (empty⁰ {ℓ} ≡ empty⁰))
+              × ((singleton⁰ y ≡ singleton⁰ b)))
+            ≃
+            ((singleton⁰ x ≡ singleton⁰ a) × (singleton⁰ y ≡ singleton⁰ b))
+    step₃ = ≃-× (Σ-contractSnd (λ _ → inhProp→isContr refl (isSetV⁰ empty⁰ empty⁰)))
+                (idEquiv (singleton⁰ y ≡ singleton⁰ b))
+    step₄ : ((singleton⁰ x ≡ singleton⁰ a) × (singleton⁰ y ≡ singleton⁰ b))
+            ≃
+            ((x ≡ a) × (y ≡ b))
+    step₄ = ≃-× (invEquiv (singleton⁰≡singleton⁰ {x = x} {y = a}))
+                (invEquiv (singleton⁰≡singleton⁰ {x = y} {y = b}))
+
 orderedPair⁰ : (V⁰ {ℓ} × V⁰ {ℓ}) → V⁰ {ℓ}
 orderedPair⁰ = uncurry ⟨_,_⟩⁰
 
 isEmbOrderedPair⁰ : isEmbedding (orderedPair⁰ {ℓ})
-isEmbOrderedPair⁰ {ℓ} = injEmbedding isSetV⁰ inj
-    where
-        inj : {s t : V⁰ {ℓ} × V⁰ {ℓ}} → orderedPair⁰ s ≡ orderedPair⁰ t → s ≡ t
-        inj {s = x , y} {t = a , b} p = ΣPathP (helper (unorderedPair⁰≡unorderedPair⁰ .fst p))
-            where
-                x≡a-helper : ((singleton⁰ x ≡ singleton⁰ a) × (empty⁰ {ℓ} ≡ empty⁰ {ℓ}))
-                              ⊎ ((singleton⁰ x ≡ empty⁰) × (empty⁰ ≡ singleton⁰ a))
-                             → x ≡ a
-                x≡a-helper (inl (p , _)) = invEq singleton⁰≡singleton⁰ p
-                x≡a-helper (inr (p , _)) = ⊥-elim (singleton⁰≢empty⁰ p)
-                helper : ((unorderedPair⁰ (singleton⁰ x) empty⁰ singleton⁰≢empty⁰
-                               ≡ unorderedPair⁰ (singleton⁰ a) empty⁰ singleton⁰≢empty⁰)
-                             × (singleton⁰ (singleton⁰ y) ≡ singleton⁰ (singleton⁰ b)))
-                           ⊎ ((unorderedPair⁰ (singleton⁰ x) empty⁰ singleton⁰≢empty⁰ ≡ singleton⁰ (singleton⁰ b))
-                             × (singleton⁰ (singleton⁰ y) ≡ unorderedPair⁰ (singleton⁰ a) empty⁰ singleton⁰≢empty⁰))
-                          → ((x ≡ a) × (y ≡ b))
-                helper (inl (u , s)) .fst = x≡a-helper (unorderedPair⁰≡unorderedPair⁰ .fst u)
-                helper (inl (u , s)) .snd = invEq singleton⁰≡singleton⁰ (invEq singleton⁰≡singleton⁰ s)
-                helper (inr (p , _)) = ⊥-elim {A = λ _ → (x ≡ a) × (y ≡ b)} (unorderedPair⁰≢singleton⁰ p)
+isEmbOrderedPair⁰ s t = E .snd
+  where
+    F : ((s .fst ≡ t .fst) × (s .snd ≡ t .snd)) ≃ (orderedPair⁰ s ≡ orderedPair⁰ t)
+    F = propBiimpl→Equiv (isProp× (isSetV⁰ (s .fst) (t .fst))
+                                  (isSetV⁰ (s .snd) (t .snd)))
+                         (isSetV⁰ (orderedPair⁰ s) (orderedPair⁰ t))
+                         (λ P i → ⟨ P .fst i , P .snd i ⟩⁰)
+                         (orderedPair⁰≡orderedPair⁰ .fst)
+     -- invEquiv (orderedPair⁰≡orderedPair⁰ {x = s .fst} {y = s .snd} {a = t .fst} {b = t .snd})
 
-orderedPair⁰≡orderedPair⁰ : {x y a b : V⁰ {ℓ}} → ((⟨ x , y ⟩⁰ ≡ ⟨ a , b ⟩⁰) ≃ ((x ≡ a) × (y ≡ b)))
-orderedPair⁰≡orderedPair⁰ {x = x} {y = y} {a = a} {b = b} = propBiimpl→Equiv
-                                          (isSetV⁰ _ _)
-                                          (isProp× (isSetV⁰ _ _) (isSetV⁰ _ _))
-                                          (PathPΣ ∘ (isEmbedding→Inj isEmbOrderedPair⁰ (x , y) (a , b)))
-                                          (λ (x≡a , y≡b) → cong ⟨_, y ⟩⁰ x≡a ∙ cong ⟨ a ,_⟩⁰ y≡b)
+    E : (s ≡ t) ≃ (orderedPair⁰ s ≡ orderedPair⁰ t)
+    E = compEquiv (isoToEquiv (invIso (ΣPathPIsoPathPΣ {x = s} {y = t}))) F
diff --git a/Cubical/Data/IterativeSets/Pi.agda b/Cubical/Data/IterativeSets/Pi.agda
new file mode 100644
index 0000000000..d7499d400b
--- /dev/null
+++ b/Cubical/Data/IterativeSets/Pi.agda
@@ -0,0 +1,142 @@
+{-# OPTIONS --lossy-unification #-}
+
+module Cubical.Data.IterativeSets.Pi where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
+open import Cubical.Data.Sigma
+open import Cubical.Functions.Embedding
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Homotopy.Base
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.IterativeMultisets.Base renaming (index to index∞ ; elements to elements-V∞)
+open import Cubical.Data.IterativeSets.Base
+open import Cubical.Data.IterativeSets.OrderedPair
+
+private
+  module _ {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) where
+    Inj : Type (ℓ-max ℓ ℓ')
+    Inj = {x y : A} → f x ≡ f y → x ≡ y
+
+module GraphElements {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ {ℓ} x → V⁰ {ℓ}} where
+  graphEl⁰ : ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → El⁰ x → V⁰ {ℓ}
+  graphEl⁰ Φ a = ⟨ elements x a , elements (y a) (Φ a) ⟩⁰
+
+  module FstConst (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) where
+    -- this is the same as graphEl⁰
+    graphEl⁰' : El⁰ x → V⁰ {ℓ}
+    graphEl⁰' = graphEl⁰ Φ
+
+    inj : Inj graphEl⁰'
+    inj {a} {b} p = isEmbedding→Inj
+                      {A = El⁰ x} {B = V⁰ {ℓ}} {f = elements x}
+                      (isEmbedding-elements x) a b
+                        (fst (orderedPair⁰≡orderedPair⁰
+                          {x = elements x a} {y = elements (y a) (Φ a)}
+                          {a = elements x b} {b = elements (y b) (Φ b)} .fst p))
+
+    emb : isEmbedding graphEl⁰'
+    emb = injEmbedding {A = El⁰ x} {B = V⁰ {ℓ}} isSetV⁰ inj
+
+  graphEl⁰-inj' : (Φ Ψ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) (a : El⁰ x)
+                   → graphEl⁰ Φ ≡ graphEl⁰ Ψ → Φ a ≡ Ψ a
+  graphEl⁰-inj' Φ Ψ a p = isEmbedding→Inj {A = index (y a)} {B = V⁰}
+                                          (isEmbedding-elements (y a)) (Φ a) (Ψ a) els≡₂
+    where
+      p' : graphEl⁰ Φ a ≡ graphEl⁰ Ψ a
+      p' = funExt⁻ p a
+
+      els≡ : (elements x a ≡ elements x a) ×
+         (elements (y a) (Φ a) ≡ elements (y a) (Ψ a))
+      els≡ = orderedPair⁰≡orderedPair⁰ {x = elements x a} {y = elements (y a) (Φ a)}
+                                    {a = elements x a} {b = elements (y a) (Ψ a)} .fst p'
+      els≡₂ : elements (y a) (Φ a) ≡ elements (y a) (Ψ a)
+      els≡₂ = els≡ .snd
+
+  graphEl⁰-inj : Inj graphEl⁰
+  graphEl⁰-inj {Φ} {Ψ} p = funExt λ a → graphEl⁰-inj' Φ Ψ a p
+
+  graphEl⁰-emb : isEmbedding graphEl⁰
+  graphEl⁰-emb = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = El⁰ x → V⁰} {f = graphEl⁰}
+                              (isSet→ {A' = V⁰ {ℓ}} {A = El⁰ {ℓ} x} (isSetV⁰ {ℓ})) graphEl⁰-inj
+
+module Graph {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ {ℓ} x → V⁰ {ℓ}} where
+  open GraphElements {ℓ} {x} {y}
+
+  graph⁰ : ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → V⁰ {ℓ}
+  graph⁰ Φ = fromEmb E
+    where
+      E : Embedding V⁰ ℓ
+      E .fst = El⁰ x
+      E .snd .fst = FstConst.graphEl⁰' Φ
+      E .snd .snd = FstConst.emb Φ
+
+  graph⁰-inj : Inj graph⁰
+  graph⁰-inj {Φ} {Ψ} p = graphEl⁰-inj P
+    where
+      F : ((z : V⁰) → z ∈⁰ graph⁰ Φ → z ∈⁰ graph⁰ Ψ)
+           × ((z : V⁰) → z ∈⁰ graph⁰ Ψ → z ∈⁰ graph⁰ Φ)
+      F = ≡V⁰-≃-≃V⁰ {x = graph⁰ Φ} {y = graph⁰ Ψ} .fst p
+
+      F₂ : (z : V⁰) → z ∈⁰ graph⁰ Ψ → z ∈⁰ graph⁰ Φ
+      F₂ = F .snd
+
+      module _ (a : El⁰ x) where
+        s : V⁰
+        s = graphEl⁰ Ψ a
+
+        s∈Ψ : s ∈⁰ graph⁰ Ψ
+        s∈Ψ .fst = a
+        s∈Ψ .snd = refl
+
+        s∈Φ : s ∈⁰ graph⁰ Φ
+        s∈Φ = F₂ s s∈Ψ
+
+        a' : El⁰ x
+        a' = s∈Φ .fst
+
+        graphEl⁰≡' : graphEl⁰ Φ a' ≡ graphEl⁰ Ψ a
+        graphEl⁰≡' = s∈Φ .snd
+
+        els≡ : elements x a' ≡ elements x a
+        els≡ = orderedPair⁰≡orderedPair⁰ {x = elements x a'} {y = elements (y a') (Φ a')}
+                                         {a = elements x a } {b = elements (y a)  (Ψ a) } .fst graphEl⁰≡' .fst
+
+        a'≡a : a' ≡ a
+        a'≡a = isEmbedding→Inj {A = El⁰ x} {B = V⁰ {ℓ}} {f = elements x}
+                (isEmbedding-elements x) a' a els≡
+
+        graphEl⁰≡ : graphEl⁰ Φ a ≡ graphEl⁰ Ψ a
+        graphEl⁰≡ = subst (λ m → graphEl⁰ Φ m ≡ graphEl⁰ Ψ a) a'≡a graphEl⁰≡'
+
+      P : graphEl⁰ Φ ≡ graphEl⁰ Ψ
+      P = funExt graphEl⁰≡
+
+  graph⁰-emb : isEmbedding graph⁰
+  graph⁰-emb = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = V⁰} {f = graph⁰} (isSetV⁰ {ℓ}) graph⁰-inj
+
+private
+  variable
+    ℓ : Level
+    x : V⁰ {ℓ}
+    y : El⁰ x → V⁰ {ℓ}
+
+Π⁰ : (x : V⁰ {ℓ}) → (El⁰ x → V⁰ {ℓ}) → V⁰ {ℓ}
+Π⁰ {ℓ} x y = fromEmb E
+  where
+    E : Embedding V⁰ ℓ
+    E .fst = (a : El⁰ x) → El⁰ (y a)
+    E .snd .fst = Graph.graph⁰ {ℓ} {x} {y}
+    E .snd .snd = Graph.graph⁰-emb {ℓ} {x} {y}
+
+El⁰Π⁰isΠ : El⁰ (Π⁰ x y) ≡ ((a : El⁰ x) → El⁰ (y a))
+El⁰Π⁰isΠ = refl
+
+_→⁰_ : V⁰ {ℓ} → V⁰ {ℓ} → V⁰ {ℓ}
+x →⁰ y = Π⁰ x (λ _ → y)
+
+El⁰→⁰is→ : {x y : V⁰ {ℓ}} → El⁰ (x →⁰ y) ≡ (El⁰ x → El⁰ y)
+El⁰→⁰is→ = refl
diff --git a/Cubical/Data/IterativeSets/UnorderedPair/Base.agda b/Cubical/Data/IterativeSets/UnorderedPair/Base.agda
index 5def6ace84..34e5f68cd6 100644
--- a/Cubical/Data/IterativeSets/UnorderedPair/Base.agda
+++ b/Cubical/Data/IterativeSets/UnorderedPair/Base.agda
@@ -1,5 +1,3 @@
-{-# OPTIONS --lossy-unification #-}
-
 module Cubical.Data.IterativeSets.UnorderedPair.Base where
 
 open import Cubical.Foundations.Prelude
@@ -8,8 +6,10 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Univalence
 open import Cubical.Functions.Embedding
 open import Cubical.Data.Sum
+open import Cubical.Data.Sum.Properties
 open import Cubical.Data.Bool
 open import Cubical.Data.Sigma
 open import Cubical.Data.Empty renaming (elim to ⊥-elim)
@@ -21,13 +21,6 @@ private
   variable
     ℓ : Level
 
--- TODO: (possibly) rename and move
-private
-    module _ where
-        ≢-move-i0→i : {ℓ : Level} {A : Type ℓ} {x y a b : A} (p : x ≡ a) (q : y ≡ b)
-                       (i : I) → ¬ (x ≡ y) → ¬ (p i ≡ q i)
-        ≢-move-i0→i p q i x≢y pi≡qi = x≢y ((λ j → p (i ∧ j)) ∙∙ pi≡qi ∙∙ λ j → q (i ∧ ~ j))
-
 unorderedPair⁰ : (x y : V⁰ {ℓ}) → ¬ (x ≡ y) → V⁰ {ℓ}
 unorderedPair⁰ {ℓ} x y x≢y = fromEmb emb
     where
@@ -99,41 +92,76 @@ unorderedPair⁰-≢-witness-agnostic {x = x} {y = y} x≢y₁ x≢y₂ = cong (
         x≢y₁≡x≢y₂ : x≢y₁ ≡ x≢y₂
         x≢y₁≡x≢y₂ = isProp→ (λ ()) x≢y₁ x≢y₂
 
+private
+  -- maybe switch a and x, as well as b and y to make it closer to the place where we use it later
+  module _ {A : Type ℓ} (a b x y : A) (a≢b : ¬ a ≡ b) where
+    ⊎-×-≡-distr : Iso (((a ≡ x) ⊎ (a ≡ y))
+                        × ((b ≡ x) ⊎ (b ≡ y)))
+                      (((a ≡ x) × (b ≡ y))
+                        ⊎ ((a ≡ y) × (b ≡ x)))
+    ⊎-×-≡-distr .Iso.fun (inl a≡x , inl b≡x) = ⊥-elim (a≢b (a≡x ∙ sym b≡x))
+    ⊎-×-≡-distr .Iso.fun (inl a≡x , inr b≡y) = inl (a≡x , b≡y)
+    ⊎-×-≡-distr .Iso.fun (inr a≡y , inl b≡x) = inr (a≡y , b≡x)
+    ⊎-×-≡-distr .Iso.fun (inr a≡y , inr b≡y) = ⊥-elim (a≢b (a≡y ∙ sym b≡y))
+
+    ⊎-×-≡-distr .Iso.inv (inl (a≡x , b≡y)) .fst = inl a≡x
+    ⊎-×-≡-distr .Iso.inv (inl (a≡x , b≡y)) .snd = inr b≡y
+    ⊎-×-≡-distr .Iso.inv (inr (a≡y , b≡x)) .fst = inr a≡y
+    ⊎-×-≡-distr .Iso.inv (inr (a≡y , b≡x)) .snd = inl b≡x
+
+    ⊎-×-≡-distr .Iso.sec (inl _) = refl
+    ⊎-×-≡-distr .Iso.sec (inr _) = refl
+
+    ⊎-×-≡-distr .Iso.ret (inl a≡x , inl b≡x) = ⊥-elim {A = λ _ → ⊎-×-≡-distr .Iso.inv (⊎-×-≡-distr .Iso.fun (inl a≡x , inl b≡x)) ≡ (inl a≡x , inl b≡x)} (a≢b (a≡x ∙ sym b≡x))
+    ⊎-×-≡-distr .Iso.ret (inl x , inr x₁) = refl
+    ⊎-×-≡-distr .Iso.ret (inr x , inl x₁) = refl
+    ⊎-×-≡-distr .Iso.ret (inr a≡y , inr b≡y) = ⊥-elim {A = λ _ → Iso.inv ⊎-×-≡-distr (Iso.fun ⊎-×-≡-distr (inr a≡y , inr b≡y))
+      ≡ (inr a≡y , inr b≡y)} (a≢b (a≡y ∙ sym b≡y))
+
 unorderedPair⁰≡unorderedPair⁰ : {x y a b : V⁰ {ℓ}} {x≢y : ¬ (x ≡ y)} {a≢b : ¬ (a ≡ b)}
                                 → ((unorderedPair⁰ x y x≢y ≡ unorderedPair⁰ a b a≢b)
                                     ≃ (((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a))))
 unorderedPair⁰≡unorderedPair⁰ {x = x} {y = y} {a = a} {b = b} {x≢y = x≢y} {a≢b = a≢b}
-                                              = propBiimpl→Equiv (isSetV⁰ _ _) isPropRHS f g
-    where
-       isPropRHS : isProp (((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a)))
-       isPropRHS = isProp⊎ (isProp× (isSetV⁰ _ _) (isSetV⁰ _ _))
-                           (isProp× (isSetV⁰ _ _) (isSetV⁰ _ _))
-                           (λ (x≡a , _) (_ , y≡a) → x≢y (x≡a ∙ (sym y≡a)))
-
-       destruct : (unorderedPair⁰ x y _ ≡ unorderedPair⁰ a b _)
-                    → ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b))
-       destruct p .fst = unorderedPair⁰-is-unordered-pair-sym .fst
-                                    (≡V⁰-≃-≃V⁰ .fst p .fst x (lift false , refl))
-       destruct p .snd = unorderedPair⁰-is-unordered-pair-sym .fst
-                                    (≡V⁰-≃-≃V⁰ .fst p .fst y (lift true , refl))
-
-       filter : ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b))
-                  → ((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a))
-       filter (inl x≡a , inl y≡a) = ⊥-elim (x≢y (x≡a ∙ (sym y≡a)))
-       filter (inl x≡a , inr y≡b) = inl (x≡a , y≡b)
-       filter (inr x≡b , inl y≡a) = inr (x≡b , y≡a)
-       filter (inr x≡b , inr y≡b) = ⊥-elim (x≢y (x≡b ∙ (sym y≡b)))
-
-       f : unorderedPair⁰ x y _ ≡ unorderedPair⁰ a b _
-             → ((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a))
-       f = filter ∘ destruct
-
-       -- TODO: make more efficient somehow
-       g : ((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a)) → unorderedPair⁰ x y _ ≡ unorderedPair⁰ a b _
-       g (inl (x≡a , y≡b)) = unorderedPair⁰-≢-witness-agnostic x≢y _
-                               ∙∙ (λ i → unorderedPair⁰ (x≡a i) (y≡b i) (≢-move-i0→i x≡a y≡b i x≢y))
-                               ∙∙ unorderedPair⁰-≢-witness-agnostic _ a≢b
-       g (inr (x≡b , y≡a)) = (unorderedPair⁰-≢-witness-agnostic x≢y _
-                               ∙∙ (λ i → unorderedPair⁰ (x≡b i) (y≡a i) (≢-move-i0→i x≡b y≡a i x≢y))
-                               ∙∙ unorderedPair⁰-≢-witness-agnostic _ (λ b≡a → a≢b (sym b≡a)))
-                             ∙ unorderedUnorderedPair⁰
+                                              = compEquiv (compEquiv ≡V⁰-≃-≃V⁰' (compEquiv L M)) (isoToEquiv (⊎-×-≡-distr x y a b x≢y))
+  where
+    L : ((z : V⁰) → (z ∈⁰ unorderedPair⁰ x y x≢y) ≃ (z ∈⁰ unorderedPair⁰ a b a≢b))
+          ≃
+        ((z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b)))
+    L = equivΠCod (λ z → equivComp unorderedPair⁰-is-unordered-pair-sym
+                                    unorderedPair⁰-is-unordered-pair-sym)
+
+    M : ((z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b)))
+           ≃
+         ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b))
+    M = propBiimpl→Equiv propLHS propRHS f g
+      where
+        propLHS : isProp ((z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b)))
+        propLHS = isPropΠ (λ z → isOfHLevel≃ 1
+                    (isProp⊎ (isSetV⁰ z x) (isSetV⁰ z y) (λ z≡x z≡y → x≢y (sym z≡x ∙ z≡y)))
+                    (isProp⊎ (isSetV⁰ z a) (isSetV⁰ z b) (λ z≡a z≡b → a≢b (sym z≡a ∙ z≡b))))
+
+        propRHS : isProp (((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b)))
+        propRHS = isProp× (isProp⊎ (isSetV⁰ x a) (isSetV⁰ x b) (λ x≡a x≡b → a≢b (sym x≡a ∙ x≡b)))
+                          (isProp⊎ (isSetV⁰ y a) (isSetV⁰ y b) (λ y≡a y≡b → a≢b (sym y≡a ∙ y≡b)))
+
+        f : ((z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b))) →
+             ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b))
+        f E .fst = E x .fst (inl refl)
+        f E .snd = E y .fst (inr refl)
+
+        g : ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b)) →
+             (z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b))
+        g (inl x≡a , inl y≡a) = ⊥-elim (x≢y (x≡a ∙ sym y≡a))
+        g (inl x≡a , inr y≡b) z = pathToEquiv (λ i → (z ≡ x≡a i) ⊎ (z ≡ y≡b i))
+        g (inr x≡b , inl y≡a) z = compEquiv (pathToEquiv (λ i → (z ≡ x≡b i) ⊎ (z ≡ y≡a i))) ⊎-swap-≃
+        g (inr x≡b , inr y≡b) = ⊥-elim (x≢y (x≡b ∙ sym y≡b))
+
+unorderedPair⁰≡unorderedPair⁰' : {x y a b : V⁰ {ℓ}} {x≢y : ¬ (x ≡ y)} {a≢b : ¬ (a ≡ b)}
+                                → ¬ x ≡ b
+                                → (unorderedPair⁰ x y x≢y ≡ unorderedPair⁰ a b a≢b)
+                                  ≃
+                                  ((x ≡ a) × (y ≡ b))
+unorderedPair⁰≡unorderedPair⁰' {x = x} {y = y} {a = a} {b = b} x≢b = compEquiv unorderedPair⁰≡unorderedPair⁰
+                                                                    (compEquiv (⊎-equiv (idEquiv ((x ≡ a) × (y ≡ b)))
+                                                                                        (uninhabEquiv⊥ (λ p → x≢b (p .fst))))
+                                                                               ⊎-IdR-⊥-≃)