Timeline for What is a universe?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 16, 2022 at 21:08 | comment | added | Ms. Molly Stewart-Gallus |
@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) ;
|
|
| Mar 5, 2022 at 19:59 | comment | added | Jonathan Sterling | (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!) | |
| Mar 5, 2022 at 19:59 | comment | added | Jonathan Sterling | 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. | |
| Mar 5, 2022 at 18:25 | history | edited | Matthew McQuaid | CC BY-SA 4.0 |
improved formatting
|
| S Feb 27, 2022 at 3:55 | review | First answers | |||
| Feb 27, 2022 at 7:08 | |||||
| S Feb 27, 2022 at 3:55 | history | answered | Matthew McQuaid | CC BY-SA 4.0 |