Symmetric core of a relation (#754)

In this PR we construct the symmetric core of a type valued relation and
show that it is the right adjoint of the restriction functor from
symmetric relations to relations. Everything we do in this PR is fully
coherent and untruncated.

---------

Co-authored-by: Fredrik Bakke <[email protected]>

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

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