# 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.cd-structures where

Imports
open import foundation.morphisms-arrows
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels


## Idea

A cd-structure on a category consists of a class 𝒟 of distinguished squares

        i
A -----> X
|        |
f |        | g
∨        ∨
B -----> Y.
j


On this page we will consider internal cd-structures, i.e., cd-structure on types. In other words, a cd-structure is a family of subtypes

  (f : A → B) (g : X → Y) → hom-arrow f g → Prop,


where hom-arrow f g is the type of morphisms of arrows from f to g.

The terminology "cd-structure" originates from the idea that a Grothendieck topology is completely decomposable if it is generated by covering families that are given as pairs of maps with a common codomain that fit in a distinguished square.

## Definitions

### Cd-structures

module _
(α : Level → Level → Level → Level → Level)
where

cd-structure : UUω
cd-structure =
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} →
(f : A → B) (g : X → Y) → subtype (α l1 l2 l3 l4) (hom-arrow f g)

is-distinguished-square-cd-structure :
(Σ : cd-structure) →
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} →
(f : A → B) (g : X → Y) → hom-arrow f g → UU (α l1 l2 l3 l4)
is-distinguished-square-cd-structure Σ f g σ =
type-Prop (Σ f g σ)


## References

[Voe10]
Vladimir Voevodsky. Unstable motivic homotopy categories in Nisnevich and cdh-topologies. Journal of Pure and Applied Algebra, 214(8):1399–1406, 08 2010. URL: https://www.sciencedirect.com/science/article/pii/S0022404909002643, arXiv:0805.4576, doi:10.1016/j.jpaa.2009.11.005.