From a3146d0d2a0c62da296fabee2729db3c8a9c1c6a Mon Sep 17 00:00:00 2001 From: Yuri Sulyma Date: Thu, 8 Jun 2017 14:03:29 -0600 Subject: [PATCH] Fix bug --- move_to_lib.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 556ec6c..340eb82 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -1,6 +1,6 @@ -- definitions, theorems and attributes which should be moved to files in the HoTT library -import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 homotopy.smash_adjoint +import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 .homotopy.smash_adjoint open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group is_trunc function sphere unit sum prod bool