This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The maybe modality on finite types

module univalent-combinatorics.maybe where

open import foundation.maybe public
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

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

add-free-point-UU-Fin :
  {l1 : Level} (k : ℕ) → UU-Fin l1 k → UU-Fin l1 (succ-ℕ k)
add-free-point-UU-Fin k X = coproduct-UU-Fin k 1 X unit-UU-Fin