# Similarity of elements in large preorders

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, Maša Žaucer, fernabnor, Gregor Perčič and louismntnu.

Created on 2023-06-08.

module order-theory.similarity-of-elements-large-preorders where

Imports
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.large-binary-relations
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.large-preorders


## Idea

Two elements x and y of a large preorder P are said to be similar if both x ≤ y and y ≤ x hold.

In informal writing we will use the notation x ≈ y to assert that x and y are similar elements in a preorder P.

## Definition

module _
{α : Level → Level} {β : Level → Level → Level} (P : Large-Preorder α β)
where

sim-prop-Large-Preorder :
{l1 l2 : Level}
(x : type-Large-Preorder P l1) (y : type-Large-Preorder P l2) →
Prop (β l1 l2 ⊔ β l2 l1)
sim-prop-Large-Preorder x y =
product-Prop
( leq-prop-Large-Preorder P x y)
( leq-prop-Large-Preorder P y x)

sim-Large-Preorder :
{l1 l2 : Level}
(x : type-Large-Preorder P l1) (y : type-Large-Preorder P l2) →
UU (β l1 l2 ⊔ β l2 l1)
sim-Large-Preorder x y = type-Prop (sim-prop-Large-Preorder x y)

is-prop-sim-Large-Preorder :
{l1 l2 : Level}
(x : type-Large-Preorder P l1) (y : type-Large-Preorder P l2) →
is-prop (sim-Large-Preorder x y)
is-prop-sim-Large-Preorder x y =
is-prop-type-Prop (sim-prop-Large-Preorder x y)


## Properties

### The similarity relation is reflexive

module _
{α : Level → Level} {β : Level → Level → Level} (P : Large-Preorder α β)
where

refl-sim-Large-Preorder :
is-reflexive-Large-Relation (type-Large-Preorder P) (sim-Large-Preorder P)
pr1 (refl-sim-Large-Preorder x) = refl-leq-Large-Preorder P x
pr2 (refl-sim-Large-Preorder x) = refl-leq-Large-Preorder P x


### The similarity relation is transitive

module _
{α : Level → Level} {β : Level → Level → Level} (P : Large-Preorder α β)
where

transitive-sim-Large-Preorder :
is-transitive-Large-Relation (type-Large-Preorder P) (sim-Large-Preorder P)
pr1 (transitive-sim-Large-Preorder x y z H K) =
transitive-leq-Large-Preorder P x y z (pr1 H) (pr1 K)
pr2 (transitive-sim-Large-Preorder x y z H K) =
transitive-leq-Large-Preorder P z y x (pr2 K) (pr2 H)


### The similarity relation is symmetric

module _
{α : Level → Level} {β : Level → Level → Level} (P : Large-Preorder α β)
where

symmetric-sim-Large-Preorder :
is-symmetric-Large-Relation (type-Large-Preorder P) (sim-Large-Preorder P)
pr1 (symmetric-sim-Large-Preorder _ _ H) = pr2 H
pr2 (symmetric-sim-Large-Preorder _ _ H) = pr1 H


### Equal elements are similar

module _
{α : Level → Level} {β : Level → Level → Level} (P : Large-Preorder α β)
where

sim-eq-Large-Preorder :
{l : Level} {x y : type-Large-Preorder P l} →
x ＝ y → sim-Large-Preorder P x y
sim-eq-Large-Preorder refl = refl-sim-Large-Preorder P _