# Similarity of elements in large preorders ```agda module order-theory.similarity-of-elements-large-preorders where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## Idea Two elements `x` and `y` of a [large preorder](order-theory.large-preorders.md) `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 ```agda 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 ```agda 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 ```agda 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 ```agda 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 ```agda 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 _ ```