Skip to main content
Proof Assistants Beta

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

3
  • 4
    $\begingroup$ Just to say a little more about (3), one perspective is that any family of types is a universe; the types are the elements of the indexing type, and the elements of a "type" are the elements of its fiber in the family. Then it is a question of whether this "universe" is closed under any interesting connectives (e.g. product, sum, etc.). Every type family can be turned into a "full internal subcategory" of the ambient type theory, and as such it is possible to ask whether this full internal subcategory is complete, cocomplete, cartesian closed, etc. $\endgroup$
    – Jonathan Sterling
    Commented Mar 5, 2022 at 19:59
  • 2
    $\begingroup$ (I don't think that's what the OP was asking about necessarily, but in the interest of sharing cool perspectives that help with understanding universes, I thought I'd bring it up!) $\endgroup$
    – Jonathan Sterling
    Commented Mar 5, 2022 at 19:59
  • $\begingroup$ @JonathanSterling I always wonder how that approach would work in practice. Abusing HOAS it feels like you would pass a lot of witnesses around. Class Logic := { type: Set ; U := type -> Prop ; unit: type ; prod: type -> type -> type ; Pi: (type -> type) -> type ; H: nat -> U ; lift_H: forall n x, H n x -> H (S n) x ; unit_H: forall n, H n unit ; and_H: forall n x y, H n x -> H n y -> H n (and x y) ; Pi_H: forall n f, (forall x, H n x -> H n (f x)) -> H (S n) (Pi f) ; $\endgroup$
    – Ms. Molly Stewart-Gallus
    Commented May 16, 2022 at 21:08