Equivalences on Maybe

module foundation.equivalences-maybe where

open import foundation.equality-coproduct-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.functoriality-coproduct-types
open import foundation.maybe
open import foundation.unit-type
open import foundation.universal-property-maybe

open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.embeddings
open import foundation-core.empty-types
open import foundation-core.equality-dependent-pair-types
open import foundation-core.functions
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.universe-levels

Idea

For any two types X and Y, we have (X ≃ Y) ↔ (Maybe X ≃ Maybe Y).

Definition

The action of the Maybe modality on equivalences

equiv-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) → Maybe X ≃ Maybe Y
equiv-Maybe e = equiv-coprod e id-equiv

Equivalences of Maybe-structures on a type

equiv-maybe-structure :
  {l1 : Level} {X : UU l1} (Y Z : maybe-structure X) → UU l1
equiv-maybe-structure Y Z =
  Σ (pr1 Y ≃ pr1 Z) (λ e → htpy-equiv (pr2 Y) (pr2 Z ∘e equiv-Maybe e))

id-equiv-maybe-structure :
  {l1 : Level} {X : UU l1} (Y : maybe-structure X) → equiv-maybe-structure Y Y
id-equiv-maybe-structure Y =
  pair id-equiv (ind-Maybe (pair refl-htpy refl))

equiv-eq-maybe-structure :
  {l1 : Level} {X : UU l1} (Y Z : maybe-structure X) →
  Y ＝ Z → equiv-maybe-structure Y Z
equiv-eq-maybe-structure Y .Y refl = id-equiv-maybe-structure Y

Properties

If f : Maybe X → Maybe Y is an injective map and f (inl x) is an exception, then f exception is not an exception

abstract
  is-not-exception-injective-map-exception-Maybe :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
    is-injective f → (x : X) → is-exception-Maybe (f (inl x)) →
    is-not-exception-Maybe (f exception-Maybe)
  is-not-exception-injective-map-exception-Maybe is-inj-f x p q =
    is-not-exception-unit-Maybe x (is-inj-f (p ∙ inv q))

abstract
  is-not-exception-map-equiv-exception-Maybe :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) →
    is-exception-Maybe (map-equiv e (inl x)) →
    is-not-exception-Maybe (map-equiv e exception-Maybe)
  is-not-exception-map-equiv-exception-Maybe e =
    is-not-exception-injective-map-exception-Maybe (is-injective-map-equiv e)

abstract
  is-not-exception-emb-exception-Maybe :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ↪ Maybe Y)
    (x : X) → is-exception-Maybe (map-emb e (inl x)) →
    is-not-exception-Maybe (map-emb e exception-Maybe)
  is-not-exception-emb-exception-Maybe e =
    is-not-exception-injective-map-exception-Maybe (is-injective-emb e)

If f is injective and f (inl x) is an exception, then f exception is a value

is-value-injective-map-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
  is-injective f → (x : X) → is-exception-Maybe (f (inl x)) →
  is-value-Maybe (f exception-Maybe)
is-value-injective-map-exception-Maybe {f = f} is-inj-f x H =
  is-value-is-not-exception-Maybe
    ( f exception-Maybe)
    ( is-not-exception-injective-map-exception-Maybe is-inj-f x H)

value-injective-map-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
  is-injective f → (x : X) → is-exception-Maybe (f (inl x)) → Y
value-injective-map-exception-Maybe {f = f} is-inj-f x H =
  value-is-value-Maybe
    ( f exception-Maybe)
    ( is-value-injective-map-exception-Maybe is-inj-f x H)

comp-injective-map-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
  (is-inj-f : is-injective f) (x : X) (H : is-exception-Maybe (f (inl x))) →
  inl (value-injective-map-exception-Maybe is-inj-f x H) ＝
  f exception-Maybe
comp-injective-map-exception-Maybe {f = f} is-inj-f x H =
  eq-is-value-Maybe
    ( f exception-Maybe)
    ( is-value-injective-map-exception-Maybe is-inj-f x H)

For any equivalence e : Maybe X ≃ Maybe Y, if e (inl x) is an exception, then e exception is a value

is-value-map-equiv-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) →
  is-exception-Maybe (map-equiv e (inl x)) →
  is-value-Maybe (map-equiv e exception-Maybe)
is-value-map-equiv-exception-Maybe e x H =
  is-value-is-not-exception-Maybe
    ( map-equiv e exception-Maybe)
    ( is-not-exception-map-equiv-exception-Maybe e x H)

value-map-equiv-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) →
  is-exception-Maybe (map-equiv e (inl x)) → Y
value-map-equiv-exception-Maybe e x H =
  value-is-value-Maybe
    ( map-equiv e exception-Maybe)
    ( is-value-map-equiv-exception-Maybe e x H)

