This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Regular cd-structures

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. 

  2. The codomain of every distinguished square is an
embedding.
    3. 

  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.
    4.