Descent for the empty type
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-07-22.
Last modified on 2023-09-06.
module foundation.descent-empty-types where
Imports
open import foundation.cones-over-cospans open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation-core.empty-types open import foundation-core.pullbacks
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 cone-empty p q = triple 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-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)
Recent changes
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).