Symmetric core of a relation

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

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) →

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

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

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)
 

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-Π :

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)))
 ```

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)))

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))
 ```

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

src/foundation/surjective-maps.lagda.md

@@ -273,15 +273,13 @@ 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
                 ( is-prop-type-trunc-Prop)
                 ( 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)))
 

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 satisfyies the universal property of the symmetric core, i.e., it satisfies
+the property that for any symmetric relation `S : unordered-pair A → 𝒰` such
+that 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)
+```

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

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)))
 ```