The maybe monad on finite types

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

Created on 2022-02-16.
Last modified on 2024-09-23.

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

Recent changes