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