Require Import Basics.Overture.Require Import Basics.Overture.

(** * Option types *)

(** Option types are a simple way to represent a value that may or may not be present. They are also known as the Maybe monad in functional programming. *)

(** [option] is functorial. *)
Definition functor_option {A B} (f : A -> B) (x : option A) : option B :=
  match x with
  | None => None
  | Some a => Some (f a)
  end.

(** The [Some] constructor is injective. *)
Definition isinj_some {A} {x y : A} (p : Some x = Some y)
  : x = y.
A: Type
x, y: A
p: Some x = Some y
x = y
Proof.
A: Type
x, y: A
p: Some x = Some y
x = y
  injection p.
A: Type
x, y: A
p: Some x = Some y
x = y -> x = y
  exact idmap.
Defined.