Content created by Egbert Rijke and Fredrik Bakke.

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

module where
open import foundation.morphisms-arrows
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels


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

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

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.



module _
  (α : Level  Level  Level  Level  Level)

  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 σ)


Vladimir Voevodsky. Unstable motivic homotopy categories in Nisnevich and cdh-topologies. Journal of Pure and Applied Algebra, 214(8):1399–1406, 08 2010. URL:, arXiv:0805.4576, doi:10.1016/j.jpaa.2009.11.005.

Recent changes