compute-map-equiv-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) →
  (H : is-exception-Maybe (map-equiv e (inl x))) →
  inl (value-map-equiv-exception-Maybe e x H) ＝ map-equiv e exception-Maybe
compute-map-equiv-exception-Maybe e x H =
  eq-is-value-Maybe
    ( map-equiv e exception-Maybe)
    ( is-value-map-equiv-exception-Maybe e x H)

Injective maps Maybe X → Maybe Y can be restricted to maps X → Y

restrict-injective-map-Maybe' :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
  is-injective f → (x : X) (u : Maybe Y) (p : f (inl x) ＝ u) → Y
restrict-injective-map-Maybe' {f = f} is-inj-f x (inl y) p = y
restrict-injective-map-Maybe' {f = f} is-inj-f x (inr star) p =
  value-injective-map-exception-Maybe is-inj-f x p

restrict-injective-map-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
  is-injective f → X → Y
restrict-injective-map-Maybe {f = f} is-inj-f x =
  restrict-injective-map-Maybe' is-inj-f x (f (inl x)) refl

compute-restrict-injective-map-is-exception-Maybe' :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
  (is-inj-f : is-injective f) (x : X) (u : Maybe Y) (p : f (inl x) ＝ u) →
  is-exception-Maybe (f (inl x)) →
  inl (restrict-injective-map-Maybe' is-inj-f x u p) ＝ f exception-Maybe
compute-restrict-injective-map-is-exception-Maybe'
  {f = f} is-inj-f x (inl y) p q =
  ex-falso (is-not-exception-unit-Maybe y (inv p ∙ q))
compute-restrict-injective-map-is-exception-Maybe'
  {f = f} is-inj-f x (inr star) p q =
  comp-injective-map-exception-Maybe is-inj-f x p

compute-restrict-injective-map-is-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
  (is-inj-f : is-injective f) (x : X) → is-exception-Maybe (f (inl x)) →
  inl (restrict-injective-map-Maybe is-inj-f x) ＝ f exception-Maybe
compute-restrict-injective-map-is-exception-Maybe {f = f} is-inj-f x =
  compute-restrict-injective-map-is-exception-Maybe' is-inj-f x (f (inl x)) refl

compute-restrict-injective-map-is-not-exception-Maybe' :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
  (is-inj-f : is-injective f) (x : X) (u : Maybe Y) (p : f (inl x) ＝ u) →
  is-not-exception-Maybe (f (inl x)) →
  inl (restrict-injective-map-Maybe' is-inj-f x u p) ＝ f (inl x)
compute-restrict-injective-map-is-not-exception-Maybe'
  is-inj-f x (inl y) p H =
  inv p
compute-restrict-injective-map-is-not-exception-Maybe'
  is-inj-f x (inr star) p H =
  ex-falso (H p)

compute-restrict-injective-map-is-not-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : Maybe X → Maybe Y} →
  (is-inj-f : is-injective f) (x : X) → is-not-exception-Maybe (f (inl x)) →
  inl (restrict-injective-map-Maybe is-inj-f x) ＝ f (inl x)
compute-restrict-injective-map-is-not-exception-Maybe {f = f} is-inj-f x =
  compute-restrict-injective-map-is-not-exception-Maybe' is-inj-f x (f (inl x))
    refl

Any equivalence Maybe X ≃ Maybe Y induces a map X → Y

We don't use with-abstraction to keep full control over the definitional equalities, so we give the definition in two steps. After the definition is complete, we also prove two computation rules. Since we will prove computation rules, we make the definition abstract.

map-equiv-equiv-Maybe' :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y)
  (x : X) (u : Maybe Y) (p : map-equiv e (inl x) ＝ u) → Y
map-equiv-equiv-Maybe' e =
  restrict-injective-map-Maybe' (is-injective-map-equiv e)

map-equiv-equiv-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) → X → Y
map-equiv-equiv-Maybe e =
  restrict-injective-map-Maybe (is-injective-map-equiv e)

compute-map-equiv-equiv-is-exception-Maybe' :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) →
  (u : Maybe Y) (p : map-equiv e (inl x) ＝ u) →
  is-exception-Maybe (map-equiv e (inl x)) →
  inl (map-equiv-equiv-Maybe' e x u p) ＝ map-equiv e exception-Maybe
compute-map-equiv-equiv-is-exception-Maybe' e =
  compute-restrict-injective-map-is-exception-Maybe' (is-injective-map-equiv e)

compute-map-equiv-equiv-is-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) →
  is-exception-Maybe (map-equiv e (inl x)) →
  inl (map-equiv-equiv-Maybe e x) ＝ map-equiv e exception-Maybe
