# Commuting squares of order preserving maps of large posets

Content created by Egbert Rijke.

Created on 2023-11-24.

module
order-theory.commuting-squares-of-order-preserving-maps-large-posets
where

Imports
open import foundation.universe-levels

open import foundation-core.commuting-squares-of-maps

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


## Idea

A square

        i
P -----> U
|        |
f |        | g
∨        ∨
Q -----> V
j


of order preserving maps between large posets is said to commute if for each x : type-Large-Poset P l the elements

  j (f x) : type-Large-Poset V (γj (γf l))
g (i x) : type-Large-Poset V (γg (γi l))


are similar. In other words, we say that the square above commutes if the composites j ∘ f and g ∘ i are similar.

## Definitions

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

coherence-square-hom-Large-Poset : UUω
coherence-square-hom-Large-Poset =
sim-hom-Large-Poset P V
( comp-hom-Large-Poset P Q V j f)
( comp-hom-Large-Poset P U V g i)