Regular cd-structures

Content created by Egbert Rijke and Fredrik Bakke.

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

module orthogonal-factorization-systems.regular-cd-structures where


A regular cd-structure is a cd-structure which satisfies the following three axioms:

  1. Every distinguished square is cartesian.
  2. The codomain of every distinguished square is an embedding.
  3. The diagonal of every distinguished square
          Δ i
       A -----> A ×_X A
       |           |
     f |           | functoriality Δ g
       ∨           ∨
       B -----> B ×_Y B.
          Δ j
    is again a distinguished square.

Recent changes