In type theory, proving a statement means to exhibit an instance/element of a type corresponding to the statement. But if the statement is unprovable, no element of the type A nor its negation A → ⊥ can be generated. How can be proven that the statement A is unprovable?