Descent for the empty type

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-07-22.
Last modified on 2026-02-02.

module foundation.descent-empty-types where
Imports 
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.empty-types
open import foundation-core.pullbacks

Idea

The descent property of empty types states that every cone of the form

  C ------> ∅
  |         |
  |         |
  ∨         ∨
  B ------> X

is a pullback.

Theorem

module _
  {l1 l2 l3 : Level} {B : UU l1} {X : UU l2} {C : UU l3} (g : B → X)
  where

  cone-empty : is-empty C → (C → B) → cone ex-falso g C
  pr1 (cone-empty p q) = p
  pr1 (pr2 (cone-empty p q)) = q
  pr2 (pr2 (cone-empty p q)) c = ex-falso (p c)

  abstract
    descent-empty : (c : cone ex-falso g C) → is-pullback ex-falso g c
    descent-empty c =
      is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone _ g c ind-empty

  abstract
    descent-empty' :
      (p : C → empty) (q : C → B) → is-pullback ex-falso g (cone-empty p q)
    descent-empty' p q = descent-empty (cone-empty p q)

Table of descent properties

ConceptFile
Descent for coproduct typesfoundation.descent-coproduct-types
Descent for dependent pair typesfoundation.descent-dependent-pair-types
Descent for empty typesfoundation.descent-empty-types
Descent for equivalencesfoundation.descent-equivalences
Descent for pushoutssynthetic-homotopy-theory.descent-pushouts
Descent for sequential colimitssynthetic-homotopy-theory.descent-sequential-colimits
Descent for surjective mapsfoundation.descent-surjective-maps
Descent for the circlesynthetic-homotopy-theory.descent-circle

Recent changes