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

refactor(hott/init/util.hlean): modify definition to make it more convenient for definitional package

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-19 21:56:26 -08:00
parent 2e93e5d6a7
commit 187f4483e9
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
hott/init/util.hlean
View file

@ -11,5 +11,6 @@ import init.trunc
open truncation
definition eq_rec_on_eq {A : Type} {B : A → Type} [h : is_hset A] {a : A} (b : B a) (p : a = a) : eq.rec_on p b = b :=
definition eq_rec_eq.{l₁ l₂} {A : Type.{l₁}} {B : A → Type.{l₂}} [h : is_hset A] {a : A} (b : B a) (p : a = a) :
b = @eq.rec.{l₂ l₁} A a (λ (a' : A) (h : a = a'), B a') b a p :=
eq.rec_on (is_hset.elim (eq.refl a) p) (eq.refl (eq.rec_on (eq.refl a) b))