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.
Last modified on 2024-02-06.

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 _

Recent changes