Regular cd-structures

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-30.
Last modified on 2024-03-02.

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

Idea

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
       V           V
       B -----> B ×_Y B.
          Δ j
    
    is again a distinguished square.

Recent changes