Commuting squares of order preserving maps of large posets

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified on 2024-04-25.

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)

Recent changes