Counting the elements in Maybe

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

Created on 2022-02-11.
Last modified on 2023-03-13.

module univalent-combinatorics.counting-maybe where
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.equivalences-maybe
open import foundation.identity-types
open import foundation.maybe
open import foundation.universe-levels

open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.counting


The elements of a type X can be counted if and only if the elements of Maybe X can be counted.

count-Maybe : {l : Level} {X : UU l}  count X  count (Maybe X)
count-Maybe {l} {X} e = count-coprod e count-unit

  is-nonzero-number-of-elements-count-Maybe :
    {l : Level} {X : UU l} (e : count (Maybe X)) 
    is-nonzero-ℕ (number-of-elements-count e)
  is-nonzero-number-of-elements-count-Maybe e p =
    is-empty-is-zero-number-of-elements-count e p exception-Maybe

is-successor-number-of-elements-count-Maybe :
  {l : Level} {X : UU l} (e : count (Maybe X)) 
  is-successor-ℕ (number-of-elements-count e)
is-successor-number-of-elements-count-Maybe e =
  is-successor-is-nonzero-ℕ (is-nonzero-number-of-elements-count-Maybe e)

count-count-Maybe :
  {l : Level} {X : UU l}  count (Maybe X)  count X
count-count-Maybe (pair k e) with
  is-successor-number-of-elements-count-Maybe (pair k e)
... | pair l refl = pair l (equiv-equiv-Maybe e)

Recent changes