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 2025-02-14.

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-Type-With-Cardinality-ℕ :
  {l1 : Level} (k : ℕ) →
  Type-With-Cardinality-ℕ l1 k →
  Type-With-Cardinality-ℕ l1 (succ-ℕ k)
add-free-point-Type-With-Cardinality-ℕ k X =
  coproduct-Type-With-Cardinality-ℕ k 1 X unit-Type-With-Cardinality-ℕ

Recent changes