compute-map-equiv-equiv-is-exception-Maybe e x =
  compute-map-equiv-equiv-is-exception-Maybe' e x (map-equiv e (inl x)) refl

compute-map-equiv-equiv-is-not-exception-Maybe' :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) →
  (u : Maybe Y) (p : map-equiv e (inl x) ＝ u) →
  is-not-exception-Maybe (map-equiv e (inl x)) →
  inl (map-equiv-equiv-Maybe' e x u p) ＝ map-equiv e (inl x)
compute-map-equiv-equiv-is-not-exception-Maybe' e x (inl y) p H =
  inv p
compute-map-equiv-equiv-is-not-exception-Maybe' e x (inr star) p H =
  ex-falso (H p)

compute-map-equiv-equiv-is-not-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) →
  is-not-exception-Maybe (map-equiv e (inl x)) →
  inl (map-equiv-equiv-Maybe e x) ＝ map-equiv e (inl x)
compute-map-equiv-equiv-is-not-exception-Maybe e x =
  compute-map-equiv-equiv-is-not-exception-Maybe' e x (map-equiv e (inl x)) refl

Any equivalence Maybe X ≃ Maybe Y induces a map Y → X

map-inv-equiv-equiv-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) → Y → X
map-inv-equiv-equiv-Maybe e =
  map-equiv-equiv-Maybe (inv-equiv e)

compute-map-inv-equiv-equiv-is-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (y : Y) →
  is-exception-Maybe (map-inv-equiv e (inl y)) →
  inl (map-inv-equiv-equiv-Maybe e y) ＝ map-inv-equiv e exception-Maybe
compute-map-inv-equiv-equiv-is-exception-Maybe e =
  compute-map-equiv-equiv-is-exception-Maybe (inv-equiv e)

compute-map-inv-equiv-equiv-is-not-exception-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (y : Y) →
  ( f : is-not-exception-Maybe (map-inv-equiv e (inl y))) →
  inl (map-inv-equiv-equiv-Maybe e y) ＝ map-inv-equiv e (inl y)
compute-map-inv-equiv-equiv-is-not-exception-Maybe e =
  compute-map-equiv-equiv-is-not-exception-Maybe (inv-equiv e)

The map map-inv-equiv-equiv-Maybe e is a section of map-equiv-equiv-Maybe e

abstract
  issec-map-inv-equiv-equiv-Maybe :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) →
    (map-equiv-equiv-Maybe e ∘ map-inv-equiv-equiv-Maybe e) ~ id
  issec-map-inv-equiv-equiv-Maybe e y with
    is-decidable-is-exception-Maybe (map-inv-equiv e (inl y))
  ... | inl p =
    is-injective-unit-Maybe
      ( ( compute-map-equiv-equiv-is-exception-Maybe e
          ( map-inv-equiv-equiv-Maybe e y)
          ( ( ap
              ( map-equiv e)
              ( compute-map-inv-equiv-equiv-is-exception-Maybe e y p)) ∙
            ( issec-map-inv-equiv e exception-Maybe))) ∙
        ( ( ap (map-equiv e) (inv p)) ∙
          ( issec-map-inv-equiv e (inl y))))
  ... | inr f =
    is-injective-unit-Maybe
      ( ( compute-map-equiv-equiv-is-not-exception-Maybe e
          ( map-inv-equiv-equiv-Maybe e y)
          ( is-not-exception-is-value-Maybe
            ( map-equiv e (inl (map-inv-equiv-equiv-Maybe e y)))
            ( pair y
              ( inv
                ( ( ap
                    ( map-equiv e)
                    ( compute-map-inv-equiv-equiv-is-not-exception-Maybe
                        e y f)) ∙
                  ( issec-map-inv-equiv e (inl y))))))) ∙
        ( ( ap
            ( map-equiv e)
            ( compute-map-inv-equiv-equiv-is-not-exception-Maybe e y f)) ∙
          ( issec-map-inv-equiv e (inl y))))

The map map-inv-equiv-equiv-Maybe e is a retraction of the map map-equiv-equiv-Maybe e

