The universal property of maybe
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-11.
Last modified on 2023-09-11.
module foundation.universal-property-maybe where
Imports
open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.maybe open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.coproduct-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types
Idea
We combine the universal property of coproducts and the unit type to obtain a universal property of the maybe modality.
Definitions
module _ {l1 l2 : Level} {A : UU l1} {B : Maybe A → UU l2} where ev-Maybe : ((x : Maybe A) → B x) → ((x : A) → B (unit-Maybe x)) × B exception-Maybe pr1 (ev-Maybe h) x = h (unit-Maybe x) pr2 (ev-Maybe h) = h exception-Maybe ind-Maybe : ((x : A) → B (unit-Maybe x)) × (B exception-Maybe) → (x : Maybe A) → B x ind-Maybe (pair h b) (inl x) = h x ind-Maybe (pair h b) (inr star) = b abstract is-section-ind-Maybe : (ev-Maybe ∘ ind-Maybe) ~ id is-section-ind-Maybe (pair h b) = refl is-retraction-ind-Maybe' : (h : (x : Maybe A) → B x) → (ind-Maybe (ev-Maybe h)) ~ h is-retraction-ind-Maybe' h (inl x) = refl is-retraction-ind-Maybe' h (inr star) = refl is-retraction-ind-Maybe : (ind-Maybe ∘ ev-Maybe) ~ id is-retraction-ind-Maybe h = eq-htpy (is-retraction-ind-Maybe' h) dependent-universal-property-Maybe : is-equiv ev-Maybe dependent-universal-property-Maybe = is-equiv-is-invertible ind-Maybe is-section-ind-Maybe is-retraction-ind-Maybe equiv-dependent-universal-property-Maybe : {l1 l2 : Level} {A : UU l1} (B : Maybe A → UU l2) → ((x : Maybe A) → B x) ≃ (((x : A) → B (unit-Maybe x)) × B exception-Maybe) pr1 (equiv-dependent-universal-property-Maybe B) = ev-Maybe pr2 (equiv-dependent-universal-property-Maybe B) = dependent-universal-property-Maybe equiv-universal-property-Maybe : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (Maybe A → B) ≃ ((A → B) × B) equiv-universal-property-Maybe {l1} {l2} {A} {B} = equiv-dependent-universal-property-Maybe (λ x → B)
Recent changes
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).