From 4817f2a18b093c6b8945112685d3c587a0984c0d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Mar 2015 11:36:02 -0700 Subject: [PATCH] refactor(hott/algebra/precategory/basic): improve basic.hlean compilation time --- hott/algebra/precategory/basic.hlean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean index a664ca0cd..e67072fa2 100644 --- a/hott/algebra/precategory/basic.hlean +++ b/hott/algebra/precategory/basic.hlean @@ -141,6 +141,10 @@ namespace category /-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) (hom1 : ob → ob → Type) (hom2 : ob → ob → Type) @@ -169,10 +173,10 @@ namespace category apply is_hprop.elim, cases PhomH, apply (ap0111 (precategory.mk hom2 homH1 comp2 ID2)), - repeat ( - apply @is_hprop.elim ; - repeat (apply is_trunc_pi ; intros) ; - apply is_trunc_eq ), + repeat + (apply @is_hprop.elim; + repeat (apply is_hprop_pi; intros); + apply is_trunc_eq) end definition precategory_eq_mk' (ob : Type)