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