abstract
  isretr-map-inv-equiv-equiv-Maybe :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) →
    (map-inv-equiv-equiv-Maybe e ∘ map-equiv-equiv-Maybe e) ~ id
  isretr-map-inv-equiv-equiv-Maybe e x with
    is-decidable-is-exception-Maybe (map-equiv e (inl x))
  ... | inl p =
    is-injective-unit-Maybe
      ( ( compute-map-inv-equiv-equiv-is-exception-Maybe e
          ( map-equiv-equiv-Maybe e x)
          ( ( ap ( map-inv-equiv e)
                 ( compute-map-equiv-equiv-is-exception-Maybe e x p)) ∙
            ( isretr-map-inv-equiv e exception-Maybe))) ∙
        ( ( ap (map-inv-equiv e) (inv p)) ∙
          ( isretr-map-inv-equiv e (inl x))))
  ... | inr f =
    is-injective-unit-Maybe
      ( ( compute-map-inv-equiv-equiv-is-not-exception-Maybe e
          ( map-equiv-equiv-Maybe e x)
          ( is-not-exception-is-value-Maybe
            ( map-inv-equiv e (inl (map-equiv-equiv-Maybe e x)))
            ( pair x
              ( inv
                ( ( ap (map-inv-equiv e)
                       ( compute-map-equiv-equiv-is-not-exception-Maybe
                          e x f)) ∙
                  ( isretr-map-inv-equiv e (inl x))))))) ∙
        ( ( ap ( map-inv-equiv e)
               ( compute-map-equiv-equiv-is-not-exception-Maybe e x f)) ∙
          ( isretr-map-inv-equiv e (inl x))))

The function map-equiv-equiv-Maybe is an equivalence

abstract
  is-equiv-map-equiv-equiv-Maybe :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) →
    is-equiv (map-equiv-equiv-Maybe e)
  is-equiv-map-equiv-equiv-Maybe e =
    is-equiv-has-inverse
      ( map-inv-equiv-equiv-Maybe e)
      ( issec-map-inv-equiv-equiv-Maybe e)
      ( isretr-map-inv-equiv-equiv-Maybe e)

equiv-equiv-Maybe :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} → (Maybe X ≃ Maybe Y) → (X ≃ Y)
pr1 (equiv-equiv-Maybe e) = map-equiv-equiv-Maybe e
pr2 (equiv-equiv-Maybe e) = is-equiv-map-equiv-equiv-Maybe e

For any set X, the type of automorphisms on X is equivalent to the type of automorphisms on Maybe X that fix the exception

module _
  {l : Level} (X : Set l)
  where

  extend-equiv-Maybe :
    (type-Set X ≃ type-Set X) ≃
    ( Σ ( Maybe (type-Set X) ≃ Maybe (type-Set X))
        ( λ e → map-equiv e (inr star) ＝ inr star))
  pr1 (pr1 extend-equiv-Maybe f) = equiv-coprod f id-equiv
  pr2 (pr1 extend-equiv-Maybe f) = refl
  pr2 extend-equiv-Maybe =
    is-equiv-has-inverse
      ( λ f → pr1 (retr-equiv-coprod (pr1 f) id-equiv (p f)))
      ( λ f →
        ( eq-pair-Σ
          ( inv
            ( eq-htpy-equiv (pr2 (retr-equiv-coprod (pr1 f) id-equiv (p f)))))
          ( eq-is-prop
            ( pr2
              ( Id-Prop
                ( pair
                  ( Maybe (type-Set X))
                  ( is-set-coprod (is-set-type-Set X) is-set-unit))
                ( map-equiv (pr1 f) (inr star))
                ( inr star))))))
      ( λ f → eq-equiv-eq-map-equiv refl)
    where
    p :
      ( f :
        ( Σ ( Maybe (type-Set X) ≃ Maybe (type-Set X))
            ( λ e → map-equiv e (inr star) ＝ inr star)))
      ( b : unit) →
      map-equiv (pr1 f) (inr b) ＝ inr b
    p f star = pr2 f

  computation-extend-equiv-Maybe :
    (f : type-Set X ≃ type-Set X) (x y : type-Set X) → map-equiv f x ＝ y →
    map-equiv (pr1 (map-equiv extend-equiv-Maybe f)) (inl x) ＝ inl y
  computation-extend-equiv-Maybe f x y p = ap inl p

  computation-inv-extend-equiv-Maybe :
    (f : Maybe (type-Set X) ≃ Maybe (type-Set X))
    (p : map-equiv f (inr star) ＝ inr star) (x : type-Set X) →
    inl (map-equiv (map-inv-equiv extend-equiv-Maybe (pair f p)) x) ＝
    map-equiv f (inl x)
  computation-inv-extend-equiv-Maybe f p x =
    htpy-eq-equiv
      ( pr1 (pair-eq-Σ (pr2 (pr1 (pr2 extend-equiv-Maybe)) (pair f p))))
      ( inl x)

  comp-extend-equiv-Maybe :
    (f g : type-Set X ≃ type-Set X) →
    htpy-equiv
      ( pr1 (map-equiv extend-equiv-Maybe (f ∘e g)))
      ( ( pr1 (map-equiv extend-equiv-Maybe f)) ∘e
        ( pr1 (map-equiv extend-equiv-Maybe g)))
  comp-extend-equiv-Maybe f g =
    preserves-comp-map-coprod (map-equiv g) (map-equiv f) id id