2
$\begingroup$

The homotopy type theory book claims in section 1.3 that "As in naive set theory, we might wish for a universe of all types" but from this one could "deduce from it that every type, including the empty type representing the proposition False, is inhabited"

The reference that it gives uses notation that I don't understand, however.

Could someone write invalid Agda code which produces a element of $\bot$, but which would be valid if Agda had a single universe that contains itself?

$\endgroup$
  • 2
    $\begingroup$ Asking for Agda code is likely to be outside the range of topics here on CS.SE. A more general question about why we can't accept Type:Type, and Girard's paradox might be appropriate. You could try Barendregt's book chapter "lambda calculi with types" Th.5.5.3. It is not a simple result. $\endgroup$ – chi Jun 15 '18 at 16:33
8
$\begingroup$

The problem is not specific to homotopy type theory. In type theory in general, if there is a type of all types, then every type is inhabited. This was shown first by Girard who encoded the Burali-Forti paradox in type theory.

A simplification of the paradox was found by Hurkens. Here is Agda code for it, and here is Coq code.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.