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

refactor(hott/algebra/precategory/basic): improve basic.hlean compilation time

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-24 11:36:02 -07:00
parent 69d1cfdd52
commit 4817f2a18b
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
hott/algebra/precategory/basic.hlean
View file

@ -141,6 +141,10 @@ namespace category
/-Characterization of paths between precategories-/ /-Characterization of paths between precategories-/
-- auxiliary definition for speeding up precategory_eq_mk
private definition is_hprop_pi (A : Type) (B : A → Type) (H : Π (a : A), is_hprop (B a)) : is_hprop (Π (x : A), B x) :=
is_trunc_pi B (-2 .+1)
definition precategory_eq_mk (ob : Type) definition precategory_eq_mk (ob : Type)
(hom1 : ob → ob → Type) (hom1 : ob → ob → Type)
(hom2 : ob → ob → Type) (hom2 : ob → ob → Type)
@ -169,10 +173,10 @@ namespace category
apply is_hprop.elim, apply is_hprop.elim,
cases PhomH, cases PhomH,
apply (ap0111 (precategory.mk hom2 homH1 comp2 ID2)), apply (ap0111 (precategory.mk hom2 homH1 comp2 ID2)),
repeat ( repeat
apply @is_hprop.elim ; (apply @is_hprop.elim;
repeat (apply is_trunc_pi ; intros) ; repeat (apply is_hprop_pi; intros);
apply is_trunc_eq ), apply is_trunc_eq)
end end
definition precategory_eq_mk' (ob : Type) definition precategory_eq_mk' (ob : Type)