∀(A : Type) → Optional A