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

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
      ∨           ∨
      B -----> B ×_Y B.
         Δ j
   

   is again a distinguished square.

Recent changes

• 2024-04-25. Fredrik Bakke. chore: Fix arrowheads in character diagrams (#1124).
• 2024-03-02. Fredrik Bakke. Factor out standard pullbacks (#1042).
• 2023-11-30. Egbert Rijke. Initial definitions for the cd-excision project (#931).