# Strict symmetrization of binary relations

Content created by Fredrik Bakke.

Created on 2024-04-11.
Last modified on 2024-04-11.

module foundation.strict-symmetrization-binary-relations where

Imports
open import foundation.binary-relations
open import foundation.binary-relations-with-extensions
open import foundation.binary-relations-with-lifts
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.identity-types
open import foundation-core.retractions


## Idea

Given a binary relation R on A, we can construct a strict symmetrization of R. This is a relation Rˢ on A that is strictly symmetric. I.e., for every r : Rˢ x y, we have a symmetry operation sym r : Rˢ y x such that

  sym (sym r) ≐ r.


We define the strict symmetrization of R as

  Rˢ x y := Σ (z : A), (R z x) × (R z y).


If the underlying binary relation is reflexive, then this construction has a unit map R → Rˢ. If the binary relation has extensions, then it has a counit map Rˢ → R. Note that we do not mean to imply that these maps are components of an adjunction.

There is also a dual notion of strict symmetrization of binary relations defined by

  Rˢ-dual x y := Σ (z : A), (R x z) × (R y z).


The dual has a counit map if the binary relation has lifts rather than extensions.

An essential fact about the strict symmetrization of a relation is that the strict symmetrization of an identity relation is equivalent to the identity relation. We consider the strict symmetrization of the standard identity relation in foundation.strictly-involutive-identity-types.

Warning. The strict symmetrization is not the symmetric closure. For instance, if the underlying relation has an initial element, i.e., there is an element a such that R a x is contractible for every x, then the strict symmetrization will be reflexive, while the symmetric closure need not be.

## Definitions

### Strict symmetrization of binary relations

module _
{l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
where

strict-symmetrization-Relation : Relation (l1 ⊔ l2) A
strict-symmetrization-Relation x y = Σ A (λ z → R z x × R z y)

symmetric-strict-symmetrization-Relation :
is-symmetric strict-symmetrization-Relation
symmetric-strict-symmetrization-Relation x y (z , p , q) = (z , q , p)

is-involution-symmetric-strict-symmetrization-Relation :
{x y : A} (p : strict-symmetrization-Relation x y) →
( symmetric-strict-symmetrization-Relation y x
( symmetric-strict-symmetrization-Relation x y p)) ＝
( p)
is-involution-symmetric-strict-symmetrization-Relation p = refl

unit-strict-symmetrization-Relation :
is-reflexive R →
{x y : A} → R x y → strict-symmetrization-Relation x y
unit-strict-symmetrization-Relation r {x} p = (x , r x , p)

counit-strict-symmetrization-Relation :
has-extensions-Relation R →
{x y : A} → strict-symmetrization-Relation x y → R x y
counit-strict-symmetrization-Relation H (_ , p , q) = H p q


### Dual strict symmetrization of binary relations

module _
{l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
where

dual-strict-symmetrization-Relation : Relation (l1 ⊔ l2) A
dual-strict-symmetrization-Relation x y = Σ A (λ z → R x z × R y z)

symmetric-dual-strict-symmetrization-Relation :
is-symmetric dual-strict-symmetrization-Relation
symmetric-dual-strict-symmetrization-Relation x y (z , p , q) = (z , q , p)

is-involution-symmetric-dual-strict-symmetrization-Relation :
{x y : A} (p : dual-strict-symmetrization-Relation x y) →
( symmetric-dual-strict-symmetrization-Relation y x
( symmetric-dual-strict-symmetrization-Relation x y p)) ＝
( p)
is-involution-symmetric-dual-strict-symmetrization-Relation p = refl

unit-dual-strict-symmetrization-Relation :
is-reflexive R →
{x y : A} → R x y → dual-strict-symmetrization-Relation x y
unit-dual-strict-symmetrization-Relation r {x} {y} p = (y , p , r y)

counit-dual-strict-symmetrization-Relation :
has-lifts-Relation R →
{x y : A} → dual-strict-symmetrization-Relation x y → R x y
counit-dual-strict-symmetrization-Relation H (_ , p , q) = H p q


## Properties

### The strict symmetrization of a reflexive relation is reflexive

In fact, R does not have to be reflexive for the strict symmetrization to be reflexive. It suffices that there for every element of A is some other element that relates to it. For instance, the strict symmetrization of a relation with an initial element is always reflexive.

module _
{l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
where

refl-strict-symmetrization-Relation' :
((x : A) → Σ A (λ y → R y x)) →
is-reflexive (strict-symmetrization-Relation R)
refl-strict-symmetrization-Relation' r x = (pr1 (r x) , pr2 (r x) , pr2 (r x))

refl-strict-symmetrization-Relation :
is-reflexive R →
is-reflexive (strict-symmetrization-Relation R)
refl-strict-symmetrization-Relation r x = (x , r x , r x)


### The strict symmetrization of a relation with extensions satisfies all 2-horn filler conditions

module _
{l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
(H : has-extensions-Relation R)
where

has-extensions-strict-symmetrization-Relation :
has-extensions-Relation (strict-symmetrization-Relation R)
has-extensions-strict-symmetrization-Relation
{x} (_ , p , q) (_ , p' , q') = (x , H p q , H p' q')

has-lifts-strict-symmetrization-has-extensions-Relation :
has-lifts-Relation (strict-symmetrization-Relation R)
has-lifts-strict-symmetrization-has-extensions-Relation
{z = z} (w , p , q) (w' , p' , q') = (z , H q p , H q' p')

transitive-strict-symmetrization-has-extensions-Relation :
is-transitive (strict-symmetrization-Relation R)
transitive-strict-symmetrization-has-extensions-Relation
x y z (w , p , q) (w' , p' , q') = (y , H q' p' , H p q)


### If the extension operation on the underlying relation is left unital, then the counit is a retraction of the unit of the strict symmetrization

module _
{l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
(r : is-reflexive R) (H : has-extensions-Relation R)
where

is-retraction-counit-strict-symmetrization-Relation :
{x y : A} →
((p : R x y) → H (r x) p ＝ p) →
is-retraction
( unit-strict-symmetrization-Relation R r {x} {y})
( counit-strict-symmetrization-Relation R H {x} {y})
is-retraction-counit-strict-symmetrization-Relation s = s