# Similarity of elements in large posets

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-posets where

Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.large-binary-relations
open import foundation.propositions
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.similarity-of-elements-large-preorders


## Idea

Two elements x and y of a large poset P are said to be similar if both x ≤ y and y ≤ x hold. Note that the similarity relation is defined across universe levels, and that only similar elements of the same universe level are equal.

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

## Definition

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

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

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

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


## Properties

### The similarity relation is reflexive

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

refl-sim-Large-Poset :
is-reflexive-Large-Relation (type-Large-Poset P) (sim-Large-Poset P)
refl-sim-Large-Poset = refl-sim-Large-Preorder (large-preorder-Large-Poset P)


### The similarity relation is transitive

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

transitive-sim-Large-Poset :
is-transitive-Large-Relation (type-Large-Poset P) (sim-Large-Poset P)
transitive-sim-Large-Poset =
transitive-sim-Large-Preorder (large-preorder-Large-Poset P)


### The similarity relation is symmetric

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

symmetric-sim-Large-Poset :
is-symmetric-Large-Relation (type-Large-Poset P) (sim-Large-Poset P)
symmetric-sim-Large-Poset =
symmetric-sim-Large-Preorder (large-preorder-Large-Poset P)


### For any universe level l, any element x is similar to at most one element of universe level l

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

all-elements-equal-total-sim-Large-Poset :
{l1 l2 : Level} (x : type-Large-Poset P l1) →
all-elements-equal (Σ (type-Large-Poset P l2) (sim-Large-Poset P x))
all-elements-equal-total-sim-Large-Poset x (y , H) (z , K) =
eq-type-subtype
( sim-prop-Large-Poset P x)
( antisymmetric-leq-Large-Poset P
( y)
( z)
( transitive-leq-Large-Poset P _ _ _ (pr1 K) (pr2 H))
( transitive-leq-Large-Poset P _ _ _ (pr1 H) (pr2 K)))

is-prop-total-sim-Large-Poset :
{l1 l2 : Level} (x : type-Large-Poset P l1) →
is-prop (Σ (type-Large-Poset P l2) (sim-Large-Poset P x))
is-prop-total-sim-Large-Poset x =
is-prop-all-elements-equal
( all-elements-equal-total-sim-Large-Poset x)

is-torsorial-sim-Large-Poset :
{l1 : Level} (x : type-Large-Poset P l1) →
is-torsorial (sim-Large-Poset P x)
is-torsorial-sim-Large-Poset x =
is-proof-irrelevant-is-prop
( is-prop-total-sim-Large-Poset x)
( x , refl-sim-Large-Poset P x)


### Similarity characterizes the identity type of elements in a large poset of the same universe level

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

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

is-equiv-sim-eq-Large-Poset :
{l1 : Level} (x y : type-Large-Poset P l1) →
is-equiv (sim-eq-Large-Poset {l1} {x} {y})
is-equiv-sim-eq-Large-Poset x =
fundamental-theorem-id
( is-torsorial-sim-Large-Poset P x)
( λ y → sim-eq-Large-Poset {_} {x} {y})

extensionality-Large-Poset :
{l1 : Level} (x y : type-Large-Poset P l1) →
(x ＝ y) ≃ sim-Large-Poset P x y
pr1 (extensionality-Large-Poset x y) = sim-eq-Large-Poset
pr2 (extensionality-Large-Poset x y) = is-equiv-sim-eq-Large-Poset x y

eq-sim-Large-Poset :
{l1 : Level} (x y : type-Large-Poset P l1) →
sim-Large-Poset P x y → x ＝ y
eq-sim-Large-Poset x y = map-inv-is-equiv (is-equiv-sim-eq-Large-Poset x y)