The universal property of maybe

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

Created on 2022-02-11.
Last modified on 2024-02-06.

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 _) = 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 _) = 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