diff --git a/src/foundation-core/functoriality-dependent-function-types.lagda.md b/src/foundation-core/functoriality-dependent-function-types.lagda.md
index 38efcd3954..45742f0be8 100644
--- a/src/foundation-core/functoriality-dependent-function-types.lagda.md
+++ b/src/foundation-core/functoriality-dependent-function-types.lagda.md
@@ -86,13 +86,13 @@ htpy-precomp-Π H C h x = apd h (H x)
 abstract
   is-equiv-map-equiv-Π-equiv-family :
     {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-    (f : (i : I) → A i → B i) (is-equiv-f : is-fiberwise-equiv f) →
+    {f : (i : I) → A i → B i} (is-equiv-f : is-fiberwise-equiv f) →
     is-equiv (map-Π f)
-  is-equiv-map-equiv-Π-equiv-family f is-equiv-f =
+  is-equiv-map-equiv-Π-equiv-family is-equiv-f =
     is-equiv-is-contr-map
       ( λ g →
         is-contr-equiv' _
-          ( compute-fiber-map-Π f g)
+          ( compute-fiber-map-Π _ g)
           ( is-contr-Π (λ i → is-contr-map-is-equiv (is-equiv-f i) (g i))))
 
 equiv-Π-equiv-family :
@@ -101,7 +101,6 @@ equiv-Π-equiv-family :
 pr1 (equiv-Π-equiv-family e) = map-Π (λ i → map-equiv (e i))
 pr2 (equiv-Π-equiv-family e) =
   is-equiv-map-equiv-Π-equiv-family
-    ( λ i → map-equiv (e i))
     ( λ i → is-equiv-map-equiv (e i))
 ```
 
@@ -121,7 +120,7 @@ is-equiv-precomp-Π-fiber-condition {f = f} {C} H =
   is-equiv-comp
     ( map-reduce-Π-fiber f (λ b u → C b))
     ( map-Π (λ b u t → u))
-    ( is-equiv-map-equiv-Π-equiv-family (λ b u t → u) H)
+    ( is-equiv-map-equiv-Π-equiv-family H)
     ( is-equiv-map-reduce-Π-fiber f (λ b u → C b))
 ```
 
@@ -153,7 +152,7 @@ abstract
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {f : A → B}
   (H : is-equiv f) (C : B → UU l3)
   where
 
@@ -187,7 +186,7 @@ equiv-precomp-Π :
   (C : B → UU l3) → ((b : B) → C b) ≃ ((a : A) → C (map-equiv e a))
 pr1 (equiv-precomp-Π e C) = precomp-Π (map-equiv e) C
 pr2 (equiv-precomp-Π e C) =
-  is-equiv-precomp-Π-is-equiv (map-equiv e) (is-equiv-map-equiv e) C
+  is-equiv-precomp-Π-is-equiv (is-equiv-map-equiv e) C
 ```
 
 ## See also
diff --git a/src/foundation-core/functoriality-function-types.lagda.md b/src/foundation-core/functoriality-function-types.lagda.md
index d2b5d257ad..f300037a71 100644
--- a/src/foundation-core/functoriality-function-types.lagda.md
+++ b/src/foundation-core/functoriality-function-types.lagda.md
@@ -184,7 +184,7 @@ abstract
     (C : UU l3) → is-equiv (precomp f C)
   is-equiv-precomp-is-equiv f is-equiv-f =
     is-equiv-precomp-is-equiv-precomp-Π f
-      ( is-equiv-precomp-Π-is-equiv f is-equiv-f)
+      ( is-equiv-precomp-Π-is-equiv is-equiv-f)
 
   is-equiv-precomp-equiv :
     {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A ≃ B) →
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index c2b7519df1..865642c731 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -255,6 +255,7 @@ open import foundation.subtypes public
 open import foundation.subuniverses public
 open import foundation.surjective-maps public
 open import foundation.symmetric-binary-relations public
+open import foundation.symmetric-cores-binary-relations public
 open import foundation.symmetric-difference public
 open import foundation.symmetric-identity-types public
 open import foundation.symmetric-operations public
diff --git a/src/foundation/descent-equivalences.lagda.md b/src/foundation/descent-equivalences.lagda.md
index bbdbb52013..0d61ed3713 100644
--- a/src/foundation/descent-equivalences.lagda.md
+++ b/src/foundation/descent-equivalences.lagda.md
@@ -55,7 +55,6 @@ module _
     is-equiv-i is-equiv-k is-pb-rectangle =
     is-pullback-is-fiberwise-equiv-map-fiber-cone j h c
       ( map-inv-is-equiv-precomp-Π-is-equiv
-        ( i)
         ( is-equiv-i)
         ( λ y → is-equiv (map-fiber-cone j h c y))
         ( λ x → is-equiv-left-factor-htpy
diff --git a/src/foundation/equivalence-extensionality.lagda.md b/src/foundation/equivalence-extensionality.lagda.md
index 0014132b70..f8d6884464 100644
--- a/src/foundation/equivalence-extensionality.lagda.md
+++ b/src/foundation/equivalence-extensionality.lagda.md
@@ -65,7 +65,7 @@ module _
             ( is-equiv-tot-is-fiberwise-equiv
               ( λ h → funext (h ∘ f) id))
             ( is-contr-map-is-equiv
-              (( is-equiv-precomp-Π-is-equiv f H) (λ y → A))
+              ( is-equiv-precomp-Π-is-equiv H (λ y → A))
               ( id))))
         ( H)
 
diff --git a/src/foundation/functoriality-dependent-function-types.lagda.md b/src/foundation/functoriality-dependent-function-types.lagda.md
index 5f118b35ed..5d4ce207f6 100644
--- a/src/foundation/functoriality-dependent-function-types.lagda.md
+++ b/src/foundation/functoriality-dependent-function-types.lagda.md
@@ -71,13 +71,9 @@ module _
             ( map-equiv (f (map-inv-is-equiv (is-equiv-map-equiv e) a)))))
         ( precomp-Π (map-inv-is-equiv (is-equiv-map-equiv e)) B')
         ( is-equiv-precomp-Π-is-equiv
-          ( map-inv-is-equiv (is-equiv-map-equiv e))
           ( is-equiv-map-inv-is-equiv (is-equiv-map-equiv e))
           ( B'))
         ( is-equiv-map-equiv-Π-equiv-family
-          ( λ a →
-            ( tr B (is-section-map-inv-is-equiv (is-equiv-map-equiv e) a)) ∘
-            ( map-equiv (f (map-inv-is-equiv (is-equiv-map-equiv e) a))))
           ( λ a →
             is-equiv-comp
               ( tr B (is-section-map-inv-is-equiv (is-equiv-map-equiv e) a))
@@ -291,8 +287,8 @@ abstract
     is-equiv (map-automorphism-Π e f)
   is-equiv-map-automorphism-Π {B = B} e f =
     is-equiv-comp _ _
-      ( is-equiv-precomp-Π-is-equiv _ (is-equiv-map-equiv e) B)
-      ( is-equiv-map-equiv-Π-equiv-family _
+      ( is-equiv-precomp-Π-is-equiv (is-equiv-map-equiv e) B)
+      ( is-equiv-map-equiv-Π-equiv-family
         ( λ a → is-equiv-map-inv-is-equiv (is-equiv-map-equiv (f a))))
 
 automorphism-Π :
diff --git a/src/foundation/global-choice.lagda.md b/src/foundation/global-choice.lagda.md
index f249ded323..6606e5f019 100644
--- a/src/foundation/global-choice.lagda.md
+++ b/src/foundation/global-choice.lagda.md
@@ -45,7 +45,7 @@ abstract
   no-global-choice :
     {l : Level} → ¬ (Global-Choice l)
   no-global-choice f =
-    no-section-type-UU-Fin-two-ℕ
+    no-section-type-2-Element-Type
       ( λ X →
         f (pr1 X) (map-trunc-Prop (λ e → map-equiv e (zero-Fin 1)) (pr2 X)))
 ```
diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md
index b413b5fec1..3b0e0e540c 100644
--- a/src/foundation/homotopies.lagda.md
+++ b/src/foundation/homotopies.lagda.md
@@ -122,7 +122,7 @@ module _
   is-equiv-left-transpose-htpy-concat :
     is-equiv (left-transpose-htpy-concat H K L)
   is-equiv-left-transpose-htpy-concat =
-    is-equiv-map-equiv-Π-equiv-family _
+    is-equiv-map-equiv-Π-equiv-family
       ( λ x → is-equiv-left-transpose-eq-concat (H x) (K x) (L x))
 
   equiv-left-transpose-htpy-concat : ((H ∙h K) ~ L) ≃ (K ~ ((inv-htpy H) ∙h L))
@@ -132,7 +132,7 @@ module _
   is-equiv-right-transpose-htpy-concat :
     is-equiv (right-transpose-htpy-concat H K L)
   is-equiv-right-transpose-htpy-concat =
-    is-equiv-map-equiv-Π-equiv-family _
+    is-equiv-map-equiv-Π-equiv-family
       ( λ x → is-equiv-right-transpose-eq-concat (H x) (K x) (L x))
 
   equiv-right-transpose-htpy-concat : ((H ∙h K) ~ L) ≃ (H ~ (L ∙h (inv-htpy K)))
diff --git a/src/foundation/law-of-excluded-middle.lagda.md b/src/foundation/law-of-excluded-middle.lagda.md
index a082e117c8..2b19911c5f 100644
--- a/src/foundation/law-of-excluded-middle.lagda.md
+++ b/src/foundation/law-of-excluded-middle.lagda.md
@@ -50,5 +50,5 @@ abstract
   no-global-decidability :
     {l : Level} → ¬ ((X : UU l) → is-decidable X)
   no-global-decidability {l} d =
-    is-not-decidable-type-UU-Fin-two-ℕ (λ X → d (pr1 X))
+    is-not-decidable-type-2-Element-Type (λ X → d (pr1 X))
 ```
diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md
index a8d8a88cf0..535c72d886 100644
--- a/src/foundation/pullbacks.lagda.md
+++ b/src/foundation/pullbacks.lagda.md
@@ -442,7 +442,6 @@ htpy-eq-square-refl-htpy :
   tr-tr-c ＝ c' → htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c c'
 htpy-eq-square-refl-htpy f g c c' =
   map-inv-is-equiv-precomp-Π-is-equiv
-    ( λ (p : Id c c') → (tr-tr-refl-htpy-cone f g c) ∙ p)
     ( is-equiv-concat (tr-tr-refl-htpy-cone f g c) c')
     ( λ p → htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c c')
     ( htpy-eq-square f g c c')
@@ -455,7 +454,6 @@ comp-htpy-eq-square-refl-htpy :
   ( htpy-eq-square f g c c')
 comp-htpy-eq-square-refl-htpy f g c c' =
   is-section-map-inv-is-equiv-precomp-Π-is-equiv
-    ( λ (p : Id c c') → (tr-tr-refl-htpy-cone f g c) ∙ p)
     ( is-equiv-concat (tr-tr-refl-htpy-cone f g c) c')
     ( λ p → htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c c')
     ( htpy-eq-square f g c c')
@@ -694,7 +692,7 @@ abstract
       ( gap (map-Π f) (map-Π g) (cone-Π f g c))
       ( triangle-map-canonical-pullback-Π f g c)
       ( is-equiv-map-canonical-pullback-Π f g)
-      ( is-equiv-map-equiv-Π-equiv-family _ is-pb-c)
+      ( is-equiv-map-equiv-Π-equiv-family is-pb-c)
 ```
 
 ```agda
diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md
index e82afd02fc..c8b8c21737 100644
--- a/src/foundation/surjective-maps.lagda.md
+++ b/src/foundation/surjective-maps.lagda.md
@@ -273,7 +273,6 @@ abstract
         ( λ h y → (h y) ∘ unit-trunc-Prop)
         ( λ h y → const (type-trunc-Prop (fiber f y)) (type-Prop (P y)) (h y))
         ( is-equiv-map-equiv-Π-equiv-family
-          ( λ y p z → p)
           ( λ y →
             is-equiv-diagonal-is-contr
               ( is-proof-irrelevant-is-prop
@@ -281,7 +280,6 @@ abstract
                 ( is-surj-f y))
               ( type-Prop (P y))))
         ( is-equiv-map-equiv-Π-equiv-family
-          ( λ b g → g ∘ unit-trunc-Prop)
           ( λ b → is-propositional-truncation-trunc-Prop (fiber f b) (P b))))
       ( is-equiv-map-reduce-Π-fiber f ( λ y z → type-Prop (P y)))
 
diff --git a/src/foundation/symmetric-cores-binary-relations.lagda.md b/src/foundation/symmetric-cores-binary-relations.lagda.md
new file mode 100644
index 0000000000..d66db85e42
--- /dev/null
+++ b/src/foundation/symmetric-cores-binary-relations.lagda.md
@@ -0,0 +1,139 @@
+# Symmetric cores of binary relations
+
+```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module foundation.symmetric-cores-binary-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.mere-equivalences
+open import foundation.symmetric-binary-relations
+open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-dependent-function-types
+open import foundation.universal-property-dependent-pair-types
+open import foundation.universal-property-identity-systems
+open import foundation.universe-levels
+open import foundation.unordered-pairs
+
+open import univalent-combinatorics.2-element-types
+open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.universal-property-standard-finite-types
+```
+
+</details>
+
+## Idea
+
+The **symmetric core** of a [binary relation](foundation.binary-relations.md)
+`R : A → A → 𝒰` on a type `A` is a
+[symmetric binary relation](foundation.symmetric-binary-relations.md) `core R`
+equipped with a counit
+
+```text
+  (x y : A) → core R {x , y} → R x y
+```
+
+that satisfies the universal property of the symmetric core, i.e., it satisfies
+the property that for any symmetric relation `S : unordered-pair A → 𝒰`, the
+precomposition function
+
+```text
+  hom-Symmetric-Relation S (core R) → hom-Relation (rel S) R
+```
+
+is an [equivalence](foundation-core.equivalences.md). The symmetric core of a
+binary relation `R` is defined as the relation
+
+```text
+  core R (I,a) := (i : I) → R (a i) (a -i)
+```
+
+where `-i` is the element of the
+[2-element type](univalent-combinatorics.2-element-types.md) obtained by
+applying the swap [involution](foundation.involutions.md) to `i`. With this
+definition it is easy to see that the universal property of the adjunction
+should hold, since we have
+
+```text
+  ((I,a) → S (I,a) → core R (I,a)) ≃ ((x y : A) → S {x,y} → R x y).
+```
+
+## Definitions
+
+### The symmetric core of a binary relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  symmetric-core-Relation : Symmetric-Relation l2 A
+  symmetric-core-Relation p =
+    (i : type-unordered-pair p) →
+    R (element-unordered-pair p i) (other-element-unordered-pair p i)
+
+  counit-symmetric-core-Relation :
+    {x y : A} →
+    relation-Symmetric-Relation symmetric-core-Relation x y → R x y
+  counit-symmetric-core-Relation {x} {y} r =
+    tr
+      ( R x)
+      ( compute-other-element-standard-unordered-pair x y (zero-Fin 1))
+      ( r (zero-Fin 1))
+```
+
+## Properties
+
+### The universal property of the symmetric core of a binary relation
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (R : Relation l2 A)
+  (S : Symmetric-Relation l3 A)
+  where
+
+  map-universal-property-symmetric-core-Relation :
+    hom-Symmetric-Relation S (symmetric-core-Relation R) →
+    hom-Relation (relation-Symmetric-Relation S) R
+  map-universal-property-symmetric-core-Relation f x y s =
+    counit-symmetric-core-Relation R (f (standard-unordered-pair x y) s)
+
+  equiv-universal-property-symmetric-core-Relation :
+    hom-Symmetric-Relation S (symmetric-core-Relation R) ≃
+    hom-Relation (relation-Symmetric-Relation S) R
+  equiv-universal-property-symmetric-core-Relation =
+    ( equiv-Π-equiv-family
+      ( λ x →
+        equiv-Π-equiv-family
+          ( λ y →
+            equiv-postcomp
+              ( S (standard-unordered-pair x y))
+              ( equiv-tr
+                ( R _)
+                ( compute-other-element-standard-unordered-pair x y
+                  ( zero-Fin 1)))))) ∘e
+    ( equiv-dependent-universal-property-pointed-unordered-pairs
+      ( λ p i →
+        S p →
+        R (element-unordered-pair p i) (other-element-unordered-pair p i))) ∘e
+    ( equiv-Π-equiv-family (λ p → equiv-swap-Π))
+
+  universal-property-symmetric-core-Relation :
+    is-equiv map-universal-property-symmetric-core-Relation
+  universal-property-symmetric-core-Relation =
+    is-equiv-map-equiv
+      ( equiv-universal-property-symmetric-core-Relation)
+```
diff --git a/src/foundation/universal-property-identity-systems.lagda.md b/src/foundation/universal-property-identity-systems.lagda.md
index a31939e189..26d0970552 100644
--- a/src/foundation/universal-property-identity-systems.lagda.md
+++ b/src/foundation/universal-property-identity-systems.lagda.md
@@ -64,6 +64,15 @@ module _
         ( λ u → P (pr1 u) (pr2 u)))
       ( is-equiv-ev-pair)
 
+  equiv-dependent-universal-property-identity-system-is-torsorial :
+    is-torsorial B →
+    {l : Level} {C : (x : A) → B x → UU l} →
+    ((x : A) (y : B x) → C x y) ≃ C a b
+  pr1 (equiv-dependent-universal-property-identity-system-is-torsorial H) =
+    ev-refl-identity-system b
+  pr2 (equiv-dependent-universal-property-identity-system-is-torsorial H) =
+    dependent-universal-property-identity-system-is-torsorial H _
+
   is-torsorial-dependent-universal-property-identity-system :
     ({l3 : Level} → dependent-universal-property-identity-system l3 {A} {B} b) →
     is-torsorial B
diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md
index 90d997f279..02368d42fc 100644
--- a/src/foundation/universal-property-propositional-truncation.lagda.md
+++ b/src/foundation/universal-property-propositional-truncation.lagda.md
@@ -346,6 +346,5 @@ abstract
         ( λ h a p' → h (f a) p')
         ( is-ptr-f (pair (type-hom-Prop P' Q) (is-prop-type-hom-Prop P' Q)))
         ( is-equiv-map-equiv-Π-equiv-family
-          ( λ a g a' → g (f' a'))
           ( λ a → is-ptr-f' Q)))
 ```
diff --git a/src/foundation/unordered-pairs.lagda.md b/src/foundation/unordered-pairs.lagda.md
index 5108f25023..7ef302bbbb 100644
--- a/src/foundation/unordered-pairs.lagda.md
+++ b/src/foundation/unordered-pairs.lagda.md
@@ -15,11 +15,13 @@ open import foundation.decidable-equality
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
 open import foundation.function-extensionality
+open import foundation.functoriality-dependent-function-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopy-induction
 open import foundation.mere-equivalences
 open import foundation.propositional-truncations
 open import foundation.structure-identity-principle
+open import foundation.type-arithmetic-dependent-function-types
 open import foundation.universal-property-dependent-pair-types
 open import foundation.universe-levels
 
@@ -39,6 +41,7 @@ open import univalent-combinatorics.2-element-types
 open import univalent-combinatorics.equality-standard-finite-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.universal-property-standard-finite-types
 ```
 
 </details>
@@ -133,8 +136,8 @@ module _
   where
 
   element-standard-unordered-pair : Fin 2 → A
-  element-standard-unordered-pair (inl (inr star)) = x
-  element-standard-unordered-pair (inr star) = y
+  element-standard-unordered-pair =
+    map-inv-ev-zero-one-Fin-two-ℕ (λ _ → A) (x , y)
 
   standard-unordered-pair : unordered-pair A
   pr1 standard-unordered-pair = Fin-UU-Fin' 2
@@ -351,6 +354,70 @@ module _
       ( swap-standard-unordered-pair)
 ```
 
+### Dependent universal property of pointed unordered pairs
+
+We will construct an equivalence
+
+```text
+  ((p : unordered-pair A) (i : type p) → B p i) ≃ ((x y : A) → B {x,y} 0)
+```
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1}
+  (B : (p : unordered-pair A) → type-unordered-pair p → UU l2)
+  where
+
+  ev-pointed-unordered-pair :
+    ((p : unordered-pair A) (i : type-unordered-pair p) → B p i) →
+    ((x y : A) → B (standard-unordered-pair x y) (zero-Fin 1))
+  ev-pointed-unordered-pair f x y =
+    f (standard-unordered-pair x y) (zero-Fin 1)
+
+  abstract
+    dependent-universal-property-pointed-unordered-pairs :
+      is-equiv ev-pointed-unordered-pair
+    dependent-universal-property-pointed-unordered-pairs =
+      is-equiv-comp
+        ( λ f x y →
+          f (Fin-UU-Fin' 2) (element-standard-unordered-pair x y) (zero-Fin 1))
+        ( ev-pair)
+        ( is-equiv-ev-pair)
+        ( is-equiv-comp
+          ( λ f x y →
+            f ( Fin-UU-Fin' 2)
+              ( zero-Fin 1)
+              ( element-standard-unordered-pair x y))
+          ( map-Π (λ I → swap-Π))
+          ( is-equiv-map-equiv-Π-equiv-family
+            ( λ I → is-equiv-swap-Π))
+          ( is-equiv-comp
+            ( λ f x y → f (element-standard-unordered-pair x y))
+            ( λ f → f (Fin-UU-Fin' 2) (zero-Fin 1))
+            ( dependent-universal-property-identity-system-type-2-Element-Type
+              ( Fin-UU-Fin' 2)
+              ( zero-Fin 1)
+              ( λ I i → (a : type-2-Element-Type I → A) → B (I , a) i))
+            ( is-equiv-comp
+              ( ev-pair)
+              ( precomp-Π
+                ( λ xy → element-standard-unordered-pair (pr1 xy) (pr2 xy))
+                ( λ g → B (Fin-UU-Fin' 2 , g) (zero-Fin 1)))
+              ( is-equiv-precomp-Π-is-equiv
+                ( is-equiv-map-inv-dependent-universal-proeprty-Fin-two-ℕ
+                  ( λ _ → A))
+                ( λ g → B (Fin-UU-Fin' 2 , g) (zero-Fin 1)))
+              ( is-equiv-ev-pair))))
+
+  equiv-dependent-universal-property-pointed-unordered-pairs :
+    ((p : unordered-pair A) (i : type-unordered-pair p) → B p i) ≃
+    ((x y : A) → B (standard-unordered-pair x y) (zero-Fin 1))
+  pr1 equiv-dependent-universal-property-pointed-unordered-pairs =
+    ev-pointed-unordered-pair
+  pr2 equiv-dependent-universal-property-pointed-unordered-pairs =
+    dependent-universal-property-pointed-unordered-pairs
+```
+
 ### Functoriality of unordered pairs
 
 ```agda
diff --git a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
index 4a8e56bb7d..490acddf2b 100644
--- a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
@@ -447,7 +447,6 @@ module _
       ( λ j →
         is-emb-is-equiv
           ( is-equiv-map-equiv-Π-equiv-family
-            ( λ x → ap g)
             ( λ x → H (i x) (j (f x)))))
 ```
 
diff --git a/src/orthogonal-factorization-systems/local-types.lagda.md b/src/orthogonal-factorization-systems/local-types.lagda.md
index e52d5d5b75..2a0fd4d288 100644
--- a/src/orthogonal-factorization-systems/local-types.lagda.md
+++ b/src/orthogonal-factorization-systems/local-types.lagda.md
@@ -194,7 +194,7 @@ module _
   is-local-dependent-type-is-equiv :
     is-equiv f → {l : Level} (A : X → UU l) → is-local-dependent-type f A
   is-local-dependent-type-is-equiv is-equiv-f =
-    is-equiv-precomp-Π-is-equiv f is-equiv-f
+    is-equiv-precomp-Π-is-equiv is-equiv-f
 
   is-local-is-equiv :
     is-equiv f → {l : Level} (A : UU l) → is-local f A
diff --git a/src/synthetic-homotopy-theory/26-descent.lagda.md b/src/synthetic-homotopy-theory/26-descent.lagda.md
index df0287e179..8fa746d036 100644
--- a/src/synthetic-homotopy-theory/26-descent.lagda.md
+++ b/src/synthetic-homotopy-theory/26-descent.lagda.md
@@ -658,10 +658,11 @@ is-equiv-Fam-pushout-cocone-UU :
   is-equiv (Fam-pushout-cocone-UU l {f = f} {g})
 is-equiv-Fam-pushout-cocone-UU l {f = f} {g} =
   is-equiv-tot-is-fiberwise-equiv
-    ( λ PA → is-equiv-tot-is-fiberwise-equiv
-      ( λ PB → is-equiv-map-equiv-Π-equiv-family
-        ( λ s → equiv-eq)
-        ( λ s → univalence (PA (f s)) (PB (g s)))))
+    ( λ PA →
+      is-equiv-tot-is-fiberwise-equiv
+        ( λ PB →
+          is-equiv-map-equiv-Π-equiv-family
+            ( λ s → univalence (PA (f s)) (PB (g s)))))
 
 htpy-equiv-eq-ap-fam :
   {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x y : A} (p : Id x y) →
diff --git a/src/synthetic-homotopy-theory/26-id-pushout.lagda.md b/src/synthetic-homotopy-theory/26-id-pushout.lagda.md
index ea0054fd33..6caac8a020 100644
--- a/src/synthetic-homotopy-theory/26-id-pushout.lagda.md
+++ b/src/synthetic-homotopy-theory/26-id-pushout.lagda.md
@@ -209,7 +209,7 @@ is-equiv-hom-Fam-pushout-dependent-cocone :
 is-equiv-hom-Fam-pushout-dependent-cocone {f = f} {g} c P Q =
   is-equiv-tot-is-fiberwise-equiv (λ hA →
     is-equiv-tot-is-fiberwise-equiv (λ hB →
-      is-equiv-map-equiv-Π-equiv-family _
+      is-equiv-map-equiv-Π-equiv-family
         ( λ s → is-equiv-square-path-over-fam-maps
           ( pr2 (pr2 c) s)
           ( hA (f s))
diff --git a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md
index 9c3de244af..a9f82ff253 100644
--- a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md
@@ -117,7 +117,7 @@ abstract
       ( map-Π (λ x → map-raise))
       ( functor-free-dependent-loop l (λ x → map-raise))
       ( square-functor-free-dependent-loop l (λ x → map-raise))
-      ( is-equiv-map-equiv-Π-equiv-family _ (λ x → is-equiv-map-raise))
+      ( is-equiv-map-equiv-Π-equiv-family (λ x → is-equiv-map-raise))
       ( is-equiv-functor-free-dependent-loop-is-fiberwise-equiv l
         ( λ x → is-equiv-map-raise))
       ( dup-circle (λ x → raise l2 (P x)))
diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md
index 68e6cf1568..a91fe3874c 100644
--- a/src/univalent-combinatorics/2-element-types.lagda.md
+++ b/src/univalent-combinatorics/2-element-types.lagda.md
@@ -27,6 +27,7 @@ open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopies
+open import foundation.identity-systems
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.involutions
@@ -43,6 +44,7 @@ open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.type-arithmetic-empty-type
 open import foundation.type-arithmetic-unit-type
 open import foundation.unit-type
+open import foundation.universal-property-identity-systems
 open import foundation.universe-levels
 
 open import univalent-combinatorics.equality-standard-finite-types
@@ -102,6 +104,14 @@ standard-2-Element-Type l = Fin-UU-Fin l 2
 
 type-standard-2-Element-Type : (l : Level) → UU l
 type-standard-2-Element-Type l = type-2-Element-Type (standard-2-Element-Type l)
+
+zero-standard-2-Element-Type :
+  {l : Level} → type-standard-2-Element-Type l
+zero-standard-2-Element-Type = map-raise (zero-Fin 1)
+
+one-standard-2-Element-Type :
+  {l : Level} → type-standard-2-Element-Type l
+one-standard-2-Element-Type = map-raise (one-Fin 1)
 ```
 
 ## Properties
@@ -339,52 +349,71 @@ module _
 #### The type of pointed `2`-element types of any universe level is contractible
 
 ```agda
+Pointed-2-Element-Type : (l : Level) → UU (lsuc l)
+Pointed-2-Element-Type l = Σ (2-Element-Type l) type-2-Element-Type
+
 abstract
-  is-contr-total-UU-Fin-two-ℕ :
-    {l : Level} → is-contr (Σ (UU-Fin l 2) (type-UU-Fin 2))
-  is-contr-total-UU-Fin-two-ℕ {l} =
+  is-contr-pointed-2-Element-Type :
+    {l : Level} → is-contr (Pointed-2-Element-Type l)
+  is-contr-pointed-2-Element-Type {l} =
     is-contr-equiv'
-      ( Σ ( UU-Fin l 2)
-          ( λ X → raise-Fin l 2 ≃ type-UU-Fin 2 X))
+      ( Σ ( 2-Element-Type l)
+          ( equiv-2-Element-Type (standard-2-Element-Type l)))
       ( equiv-tot
         ( λ X →
           ( equiv-ev-zero-equiv-Fin-two-ℕ X) ∘e
           ( equiv-precomp-equiv (compute-raise-Fin l 2) (pr1 X))))
       ( is-contr-total-equiv-subuniverse
-        ( mere-equiv-Prop (Fin 2))
+        ( has-cardinality-Prop 2)
         ( standard-2-Element-Type l))
 ```
 
 #### Completing the characterization of the identity type of the type of `2`-element types of arbitrary universe level
 
 ```agda
-point-eq-UU-Fin-two-ℕ :
-  {l : Level} {X : UU-Fin l 2} →
-  standard-2-Element-Type l ＝ X → type-UU-Fin 2 X
-point-eq-UU-Fin-two-ℕ refl = map-raise (zero-Fin 1)
+point-eq-2-Element-Type :
+  {l : Level} {X : 2-Element-Type l} →
+  standard-2-Element-Type l ＝ X → type-2-Element-Type X
+point-eq-2-Element-Type refl = map-raise (zero-Fin 1)
 
 abstract
-  is-equiv-point-eq-UU-Fin-two-ℕ :
-    {l : Level} (X : UU-Fin l 2) →
-    is-equiv (point-eq-UU-Fin-two-ℕ {l} {X})
-  is-equiv-point-eq-UU-Fin-two-ℕ {l} =
+  is-equiv-point-eq-2-Element-Type :
+    {l : Level} (X : 2-Element-Type l) →
+    is-equiv (point-eq-2-Element-Type {l} {X})
+  is-equiv-point-eq-2-Element-Type {l} =
     fundamental-theorem-id
-      ( is-contr-total-UU-Fin-two-ℕ)
-      ( λ X → point-eq-UU-Fin-two-ℕ {l} {X})
-
-equiv-point-eq-UU-Fin-two-ℕ :
-  {l : Level} {X : UU-Fin l 2} →
-  (standard-2-Element-Type l ＝ X) ≃ type-UU-Fin 2 X
-pr1 (equiv-point-eq-UU-Fin-two-ℕ {l} {X}) =
-  point-eq-UU-Fin-two-ℕ
-pr2 (equiv-point-eq-UU-Fin-two-ℕ {l} {X}) =
-  is-equiv-point-eq-UU-Fin-two-ℕ X
-
-eq-point-UU-Fin-two-ℕ :
-  {l : Level} {X : UU-Fin l 2} →
-  type-UU-Fin 2 X → standard-2-Element-Type l ＝ X
-eq-point-UU-Fin-two-ℕ =
-  map-inv-equiv equiv-point-eq-UU-Fin-two-ℕ
+      ( is-contr-pointed-2-Element-Type)
+      ( λ X → point-eq-2-Element-Type {l} {X})
+
+equiv-point-eq-2-Element-Type :
+  {l : Level} {X : 2-Element-Type l} →
+  (standard-2-Element-Type l ＝ X) ≃ type-2-Element-Type X
+pr1 (equiv-point-eq-2-Element-Type {l} {X}) =
+  point-eq-2-Element-Type
+pr2 (equiv-point-eq-2-Element-Type {l} {X}) =
+  is-equiv-point-eq-2-Element-Type X
+
+eq-point-2-Element-Type :
+  {l : Level} {X : 2-Element-Type l} →
+  type-2-Element-Type X → standard-2-Element-Type l ＝ X
+eq-point-2-Element-Type =
+  map-inv-equiv equiv-point-eq-2-Element-Type
+
+is-identity-system-type-2-Element-Type :
+  {l1 l2 : Level} (X : 2-Element-Type l1) (x : type-2-Element-Type X) →
+  is-identity-system l2 (type-2-Element-Type {l1}) X x
+is-identity-system-type-2-Element-Type X x =
+  is-identity-system-is-torsorial X x (is-contr-pointed-2-Element-Type)
+
+dependent-universal-property-identity-system-type-2-Element-Type :
+  {l1 l2 : Level} (X : 2-Element-Type l1) (x : type-2-Element-Type X) →
+  dependent-universal-property-identity-system l2
+    { B = type-2-Element-Type {l1}}
+    { a = X}
+    ( x)
+dependent-universal-property-identity-system-type-2-Element-Type X x =
+  dependent-universal-property-identity-system-is-torsorial x
+    ( is-contr-pointed-2-Element-Type)
 ```
 
 ### For any `2`-element type `X`, the type of automorphisms on `X` is a `2`-element type
@@ -463,19 +492,19 @@ module _
 
 ```agda
 abstract
-  no-section-type-UU-Fin-two-ℕ :
-    {l : Level} → ¬ ((X : UU-Fin l 2) → type-UU-Fin 2 X)
-  no-section-type-UU-Fin-two-ℕ {l} f =
+  no-section-type-2-Element-Type :
+    {l : Level} → ¬ ((X : 2-Element-Type l) → type-2-Element-Type X)
+  no-section-type-2-Element-Type {l} f =
     is-not-contractible-Fin 2
       ( Eq-eq-ℕ)
       ( is-contr-equiv
         ( standard-2-Element-Type l ＝ standard-2-Element-Type l)
-        ( ( inv-equiv equiv-point-eq-UU-Fin-two-ℕ) ∘e
+        ( ( inv-equiv equiv-point-eq-2-Element-Type) ∘e
           ( compute-raise-Fin l 2))
         ( is-prop-is-contr
           ( pair
             ( standard-2-Element-Type l)
-            ( λ X → eq-point-UU-Fin-two-ℕ (f X)))
+            ( λ X → eq-point-2-Element-Type (f X)))
           ( standard-2-Element-Type l)
           ( standard-2-Element-Type l)))
 ```
@@ -484,11 +513,11 @@ abstract
 
 ```agda
 abstract
-  is-not-decidable-type-UU-Fin-two-ℕ :
+  is-not-decidable-type-2-Element-Type :
     {l : Level} →
-    ¬ ((X : UU-Fin l 2) → is-decidable (type-UU-Fin 2 X))
-  is-not-decidable-type-UU-Fin-two-ℕ {l} d =
-    no-section-type-UU-Fin-two-ℕ
+    ¬ ((X : 2-Element-Type l) → is-decidable (type-2-Element-Type X))
+  is-not-decidable-type-2-Element-Type {l} d =
+    no-section-type-2-Element-Type
       ( λ X →
         map-right-unit-law-coprod-is-empty
           ( pr1 X)
@@ -539,7 +568,7 @@ module _
   is-involution-aut-2-element-type e x =
     apply-universal-property-trunc-Prop
       ( has-two-elements-type-2-Element-Type X)
-      ( Id-Prop (set-UU-Fin 2 X) (map-equiv (e ∘e e) x) x)
+      ( Id-Prop (set-2-Element-Type X) (map-equiv (e ∘e e) x) x)
       ( λ h →
         ( ap (map-equiv (e ∘e e)) (inv (is-section-map-inv-equiv h x))) ∙
         ( ( ap (map-equiv e) (inv (is-section-map-inv-equiv h _))) ∙
diff --git a/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md b/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md
index 29a39526bd..3d655eb3b9 100644
--- a/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md
@@ -12,9 +12,14 @@ open import elementary-number-theory.natural-numbers
 open import foundation.cartesian-product-types
 open import foundation.contractible-types
 open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.equality-cartesian-product-types
 open import foundation.equivalences
+open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
+open import foundation.homotopies
+open import foundation.identity-types
 open import foundation.unit-type
 open import foundation.universal-property-empty-type
 open import foundation.universal-property-maybe
@@ -63,10 +68,84 @@ equiv-dependent-universal-property-Fin (succ-ℕ (succ-ℕ n)) A =
     ( equiv-dependent-universal-property-Fin (succ-ℕ n) (A ∘ inl))
     ( id-equiv)) ∘e
   ( equiv-dependent-universal-property-Maybe A)
+```
+
+### The dependent universal property of the standard 2-element type
+
+```agda
+module _
+  {l : Level} (A : Fin 2 → UU l)
+  where
+
+  ev-zero-one-Fin-two-ℕ :
+    ((i : Fin 2) → A i) → A (zero-Fin 1) × A (one-Fin 1)
+  pr1 (ev-zero-one-Fin-two-ℕ f) = f (zero-Fin 1)
+  pr2 (ev-zero-one-Fin-two-ℕ f) = f (one-Fin 1)
+
+  map-inv-ev-zero-one-Fin-two-ℕ :
+    A (zero-Fin 1) × A (one-Fin 1) → (i : Fin 2) → A i
+  map-inv-ev-zero-one-Fin-two-ℕ (x , y) (inl (inr star)) = x
+  map-inv-ev-zero-one-Fin-two-ℕ (x , y) (inr star) = y
+
+  is-section-map-inv-ev-zero-one-Fin-two-ℕ :
+    ev-zero-one-Fin-two-ℕ ∘ map-inv-ev-zero-one-Fin-two-ℕ ~ id
+  is-section-map-inv-ev-zero-one-Fin-two-ℕ (x , y) = refl
+
+  abstract
+    is-retraction-map-inv-ev-zero-one-Fin-two-ℕ :
+      map-inv-ev-zero-one-Fin-two-ℕ ∘ ev-zero-one-Fin-two-ℕ ~ id
+    is-retraction-map-inv-ev-zero-one-Fin-two-ℕ f =
+      eq-htpy
+        ( λ { (inl (inr star)) → refl ; (inr star) → refl})
+
+  dependent-universal-property-Fin-two-ℕ :
+    is-equiv ev-zero-one-Fin-two-ℕ
+  dependent-universal-property-Fin-two-ℕ =
+    is-equiv-is-invertible
+      map-inv-ev-zero-one-Fin-two-ℕ
+      is-section-map-inv-ev-zero-one-Fin-two-ℕ
+      is-retraction-map-inv-ev-zero-one-Fin-two-ℕ
+
+  is-equiv-map-inv-dependent-universal-proeprty-Fin-two-ℕ :
+    is-equiv map-inv-ev-zero-one-Fin-two-ℕ
+  is-equiv-map-inv-dependent-universal-proeprty-Fin-two-ℕ =
+    is-equiv-is-invertible
+      ev-zero-one-Fin-two-ℕ
+      is-retraction-map-inv-ev-zero-one-Fin-two-ℕ
+      is-section-map-inv-ev-zero-one-Fin-two-ℕ
+
+  equiv-dependent-universal-property-Fin-two-ℕ :
+    ((i : Fin 2) → A i) ≃ (A (zero-Fin 1) × A (one-Fin 1))
+  pr1 equiv-dependent-universal-property-Fin-two-ℕ =
+    ev-zero-one-Fin-two-ℕ
+  pr2 equiv-dependent-universal-property-Fin-two-ℕ =
+    dependent-universal-property-Fin-two-ℕ
+```
+
+### The universal property of the standard finite types
+
+```agda
+equiv-universal-property-Fin :
+  {l : Level} (n : ℕ) {X : UU l} →
+  (Fin n → X) ≃ iterated-prod n (λ _ → X)
+equiv-universal-property-Fin n =
+  equiv-dependent-universal-property-Fin n (λ _ → _)
+```
+
+### The universal property of the standard 2-element type
+
+```agda
+module _
+  {l : Level} {X : UU l}
+  where
+
+  universal-property-Fin-two-ℕ :
+    is-equiv (ev-zero-one-Fin-two-ℕ (λ _ → X))
+  universal-property-Fin-two-ℕ =
+    dependent-universal-property-Fin-two-ℕ (λ _ → X)
 
-equiv-dependent-universal-property-Fin-two-ℕ :
-  {l : Level} (A : Fin 2 → UU l) →
-  ((i : Fin 2) → A i) ≃ (A (zero-Fin 1) × A (one-Fin 1))
-equiv-dependent-universal-property-Fin-two-ℕ =
-  equiv-dependent-universal-property-Fin 2
+  equiv-universal-property-Fin-two-ℕ :
+    (Fin 2 → X) ≃ X × X
+  equiv-universal-property-Fin-two-ℕ =
+    equiv-dependent-universal-property-Fin-two-ℕ (λ _ → X)
 ```