# Similarity of order preserving maps between large posets

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified on 2023-11-24.

module order-theory.similarity-of-order-preserving-maps-large-posets where

Imports
open import foundation.cartesian-product-types
open import foundation.universe-levels

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


## Idea

Consider two order preserving maps f : hom-Large-Poset γf P Q and g : hom-Large-Poset γg P Q between the same two large posets P and Q, but each specified with their own universe level reindexing functions. We say that f and g are similar if the values f x and g x are similar for each x : P. In other words, a similarity of order preserving maps between f and g consists of an assignment x ↦ h x where

  h x : f x ≈ g x


for each x : type-Large-Poset P. In informal writing we will use the notation f ≈ g to assert that the order preserving map f is similar to the order preserving map g.

## Definitions

### Similarity of order preserving maps between large posets

module _
{αP αQ γf γg : Level → Level} {βP βQ : Level → Level → Level}
(P : Large-Poset αP βP)
(Q : Large-Poset αQ βQ)
(f : hom-Large-Poset γf P Q)
(g : hom-Large-Poset γg P Q)
where

sim-hom-Large-Poset : UUω
sim-hom-Large-Poset =
sim-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( f)
( g)


### The reflexive similarity of order preserving maps between large posets

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

refl-sim-hom-Large-Poset : sim-hom-Large-Poset P Q f f
refl-sim-hom-Large-Poset =
refl-sim-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( f)


## Properties

### Order preserving maps with the same universe level reindexing function are homotopic if and only if they are similar

module _
{αP αQ γ : Level → Level} {βP βQ : Level → Level → Level}
(P : Large-Poset αP βP)
(Q : Large-Poset αQ βQ)
(f : hom-Large-Poset γ P Q)
(g : hom-Large-Poset γ P Q)
where

sim-htpy-hom-Large-Poset :
htpy-hom-Large-Poset P Q f g → sim-hom-Large-Poset P Q f g
sim-htpy-hom-Large-Poset =
sim-htpy-hom-Large-Preorder
( large-preorder-Large-Poset P)
( large-preorder-Large-Poset Q)
( f)
( g)

htpy-sim-hom-Large-Poset :
sim-hom-Large-Poset P Q f g → htpy-hom-Large-Poset P Q f g
htpy-sim-hom-Large-Poset H x =
eq-sim-Large-Poset Q
( map-hom-Large-Poset P Q f x)
( map-hom-Large-Poset P Q g x)
( H x)