Newer
Older
namespace latin:/❚
fixmeta ur:?LF❚
/T Universes as a soft typing relation (level) on types
tp is now no longer the base universe -- instead, it is the union of all universes
We define a universe to be any type that occurs on the left of the level relation.❚
theory SoftUniverses =
include ?TypedLogic❙
level : tp ⟶ tp ⟶ prop❘ # 1 ⋳ 2 prec 30❙
univTm: {A,U} ⊦A⋳U ⟶ tm U❙
❚
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
theory TwoUniverses =
include ?SoftUniverses❙
utp: tp❙
ukd: tp❙
utp_kd: ⊦ utp⋳ukd❙
❚
/T natural number-based hierarchy of universes❚
theory UniverseHierarchy =
include ?SoftUniverses❙
univ: type❙
univ_zero: univ❙
univ_next: univ ⟶ univ❙
univTp: univ ⟶ tp❙
univ_in: {U} ⊦ univTp U ⋳ univTp (univ_next U)❙
realize ?TwoUniverses❙
utp = univTp univ_zero❙
ukd = univTp (univ_next univ_zero)❙
utp_kd = univ_in❙
❚
/T Universes as a soft element typing relation on types❚
theory InclusiveUniverses =
include ?UniverseHierarchy❙
inclusive : {A,U} ⊦ A ⋳ univTp U ⟶ ⊦ A ⋳ univTp (univ_next U)❙
❚
theory UniverseDepFunExample =
include ?SoftUniverses❙
Pi_legal : tp ⟶ tp ⟶ type❙
Pi : {A} (tm A ⟶ tp) ⟶ tp❘ # Π 2 prec 50❙
Pi_univ: {U,V,A,B}⊦ A⋳U ⟶ ({x:tm A} ⊦ B x ⋳ V) ⟶ Pi_legal U V ⟶ ⊦ Π B ⋳ V❙
// lambda, apply, etc. as usual❙
// LF as a λ-cube example❙
include ?TwoUniverses❙
function_types: Pi_legal utp utp❙
dependent_types: Pi_legal utp ukd❙
❚
// TODO these universes should be realized by corresponding theories of set-theoretical universe❚