michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott/init): make sure eq is universe polymorphic

Browse source 
Jakob and Floris needed path equality to be universe polymorphic when
proving univalence.
This commit is contained in:
Leonardo de Moura 2014-12-06 09:43:42 -08:00
parent 466b671752
commit ec7f90cb16
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/init/datatypes.hlean
View file

@ -19,7 +19,7 @@ star : unit
inductive empty : Type
inductive eq {A : Type} (a : A) : A → Type :=
inductive eq.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
refl : eq a a
structure prod (A B : Type) :=

3
src/frontends/lean/structure_cmd.cpp
View file

@ -762,7 +762,8 @@ struct structure_cmd_fn {
lhs = mk_app(lhs, proj);
}
expr eq = mk_app(mk_constant("eq", to_list(sort_level(m_type))), st_type, lhs, st);
levels rec_ls = levels(mk_level_zero(), st_ls);
level eq_lvl = sort_level(m_tc->ensure_type(eq).first);
levels rec_ls = levels(eq_lvl, st_ls);
expr rec = mk_app(mk_constant(inductive::get_elim_name(m_name), rec_ls), m_params);
expr type_former = Fun(st, eq);
expr mk = mk_app(mk_app(mk_constant(m_mk, st_ls), m_params), m_fields);