Symmetric cores of binary relations

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2023-09-14.

module foundation.symmetric-cores-binary-relations where
Imports
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 1))
( r (zero-Fin 1))

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