This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Symmetric cores of binary relations

module foundation.symmetric-cores-binary-relations where

open import foundation.binary-relations
open import foundation.morphisms-binary-relations
open import foundation.postcomposition-functions
open import foundation.symmetric-binary-relations
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-dependent-function-types
open import foundation.universe-levels
open import foundation.unordered-pairs

open import foundation-core.equivalences
open import foundation-core.functoriality-dependent-function-types

open import univalent-combinatorics.standard-finite-types

Idea

The symmetric core of a binary relation R : A → A → 𝒰 on a type A is a symmetric binary relation core R equipped with a counit

  (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

  hom-Symmetric-Relation S (core R) → hom-Relation (rel S) R

is an equivalence. The symmetric core of a binary relation R is defined as the relation

  core R (I,a) := (i : I) → R (a i) (a -i)

where -i is the element of the 2-element type obtained by applying the swap involution to i. With this definition it is easy to see that the universal property of the adjunction should hold, since we have

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

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 ))
      ( r (zero-Fin ))

Properties

The universal property of the symmetric core of a binary relation

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